[plt-scheme] Recursive types and their specification

At Tue, 9 Aug 2005 07:58:44 -0700 (PDT), Noel Welsh wrote:
> The FSM returns two values: the action to take (up, down,
> left, or right) and the continuation for the policy.  How
> does one specify the type of the continuation?  It's a
> function that returns two values, the first of which is an
> action, and the second of which is a function that returns
> two values, the first of which...
> 
> Is this something that would cause HM to blow up (I think
> so)?

[Robby gave the short answer. Here's a longer one that I had mostly
typed already.]

Yes. As your subject line says, the problem is a equi-recursive
function type

  mu x . () -> (action * x)

which is not in the type system.

The solution is to introduce a constructor and a separate `apply':

 (* mangled syntax, probably *)
  datatype fsm = F of (() -> (action * fsm))
  applyFSM F(f) = f()

  policy : (() -> (action * fsm))

Uses of the constructor `F' in expressions and pattern-matching tell
the type checker where to roll and unroll the iso-recursive type.

OCaml supports a command-line flag to extend the type system and
inference with recursive types, and I think it would probably handle
the program you describe. The trade-off is that type inference isn't
decidable anymore (as long as you keep polymorphism, too).

Matthew