From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA06060; Mon, 22 Dec 2003 21:26:27 +0100 (MET)
X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA05707 for <caml-list@pauillac.inria.fr>; Mon, 22 Dec 2003 21:26:26 +0100 (MET)
Received: from null.cs.brown.edu (null.cs.brown.edu [128.148.38.190])
	by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id hBMKQPb06946
	for <caml-list@inria.fr>; Mon, 22 Dec 2003 21:26:25 +0100 (MET)
Received: from cslab5c (cslab5c [128.148.33.185])
	by null.cs.brown.edu (Postfix) with ESMTP
	id 965552EFE2; Mon, 22 Dec 2003 15:26:24 -0500 (EST)
Received: from gmarceau (helo=localhost)
	by cslab5c with local-esmtp (Exim 3.36 #1 (Debian))
	id 1AYWdE-0005Cc-00; Mon, 22 Dec 2003 15:26:24 -0500
Date: Mon, 22 Dec 2003 15:26:24 -0500 (EST)
From: Guillaume Marceau <gmarceau@cs.brown.edu>
X-X-Sender: gmarceau@cslab5c
To: Alex Baretta <alex@baretta.com>
Cc: Ocaml <caml-list@inria.fr>
Subject: Re: [Caml-list] Polymorphic records typing question
In-Reply-To: <3FE6CC78.8050506@baretta.com>
Message-ID: <Pine.LNX.4.58.0312221504060.19513@cslab5c>
References: <3FE6CC78.8050506@baretta.com>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Loop: caml-list@inria.fr
X-Spam: no; 0.00; guillaume:01 caml-list:01 baretta:01 val:01 foo:01 val:01 foo:01 unacceptable:01 inference:01 inference:01 recursion:01 america:99 guillaume:01 computed:01 caml:01 
Sender: owner-caml-list@pauillac.inria.fr
Precedence: bulk


On Mon, 22 Dec 2003, Alex Baretta wrote:

> Here's a puzzle for the Caml breeders:
>
> # type poly = { f : 'a . 'a -> 'a };;
> type poly = { f : 'a. 'a -> 'a; }
> # let id x = x;;
> val id : 'a -> 'a = <fun>
> # let foo = { f = id };;
> val foo : poly = {f = <fun>}
> # let rec id x = x and foo = { f = id } ;;
> This field value has type 'a -> 'a which is less general than 'b. 'b -> 'b
>
> Why is this last recursive definition unacceptable?
>
> Alex
>

Types are not generalized within the scope of their recursive declaration.

For instance, take this contrived definition of the identity function :

   let rec id x =
     if true then (ignore(id 1); x)
     else ((ignore (id [])); x)
                       ^^
   This expression has type 'a list but is here used with type int

Although id could be safely be assigned the type 'a . 'a -> 'a, the type
inference algorithm cannot figure it out.

It is a limitation that raises from the way the type inference is
computed. Then again, it isn't much of a limitation: both my example and
yours can trivially be rewritten such that they type.


Also, this is one good reason to not use the 'and' keyword unless you
actually need a mutual recursion. Instead of writing this:

      let a = ... body_a ...
      and b = ... body_b ... in
      ...

write this:

      let a = ... body_a ... in
      let b = ... body_b ... in
      ...

It will save you the above error in the case 'body_b' uses 'a' polymorphically.



-- 
"The thing I remember most about America is that it's silly.
 That can be quite a relief at times."  -- Thom Yorke, Radiohead

- Guillaume

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners