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
foois expecting a function of type
float -> floatbecause I called
abefore calling it with
b. If I swap the last two lines, I get an error saying that it expects a function of type
string -> stringbecause
foowas called with
bbefore 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
Why? My understanding is that OCaml separately type-checks each
let and generalizes the resulting types. So if you
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,
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
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
inwithout 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
andcases as far as type checking may also happen with
Hrm! Thanks for pointing this out. I think it has to do with
your putting the type annotations on
(foo f x)—if you just say
foo f x = f x then it works with the “
in” sequence (but still not with “
'a means “a certain type I hereby omit”
rather than (as in Haskell) “a generic type variable”. For
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: