From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA03598 for caml-red; Mon, 18 Dec 2000 15:53:04 +0100 (MET)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA05296 for <caml-list@pauillac.inria.fr>; Mon, 18 Dec 2000 09:30:19 +0100 (MET)
Received: from cs.huji.ac.il (cs.huji.ac.il [132.65.16.10])
	by nez-perce.inria.fr (8.11.1/8.10.0) with ESMTP id eBI8UIH02817
	for <caml-list@inria.fr>; Mon, 18 Dec 2000 09:30:18 +0100 (MET)
Received: from zigzag.cs.huji.ac.il ([132.65.208.204])
	by cs.huji.ac.il with esmtp (Exim 3.20 #1)
	id 147vgX-0002Kt-00; Mon, 18 Dec 2000 10:30:17 +0200
Received: (from orodeh@localhost) by zigzag.cs.huji.ac.il (8.9.3/1.1c)
  id KAA19398; Mon, 18 Dec 2000 10:30:17 +0200
Date: Mon, 18 Dec 2000 10:30:17 +0200 (IST)
From: Ohad Rodeh <orodeh@cs.huji.ac.il>
To: Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>
cc: Caml List <caml-list@inria.fr>
Subject: Type annotations. 
Message-ID: <Pine.LNX.4.20_heb2.08.0012181025210.19337-100000@zigzag.cs.huji.ac.il>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: weis@pauillac.inria.fr

Jacques,
  I'd love to see this added to the distribution, even if only 
as an optional compile time flag. Allowing polymorphic recursion, and
mitigating the record naming problem are worthy goals, 

   Ohad.

> There are a few things that work well with this approach, polymorphic
> recursion being one. But it is not as general as it seems.
> A simple scheme is to assume that you can give explicitely a type to
> an identifier, use this type to resolve ambiguities, and check
> afterwards that this type is correct.
> With such a scheme,
>      let w : t = {x=1;y=2} in w.x
> will indeed be correctly handled.
> However, this breaks as soon as an annotation is lacking:
>      let w : t = {x=1;y=2} in
>      let v = w in
>      w.x
> Similarly, pairs won't work
>      let w : t * int = ({x=1;y=2}, 3) in (fst w).x
> Indeed, while w was given a special "assumed" type, propagating such
> assumed types through definitions and function calls is much more
> subtle.
> In a paper by Didier Remy and myself [1], we designed a system that
> could do a fair amount of "assumed" type propagation. This was
> intended for providing first class polymorphism and polymorphic
> methods, and was implemented in Objective Label. This could also be
> used for typing records, while some might see it as an overkill.
> But this is much more complex than what you are calling PRIOR.
> And this is not principal in the strict meaning (due to a mischevious
> side-effect of the value only prolymorphism rule).
> 
> I am currently working on reintegrating this feature in ocaml. However
> it is not yet clear whether it can be made cheap enough to make it
> into the main stream version (type inference becomes slower).
> And then some might discuss the fact it would require people to learn
> yet another set of rules about how assumed types are propagated.
> 
> Cheers,
> 
> Jacques
> 
> [1] Extending ML with semi-explicit higher order polymorphism,
>     Information and Computation 155, december 1999, pages 134-171.