**Next message:**Simon Helsen: "Re: polymorphic recursion"**Previous message:**Mark Andrew: "OCaml 2.0 Binary for the Mac ?"**In reply to:**Simon Helsen: "Re: polymorphic recursion"**Next in thread:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Pierre CREGUT - FT.BD/CNET/DTL/MSV: "Re: polymorphic recursion"**Reply:**Ian T Zimmerman: "Patches for ocaml 2.00 library"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

From: Pierre Weis <Pierre.Weis@inria.fr>

Message-Id: <199809221506.RAA17926@pauillac.inria.fr>

Subject: Re: polymorphic recursion

To: helsen@informatik.uni-tuebingen.de (Simon Helsen)

Date: Tue, 22 Sep 1998 17:06:41 +0200 (MET DST)

In-Reply-To: <Pine.A32.3.96.980922113949.2728U-100000@modas> from "Simon Helsen" at Sep 22, 98 12:00:11 pm

*> This might be the case for OCaml, but note that SML97 disallows more
*

*> general type-constraints 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 type-inference engine to
*

*> detect type-errors "earlier" (the latter is practical while debugging
*

*> type-errors).
*

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
*

*> top-level monomorphism and the resolution of variable record patterns) A
*

*> SML type-constraint 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, type-inference
*

*> for this is undecidable.
*

Yes polymorphic recursion type-inference 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/

**Next message:**Simon Helsen: "Re: polymorphic recursion"**Previous message:**Mark Andrew: "OCaml 2.0 Binary for the Mac ?"**In reply to:**Simon Helsen: "Re: polymorphic recursion"**Next in thread:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Pierre CREGUT - FT.BD/CNET/DTL/MSV: "Re: polymorphic recursion"**Reply:**Ian T Zimmerman: "Patches for ocaml 2.00 library"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b29
: Sun Jan 02 2000 - 11:58:16 MET
*