On 2010-12-18T06:36:54-0500, Jesse Howarth wrote:

Say I have functions like so:

let rec foo (f: 'a ->'a) (x: 'a) : 'a =
  f x
and a (x: float) = x
and b (x: string) = x
and bar = foo a 1.0
and baz = foo b "a"

I get an error on the last line that foo is expecting a function of type float -> float because I called foo with a before calling it with b. If I swap the last two lines, I get an error saying that it expects a function of type string -> string because foo was called with b before calling it with a. It seems like once I call foo, it saves the type of the polymorphic variable 'a. This is bizarre to me.

Do you have any idea what the problem might be?

You can get around this problem by splitting up the one big “let … and … and …” into “let … in let … in let …”.

Why? My understanding is that OCaml separately type-checks each let and generalizes the resulting types. So if you write

let rec (f: 'a -> 'a) (x: 'a) : 'a = f x in ...

then OCaml would look at this single definition and say, let me figure out what type 'a can be. Well, 'a can be any single type, so I’m going to put f into the type environment with the polymorphic type

forall 'a.  ('a -> 'a) -> 'a -> 'a

Then, each time you use foo, in bar and baz, the type variable 'a can be instantiated differently. So, each occurrence of let triggers generalizing type variables into polymorphic types. That’s the key of the Hindley-Milner type system behind the ML family of languages.

When you write everything with and, OCaml looks at the whole set of definitions and tries to figure out what type 'a can be. Well, this time 'a cannot be any single type, hence the type error.

Remember this program from CS314 last year?

let twice = proc (f) proc (x) (f (f x)) in
(((twice twice) proc (y) -(y,1)) 0)

Because we didn’t have Hindley-Milner polymorphism, type-checking this program gives the same type error.

On 2010-12-18T17:05:37-0500, Jesse Howarth wrote:

Thank you for the response.

I changed the definition to:

let fn =
let foo (f: 'a ->'a) (x: 'a) : 'a = (f x) in
let a (x: float) = x in
let b (x: string) = x in
let bar = foo a 1.0 in
let baz = foo b "a" in 0

(It wouldn’t allow me to just do the let … in without wrapping it with let fn = … in 0, I think because I am defining at the base of a file.)

I’m still receiving the error. What’s interesting is if I change it to:

let foo (f: 'a ->'a) (x: 'a) : 'a = (f x)
let a (x: float) = x
let b (x: string) = x
let bar = foo a 1.0
let baz = foo b "a"

Then it will not complain.

This also works:

let foo (f: 'a ->'a) (x: 'a) : 'a = (f x)
let fn =
let a (x: float) = x in
let b (x: string) = x in
let bar = foo a 1.0 in
let baz = foo b "a" in 0

Your explanation makes sense, but what happens in and cases as far as type checking may also happen with in cases.

Hrm! Thanks for pointing this out. I think it has to do with your putting the type annotations on f and x and (foo f x)—if you just say foo f x = f x then it works with the “let … in” sequence (but still not with “let … and”).

In OCaml, 'a means “a certain type I hereby omit” rather than (as in Haskell) “a generic type variable”. For example:

    Objective Caml version 3.11.2

# let f (x:'a) : 'a = x + 2;;
val f : int -> int = <fun>

So it’s hard to annotate a function with a polymorphic type. I believe OCaml 3.12 tried to address this:

“Type variables can be bound as type parameters to functions; such types are treated like abstract types within the function body, and like type variables (possibly generalized) outside.”