Why does OCaml succeed in matching 'a list with int list, while Standard ML fails to do so?

user_5916915 0
Viewed 80

In OCaml, let f (x : 'a) : 'a list = x :: [0] has signature val f : int -> int list.

When I try to define a similar function in Standard ML, fun f (x : 'a) : 'a list = x :: [0], there is an error.

SML/NJ:

- fun f (x : 'a) : 'a list = x :: [0];
stdIn:2.6-2.14 Error: operator and operand do not agree [overload - user bound tyvar]
  operator domain: 'a * 'a list
  operand:         'a * 'Z[INT] list
  in expression:
    x :: 0 :: nil

Poly/ML:

> fun f (x : 'a) : 'a list = x :: [0];
poly: : error: Type error in function application.
   Function: :: : 'a * 'a list -> 'a list
   Argument: (x, [0]) : 'a * int list
   Reason: Can't unify int to 'a (Cannot unify with explicit type variable)
Found near x :: [0]
Static Errors

What is the difference between the type system in OCaml and Standard ML that causes an error to appear for Standard ML but not for OCaml?

sml ocaml types
1 Answers

In OCaml, a type variable in a type ascription represents a unification variable. It doesn't indicate that the type is polymorphic, it just gives a name to the type, which will participate in unification with other types.

As I recall, in SML, using a type variable in a type ascription means that the type is specifically polymorphic. So when you ascribe the type 'a to x you're saying that the actual parameter must have a polymorphic type. Since there's no valid value that's fully polymorphic like this, this is bound to lead to errors.

(I believe this is right, but others are far more knowledgeable than I am.)

user_8216790
Related