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: