**Next message:**Mark Andrew: "OCaml 2.0 Binary for the Mac ?"**Previous message:**Basile STARYNKEVITCH: "micro wish: ocamlfat"**In reply to:**Pierre Weis: "Re: polymorphic recursion"**Next in thread:**Pierre Weis: "Re: polymorphic recursion"**Reply:**Pierre Weis: "Re: polymorphic recursion"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

Date: Tue, 22 Sep 1998 12:00:11 +0200 (MST)

From: Simon Helsen <helsen@informatik.uni-tuebingen.de>

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

Subject: Re: polymorphic recursion

In-Reply-To: <199809220922.LAA11296@pauillac.inria.fr>

Message-Id: <Pine.A32.3.96.980922113949.2728U-100000@modas>

*> Unfortunately, the problem here is the semantics of type constraints
*

*> in ML: type constraints are not mandatory type assigment declarations,
*

*> but just annotations which should be compatible with the type infered
*

*> for the given expression. This means that a type constraint has to be
*

*> more general than the principal type of the annotated expression. For
*

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)

*> let (f : 'a -> int) = function x -> x + 1;;
*

*> val f : int -> int = <fun>
*

in SML/NJ 110 this yields:

- val (f : 'a -> int) = fn x => x + 1;

stdIn:1.1-2.31 Error: pattern and expression in val dec don't agree

[literal]

pattern: 'a -> int

expression: int -> int

in declaration:

f : 'a -> int = (fn x => x + 1)

*> This has many drawbacks, the most important being that no type
*

*> annotation in a program is reliable to the reader (except if the type
*

*> annotation does not posses any type variable at all).
*

I suppose that this is exactly why Standard ML wants the type annotation

to have the exact degree of polymorphism as present in the expression.

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).

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

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.

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)

Simon

----------------------- Simon Helsen ------------------------

-- Wilhelm-Schickard-Institut fuer Informatik --

-- Arbeitsbereich Programmierung (PU) --

-- Universitaet Tuebingen, Germany --

-------------------------------------------------------------

-- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

**Next message:**Mark Andrew: "OCaml 2.0 Binary for the Mac ?"**Previous message:**Basile STARYNKEVITCH: "micro wish: ocamlfat"**In reply to:**Pierre Weis: "Re: polymorphic recursion"**Next in thread:**Pierre Weis: "Re: polymorphic recursion"**Reply:**Pierre Weis: "Re: polymorphic recursion"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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