Re: Type issue
 oleg@p...
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
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 firstclass 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 biglambda is introduced and eliminated. Luckily, the extended value restriction (or should I say, restricted value restriction) helps us avoid etaexpansion in the definition of f.