smlsmlnj

Defined functions in structures in SML results in "value type in structure does not match signature spec"


It has been quite a while since I've been programming in SML and now I'm stuck on what looks to me a very simple issue.

I'm defining a datatype like

datatype 'a Something = Something of 'a

then I'm defining a signature as follows

signature A = sig
  val some : 'a -> 'a -> 'a Something
end

the structure implementing that signature instead looks like this

structure B : A = struct
  fun some(a) = fn x => if a=x then Something a else Something x
end

That end up producing the following error and I don't understand why

Error: value type in structure does not match signature spec
  name: some
spec:   'a -> 'a -> 'a Something
actual: ''a -> ''a -> ''a Something

If I define the structure as follows instead

structure C : A = struct
  fun some(a) = fn x => Something a
end

everything works smoothly.

What am I missing here?


Solution

  • TLDR:

    The type variable 'a doesn't support equality comparison. You need an "equality type variable" instead. These are written with two leading apostrophes, i.e. ''a. Here's the fixed code. Both SML/NJ and MLton accept it.

    datatype ''a Something = Something of ''a
    signature A = sig
      val some : ''a -> ''a -> ''a Something
    end
    structure B : A = struct
      fun some(a) = fn x => if a=x then Something a else Something x
    end
    

    An alternative solution is continue using 'a, and explicitly pass around a function to test for equality.

    datatype 'a Something = Something of 'a
    signature A = sig
      (* first arg is equality function *)
      val some : ('a * 'a -> bool) -> 'a -> 'a -> 'a Something
    end
    structure B : A = struct
      fun some eq a = fn x => if eq (a, x) then Something a else Something x
    end
    

    Details

    The equality test if a=x then ... else ... is attempting to check for equality between two values of type 'a.

    The problem is that not all possible instantiations of 'a support equality tests.

    For example, what if you wanted to do B.some (fn i => i) (fn i => 2*i)? This instantiates 'a with the concrete type int -> int. Your code now wants to attempt to perform an equality comparison between the functions fn i => i and fn i => 2*i, but SML doesn't know how to compare functions for equality.

    To work around this problem, SML has a... somewhat hacky solution. It distinguishes between two kinds of polymorphism: types that support equality, and types that do not.

    Normal type variables are written with a single apostrophe ('a, 'b, 'whatever, etc.), and these do not allow for polymorphic equality.

    Equality type variables are written with two apostrophes (''a, ''b, etc.), and these allow for polymorphic equality.

    Equality type variables are more restrictive than normal type variables.

    See http://mlton.org/PolymorphicEquality for more info!