(* Double-generic operations How to express transformations such as mapping or equality testing so that they are generic not only over the data types but also over the number of arguments. The goal is to use one formulation (or: structure, function) to describe both the family of map functions and the family of zipWithN functions. We should get various map/zip functions by instantiating the single framework, or `generic function'. This file shows how to do that using simple Hindley-Milner system, without kind polymorphism or type-level computations. The inspiration comes from type-indexed terms by Zhe Yang and functional unparsing by Olivier Danvy. *) (* The central combinator. One may claim it to be `the essence' of double genericity. *) let ( ** ) app k = fun x y -> k (app x y);; (* right-associative *) (* Given below are the instantiations of that `double generic function' to particular datatypes, and further instantiations to particular arities. *) (* Products *) (* For each data type, we have to define constructor, applicator, and projector. Here they are for pairs. *) let pc k a b = k (a,b);; let papp (f1,f2) (x1,x2) = (f1 x1, f2 x2);; let pu x = x;; (* Maps over pairs; instantiated to the different number of arguments *) (* The argument x below is merely for the sake of value restriction *) let pair_map1 x = pc pu x;; (* val pair_map1 : 'a -> 'b -> 'a * 'b = *) let pair_map2 x = pc (papp ** pu) x;; (* val pair_map2 : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd = *) let pair_map3 x = pc (papp ** papp ** pu) x;; (* val pair_map3 : ('a -> 'b -> 'c) -> ('d -> 'e -> 'f) -> 'a * 'd -> 'b * 'e -> 'c * 'f = *) let pair_map4 x = pc (papp ** papp ** papp ** pu) x;; (* val pair_map4 : ('a -> 'b -> 'c -> 'd) -> ('e -> 'f -> 'g -> 'h) -> 'a * 'e -> 'b * 'f -> 'c * 'g -> 'd * 'h = *) let testp1 = pair_map3 (+) (-) (1,2) (3,4);; (* (4,-2) *) (* Sums *) type ('a,'b) either = Left of 'a | Right of 'b;; (* To choose the shape of the data type (e.g., the branch of Either), we have to see the first argument. If we are certain about the shape, we use the D (decided) alternative below. Until then, we delay our decision and just carry all the information needed to make the decision, in the U (undetermined) alternative. *) type ('a,'b) choice = U of 'a | D of 'b;; let sc k a b = k (U (a,b));; (* Undecided *) let sapp f x = match (f,x) with | (U (f1,f2), Left x) -> D (Left (f1 x)) | (U (f1,f2), Right x) -> D (Right (f2 x)) | (D (Left f), Left x) -> D (Left (f x)) (* Decided branches must match *) | (D (Right f), Right x) -> D (Right (f x)) | _ -> failwith "sum: inconsistent shapes" ;; let su = function | D x -> x | U (x,y) -> Left x;; (* arbitrarily chose left *) (* Maps over sums; instantiated to the different number of arguments *) let sum_map1 x = sc su x;; (* val sum_map1 : 'a -> 'b -> ('a, 'c) either = *) let sum_map2 x = sc (sapp ** su) x;; (* val sum_map2 : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) either -> ('b, 'd) either *) let sum_map3 x = sc (sapp ** sapp ** su) x;; (* val sum_map3 : ('a -> 'b -> 'c) -> ('d -> 'e -> 'f) -> ('a, 'd) either -> ('b, 'e) either -> ('c, 'f) either *) let tests1 = sum_map3 (+) (-) (Left 1) (Left 2);; (* Left 3 *) let tests2 = sum_map1 0 1;; (* Left 0 *) (* Int *) (* This is a degenerate case. We do it just because we can. *) let ic k = k (U ());; let iapp f x = match (f,x) with | (U _, x) -> D x | (D x, y) when x = y -> D x | _ -> failwith "int: inconsistent shape, different integers" let iu = function | D x -> x | U _ -> 0 ;; let int_map1 = ic iu;; (* val int_map1 : int = 0 *) let int_map2 x = ic (iapp ** iu) x;; (* val int_map2 : int -> int = *) let int_map3 x = ic (iapp ** iapp ** iu) x;; (* val int_map3 : int -> int -> int = *) let testi1 = int_map1;; (* 0 *) let testi2 = int_map3 1 1;; (* 1 *) (* Lists: recursive sums of products *) let lc k a = k (U a);; (* Undecided *) let lu = function | D x -> x | U _ -> [];; let rec lapp f x = match (f,x) with | (U f, []) -> D [] | (U f, (x::xs)) -> D ((f x) :: lu (lapp (U f) xs)) | (D (f::fs), (x::xs)) -> D ((f x) :: lu (lapp (D fs) xs)) | (D [], []) -> D [] | _ -> failwith "list: inconsistent shapes" ;; let list_map1 x = lc lu x;; (* val list_map1 : 'a -> 'b list = *) let list_map2 x = lc (lapp ** lu) x;; (* val list_map2 : ('a -> 'b) -> 'a list -> 'b list *) let list_map3 x = lc (lapp ** lapp ** lu) x;; (* val list_map3 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list *) let testl1 = list_map3 (+) [1;2;3] [4;5;6];; (* zipWith (+), essentially *) (* [5;7;9] *) (* Equality: a different doubly-generic function *) (* We reuse most of the previous structure *) let peu = function | (true,true) -> true | _ -> false;; let pair_eq1 x = pc peu x;; (* this is AND *) (* val pair_eq1 : bool -> bool -> bool = *) let pair_eq2 x = pc (papp ** peu) x;; (* val pair_eq2 : ('a -> bool) -> ('b -> bool) -> 'a * 'b -> bool *) let pair_eq3 x = pc (papp ** papp ** peu) x;; (* val pair_eq3 : ('a -> 'b -> bool) -> ('c -> 'd -> bool) -> 'a * 'c -> 'b * 'd -> bool *) let teste1 = pair_eq3 (>) (<) (1,2) (2,3);; (* false *) let teste2 = pair_eq3 (<) (<) (1,2) (2,3);; (* true *)