Re: polymorphic recursion
[
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:  Pierre Weis <Pierre.Weis@i...> 
Subject:  Re: polymorphic recursion 
> This might be the case for OCaml, but note that SML97 disallows more > general typeconstraints than the type apparent in the expression without > the constraint (cf. rule (9) and comment in the 97 Definition  p22) That's a good point. It's simple to state and understand. > This makes sense in the filosophy that type constraints are only supposed > to be programmer documentation or to help the typeinference engine to > detect typeerrors "earlier" (the latter is practical while debugging > typeerrors). Yes, but furthermore it can be used to help the typechecker to find types more general than it will normally find. > Unfortunately, SML is not very consistent on this matter as well, since it > might require type annotations to succeed its type inference (e.g. at > toplevel monomorphism and the resolution of variable record patterns) A > SML typeconstraint cannot be more general, but is allowed to be more > specific. e.g: > >  val (f : 'a > 'a > 'a) = fn x => fn y => y; > val f = fn : 'a > 'a > 'a This is necessary to ``constrain'' the types of programs, when you want to obtain a type more specific than the one synthetized by the typechecker, in order to get more precise typing verifications. This is also useful to get rid of spurious type unknowns at modules boundaries, since you cannot let them escape from the module. > And if SML "would" follow this filosophy properly, there is no room for > polymorphic recursion in general since, as you indicate, typeinference > for this is undecidable. Yes polymorphic recursion typeinference is undecidable. No, ``exact'' type constraints do not preclude polymorphic recursion. Starting with the ``exact'' type annotation as hypothesis, it is easy to verify that the polymorphic recursion is sound. This is simple and easy. The only drawback is that you have to find the type yourself, and that you may indicate a too specific type. > I don't know why Caml allows more general type constraints, but it might > be a good idea to follow SML on this matter (and I am interested to know > if there are good reasons for not doing this) If we use it to get polymorphic recursion, there is a good reason to do this. Another problem is the scope of type variables in type constraints. What's the meaning of let f (x : 'a) (y : 'a) = y;; We may need explicit Forall keywords to express type schemes in constraints. Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/