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 MAA21688; Mon, 23 Jun 2003 12:27:28 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 MAA21308 for ; Mon, 23 Jun 2003 12:27:27 +0200 (MET DST) Received: from fichte.ai.univie.ac.at (fichte.ai.univie.ac.at [131.130.174.156]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id h5NARQ928385 for ; Mon, 23 Jun 2003 12:27:26 +0200 (MET DST) Received: from fichte.ai.univie.ac.at (markus@localhost [127.0.0.1]) by fichte.ai.univie.ac.at (8.12.3/8.12.3/Debian-6.4) with ESMTP id h5NARNqF004958; Mon, 23 Jun 2003 12:27:23 +0200 Received: (from markus@localhost) by fichte.ai.univie.ac.at (8.12.3/8.12.3/Debian-6.4) id h5NARNQq004957; Mon, 23 Jun 2003 12:27:23 +0200 Date: Mon, 23 Jun 2003 12:27:23 +0200 From: Markus Mottl To: Michal Moskal Cc: John Max Skaller , caml-list@inria.fr Subject: Re: [Caml-list] First order compile time functorial polymorphism in Ocaml Message-ID: <20030623102723.GB3386@fichte.ai.univie.ac.at> Mail-Followup-To: Michal Moskal , John Max Skaller , caml-list@inria.fr References: <3EF5F48E.6010209@ozemail.com.au> <20030622190353.GA9806@roke.freak> <3EF6796E.20004@ozemail.com.au> <20030623095857.GA23772@roke.freak> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20030623095857.GA23772@roke.freak> User-Agent: Mutt/1.4.1i X-Spam: no; 0.00; caml-list:01 functorial:01 michal:01 moskal:01 foo:01 covariant:01 variance:01 annotations:01 ocaml:01 logical:02 mottl:02 compile:02 wrote:03 variable:03 markus:04 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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 > 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. Sorry for my nitpicking ;-) Regards, Markus Mottl -- Markus Mottl http://www.oefai.at/~markus markus@oefai.at ------------------- 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