Re: Type issue

Re: Type issue

[oleg]

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.

Type issue

[Jonathan T Bryant]

List,

I don't understand the following typing:

# 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

# let rec f t = match t with
      Cond (c,t,e) -> if f c then f t else f e
    | Value x -> x
  ;;
val f : bool t -> bool = <fun>

I don't understand why f isn't of type 'a t -> 'a.  I understand that f 
is applied to a bool t, but I would think that that would just be a 
particular instantiation of 'a, not enough to fully determine its type.

--Jonathan Bryant