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