What is the difference between 'a and ''a in SML?

Question

For example:

fun example (a:'a list) : list = a

will have a signatures of:

'a list -> 'a list 

What if I define it differently but with same content like

fun example (a : ''a list) : list = a

its signature will be:

''a list -> ''a list

What's the difference?

Answer 1

A plain type variable like 'a can be substituted with an arbitrary type. The form ''a is a so-called equality type variable, which means that it can only be substituted by types that admit the use of the equality operator = (or <>) on their values.

For example, this function:

fun contains(x, [])    = false
  | contains(x, y::ys) = x = y orelse contains (x, ys)

cannot have type 'a * 'a list -> bool because it uses equality on x. It is given the more restrictive type ''a * ''a list -> bool.

Most types allow equality, but some don't, e.g., real, exn, and in particular, any function type t -> u. Composed types like records, tuples, or datatypes admit equality if all their components do.

Side remark: Haskell later generalised this concept to its notion of type classes, which allows arbitrary user-defined constraints of this sort on types. Equality type variables are replaced by the Eq type class.