Re: polymorphic recursion

Pierre Weis
 Anton Moscal
 Peter Thiemann
[
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:  Peter Thiemann <pjt@c...> 
Subject:  Re: polymorphic recursion 
>>>>> "Pierre" == Pierre Weis <Pierre.Weis@inria.fr> writes: Pierre> I suggest the following simple rules: Pierre> (1) type expressions appearing in type constraints are supposed to be Pierre> type schemes, implicitely quantified as usual. Scope of type variables Pierre> is simply delimited by the parens surrounding the type constraint. Pierre> (2) a type constraint (e : sigma) is mandatory. It means that sigma IS Pierre> a valid type scheme for e, and indeed sigma is the type scheme Pierre> associated to e by the compiler. (This implies that sigma is an Pierre> instance of the most general type scheme of e.) This suggestion is quite close to what Haskell imposes, as far as I know: if there is a toplevel type signature for an identifier f, then it is taken as a type scheme (implicitly allquantifying all type variables) and *all* occurrence of f (including recursive ones) are typechecked using this signature as assumption. Furthermore, the inferred type scheme for the body of f must be more general than its type signature prescribes. This corresponds to the typing rule A, f:sigma  e : sigma'  sigma is a generic instance of sigma' A  fix f:sigma. e : sigma Here is a drawback of your proposal that the Haskell folks are currently addressing in a revision of the standard: you cannot always write a type signature for a nested function. Suppose let (f : 'a * 'b > 'b) = fun (x, y) > let (g : unit > 'b) = fun () > y in g () [this would not type check] In this case, g really has *type* unit > 'b without 'b being allquantified. Of course, you could write something like: let (f : 'a * 'b > 'b) = fun (x, (y : '_b)) > let (g : unit > '_b) = fun () > y in g () but that would not be nice. If I recall correctly, the current Haskell proposal says that variables in the outermost type signature are bound in the body of the corresponding definition. That's not nice, either. An alternative that I could imagine is to include explicit binders for the type variables, i.e., big Lambdas, to indicate their scope precisely in the rare cases where it is necessary. It could be regarded an error to mix explicitly bound and implicitly bound type variables, as this might give rise to misunderstandings. Having a unified treatment for these things would really make life easier. Peter