Standard ML doesn't have polymorphic recursion. Adding recursion to the module language allows us to recover polymorphic recursion as a special case, using fixed points of endofunctors. For example:
signature SEQ =
sig
type 'a seq
(* operations on sequences *)
end
functor BootstrapSeq (S : SEQ) =
struct
datatype 'a seq
= Nil
| Zero of ('a * 'a) S.seq
| One of 'a * ('a * 'a) S.seq
(* operations on sequences *)
end
structure rec Seq = BootstrapSeq (Seq)
It's known that polymorphic recursion makes type inference undecidable. However, a functor definition already contains partial type information, namely, the signature of its argument. Is this information sufficient to make type inference decidable again?
Yes, because the signature provides a "forward declaration" of the polymorphic type, so it doesn't have to be inferred recursively. Also, you don't need a functor, you can write a recursive structure binding directly. But that requires a signature annotation, and thus amounts to the same.