Re: [Caml-list] First order compile time functorial polymorphism in Ocaml

[John Max Skaller <skaller@ozemail.com.au>]

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?

> 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]

 
> 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.

> What about t1 -> t2? (this is the real problem).


And perhaps more generally, 'a t where t is
contravariant?

  
> Automatic definition of iterators and recursors for types also isn't
> that simple, it requires good dose of theory.


Sure. So: either add a restriction to avoid contravariance,

or generalise my proposal.

I have an actual problem, a large amount of my code is

involved in mapping large variants. Sometimes the map
is combined with some folding and other rewriting.

Every time I add a new feature I have to write the map
out again by hand. Every time I add a new term, I have to change
all the maps to cope. The syntax for defining terms is
inconveniently different to that required in a match,
making cut and paste only marginally useful:

	Ctor of xyz ==> Ctor (xyz) -> 	
	a * b ==> (a,b) ->

There's got to be a better way. Particularly, I do multiple

re-mappings of a term structure, one for each feature.
Then, I can see I can merge some of them into one map.
Or worse, the other way around: I have a single recursion
doing two jobs and find I need to unravel them.

It would be good to separate out the functorial part of
the operation and just write my mapping function for the
cases that are special, and also to be able to interwine
them into a single mapping.

None of my data structures contain functions.

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850


-------------------
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