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 IAA04104; Sat, 13 Sep 2003 08:59:26 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 IAA25165 for ; Sat, 13 Sep 2003 08:59:25 +0200 (MET DST) Received: from mail3.tpgi.com.au (mail.tpgi.com.au [203.12.160.59]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h8D6xNT12047 for ; Sat, 13 Sep 2003 08:59:23 +0200 (MET DST) Received: from 203-219-234-208-syd-ts25-2600.tpgi.com.au (203-219-234-208-syd-ts25-2600.tpgi.com.au [203.219.234.208]) by mail3.tpgi.com.au (8.11.6/8.11.6) with ESMTP id h8D6xJS04018 for ; Sat, 13 Sep 2003 16:59:20 +1000 Subject: [Caml-list] inference engine From: skaller Reply-To: skaller@ozemail.com.au To: caml-list@inria.fr Content-Type: text/plain Message-Id: <1063436331.12717.11.camel@pelican> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 13 Sep 2003 16:58:51 +1000 Content-Transfer-Encoding: 7bit X-Loop: caml-list@inria.fr X-Spam: no; 0.00; inference:01 ozemail:01 inference:01 'int':01 narrower:01 theorist:01 variants:01 int:01 int:01 polymorphic:01 float:02 typing:03 compares:03 interface:03 variable:03 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk In an example like: let f (x:int) = 1 + x the inference engine first examines: let (f:'a -> 'b) (x:'c) = 1 + x to specialise 'a, 'b, 'c, and then compares the infered value of 'c with the constraint on x, which is 'int' in this case. For example in let f (x:int) = x x is first an un specialised type variable, but the interface seen by outside clients is constrained to int -> int Having seen the typing used in polymorphic variants, of the kind [> .. ] and [< .. ] (I can never remember which is which .. ) I wonder if it isn't possible for the inference engine to make the type of 'x' on entry to the function something like [> int ] meaning 'at least constrainable to '"int" '. If that were possible the following error would be caught earlier: let f (x:int) = x +. 1.0 at the point 'float' is infered for x, since float & [> int] is empty. On the other hand, in the case let f (x:int) = x the return type (before constraint is applied) is still [> int] & 'a which is 'a. That is: by attaching 'at least T' for annotation t (in positive position?? and at most in negative??) to the type accumulated in the inference engine's tables, we get earlier error diagnosis, without changing the actual result. This is 'mandatory typing', but the type which is mandatory isn't the one of the annotation, but 'some type wider than it' (or, perhaps narrower in negative position ..??) Well, I'm not a type theorist, its just an idea .. ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners