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 MAA20960; Mon, 23 Jun 2003 12:01:22 +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 MAA20741 for ; Mon, 23 Jun 2003 12:01:21 +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 h5NA1JD04496 for ; Mon, 23 Jun 2003 12:01:19 +0200 (MET DST) Received: (qmail 5405 invoked by uid 566); 23 Jun 2003 10:01:15 -0000 Date: Mon, 23 Jun 2003 11:58:57 +0200 From: Michal Moskal To: John Max Skaller Cc: caml-list@inria.fr Subject: Re: [Caml-list] First order compile time functorial polymorphism in Ocaml Message-ID: <20030623095857.GA23772@roke.freak> References: <3EF5F48E.6010209@ozemail.com.au> <20030622190353.GA9806@roke.freak> <3EF6796E.20004@ozemail.com.au> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <3EF6796E.20004@ozemail.com.au> 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 polynomial:01 avoiding:01 kernel:01 ocaml:01 mutable:01 exists:01 logical:02 compile:02 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Mon, Jun 23, 2003 at 01:52:14PM +1000, John Max Skaller wrote: > Michal Moskal wrote: > > >On Mon, Jun 23, 2003 at 04:25:18AM +1000, John Skaller wrote: > > >First thing to consider: map function of this kind only exists for types, > >where type variables occur only positively. > > What does that mean? 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 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. > >Even then, for inductive > >types it requires proof (it isn't as simple as it first seems). > > > The proof has been constructed for all polynomial types, > > i.e. types using only sums and products. > [Paper:Functorial ML, Author:Barry Jaye, the mechanism > there generalises over 'arbitrary' algorithms: I'm not proposing > that, rather that the theory can be applied to hand write > the generators for popular functions like map and fold] Ah, you mean only sums and products. Then you're correct (you are avoiding the hard case :-). > >For example consider: > > > >type 'a t = Foo 'a -> unit > > > >To map : 'a t -> 'b t here, you need f : 'b -> 'a. > > > Ah, ok, exponential is contravariant. > > Probably have to think about > > 'a ref > > too. type 'a ref = {mutable contents : 'a} which is much the same as product type. -- : 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