10 Polymorphic Functions
Combining polymorphic functions with refinements needs some care. Consider the
polymorphic identity function, fun id(x :: ?a) :: ?a. It does not say
anything about how the return relates to its parameter except that they will be
the same type. Therefore, if we try to use it with a function that consumes and
promises to return a positive integer, it will fail:
To pass, id must relate its result to its argument:
fun id(x :: ?a) :: {r :: ?a | r == x}:
x
Inside id, the type variable stands for any type, so the only thing a predicate can say about a value of type ?a is whether or not it is definitely equal to another.