From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id MAA24410; Tue, 20 Nov 2001 12:16:47 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id MAA24647 for caml-list@pauillac.inria.fr; Tue, 20 Nov 2001 12:16:46 +0100 (MET) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA23225 for ; Tue, 20 Nov 2001 10:58:16 +0100 (MET) Received: from morgon.inria.fr (morgon.inria.fr [128.93.8.33]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id fAK9w8b25481; Tue, 20 Nov 2001 10:58:08 +0100 (MET) Received: (from remy@localhost) by morgon.inria.fr (8.11.6/8.11.6) id fAK9w0C08700; Tue, 20 Nov 2001 10:58:00 +0100 To: Alain Frisch Cc: Jacques Garrigue , , Subject: Re: [Caml-list] [Q]: Co(ntra)variance and subtyping? References: From: Didier Remy Date: 20 Nov 2001 10:58:00 +0100 In-Reply-To: Message-ID: User-Agent: Gnus/5.0808 (Gnus v5.8.8) Emacs/20.7 MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Alain Frisch writes: > > In the ML world, we mean complete type inference. >=20 > What does complete type inference mean ? I would say that it implies > that no type annotation is mandatory (if a program typechecks with a type > annotation, it should also typecheck without). This property does not hold > in OCaml; you can't remove type annotation in: >=20 > class o =3D object method f (x : int) =3D x end Just to mention that examples can also be found in (almost) the core language as well, you could choose ``ref []'' alone, which program will be rejected by the compiler. ---------------- I take this opportunity to raise a question about the meaning of "type inference". Indeed, the answer of whether a language has type inference may be more subtle than it first appears. Checking whether types are/must be mentioned in source programs may not be sufficient. Consider data-type declarations: type 'a list =3D [] | Cons of 'a * 'a list=20 Is this a type annotation? Indeed, this declaration amounts to later implicitly annotate every occurrence of a Cons as carrying arguments of types 'a and 'a list. The situation apparently looks simpler for the raw lambda-calculus, which comes in two flavors untyped and typed and where the untyped version does not mention types at all. However, there is no untyped version of ML (with datatypes/exceptions, etc.) in the sense that types would not be mentioned at all. Even in the lambda-calculus it should be fair to consider that (fun x -> a) carries the (implicit) type annotations ('a -> 'b). So, isn't it unfair to make a difference between type annotations that are plugged into the syntax and more elaborated type annotations that would are explicitly in the syntax. Formally, the distinction is not obvious: syntactic nodes (_ : t) can well be seen as (i.e. replaced by) built-in primitives of types t -> t (and given the same semantics as the identity). Hopefully, there is always a lot of type information in programs, whether it is implicit or explicit ---otherwise, type inference could not do much. Furthermore, the difference between explicit and implicit annotations is not always so clear, certainly not a binary notion. My conclusions are that=20 - the typed and untyped version cannot be left implicit when talking about type inference. - the property of ``having type inference'' should rather be replaced by a measure of ``how much type inference'' (1) or ``what are the properties of type inference'' (2).=20 Answers to (2) the later can be made formal. Answers to (1) tend to be informal ---but it would be interesting to find a formal criteria... Didier R=E9my ------------------- Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr