(* Higher-kinded polymorphism: polymorphism over sequences
The running example from the article.
*)
(* Lead-up to the higher-kind polymorphism *)
let rec sumi : int list -> int = function [] -> 0 | h::t -> h + sumi t
(* abstracting over 0 and (+) *)
let rec foldi (f: int->int->int) (z: int) : int list -> int =
function [] -> z | h::t -> f h (foldi f z t)
(* abstracting over int type *)
let rec fold (f: 'a->'a->'a) (z: 'a) : 'a list -> 'a =
function [] -> z | h::t -> f h (fold f z t)
(* collecting 'f' and 'z' into a record: a polymorphic record *)
type 'a monoid = {op: 'a->'a->'a; unit: 'a}
(* Monoidal fold *)
let rec foldm (m: 'a monoid) : 'a list -> 'a =
function [] -> m.unit | h::t -> m.op h (foldm m t)
(* examples *)
let monoid_plus : int monoid = {op=(+); unit=0}
let[@warning "-8"] 6 = foldm monoid_plus [1;2;3]
let monoid_maxchar : char monoid = {op=max; unit=Char.chr 0}
let[@warning "-8"] 'c' = foldm monoid_maxchar ['b';'c';'a']
(* We would like now to abstract over 'list' as we earlier abstracted over
'int'. In a hypothetical OCaml, in which 'F is a * -> * type variable,
we could write
type ('a,'F) seq = {decon: 'a 'F -> ('a * 'a 'F) option}
let rec folds (m:'a monoid) (s:('a,'F) seq) : 'a 'F -> 'a = fun c ->
match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
*)
(* ------------------------------------------------------------------------
The first approach to higher-kind polymorphism: using the module system
It is rather verbose and cumbersome
*)
module type seq_i = sig
type 'a t (* sequence type *)
val decon : 'a t -> ('a * 'a t) option
end
module FoldS(S:seq_i) = struct
let rec fold (m:'a monoid) : 'a S.t -> 'a = fun c ->
match S.decon c with None -> m.unit | Some (h,t) -> m.op h (fold m t)
end
(* Using FoldS.fold, to sum up a sequence. It also becomes a functor *)
module SumS(S:seq_i) = struct
open S
open FoldS(S)
let sum : int t -> int = fold monoid_plus
end
(* Usage example *)
module ListS = struct
type 'a t = 'a list
let decon = function [] -> None | h::t -> Some (h,t)
end
let[@warning "-8"] 6 =
let module M = SumS(ListS) in M.sum [1;2;3]
module ArrS = struct
type 'a t = int * 'a array
let decon (i,a) =
if i >= Array.length a || i < 0 then None else Some (a.(i), (i+1,a))
end
let[@warning "-8"] 6 =
let module M = SumS(ArrS) in M.sum (0,[|1;2;3|])
(* ------------------------------------------------------------------------
The second approach to the higher-kinded polymorphism:
Yallop and White's `Lightweight higher-kinded polymorphism'
Consider the type 'a list again. It is a parameterized type: 'a is the
type of elements, and `list' tells `the base name', so to speak.
Exactly the same information can be expressed differently, as the type
('a,list_name) app
Here, ('a,'b) app is a fixed type, and list_name is the ordinary type
that tells the base name.
The fact that the two representations are equivalent is witnessed by the
bijection:
inj: 'a list -> ('a,list_name) app
prj: ('a,list_name) app -> 'a list
Here is a way to implement it.
*)
type ('a,'b) app = ..
type list_name
type ('a,'b) app += List_name : 'a list -> ('a,list_name) app
(* it is easy to verify that in this case, inj x = List_name x and
prj (List_name x) = x
and the two are indeed inverses of each other
*)
(* The key is that list_name is the ordinary, kind *, type
Thus the base-name-polymorphism becomes the ordinary polymorphism
*)
(* Then we can write the earlier desired code almost exactly as we
wanted
*)
type ('a,'n) seq = {decon: ('a,'n) app -> ('a * ('a,'n) app) option}
let rec folds (m:'a monoid) (s:('a,'n) seq) : ('a,'n) app -> 'a = fun c ->
match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
(* example of using folds: straightforward as folds is an ordinary
polymorphic function
*)
let sums s c = folds monoid_plus s c
(* val sums : (int, 'a) seq -> (int, 'a) app -> int = *)
(* usage example *)
let[@warning "-8"] list_seq : ('a,list_name) seq =
{decon = fun (List_name l) ->
match l with [] -> None | h::t -> Some (h,List_name t)}
let[@warning "-8"] 6 = sums list_seq (List_name [1;2;3])
(* There is still a bit of awkwardness remains: the user have to think up
the base name like list_name and the tag like List_name,
and ensure uniqueness.
Yallop and White automate using the module system:
*)
module Newtype1(S:sig type 'a t end)() = struct
type tname (* the functor is generative, so
tname and Tag are unique
*)
type ('a,'b) app += Tag : 'a S.t -> ('a,tname) app
let inj : 'a S.t -> ('a,tname) app = fun x -> Tag x
let prj : ('a,tname) app -> 'a S.t = function
| Tag x -> x
| _ -> assert false
end
module ArrSeq = Newtype1(struct type 'a t = int * 'a array end)()
let arr_seq =
{decon = fun c ->
let (i,a) = ArrSeq.prj c in
if i >= Array.length a || i < 0 then None else
Some (a.(i), ArrSeq.inj (i+1, a))}
(* val arr_seq : ('a, ArrSeq.tname) seq = {decon = } *)
let[@warning "-8"] 6 = sums arr_seq (ArrSeq.inj (0,[|1;2;3|]))
(* There is a different variation of the same idea: see the end of the file *)
(* ------------------------------------------------------------------------
Again reduction to the ordinary polymorphism
*)
module type seq_i = sig
type a (* element type *)
type t (* sequence type *)
val decon : t -> (a * t) option
end
type ('a,'t) seq = (module seq_i with type a='a and type t='t)
(* The signature is needed here! Artifact of first-class modules *)
let rec folds : type a t. a monoid -> (a,t) seq -> t -> a =
fun m ((module S) as s) c ->
match S.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
(* As easy as with Yallop & White method: after all, folds is
ordinarily polymorphic
*)
let sums s c = folds monoid_plus s c
(* val sums : (int, 'a) seq -> 'a -> int = *)
(* Usage example *)
let list_seq : type e. (e,e list) seq = (* signature is needed *)
(module struct
type a = e
type t = e list
let decon l = match l with [] -> None | h::t -> Some (h,t)
end)
let[@warning "-8"] 6 = sums list_seq [1;2;3]
(* we can do even beter: non-polymorphic data structure
cf. data families in Haskell
Yallop and White method can do the same.
*)
let string_seq : (char,int*string) seq =
(module struct
type a = char
type t = int*string
let decon (i,s) =
if i >= String.length s || i < 0 then None else Some (s.[i], (i+1, s))
end)
let[@warning "-8"] 'c' = folds monoid_maxchar string_seq (0,"bca")
(* Likewise, we can represent an in_channel as a seq of chars *)
(* ------------------------------------------------------------------------
Avoiding higher-kinded polymorphism
Upon close inspection, it is not actually needed in our running example.
*)
(* Essentially: the type plus the free type variables of a type *)
type ('a,'t) seq = {decon: 't -> ('a * 't) option}
(* ordinary polymorphic function *)
let rec folds (m: 'a monoid) (s: ('a,'t) seq) : 't -> 'a = fun c ->
match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
let sums s c = folds monoid_plus s c
(* val folds : 'a monoid -> ('a, 't) seq -> 't -> 'a = *)
(* usage example *)
let list_seq : ('a,'a list) seq =
{decon = function [] -> None | h::t -> Some (h,t)}
let[@warning "-8"] 6 = sums list_seq [1;2;3]
(* we can do even beter: non-polymorphic data structure
cf. data families in Haskell
Yallop and White method can do the same.
*)
let string_seq : (char,int*string) seq =
{decon = fun (i,s) ->
if i >= String.length s || i < 0 then None else Some (s.[i], (i+1, s))}
let[@warning "-8"] 'c' = folds monoid_maxchar string_seq (0,"bca")
(* A different example, for map *)
type ('a,'b,'at,'bt) ftor = {map: ('a->'b) -> ('at -> 'bt)}
(* A way to avoid too many type parameters, at least, overtly,
and group them
*)
type ('f,'g) ftor = {map: ('a->'b) -> ('at -> 'bt)}
constraint 'a*'at = 'f
constraint 'b*'bt = 'g
let ftor_list = {map = fun f l -> List.map f l}
(* val ftor_list : ('a * 'a list, 'b * 'b list) ftor = {map = } *)
let char_int ft c = ft.map Char.chr c
let _ = char_int ftor_list [49;50;51]
(* ------------------------------------------------------------------------
Perfect tree folding: example from Yallop and White (2014), Sec 2.1
The example is quite a bit contrived: instead of defining
'a perfect as a data type, use the tagless-final style to
start with. Then fold is automatic.
It is particularly better to define perfect as the following
algebra:
type ('a,'depth) f
val zero : 'a -> ('a,z) f
val succ : ('a,'d) f * ('a,'d) f -> ('a, 'd s) f
we get the same perfection guarantees, plus we can actually sum up
the elements of (int,'d) f, without jumping through lots of hoops.
The whole topic of nested data types seems awfully contrived
*)
(* Perfectly balanced binary trees, with 2^n elements
It is a nested (not regular) data type
*)
type 'a perfect = Zero of 'a | Succ of ('a * 'a) perfect
(* reminds of tagless-final. It is an algebra, rather than a co-algebra
as seq before
*)
module type perfect_folder = sig
type 'a f
val zero : 'a -> 'a f
val succ : ('a * 'a) f -> 'a f
end
module FoldP(F:perfect_folder) = struct
(* polymorphic recursion *)
let rec foldp : type a. a perfect -> a F.f = function
| Zero x -> F.zero x
| Succ x -> foldp x |> F.succ
end
(* instances (interpreters) *)
module FolderPTree = struct
type 'a f = 'a perfect
let zero x = Zero x
let succ x = Succ x
end
module FolderList = struct
type 'a f = 'a list
let zero x = [x]
let succ x = x |> List.map (fun (x,y) -> [x;y]) |> List.concat
end
(* trying to make it first-class
module Folded : functor (F:perfect_folder) -> sig val res : 'a F.f end
*)
module type folded = sig
type a
module M: functor (F:perfect_folder) -> sig val res : a F.f end
end
type 'a folded = (module folded with type a = 'a)
(* making foldp a term *)
let foldp : type b. b perfect -> b folded = fun ptree ->
(module struct
type a = b
module M(F:perfect_folder) = struct
module M'=FoldP(F)
let res = M'.foldp ptree
end
end)
let ptree1 = Succ (Succ (Zero ((1,2),(3,4))))
let _ = let module R = (val (foldp ptree1)) in
let module RM = R.M(FolderList) in
RM.res
(* This is Dolan's solutions from 2015 *)
(* needs set up, but can hide the passing of perfect_folder implementations
*)
;;