This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Re: Type issue
• oleg@p...
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-11-24 (05:50) From: oleg@p... Subject: Re: Type issue
```
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.

```