Is there a way to make polymorphic references constants in signatures?
This code compiles, but is not what I need:
signature NAME = sig
type 'a name
val empty : 'a name
end
structure Name :> NAME = struct
datatype 'a name = Nil | Val of 'a
val empty = Nil
end
Adding the required references:
signature NAME = sig
type 'a name
val empty : 'a name ref
end
structure Name :> NAME = struct
datatype 'a name = Nil | Val of 'a
val empty = ref Nil
end
Produces the following error:
error: Structure does not match signature.
Signature: val empty: 'a name ref
Structure: val empty: 'a name ref
Reason: Can't match 'a to 'a (Type variable is free in surrounding scope)
Found near struct datatype 'a name = Nil | Val of 'a val empty = ref Nil end
This doesn't actually have to do with signatures; you'd get the same sort of issue if you wrote (at top-level):
val emptyListRef = ref nil
val emptyIntList = (! emptyListRef) : int list
val emptyStringList = (! emptyListRef) : string list
The issue is that emptyListRef — or in your case empty — can't be polymorphic. (Your compiler claims that empty has type 'a name ref, but what it really means is that empty will have some type of the form ?? name ref, and it hasn't yet figured out what ?? will be.)
This restriction makes sense when you consider that if empty were polymorphic, then you'd be able to write things like:
val () = empty := Val 3
val Val (x : string) = !empty
where you set empty to hold an int Name and then read from it as if it held a string Name. There's no way the convince the compiler to trust that you won't do that.
The general rule is that value bindings are only allowed to be polymorphic if the right-hand side takes one of a few simple forms, like combinations of constructors (other than ref!) and constants and fn-expressions, that are known to be safe (in that they can't enable the above-described misbehavior). This rule is called the value restriction; you can Google that term to get much more information.