caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] First order compile time functorial polymorphism in Ocaml
@ 2003-06-22 18:25 John Skaller
  2003-06-22 19:03 ` Michal Moskal
                   ` (3 more replies)
  0 siblings, 4 replies; 18+ messages in thread
From: John Skaller @ 2003-06-22 18:25 UTC (permalink / raw)
  To: caml-list

In ML style functional programming languages like Ocaml,
we have what is termed data polymorphism. This provides
a kind of code reuse we're all familiar with.

However, there is another kind of polymophism
which Ocaml does not provide. Two things to consider here:

1. Every data structure has a map function.
2. User defined algebraic type require a hand written map function

It sure is inconvenient to have to remember the names
of all those map functions, not to mention having to hand
write them. Lets look at a map function:

type 'a mylist = Empty | Cons of 'a * 'a list

let rec map_mylist f a = match a with
| Empty -> Empty
| Cons (h,t) -> Cons (f h, map_mylist f t)

It is clear from this example, that every inductive type
can have a map function generated by a purely mechanical
transformation on the type terms: that is, there
is no reason to ever write map functions again.

The result extends easily to multiple type variables,
a map function then requires multiple function arguments.

The result can *also* be extended to folds, iterators,
and other polymorphic algorithms (provided they're natural).

Notation: I suggest

	polymap[t]

denoted the map for an algebraic type, it has arity n+1
where n is the arity of the type functor.

Rules for generation of the map function
[brain dead non-tail recursive version]

1. We write let rec (mapname) (argumentlist) = function

2. If the type is a tuple, the result is a tuple of
mapped subterms (ditto for records).

3. If the type is a sum (either kind), the result is
a function with a list of match cases, the result
is the same constructor with mapped arguments.

4. If the type is a constant, the result is that constant

5. If the type is a type variable, the corresponding
mapping function applied to the subterm: 'f is replaced
by f x (where x names the subterm).

6. If the type is a functor application (type constructor),
the result is a polymap of the functor applied to the mapped
arguments and the corresponding match term.

7. Handling abstract types. In order to actually summon
the above code generations, we posit a new binding construction:

	let <new_name> = polymap <type> in

if the definition of <type> contains any opaque types,
including any abstract type of a module, primitive
not known in Pervasives, or, a class, then the client
must supply the mapping function as follows:

	let <new_name> = polymap <type> with polymap list = List.map in
etc.

The same mechanism can be provided for folds, iterators,
etc. Because this is a first order system, we have to hand
write the functorial transformation each time.

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-22 18:25 [Caml-list] First order compile time functorial polymorphism in Ocaml John Skaller
@ 2003-06-22 19:03 ` Michal Moskal
  2003-06-23  3:52   ` John Max Skaller
  2003-06-23  8:07 ` Francois Rouaix
                   ` (2 subsequent siblings)
  3 siblings, 1 reply; 18+ messages in thread
From: Michal Moskal @ 2003-06-22 19:03 UTC (permalink / raw)
  To: John Skaller; +Cc: caml-list

On Mon, Jun 23, 2003 at 04:25:18AM +1000, John Skaller wrote:
> In ML style functional programming languages like Ocaml,
> we have what is termed data polymorphism. This provides
> a kind of code reuse we're all familiar with.
> 
> However, there is another kind of polymophism
> which Ocaml does not provide. Two things to consider here:
> 
> 1. Every data structure has a map function.
> 2. User defined algebraic type require a hand written map function
> 
> It sure is inconvenient to have to remember the names
> of all those map functions, not to mention having to hand
> write them. Lets look at a map function:
> 
> type 'a mylist = Empty | Cons of 'a * 'a list
> 
> let rec map_mylist f a = match a with
> | Empty -> Empty
> | Cons (h,t) -> Cons (f h, map_mylist f t)
>
> It is clear from this example, that every inductive type
> can have a map function generated by a purely mechanical
> transformation on the type terms: that is, there
> is no reason to ever write map functions again.

First thing to consider: map function of this kind only exists for types,
where type variables occur only positively. Even then, for inductive
types it requires proof (it isn't as simple as it first seems).

For example consider:

type 'a t = Foo 'a -> unit

To map : 'a t -> 'b t here, you need f : 'b -> 'a.

[...]
> 7. Handling abstract types. In order to actually summon
> the above code generations, we posit a new binding construction:
> 
> 	let <new_name> = polymap <type> in
> 
> if the definition of <type> contains any opaque types,
> including any abstract type of a module, primitive
> not known in Pervasives, or, a class, then the client
> must supply the mapping function as follows:
> 
> 	let <new_name> = polymap <type> with polymap list = List.map in
> etc.

What about t1 -> t2? (this is the real problem).
 
> The same mechanism can be provided for folds, iterators,
> etc. Because this is a first order system, we have to hand
> write the functorial transformation each time.

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

I once wrote (in OCaml) interpreter for language with automatic
definitions of iterators and recursors, based on PhD thesis of Zdzislaw
Splawski. Unfortunately while I can provide source code, thesis is not
available online, and without it it will be hard to understand source
(i.e. the iterator/recursor generation part).

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-22 19:03 ` Michal Moskal
@ 2003-06-23  3:52   ` John Max Skaller
  2003-06-23  9:58     ` Michal Moskal
  2003-06-23 10:08     ` Markus Mottl
  0 siblings, 2 replies; 18+ messages in thread
From: John Max Skaller @ 2003-06-23  3:52 UTC (permalink / raw)
  To: Michal Moskal; +Cc: caml-list

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-22 18:25 [Caml-list] First order compile time functorial polymorphism in Ocaml John Skaller
  2003-06-22 19:03 ` Michal Moskal
@ 2003-06-23  8:07 ` Francois Rouaix
  2003-06-23  9:03   ` Roberto Di Cosmo
  2003-06-23 17:37   ` John Max Skaller
  2003-06-23  9:03 ` Jun.Furuse
  2003-06-23 18:02 ` Jacques Carette
  3 siblings, 2 replies; 18+ messages in thread
From: Francois Rouaix @ 2003-06-23  8:07 UTC (permalink / raw)
  To: John Skaller; +Cc: caml-list

John,
Sounds like Camlp4 work to me.
If you haven't seen IoXML, you might want to look at it.
It generates type-specific code at
compile-time to support marshalling to and from XML.
Copy-pasting and adapting to morphisms should be
a simple exercise.

--f


On Sunday, Jun 22, 2003, at 20:25 Europe/Paris, John Skaller wrote:

> In ML style functional programming languages like Ocaml,
> we have what is termed data polymorphism. This provides
> a kind of code reuse we're all familiar with.
>
> However, there is another kind of polymophism
> which Ocaml does not provide. Two things to consider here:
>
> 1. Every data structure has a map function.
> 2. User defined algebraic type require a hand written map function
>
> It sure is inconvenient to have to remember the names
> of all those map functions, not to mention having to hand
> write them. Lets look at a map function:
>
> type 'a mylist = Empty | Cons of 'a * 'a list
>
> let rec map_mylist f a = match a with
> | Empty -> Empty
> | Cons (h,t) -> Cons (f h, map_mylist f t)
>
> It is clear from this example, that every inductive type
> can have a map function generated by a purely mechanical
> transformation on the type terms: that is, there
> is no reason to ever write map functions again.
>
> The result extends easily to multiple type variables,
> a map function then requires multiple function arguments.
>
> The result can *also* be extended to folds, iterators,
> and other polymorphic algorithms (provided they're natural).
>
> Notation: I suggest
>
> 	polymap[t]
>
> denoted the map for an algebraic type, it has arity n+1
> where n is the arity of the type functor.
>
> Rules for generation of the map function
> [brain dead non-tail recursive version]
>
> 1. We write let rec (mapname) (argumentlist) = function
>
> 2. If the type is a tuple, the result is a tuple of
> mapped subterms (ditto for records).
>
> 3. If the type is a sum (either kind), the result is
> a function with a list of match cases, the result
> is the same constructor with mapped arguments.
>
> 4. If the type is a constant, the result is that constant
>
> 5. If the type is a type variable, the corresponding
> mapping function applied to the subterm: 'f is replaced
> by f x (where x names the subterm).
>
> 6. If the type is a functor application (type constructor),
> the result is a polymap of the functor applied to the mapped
> arguments and the corresponding match term.
>
> 7. Handling abstract types. In order to actually summon
> the above code generations, we posit a new binding construction:
>
> 	let <new_name> = polymap <type> in
>
> if the definition of <type> contains any opaque types,
> including any abstract type of a module, primitive
> not known in Pervasives, or, a class, then the client
> must supply the mapping function as follows:
>
> 	let <new_name> = polymap <type> with polymap list = List.map in
> etc.
>
> The same mechanism can be provided for folds, iterators,
> etc. Because this is a first order system, we have to hand
> write the functorial transformation each time.
>
> -- 
> 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
>
>

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23  8:07 ` Francois Rouaix
@ 2003-06-23  9:03   ` Roberto Di Cosmo
  2003-06-23 17:37   ` John Max Skaller
  1 sibling, 0 replies; 18+ messages in thread
From: Roberto Di Cosmo @ 2003-06-23  9:03 UTC (permalink / raw)
  To: francois, skaller; +Cc: caml-list

As far as I remember, automatic generation of map/fold etc. is one of the example
found in the seminal paper on CamlP4 ... I think Daniel and Michel might give
you the example out oh their head :-)

--Roberto

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-22 18:25 [Caml-list] First order compile time functorial polymorphism in Ocaml John Skaller
  2003-06-22 19:03 ` Michal Moskal
  2003-06-23  8:07 ` Francois Rouaix
@ 2003-06-23  9:03 ` Jun.Furuse
  2003-06-23 17:53   ` John Max Skaller
  2003-06-23 18:02 ` Jacques Carette
  3 siblings, 1 reply; 18+ messages in thread
From: Jun.Furuse @ 2003-06-23  9:03 UTC (permalink / raw)
  To: John Skaller; +Cc: caml-list

Hello,

At Mon, 23 Jun 2003 04:25:18 +1000,
John Skaller wrote:
> 
> In ML style functional programming languages like Ocaml,
> we have what is termed data polymorphism. This provides
> a kind of code reuse we're all familiar with.
> 
> However, there is another kind of polymophism
> which Ocaml does not provide. Two things to consider here:
> 
> 1. Every data structure has a map function.
> 2. User defined algebraic type require a hand written map function

Yes, I agree that writing map or fold function over again and again is 
trivial and boring.

Your approach reminds me polytypic programming or so-called 
"generic programming"[1] in Haskell. I have also considered a bit about 
the possibility of this "generic programming" in O'Caml. Actually, 
I think our "generics" (= G'Caml) has already had allmost of all 
the internal functionalities for so-called "generics" in Haskell
community. Only one possible problem of "generics" on Caml is that
type constructors of Caml is not so "mathematically pure" as Haskell.
I still do not have clear idea how to declare generic case for n-ary
tuples, objects and labeled function types of Caml...

Anyway, "generics" are too general solution for your purpose.
This is not something I can prepare for you in this week. :-)

[1]: Generic Haskell project
	http://www.cs.uu.nl/research/projects/generic-haskell/

--
Jun

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23  3:52   ` John Max Skaller
@ 2003-06-23  9:58     ` Michal Moskal
  2003-06-23 10:27       ` Markus Mottl
  2003-06-23 10:08     ` Markus Mottl
  1 sibling, 1 reply; 18+ messages in thread
From: Michal Moskal @ 2003-06-23  9:58 UTC (permalink / raw)
  To: John Max Skaller; +Cc: caml-list

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23  3:52   ` John Max Skaller
  2003-06-23  9:58     ` Michal Moskal
@ 2003-06-23 10:08     ` Markus Mottl
  1 sibling, 0 replies; 18+ messages in thread
From: Markus Mottl @ 2003-06-23 10:08 UTC (permalink / raw)
  To: John Max Skaller; +Cc: Michal Moskal, caml-list

On Mon, 23 Jun 2003, John Max Skaller wrote:
> >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.

This problem (generalizing fold/unfold to exponentials that use
the type constructor also in contravariant positions) is solved by
applying a solution for modelling recursive datatypes as fixed points
of difunctors. See the following very nice paper for details:

  Title:   Bananas in space: extending fold and unfold to exponential types
  Authors: Erik Meijer and Graham Hutton

What you need in your example is a cofunctor "f" together with a function
"comap", which takes the functional (a -> b) to (f b -> f a).

In the mixed case (co- and contravariant occurrences in the same type
definition) you need difunctors (see paper for details).

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23  9:58     ` Michal Moskal
@ 2003-06-23 10:27       ` Markus Mottl
  2003-06-23 10:35         ` Michal Moskal
  0 siblings, 1 reply; 18+ messages in thread
From: Markus Mottl @ 2003-06-23 10:27 UTC (permalink / raw)
  To: Michal Moskal; +Cc: John Max Skaller, caml-list

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23 10:27       ` Markus Mottl
@ 2003-06-23 10:35         ` Michal Moskal
  0 siblings, 0 replies; 18+ messages in thread
From: Michal Moskal @ 2003-06-23 10:35 UTC (permalink / raw)
  To: caml-list

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23  8:07 ` Francois Rouaix
  2003-06-23  9:03   ` Roberto Di Cosmo
@ 2003-06-23 17:37   ` John Max Skaller
  1 sibling, 0 replies; 18+ messages in thread
From: John Max Skaller @ 2003-06-23 17:37 UTC (permalink / raw)
  To: Francois Rouaix; +Cc: caml-list

Francois Rouaix wrote:

> John,
> Sounds like Camlp4 work to me.


That's my thinking too. I'm less worried about
a total solution than finding out just how
useful it actually is: not even much point
to do nasty proofs if the simple cases
prove useless. Still, I'm not sure if Camlp4
is smart enough to gather the required information.

[In my case, all the types are in an .mli file
which has no corresponding .ml file]

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23  9:03 ` Jun.Furuse
@ 2003-06-23 17:53   ` John Max Skaller
  0 siblings, 0 replies; 18+ messages in thread
From: John Max Skaller @ 2003-06-23 17:53 UTC (permalink / raw)
  To: Jun.Furuse; +Cc: caml-list

Jun.Furuse@inria.fr wrote:

> Yes, I agree that writing map or fold function over again and again is 
> trivial and boring.

	

	.. and leads to errors and poor design, when the design

	is based on laziness instead of modularity :-)

 
> Your approach reminds me polytypic programming or so-called 
> "generic programming"[1] in Haskell. 


	Its a jumbled up cut down verion of functorial
polymorphism, which i think is also called polytypy.

> I have also considered a bit about 
> the possibility of this "generic programming" in O'Caml. Actually, 
> I think our "generics" (= G'Caml) has already had allmost of all 
> the internal functionalities for so-called "generics" in Haskell
> community. 


	Hmm. Being a C++ programmer, saying 'generic' sounds
too much like dependent name lookup in templates :(

	template<class T> void f(T t) { g(t); }

Here, lookup on the dependent name g is delayed until
the template is instantiated, then the search is done in the
namespace in which the argument type is defined.

This 'genericity' is both very powerful, and also not very
robust. (I'd say it's not well-principled, but in practice
it is very expressive).

At least the idea with 'polymap' et al, is that it's based
on type *structure* not overloading (in particular,
separating the data from the shape).

Using the 'type variable' to denote the data part is
a bit of a hack. It isn't right. But in practice,
it may be workable for a first order solution.

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-22 18:25 [Caml-list] First order compile time functorial polymorphism in Ocaml John Skaller
                   ` (2 preceding siblings ...)
  2003-06-23  9:03 ` Jun.Furuse
@ 2003-06-23 18:02 ` Jacques Carette
  2003-06-24  1:00   ` Jacques Garrigue
  2003-06-24 12:45   ` John Max Skaller
  3 siblings, 2 replies; 18+ messages in thread
From: Jacques Carette @ 2003-06-23 18:02 UTC (permalink / raw)
  To: John Skaller, caml-list

I most certainly would welcome such a set of tools for reuse.

Has anyone seriously looked (from an ML point of view) at the "scrap your boilerplate" paper from the Haskell crowd ?

When faced with the following issue myself for a 'monster' algebraic datatype (but containing no negatives), I wrote 
the code found below.  I would welcome any and all criticisms of it [the code works and is useful, but is doubtless a 
horrible hack].

Jacques

(* part of a toy interpreted for a Maple-like language *)
open Maple;;

let rec generic_traverse filter f x = 
    let traverse r = generic_traverse filter f r in
    let activate z = if filter z then f z else z in
    let tt = function
    | Mint x as z -> activate z
    | Mbool x as z -> activate z
    | Mfloat(x,y) as z -> activate z
    | Mname x as z -> activate z
    | Mstring x as z -> activate z
    | Mlocal x as z -> activate z
    | Mexport x as z -> activate z
    | Mparam x as z -> activate z
    | Msum x -> activate(Msum (List.map traverse x))
    | Mprod x -> activate(Mprod (List.map traverse x))
    | Mpow(x,y) -> activate(Mpow(traverse x, traverse y))
    | Mcomp(o,x,y) -> activate(Mcomp(o, traverse x, traverse y))
    | Mtableref(n,i) -> activate(Mtableref( traverse n, List.map traverse i))
    | Mnot x -> activate(Mnot(traverse x))
    | Mand(x,y) -> activate(Mand(traverse x, traverse y))
    | Mor(x,y) -> activate(Mor(traverse x, traverse y))
    | Mxor(x,y) -> activate(Mxor(traverse x, traverse y))
    | Mimplies(x,y) -> activate(Mimplies(traverse x, traverse y))
    | Mrange(x,y) -> activate(Mrange(traverse x, traverse y))
    | Mproc x -> 
        let f = function
            | None -> None
            | Some z -> Some(traverse z) in
        let y=f x.mresult_type in 
        activate(Mproc( {
            mparams = List.map traverse x.mparams;
            mresult_type = y;
            mlocals = List.map traverse x.mlocals;
            mclosure = x.mclosure; (* do not traverse the closure! *)
            moptions = List.map traverse x.moptions;
            mdescription = List.map traverse x.mdescription;
            mbody = List.map traverse x.mbody
            } ))
    | Mmodule x -> activate(Mmodule( {
        mmod_params = List.map traverse x.mmod_params;
        mmod_locals = List.map traverse x.mmod_locals;
        mmod_exports = List.map traverse x.mmod_exports;
        mmod_closure = x.mmod_closure; (* do not traverse the closure! *)
        mmod_options = List.map traverse x.mmod_options;
        mmod_description = List.map traverse x.mmod_description;
        mbody_of_module = List.map traverse x.mbody_of_module
        } ))
    | Mfunc(n,i) -> activate(Mfunc( traverse n, List.map traverse i))
    | Mforfrom(i,ifrom,ito,iby,iwhile,body) ->
            activate(Mforfrom(traverse i, traverse ifrom, traverse ito,
                traverse iby, traverse iwhile, List.map traverse body))
    | Mforin(i,iin,iwhile,body) ->
            activate(Mforin(traverse i, traverse iin, traverse iwhile,
                List.map traverse body))
    | Mreturn x -> activate(Mreturn(traverse x))
    | Merror x -> activate(Merror(traverse x))
    | Mread x -> activate(Mread(traverse x))
    | Muneval x -> activate(Muneval(traverse x))
    | Msave x -> activate(Msave(List.map traverse x))
    | Mdcolon(x,y) -> activate(Mdcolon(traverse x, traverse y))
    | Massign(x,y) -> activate(Massign(List.map traverse x, List.map traverse y))
    | Mseq x -> activate(Mseq(List.map traverse x))
    | Mlist x -> activate(Mlist(List.map traverse x))
    | Mif (x,y,z) -> activate(Mif( (traverse x), (traverse y), (traverse z) ))
    | Mstatseq x -> activate(Mstatseq(List.map traverse x))
    (*| _ as x -> activate x *)
    in
    tt x
      ;;

(* example [fake] use *)

let filt = function
     | Mlist _ | Mseq _ -> true
     | _ -> false
and
     do_something = function
     | Mlist x -> List.map Simpl.flatten x
     | Mseq x -> List.map Simpl.flatten2 x
     | _ -> raise CannotHappenButCompilerCantKnowIt ;;

generic_traverse filt do_something my_maple_dag;;


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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23 18:02 ` Jacques Carette
@ 2003-06-24  1:00   ` Jacques Garrigue
  2003-06-24 12:45   ` John Max Skaller
  1 sibling, 0 replies; 18+ messages in thread
From: Jacques Garrigue @ 2003-06-24  1:00 UTC (permalink / raw)
  To: carette; +Cc: caml-list

From: "Jacques Carette" <carette@mcmaster.ca>

> I most certainly would welcome such a set of tools for reuse.
> 
> Has anyone seriously looked (from an ML point of view) at the "scrap
> your boilerplate" paper from the Haskell crowd ?
> 
> When faced with the following issue myself for a 'monster' algebraic
> datatype (but containing no negatives), I wrote the code found
> below.  I would welcome any and all criticisms of it [the code works
> and is useful, but is doubtless a horrible hack].
> 
> Jacques

My standard way to approach such problems is to use open recursion: I
find it simpler and more general. Yet you have to understand fixpoints
to use it properly.

let map_one f = function
  | Msum x -> Msum (List.map f x)
  | Mprod x -> Mprod (List.map f x)
  | Mpow(x,y) -> Mpow (f x, fy)
  ...
  | Mstateseq x -> Mstateseq (List.map f x)
  | Mint _ | Mbool _ | Mfloat _ | Mstring _ | Mlocal _
  | Mexport _ | Mparam _ as x -> x

Then you can derive all other mapping functions easily.

let rec generic_traverse filter f x =
  let z = map_one (generic_traverse filter f) x in
  if filter z then f z else z

let rec deep_map f x = f (map_one f x)

etc...

Or you can use it directly

let rec flatten x =
  match map_one flatten x with
  | Mlist x -> List.map Simpl.flatten x
  | Mseq x -> List.map Simpl.flatten2 x
  | x ->  x

Jacques (aussi)

Your original code:
> (* part of a toy interpreted for a Maple-like language *)
> open Maple;;
> 
> let rec generic_traverse filter f x = 
>     let traverse r = generic_traverse filter f r in
>     let activate z = if filter z then f z else z in
>     let tt = function
>     | Mint x as z -> activate z
>     | Mbool x as z -> activate z
>     | Mfloat(x,y) as z -> activate z
>     | Mname x as z -> activate z
>     | Mstring x as z -> activate z
>     | Mlocal x as z -> activate z
>     | Mexport x as z -> activate z
>     | Mparam x as z -> activate z
>     | Msum x -> activate(Msum (List.map traverse x))
>     | Mprod x -> activate(Mprod (List.map traverse x))
>     | Mpow(x,y) -> activate(Mpow(traverse x, traverse y))
>     | Mcomp(o,x,y) -> activate(Mcomp(o, traverse x, traverse y))
>     | Mtableref(n,i) -> activate(Mtableref( traverse n, List.map traverse i))
>     | Mnot x -> activate(Mnot(traverse x))
>     | Mand(x,y) -> activate(Mand(traverse x, traverse y))
>     | Mor(x,y) -> activate(Mor(traverse x, traverse y))
>     | Mxor(x,y) -> activate(Mxor(traverse x, traverse y))
>     | Mimplies(x,y) -> activate(Mimplies(traverse x, traverse y))
>     | Mrange(x,y) -> activate(Mrange(traverse x, traverse y))
>     | Mproc x -> 
>         let f = function
>             | None -> None
>             | Some z -> Some(traverse z) in
>         let y=f x.mresult_type in 
>         activate(Mproc( {
>             mparams = List.map traverse x.mparams;
>             mresult_type = y;
>             mlocals = List.map traverse x.mlocals;
>             mclosure = x.mclosure; (* do not traverse the closure! *)
>             moptions = List.map traverse x.moptions;
>             mdescription = List.map traverse x.mdescription;
>             mbody = List.map traverse x.mbody
>             } ))
>     | Mmodule x -> activate(Mmodule( {
>         mmod_params = List.map traverse x.mmod_params;
>         mmod_locals = List.map traverse x.mmod_locals;
>         mmod_exports = List.map traverse x.mmod_exports;
>         mmod_closure = x.mmod_closure; (* do not traverse the closure! *)
>         mmod_options = List.map traverse x.mmod_options;
>         mmod_description = List.map traverse x.mmod_description;
>         mbody_of_module = List.map traverse x.mbody_of_module
>         } ))
>     | Mfunc(n,i) -> activate(Mfunc( traverse n, List.map traverse i))
>     | Mforfrom(i,ifrom,ito,iby,iwhile,body) ->
>             activate(Mforfrom(traverse i, traverse ifrom, traverse ito,
>                 traverse iby, traverse iwhile, List.map traverse body))
>     | Mforin(i,iin,iwhile,body) ->
>             activate(Mforin(traverse i, traverse iin, traverse iwhile,
>                 List.map traverse body))
>     | Mreturn x -> activate(Mreturn(traverse x))
>     | Merror x -> activate(Merror(traverse x))
>     | Mread x -> activate(Mread(traverse x))
>     | Muneval x -> activate(Muneval(traverse x))
>     | Msave x -> activate(Msave(List.map traverse x))
>     | Mdcolon(x,y) -> activate(Mdcolon(traverse x, traverse y))
>     | Massign(x,y) -> activate(Massign(List.map traverse x, List.map traverse y))
>     | Mseq x -> activate(Mseq(List.map traverse x))
>     | Mlist x -> activate(Mlist(List.map traverse x))
>     | Mif (x,y,z) -> activate(Mif( (traverse x), (traverse y), (traverse z) ))
>     | Mstatseq x -> activate(Mstatseq(List.map traverse x))
>     (*| _ as x -> activate x *)
>     in
>     tt x
>       ;;
> 
> (* example [fake] use *)
> 
> let filt = function
>      | Mlist _ | Mseq _ -> true
>      | _ -> false
> and
>      do_something = function
>      | Mlist x -> List.map Simpl.flatten x
>      | Mseq x -> List.map Simpl.flatten2 x
>      | _ -> raise CannotHappenButCompilerCantKnowIt ;;

---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-23 18:02 ` Jacques Carette
  2003-06-24  1:00   ` Jacques Garrigue
@ 2003-06-24 12:45   ` John Max Skaller
  2003-06-24 14:34     ` Jacques Carette
  1 sibling, 1 reply; 18+ messages in thread
From: John Max Skaller @ 2003-06-24 12:45 UTC (permalink / raw)
  To: Jacques Carette; +Cc: caml-list

Jacques Carette wrote:

> I most certainly would welcome such a set of tools for reuse.

> would welcome any and all criticisms of it [the code works and is 
> useful, but is doubtless a horrible hack].
 
Curious: how useful? How many times did you reuse it?


Its a hack yes, looks ugly :(

Perhaps can do better with polymorphic variants.

Ugly separating the filter

for the special actions from those actions:

let filt = function
     | Mlist _ | Mseq _ -> true
     | _ -> false
and
     do_something = function
     | Mlist x -> List.map Simpl.flatten x
     | Mseq x -> List.map Simpl.flatten2 x

    | _ -> raise CannotHappenButCompilerCantKnowIt ;; 


Uggh. Like to be writing something like


	| `Mlist args -> ..
	| `Mseq args -> ..
	| _ -> ..

or perhaps

	| #usual_case ->

instead of the last line if there happens to be
a type partition matching the requirements.

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-24 12:45   ` John Max Skaller
@ 2003-06-24 14:34     ` Jacques Carette
  2003-06-24 23:45       ` Jacques Garrigue
  0 siblings, 1 reply; 18+ messages in thread
From: Jacques Carette @ 2003-06-24 14:34 UTC (permalink / raw)
  To: Jacques Carette; +Cc: caml-list

John Max Skaller <skaller@ozemail.com.au> wrote:
> Jacques Carette wrote:
> Curious: how useful? How many times did you reuse it?

I've used generic_traverse in a dozen places, and will likely use it more often.

> Its a hack yes, looks ugly :(

Oh, fully agreed!  The point of posting it was to get some constructive criticism in the hopes of being able to do 
better.

> Perhaps can do better with polymorphic variants.

My first prototype (which got wiped out in some disk crash) did use polymorphic variants.  I decide to not use them 
again to see if I really needed them.  And perhaps I do.

> Ugly separating the filter
> for the special actions from those actions:

Very much so, but I found the combined filter/action routines even harder to read, with more code duplication than I 
could swallow!!  So I used this 2-stage approach.

> Uggh. Like to be writing something like
> 	| `Mlist args -> ..
> 	| `Mseq args -> ..
> 	| _ -> ..

I will re-explore this.

> or perhaps
> 	| #usual_case ->
> instead of the last line if there happens to be
> a type partition matching the requirements.

I read about #types in the Ocaml manual.  Are you referring to using classes or the (documented obsolete) expansion of 
variant types ?

Even though  S. Boulmé, Th. Hardin, and R. Rioboo in
"Polymorphic Data Types, Objects, Modules and Functors: is it too much ?" (see 
http://www.lip6.fr/reports/lip6.2000.014.html) argue quite cogently about the use of the full power of Ocaml for doing 
mathematics [my real goal], I was hoping that for writing a language interpreter I did not need to go that far.

Jacques

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-24 14:34     ` Jacques Carette
@ 2003-06-24 23:45       ` Jacques Garrigue
  2003-06-25  2:27         ` John Max Skaller
  0 siblings, 1 reply; 18+ messages in thread
From: Jacques Garrigue @ 2003-06-24 23:45 UTC (permalink / raw)
  To: carette; +Cc: caml-list

From: "Jacques Carette" <carette@mcmaster.ca>

> > or perhaps
> > 	| #usual_case ->
> > instead of the last line if there happens to be
> > a type partition matching the requirements.
> 
> I read about #types in the Ocaml manual.  Are you referring to using
> classes or the (documented obsolete) expansion of variant types ?

I know this is a bit confusing, but this is the pattern case expansion
of polymorphic variants (the above is a pattern-matching, not a type),
and this is not obsolete.
The notatation is obsolete in types, as [< usual_case] is more
symmetric with [> usual_case]. By the way,
  fun #usual_case as x -> x
has type
  [< usual_case] -> [> usual_case]

But honestly, if you have no particular need to cut your type in small
pieces (you need it for incremental extension for instance), you're
better off with sum types, and the safe approach I presented in my
previous mail.

Jacques

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
  2003-06-24 23:45       ` Jacques Garrigue
@ 2003-06-25  2:27         ` John Max Skaller
  0 siblings, 0 replies; 18+ messages in thread
From: John Max Skaller @ 2003-06-25  2:27 UTC (permalink / raw)
  To: Jacques Garrigue; +Cc: carette, caml-list

Jacques Garrigue wrote:

> From: "Jacques Carette" <carette@mcmaster.ca>
 
> But honestly, if you have no particular need to cut your type in small
> pieces (you need it for incremental extension for instance), you're
> better off with sum types, and the safe approach I presented in my
> previous mail.

That was very cute! I'm implementing it now.
WITH polymorphic variants. WITH cutting up the types.
Even supports covariance via parameterisation trick.
Seems to work so far. I do use exact types though.

I expect the open recursion technique will actually
solve an outstanding problem. I have a two functions,
fold and unfold which operate on type representations.
Unfold is fine: its the identity unless the fixpoint
binder is the top term.

Fold doesn't work properly: it will undo a fold,
but it doesn't do what I really need: to minimise
the representation of a type be recursively
folding every node.

You just showed me how to fix that (in principle
at least): its very cute to modify a function that
works on the top level only, into one rebuilds the tree
bottom up.

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


^ permalink raw reply	[flat|nested] 18+ messages in thread

end of thread, other threads:[~2003-06-25  2:28 UTC | newest]

Thread overview: 18+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2003-06-22 18:25 [Caml-list] First order compile time functorial polymorphism in Ocaml John Skaller
2003-06-22 19:03 ` Michal Moskal
2003-06-23  3:52   ` John Max Skaller
2003-06-23  9:58     ` Michal Moskal
2003-06-23 10:27       ` Markus Mottl
2003-06-23 10:35         ` Michal Moskal
2003-06-23 10:08     ` Markus Mottl
2003-06-23  8:07 ` Francois Rouaix
2003-06-23  9:03   ` Roberto Di Cosmo
2003-06-23 17:37   ` John Max Skaller
2003-06-23  9:03 ` Jun.Furuse
2003-06-23 17:53   ` John Max Skaller
2003-06-23 18:02 ` Jacques Carette
2003-06-24  1:00   ` Jacques Garrigue
2003-06-24 12:45   ` John Max Skaller
2003-06-24 14:34     ` Jacques Carette
2003-06-24 23:45       ` Jacques Garrigue
2003-06-25  2:27         ` John Max Skaller

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).