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 MAA14135; Mon, 23 Jun 2003 12:36:20 +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 MAA21891 for ; Mon, 23 Jun 2003 12:36:19 +0200 (MET DST) Received: from ep09.kernel.pl (ep09.kernel.pl [212.87.11.162]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h5NAaGD05929 for ; Mon, 23 Jun 2003 12:36:17 +0200 (MET DST) Received: (qmail 28782 invoked by uid 566); 23 Jun 2003 10:36:11 -0000 Date: Mon, 23 Jun 2003 12:35:56 +0200 From: Michal Moskal To: caml-list@inria.fr Subject: Re: [Caml-list] First order compile time functorial polymorphism in Ocaml Message-ID: <20030623103556.GC28158@roke.freak> References: <3EF5F48E.6010209@ozemail.com.au> <20030622190353.GA9806@roke.freak> <3EF6796E.20004@ozemail.com.au> <20030623095857.GA23772@roke.freak> <20030623102723.GB3386@fichte.ai.univie.ac.at> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20030623102723.GB3386@fichte.ai.univie.ac.at> User-Agent: Mutt/1.4.1i X-PGP-Fingerprint: CF89 1B14 11BE 1CC9 2CA3 7497 5E32 69B4 BC71 B4C2 X-AntiVirus: scanned for viruses by AMaViS 0.2.1 (http://amavis.org/) X-Spam: no; 0.00; michal:01 moskal:01 malekith:01 pld-linux:01 caml-list:01 functorial:01 foo:01 covariant:01 variance:01 annotations:01 kernel:01 ocaml:01 0200,:01 logical:02 mottl:02 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Mon, Jun 23, 2003 at 12:27:23PM +0200, Markus Mottl wrote: > On Mon, 23 Jun 2003, Michal Moskal wrote: > > Variable occurs positively in type, if it's preceded by even number of > > negations. > > > > When you treat -> as logical implication, you get: > > > > a -> b == a & !b > > This is incorrect, your right hand side would correspond to !(a -> b). > The correct, minimal definition of implication in terms of negations, > conjunctions and disjunctions is: > > a -> b = !a \/ b Sorry, you're of course right. > > > So 'a -> t, 'a -> (t -> 'a) are 'a-positive, t -> 'a is 'a-negative, > > and 'a -> 'a isn't neither 'a positive nor 'a negative. Other tycons > > (like *) doesn't change sign. But when you define new type, say: > > > > type ('a, 'b) t = Foo of 'a -> 'b > > > > then ('c, 'd) t is 'd negative, and 'c positive. > > As a consequence, you need to interchange "positive" and "negative" > against each other in the upper paragraph. Then "covariant" and "positive" > fall together as do "contravariant" and "negative". This is also the > way OCaml treats variance annotations. Yes. I just googled for covariant/contravariant and found the same. -- : Michal Moskal :: http://www.kernel.pl/~malekith : GCS {C,UL}++++$ a? !tv : When in doubt, use brute force. -- Ken Thompson : {E-,w}-- {b++,e}>+++ h ------------------- 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