Re: [Caml-list] Polymorphic records typing question

[Guillaume Marceau <gmarceau@cs.brown.edu>]

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