Search code examples
recursionpolymorphismsmltype-inferenceml

Type inference for polymorphic recursion encoded as module recursion


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?


Solution

  • 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.