🚀 go-pugleaf

Continuing the discussion about generic free types,
it seems to me that they would be prefectly OK in Z because
they have a direct translation into existing Z.

At present we can define a tree of integers (using Z for the integers):


	ITREE = leaf<<Z>> | join<< Z X ITREE X ITREE>>

This stands for (more or less)

	[ITREE]

	[ leaf: Z -> ITREE; join: Z X ITREE X ITREE -> ITREE |
	  
	  your favourite axiomatisation of freely generated ]

and is a convenient shorthand for the axioms defining
freely generated.


A similar interpretation can be given to generic free types.
Consider a putative generic tree type:

	TREE[A] = leaf<<A>> | join<< A X TREE[A] X TREE[A]>>

with ITREE defined using it:

	ITREE = TREE[Z]

What does this mean? Consider the schema


 *- TREE[A, B] -----------------------------------------
 |
 | leaf: A -> B
 |
 | join: A X B X B -> B
 |
 +------------------------------------------------------
 |
 | leaf and join are bijections onto their ranges,
 | their ranges partition B,
 | B is the least set closed under join
 | (or any of the many equivalent closure properties)
 +------------------------------------------------------

We can now declare ITREE and assert the TREE property of it:

	[ITREE]

	TREE[Z, ITREE]

More generally, a generic free type


	Free[A] = f1<< Type1>> | .... | fn<< Typen>>

Corresponds to the schema

 *- Free[A, B] -----------------------------------------
 |
 | f1: Type1(B/Free[A]) -> B
 |
 | ...
 |
 | fn: Typen(B/Free[A]) -> B
 |
 +------------------------------------------------------
 | The fi are bijections onto their ranges,
 | the ranges partition B,
 | closure property (B is closed under any fj with B as 
 | an argument type)
 +------------------------------------------------------

 where Type1(B/Free[A]) means Type1 with B substituted for Free[A].


 An instance C = Free[D] corresponds to

	[C]
	Free[C,D]

Thus, we interpret a generic free type as a schema which can be
used to define instances.  Indeed, one can use this technique to
simulate generic free types in Z today.
The same technique extends to free types of more than one 
parameter, and is equivalent to the present semantics for
zero parameters.


Mike Wray

 
 +----------------------------------+-------------------------------------+
 |                                  |   Mike Wray                         |
 |     mjw@hplb.hpl.hp.co.uk        |   Hewlett-Packard Laboratories      |
 |     mjw@hplb.hpl.hp.com          |   Filton Road                       |
 |                                  |   Stoke Gifford                     |
 +----------------------------------+   Bristol        BS12 6QZ           |
 | Phone +44 272 228262 Direct      |   UK                                |
 |       +44 272 799910 Switchboard |                                     |
 +----------------------------------+-------------------------------------+