Merge pull request #2 from ocamllabs/flops-examples

Example code from the FLOPS paper.

Makefile

@@ -12,7 +12,10 @@ LIBINSTALL_FILES := higher.mli higher.cmi \
 
 all: byte-code-library native-code-library
 
-install: libinstall
+examples-install:
+	ocamlfind install -add higher examples/*
+
+install: libinstall examples-install
 uninstall: libuninstall
 
 include $(OCAMLMAKEFILE)

examples/README.md

@@ -0,0 +1,28 @@
+The code in this directory is taken from the paper "[Lightweight Higher-Kinded Polymorphism][higher-paper]" (Jeremy Yallop and Leo White).  The following examples are available:
+
+[higher-paper]: https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf
+
+* [typed defunctionalization](typed-defunctionalization.ml) (Section 1.2)
+* [folds over perfect trees](example-1-perfect-trees.ml) (Section 2.1)
+* [Leibniz equality](example-2-leibniz.ml) (Section 2.2)
+* [the codensity transform](example-3-codensity.ml) (Section 2.3)
+* [kind polymorphism](example-4-kind-polymorphism.ml) (Section 2.4)
+
+Most of the code depends on the [higher][higher] library, which you can install using [opam][opam].  Once higher is installed you can load the examples into the top level directly:
+
+```
+  $ ocaml
+        OCaml version 4.01.0
+
+  # #use "topfind";;
+  [...]
+  # #require "higher";;
+  [...]
+  # #use "example-1-perfect-trees.ml";;
+  type 'a perfect = Zero of 'a | Succ of ('a * 'a) perfect
+  [...]
+  # 
+```
+
+[higher]: https://github.com/ocamllabs/higher
+[opam]: http://opam.ocaml.org/

examples/example-1-perfect-trees.ml

@@ -0,0 +1,27 @@
+(* Folds over perfect trees using the Higher library.
+
+   From Section 2.1 of
+
+      Lightweight Higher-Kinded Polymorphism
+      Jeremy Yallop and Leo White
+      Functional and Logic Programming 2014
+*)
+
+open Higher
+
+type 'a perfect = Zero of 'a | Succ of ('a * 'a) perfect
+
+type 'f perfect_folder = {
+  zero: 'a. 'a -> ('a, 'f) app;
+  succ: 'a. ('a * 'a, 'f) app -> ('a, 'f) app;
+}
+
+let rec foldp : 'f 'a. 'f perfect_folder -> 'a perfect -> ('a, 'f) app =
+   fun { zero; succ } -> function
+   | Zero l -> zero l
+   | Succ p -> succ (foldp { zero; succ } p)
+
+module Perfect = Newtype1(struct type 'a t = 'a perfect end)
+
+let idp p = Perfect.(prj (foldp { zero = (fun l -> inj (Zero l));
+                                  succ = (fun b -> inj (Succ (prj b)))} p))

examples/example-2-leibniz.ml

@@ -0,0 +1,58 @@
+(* Leibniz equality using the Higher library.
+
+   From Section 2.2 of
+
+      Lightweight Higher-Kinded Polymorphism
+      Jeremy Yallop and Leo White
+      Functional and Logic Programming 2014
+*)
+
+open Higher
+
+module Leibniz :
+sig
+  module Eq : Newtype2
+
+  type ('a, 'b) eq = ('b, ('a, Eq.t) app) app
+  (** A value of type [(a, b) eq] is a proof that the types [a] and [b] are
+      equal. *)
+
+  val refl : unit -> ('a, 'a) eq
+  (** Equality is reflexive: [refl ()] builds a proof that any type [a] is
+      equal to itself. *)
+
+  val subst : ('a, 'b) eq -> ('a, 'f) app -> ('b, 'f) app
+  (** If types [a] and [b] are equal then they are interchangeable in any
+      context [f]. *)
+
+  val trans : ('a, 'b) eq -> ('b, 'c) eq -> ('a, 'c) eq
+  (** Equality is transitive: if [a] and [b] are equal and [b] and [c] are
+      equal then [a] and [c] are equal. *)
+
+  val symm : ('a, 'b) eq -> ('b, 'a) eq
+  (** Equality is symmetric: if [a] and [b] are equal then [b] and [a] are
+      equal *)
+
+  val cast : ('a, 'b) eq -> 'a -> 'b
+  (** If types [a] and [b] are equal then we can coerce a value of type [a] to
+     a value of type [b]. *)
+end =
+struct
+  module Id = Newtype1(struct type 'a t = 'a end)
+
+  type ('a, 'b) eqaux = { eqaux : 'f. ('a, 'f) app -> ('b, 'f) app }
+  (** The proof of equality of types [a] and [b] is implemented as a coercion
+      from [a] to [b] in an arbitrary context [f]. *)
+
+  module Eq = Newtype2(struct type ('b, 'a) t = ('a, 'b) eqaux end)
+
+  type ('a, 'b) eq = ('b, ('a, Eq.t) app) app
+
+  let refl () = Eq.inj { eqaux = fun x -> x }
+  let subst ab ctxt = (Eq.prj ab).eqaux ctxt
+  let trans ab bc = subst bc ab
+  let cast eq x = Id.prj (subst eq (Id.inj x))
+  let symm (type a) eq =
+    let module S = Newtype1(struct type 'a t = ('a, a) eq end) in
+    S.prj (subst eq (S.inj (refl ())))
+end

examples/example-3-codensity.ml

@@ -0,0 +1,143 @@
+(* The codensity transform using the Higher library.
+
+   From Section 2.3 of
+
+      Lightweight Higher-Kinded Polymorphism
+      Jeremy Yallop and Leo White
+      Functional and Logic Programming 2014
+*)
+
+open Higher
+
+(* class Monad *)
+class virtual ['m] monad = object
+  method virtual return : 'a. 'a -> ('a, 'm) app
+  method virtual bind : 'a 'b. ('a, 'm) app -> ('a -> ('b, 'm) app) -> ('b, 'm) app
+end
+
+(* class Functor *)
+class virtual ['f] functor_ = object
+  method virtual fmap : 'a 'b. ('a -> 'b) -> ('a, 'f) app -> ('b, 'f) app
+end
+
+(* class (Functor f, Monad m) => Freelike f m *)
+class virtual ['f, 'm] freelike (pf : 'f functor_) (mm : 'm monad) = object
+  method pf : 'f functor_ = pf
+  method mm : 'm monad = mm
+  method virtual wrap : 'a. (('a, 'm) app, 'f) app -> ('a, 'm) app
+end
+
+(* newtype C m a = C { forall b. (a -> m b) -> m b } *)
+type ('a, 'm) c = { c : 'b. ('a -> ('b, 'm) app) -> ('b, 'm) app }
+module C = Newtype2(struct type ('a, 'm) t = ('a, 'm) c end)
+
+(* instance Monad (C m) *)
+let monad_c () = object
+  inherit [('m, C.t) app] monad
+  method return a = C.inj {c = fun h -> h a }
+  method bind =
+    let bind = fun { c = p } k -> {c = fun h -> p (fun a -> (k a).c h) } in
+      fun m k -> (C.inj (bind (C.prj m) (fun a -> C.prj (k a))))
+end
+
+(* rep :: Monad m => m a -> C m a *)
+let rep : 'a 'm. 'm #monad -> ('a, 'm) app -> ('a, 'm) c =
+  fun o m -> { c = fun k -> o#bind m k }
+
+(* abs :: Monad m => C m a -> m a *)
+let abs : 'a 'm. 'm #monad -> ('a, 'm) c -> ('a, 'm) app =
+  fun o c -> c.c o#return
+
+(* data Free = Return a | Wrap (f (Free f a)) *)
+type ('a, 'f) free = Return of 'a | Wrap of (('a, 'f) free, 'f) app
+module Free = Newtype2(struct type ('a, 'f) t = ('a, 'f) free end)
+
+(* instance Functor f => Monad (Free f) *)
+let monad_free (functor_free : 'f #functor_) = object
+  inherit [('f, Free.t) app] monad
+  method return v = Free.inj (Return v)
+  method bind = 
+    let rec bind m k = match m with
+      | Return a -> k a
+      | Wrap t -> Wrap (functor_free#fmap (fun m -> bind m k) t) in
+    fun m k -> Free.inj (bind (Free.prj m) (fun a -> Free.prj (k a)))
+end
+
+(* instance Functor f => FreeLike (Free f) *)
+let freelike_free (ff : 'f #functor_) = object
+  inherit ['f,  ('f, Free.t) app] freelike ff (monad_free ff)
+  method wrap =
+    (* We need the fmap to handle the conversion between ('a, 'f)
+       free and the app version in the argument of Wrap *)
+    fun x -> Free.inj (Wrap (ff#fmap Free.prj x))
+end
+
+(* instance FreeLike f m => FreeLike f (C m) *)
+let freelike_c (f_functor : 'f #functor_) (freelike : ('f, 'm) #freelike) =
+object
+  inherit ['f, ('m, C.t) app] freelike f_functor (monad_c ())
+  method wrap t =
+    C.inj { c = fun h ->
+      freelike#wrap (f_functor#fmap (fun p -> (C.prj p).c h) t)}
+end
+
+type ('a, 'f) freelike_poly = {
+  fl: 'm 'd. (('f, 'm) #freelike as 'd) -> ('a, 'm) app
+}
+
+(* improve :: Functor f => (forall m. FreeLike f m => m a) -> Free f a *)
+let improve : 'a 'f. 'f #functor_ -> ('a, 'f) freelike_poly -> ('a, 'f) free =
+  fun d { fl } -> Free.prj (abs (monad_free d)
+                              (C.prj (fl (freelike_c d 
+                                          (freelike_free d)))))
+
+(* data F_IO b = GetChar (Char -> b) | PutChar Char b *)
+type 'b f_io = GetChar of (char -> 'b) | PutChar of char * 'b
+module F_io = Newtype1(struct type 'b t = 'b f_io end)
+
+(* instance Functor F_IO *)
+let functor_f_io = object
+  inherit [F_io.t] functor_
+  method fmap h l = F_io.inj (match F_io.prj l with
+  | GetChar f -> GetChar (fun x -> h (f x))
+  | PutChar (c, x) -> PutChar (c, h x))
+end
+
+(* getChar :: FreeLike F_IO m => m Char *)
+let getChar : 'm. (F_io.t, 'm) #freelike -> (char, 'm) app
+  = fun f -> f#wrap (F_io.inj (GetChar f#mm#return))
+
+(* putChar :: FreeLike F_IO m => Char -> m () *)
+let putChar : 'm. (F_io.t, 'm) #freelike -> char -> (unit, 'm) app
+  = fun f c -> f#wrap (F_io.inj (PutChar (c, (f#mm#return ()))))
+
+(* revEcho :: FreeLike F_IO m => m () *)
+let rec revEcho : 'm. (F_io.t, 'm) #freelike -> (unit, 'm) app
+  = fun f ->
+    let (>>=) c = f#mm#bind c in
+    getChar f >>= fun c ->
+    if (c <> ' ') then
+      (revEcho f >>= fun () ->
+       putChar f c)
+    else f#mm#return ()
+
+(* data Output a = Read (Output a) | Print Char (Output a) | Finish a *)
+type 'a output = Read of 'a output | Print of char * 'a output | Finish of 'a
+
+(* run :: Free F_IO a -> Stream Char -> Output a *)
+let rec run : 'a. ('a, F_io.t) free -> char list -> 'a output =
+  fun f cs -> match f with
+  | Return a -> Finish a
+  | Wrap x ->
+    match F_io.prj x with
+    | GetChar f -> Read (run (f (List.hd cs)) (List.tl cs))
+    | PutChar (c, p) -> Print (c, run p cs)
+
+(* run revEcho stream *)
+let simulate_original stream =
+  run (Free.prj (revEcho (freelike_free functor_f_io)))
+    stream
+
+(* run (improve revEcho) stream *)
+let simulate_improved stream =
+  run (improve functor_f_io { fl = fun d -> revEcho d }) stream

examples/example-4-kind-polymorphism.ml

@@ -0,0 +1,68 @@
+(* Kind polymorphism using the Higher library.
+
+   From Section 2.4 of
+
+      Lightweight Higher-Kinded Polymorphism
+      Jeremy Yallop and Leo White
+      Functional and Logic Programming 2014
+*)
+
+open Higher
+
+let id x = x
+
+class virtual ['f] category = object
+  method virtual ident : 'a. ('a, ('a, 'f) app) app
+  method virtual compose : 'a 'b 'c.
+     ('b, ('a, 'f) app) app -> ('c, ('b, 'f) app) app -> ('c, ('a, 'f) app) app
+end
+
+module Fun = Newtype2(struct type ('a, 'b) t = 'b -> 'a end)
+let category_fun = object
+  inherit [Fun.t] category
+  method ident = Fun.inj id
+  method compose f g = Fun.inj (fun x -> Fun.prj g (Fun.prj f x))
+end
+
+type ('n, 'm) ip = { ip: 'a. ('a, 'm) app -> ('a, 'n) app }
+module Ip = Newtype2(struct type ('n, 'm) t = ('n, 'm) ip end)
+let category_ip = object
+  inherit [Ip.t] category
+  method ident = Ip.inj { ip = id }
+  method compose f g = Ip.inj {ip = fun x -> (Ip.prj g).ip ((Ip.prj f).ip x) }
+end
+
+(* The type of category computations in left-associative form.  All
+   values are of the form
+
+      Compose (Compose(...(Ident, c1), c2), ... cn)
+*)
+type ('b, 'a, 'f) cat_left =
+| Ident : ('a, 'a, 'f) cat_left
+| Compose : ('b, 'a, 'f) cat_left * ('c, ('b, 'f) app) app -> ('c, 'a, 'f) cat_left
+module CL = Newtype3(struct type ('b, 'a, 'f) t = ('b, 'a, 'f) cat_left end)
+
+(* An instance of category that puts computations into normal form. *)
+let category_cat_left (_ : 'f #category) = object (self)
+  inherit [('f, CL.t) app] category
+  method ident = CL.inj Ident
+  method compose : type a b c. (b, (a, ('f, CL.t) app) app) app -> 
+                               (c, (b, ('f, CL.t) app) app) app ->
+                               (c, (a, ('f, CL.t) app) app) app =
+    fun (type a) (type b) (type c) 
+      (f : (b, (a, ('f, CL.t) app) app) app)
+      (j : (c, (b, ('f, CL.t) app) app) app) ->
+     CL.(match (prj j : (c, b, 'f) cat_left) with
+      Ident -> (f : (c, (a, ('f, CL.t) app) app) app)
+    | Compose (g, h) -> inj (Compose (prj (self#compose f (inj g)), h)))
+end
+
+(* Run a left-associative computation. *)
+let rec observe : type f a b. f #category -> (b, a, f) cat_left -> (b, (a, f) app) app =
+  fun cat -> function
+  | Ident -> cat#ident
+  | Compose (f, g) -> cat#compose (observe cat f) g
+
+(* Lift a value into cat_left. *)
+let promote : type f a b. (b, (a, f) app) app -> (b, a, f) cat_left =
+  fun c  -> Compose (Ident, c)

examples/typed-defunctionalization.ml

@@ -0,0 +1,43 @@
+(* An example of typed defunctionalization.
+
+   From Section 1.2 of
+
+      Lightweight Higher-Kinded Polymorphism
+      Jeremy Yallop and Leo White
+      Functional and Logic Programming 2014
+*)
+
+(** A higher-order program: folds over lists, together with functions
+    defined using folds. *)
+module Original =
+struct
+  let rec fold : type a b. (a * b -> b) * b * a list -> b =
+    fun (f, u, l) -> match l with
+     | [] -> u
+     | x :: xs -> f (x, fold (f, u, xs))
+
+  let sum l = fold ((fun (x, y) -> x + y), 0, l)
+  let add (n, l) = fold ((fun (x, l') -> x + n :: l'), [], l)
+end
+
+
+(** The higher-order program in defunctionalized form. *)
+module Defunctionalized =
+struct
+  type (_, _) arrow =
+    Fn_plus : ((int * int), int) arrow
+  | Fn_plus_cons : int -> ((int * int list), int list) arrow
+
+  let apply : type a b. (a, b) arrow * a -> b =
+    fun (appl, v) -> match appl with
+     | Fn_plus -> let (x, y) = v in x + y
+     | Fn_plus_cons n -> let (x, l') = v in x + n :: l'
+
+  let rec fold : type a b. (a * b, b) arrow * b * a list -> b =
+   fun (f, u, l) -> match l with
+    | [] -> u
+    | x :: xs -> apply (f, (x, fold (f, u, xs)))
+
+  let sum l = fold (Fn_plus, 0, l)
+  let add (n, l) = fold (Fn_plus_cons n, [], l)
+end