Re: polymorphic recursion

[Simon Helsen <helsen@informatik.uni-tuebingen.de>]

> 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/ --