We explore the possibility of doing generic programming with ornaments. The idea is that any first-order datatype with one type argument can be mapped to the following structure representing sums of products:
| type 'a gsum = | GSumZ of 'a gprod | GSumS of 'a gsum and 'a gprod = | GNil | GCons of 'a gval * 'a gprod and 'a gval = | GData of 'a gsum | GParam of 'a |
A value is then given by a choice of a constructor (whose position
is encoded in unary by the constructors GSumZ and GSumS
of the type 'a gsum). Then, the arguments of the constructors
are encoded as a list ('a gprod) of generic values
('a gval). A generic value is either a value of a datatype
(again represented as a sum of products), or a value whose type
is the type argument 'a, represented by the constructor
'a gparam.
We can define a generic gmap function on this type, that
applies a function to all GParam:
| let gmap f = let rec gsum x = match x with | GSumZ p -> GSumZ (gprod p) | GSumS s -> GSumS (gsum s) and gprod x = match x with | GNil -> GNil | GCons(v,vs) -> GCons(gval v, gprod vs) and gval x = match x with | GData s -> GData (gsum s) | GParam y -> GParam (f y) in gval |
Now, let us consider the type of lists:
| type 'a list = | Nil | Cons of 'a * 'a list |
As an intermediate step for ornamentation, we will use the following representation of lists
where tuples of arguments have been transformed into right-nested pairs, terminated with
unit (mimicking the structure of 'a gsum).
| type u = U type 'a alist = | ANil of u | ACons of ('a * ('a alist * u)) |
This is isomorphic to lists, as witnessed by the following ornament:
| type ornament 'a alist_list : 'a alist => 'a list with | ANil U => Nil | ACons(x,xs) => Cons(x,xs) when xs : 'a alistu_list and 'a alistu_list : ('a alist * u) => 'a list with | (xs, U) => xs when xs : 'a alist_list |
We now define lists as an ornament of the generic reprensentation. The ornament is quite heavy, but the constructions is completely systematic and could be automated:
| type ornament 'a gval_list : 'a gval => 'a alist with | GData s => s when s : 'a gsum1_list | GParam x => ~ and 'a gval_val : 'a gval => 'a with | GData s => ~ when s : 'a gsum1_list | GParam x => x and 'a gsum1_list : 'a gsum => 'a alist with | GSumZ p => ANil p when p : 'a gprodNil0_list | GSumS s => ACons s when s : 'a gsum0_list and 'a gsum0_list : 'a gsum => ('a * ('a alist * u)) with | GSumZ p => p when p : 'a gprodCons2_list | GSumS s => ~ when s : 'a gsum0_list and 'a gprodNil0_list : 'a gprod => u with | GNil => U | GCons(v,vs) => ~ when v : 'a gval_list, vs : 'a gprodNil0_list and 'a gprodCons0_list : 'a gprod => u with | GNil => U | GCons(v,vs) => ~ when v : 'a gval_list, vs : 'a gprodCons0_list and 'a gprodCons1_list : 'a gprod => ('a alist * u) with | GNil => ~ | GCons(v,vs) => (v,vs) when v : 'a gval_list, vs : 'a gprodCons0_list and 'a gprodCons2_list : 'a gprod => 'a * ('a alist * u) with | GNil => ~ | GCons(v,vs) => (v,vs) when v : 'a gval_val, vs : 'a gprodCons1_list |
Unfortunately, we cannot lift gmap directly using this ornament,
because some calls to (e.g.) gprod will be ornamented with different
types. We have to unfold the function gmap following the structure
of the ornament. Thus, the unfolded versions will be named according to the
ornament that they match:
| let gmap_unfolded f = let rec gsum0 x = match x with | GSumZ p -> GSumZ (gprodCons2 p) | GSumS s -> GSumS (gsum0 s) and gsum1 x = match x with | GSumZ p -> GSumZ (gprodNil0 p) | GSumS s -> GSumS (gsum0 s) and gprodNil0 x = match x with | GNil -> GNil | GCons(v,vs) -> GCons(gval_list v, gprodNil0 vs) and gprodCons2 x = match x with | GNil -> GNil | GCons(v,vs) -> GCons(gval_val v, gprodCons1 vs) and gprodCons1 x = match x with | GNil -> GNil | GCons(v,vs) -> GCons(gval_list v, gprodCons0 vs) and gprodCons0 x = match x with | GNil -> GNil | GCons(v,vs) -> GCons(gval_list v, gprodCons0 vs) and gval_list x = match x with | GData s -> GData (gsum1 s) | GParam y -> GParam (f y) and gval_val x = match x with | GData s -> GData (gsum1 s) | GParam y -> GParam (f y) in gval_list |
This unfolding depends on the ornament we want to use. As future work, we want to make the generation of such unfoldings automatic given the desired ornament.
We can then ask for a lifting, first to alist, then to list:
| let map_alist = lifting gmap_unfolded : ('a -> 'b) -> 'a gval_list -> 'b gval_list let map_list = lifting map_alist : ('a -> 'b) -> 'a alist_list -> 'b alist_list |
We obtain the following codes for map_alist and map_list:
| let map_alist f = let rec gsum0 x = gprodCons2 x and gsum1 x = match x with | ANil p -> ANil (gprodNil0 p) | ACons s -> ACons (gsum0 s) and gprodNil0 x = U and gprodCons2 x = match x with | (v, vs) -> (gval_val v, gprodCons1 vs) and gprodCons1 x = match x with | (v, vs) -> (gval_list v, gprodCons0 vs) and gprodCons0 x = U and gval_list x = gsum1 x and gval_val x = f x in gval_list let map_list f = let rec gsum0 x = gprodCons2 x and gsum1 x = match x with | Nil -> Nil | Cons(x, xs) -> begin match gsum0 (x, xs) with | (x, xs) -> Cons(x, xs) end and gprodCons2 x = match x with | (v, vs) -> (gval_val v, gprodCons1 vs) and gprodCons1 x = gval_list x and gval_list x = gsum1 x and gval_val x = f x in gval_list |
Notice that the code of map_list contains construction and destruction of
intermediate structures: these are the intermediate structures used in
alist. The compiler can inline the recursive calls to eliminate these structures.
We could also provide hints to the prototype indicating which calls to inline.
The elimination of redundant structure would then be done by match elimination,
giving back a more natural term.