Re: Type issue

[oleg@pobox.com]

As Alain Frisch mentioned, with polymorphic recursion, inference is in
general impossible. Luckily, polymorphic recursion can be integrated
into a HM system if we require a type annotation on polymorphically
recursive functions. The annotation can come in various forms: for
example, if we use recursive modules, the annotation is given in the
signature. It seems using first-class polymorphism of OCaml records
might be a bit simpler:

type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
  type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a

type ft = {ft : 'a . 'a t -> 'a};;
  type ft = { ft : 'a. 'a t -> 'a; }

let f = 
  let rec f' = {ft = function 
    | Cond (c,t,e) -> if f'.ft c then f'.ft t else f'.ft e
    | Value x -> x}
  in f'.ft;;

 val f : 'a t -> 'a = <fun>

f (Cond ((Value true),(Value 1),(Value 2)));;
- : int = 1

One should think of 'ft' as marking the places where the big-lambda is
introduced and eliminated.  Luckily, the extended value restriction
(or should I say, restricted value restriction) helps us avoid
eta-expansion in the definition of f.