GADT examples: composable functions list (Was: Re: [Caml-list] Wanted: GADT examples: string length, counting module x)

GADT examples: composable functions list (Was: Re: [Caml-list] Wanted: GADT examples: string length, counting module x)

[Roberto Di Cosmo]

GADT come in really handy is when you have data structures that need existential
type variables.

A nice example is the case of lists of composable functions: say you want to
build a list containing functions f_i : A_i -> A_{i+1}

Without GADT
------------

 One can get away cheating the type system and declaring the type

  type ('a,'b) cfl = ('a -> 'b) list;;

 which is really incorrect: 'a is the first input type, 'b is the last output
 type, and that's ok, but it is really not true that the list will contain
 functions of type 'a -> 'b ... 

 This shows up as soon as one tries to do something useful with this list, like
 adding one element at the bebinning: to keep the type checker happy, we call
 Obj.magic in for help

  let add (f: 'a -> 'b)  (fl : ('b,'c) cfl) : ('a,'c) cfl = 
   (Obj.magic f):: (Obj.magic fl);;

 And you will need Obj.magic's help in writing map, fold, compute, whatever...

 You may argue that if all the hectic primitives are well hidden behind a module
 signature, and the module programmer is very smart, all will be well, but
 that's ugly, isn't it?
 

Here is the elegant way of doing it using GADT
----------------------------------------------

 Declare the type cfl of a composable function list as follows

  type ('a,'b) cfl = 
   Nilf: ('a,'a) cfl
  |Consf: ('a -> 'b) * ('b,'c) cfl -> ('a,'c) cfl;;

 Now you can write useful functions which are well typed

  let rec compute : type a b. a -> (a,b) cfl -> b = fun x -> 
  function
  | Nilf -> x (* here 'a = 'b *)
  | Consf (f,rl) -> compute (f x) rl;;

 Try it... it works!

  let cl = Consf ((fun x -> Printf.sprintf "%d" x), Nilf);;
  let cl' = Consf ((fun x -> truncate x), cl);;
  compute 3.5 cl';;

 Notice that the type of Consf contains a variable 'b which is 
 not used in the result type: one can check that 

   ('a -> 'b) * ('b,'c) cfl -> ('a,'c) cfl

 can be seen as 

   \forall 'a 'c. (\exists 'b.('a -> 'b) * ('b,'c) cfl) -> ('a,'c) cfl

 so, when deconstructing a cfl, one gets of course a function and the
 rest of the list, but now we know that their type is

       \exists 'b.('a -> 'b) * ('b,'c) cfl

Well, isn't this a contrived example?
-------------------------------------

Actually, not at all... back in 1999, when developing a parallel
programming library named ocamlp3l, we implemented high-level
parallelism combinators that allowed to write expressions like this
(hey, isn't this map/reduce? well, yes... indeed that was an ooold idea)

    (seq(intervals 10) ||| mapvector(seq(seq_integr f),5) ||| reducevector(seq(sum),2))

These combinators could be interpreted sequentially or graphically quite
easily, but turning them into a distributed program required a lot of
work, and the first step was to build an AST from these expressions:
here is a snippet of the actual type declaration from the old code in parp3l.ml

 (* the type of the p3l cap *)

 type ('a,'b) p3ltree = Farm of (('a,'b) p3ltree * int)
                | Pipe of ('a,'b) p3ltree list
                | Map of (('a,'b) p3ltree * int)
                | Reduce of (('a,'b) p3ltree * int)
                | Seq of ('a -> 'b)
                ;;

And here is one of the simplification steps we had to perform on the AST

 let (|||) (t1 : ('a,'b) p3ltree) (t2 : ('b,'c) p3ltree) =
   match ((Obj.magic t1 : ('a,'c) p3ltree), (Obj.magic t2 : ('a,'c) p3ltree)) with
     (Pipe l1, Pipe l2) -> Pipe(l1 @ l2)
   | (s1, Pipe l2) -> Pipe(s1 :: l2)
   | (Pipe l1, s2) -> Pipe(l1 @ [s2])
   | (s1, s2) -> Pipe [s1; s2];;

I am sure you see the analogy with the composable function list: a series
of functions in a paralle pipeline have exactly the same type structure.

With GADTs, onw can can finally write this 1999 code in a clean way in OCaml,
so many thanks to the OCaml team, and keep up the good work!

--Roberto
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 6C08 (6th floor)
175, rue du Chevaleret, XIII
Metro Chevaleret, ligne 6
------------------------------------------------------------------                                                 

Re: GADT examples: composable functions list (Was: Re: [Caml-list] Wanted: GADT examples: string length, counting module x)

[Daniel Bünzli]

Le jeudi, 22 mars 2012 à 10:28, Roberto Di Cosmo a écrit :

> Without GADT
> ------------
>  
> One can get away cheating the type system and declaring the type
You don't need to cheat the type system with Obj without GADT.

http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f55650778d883ae5e9.en.html

Not to say that it's not involved, but it's possible.  

Best,

Daniel

Re: GADT examples: composable functions list (Was: Re: [Caml-list] Wanted: GADT examples: string length, counting module x)

[Roberto Di Cosmo]

Hi Daniel,
  sure, never said you need, just that you can get away cheating
the type system.

But I need to show my students elegant and simple solutions:
I want to get more OCaml users around, not scare them off :-)

--Roberto




On Thu, Mar 22, 2012 at 10:46:33AM +0100, Daniel Bünzli wrote:
> 
> 
> Le jeudi, 22 mars 2012 à 10:28, Roberto Di Cosmo a écrit :
> 
> > Without GADT
> > ------------
> >  
> > One can get away cheating the type system and declaring the type
> You don't need to cheat the type system with Obj without GADT.
> 
> http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f55650778d883ae5e9.en.html
> 
> Not to say that it's not involved, but it's possible.  
> 
> Best,
> 
> Daniel
> 
> 
> 

-- 
--Roberto Di Cosmo
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 6C08 (6th floor)
175, rue du Chevaleret, XIII
Metro Chevaleret, ligne 6
------------------------------------------------------------------                                                 

Re: GADT examples: composable functions list (Was: Re: [Caml-list] Wanted: GADT examples: string length, counting module x)

[Markus Mottl]

On Thu, Mar 22, 2012 at 05:46, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> You don't need to cheat the type system with Obj without GADT.
>
> http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f55650778d883ae5e9.en.html
>
> Not to say that it's not involved, but it's possible.

Indeed, this encoding is not the easiest to reason about.  The pipe
operator mentioned earlier is essentially arrow composition.  I once
played around with this encoding and arrows and though it's kind of
fun, I'm not sure I'd want to write significant amounts of code that
way.

The code is below if anybody is curious.  The "SimpleDataContArrow"
demonstrates how it can be done.  It also uses continuation passing
style for "chasing arrows" (i.e. running computations) to prevent
stack overflows.

--------- arrow.ml
let id x = x

(* Simple arrows with application *)

module type SIMPLE_ARROW = sig
  type ('a, 'b) t  (* Type of arrows *)

  val arr : ('a -> 'b) -> ('a, 'b) t
  (* [arr f] projects an OCaml-function to a morphism (arrow) in the category
     of computations. *)

  val (>>>) : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
  (* [af >>> ag] composes the two computations [af] and [ag]. *)

  val app : unit -> (('a, 'b) t * 'a, 'b) t
  (* [app ()] @return an arrow that represents a computation which takes
     another arrow and a value as argument and returns the result of applying
     the latter to the former. *)

  val run : ('a, 'b) t -> 'a -> 'b
  (* [run af x] runs the computation represented by arrow [af] on input [x]. *)
end

(* Implementation of simple arrows using plain functions *)
module SimpleArrow : SIMPLE_ARROW = struct
  type ('a, 'b) t = 'a -> 'b

  let arr f = f
  let (>>>) f g x = g (f x)
  let app () (f, x) = f x
  let run = arr
end

(* Implementation of simple arrows using continuations.
   Does not blow stack with deeply nested arrows! *)
module SimpleContArrow : SIMPLE_ARROW = struct
  type ('a, 'b) t = { f : 'z. 'a -> ('b -> 'z) -> 'z }

  let arr f = { f = fun x cont -> cont (f x) }
  let (>>>) af ag = { f = fun x cont -> af.f x (fun yf -> ag.f yf cont) }
  let app () = { f = fun (af, x) -> af.f x }
  let run af x = af.f x id
end

(* Helper signature required for recursive module below *)
module type DATA_ARROW = sig
  include SIMPLE_ARROW

  val run_cont : ('a, 'b) t -> 'a -> cont : ('b -> 'c) -> 'c
end

(* Implementation of simple arrows using continuations and representing
   them as variants *)
module rec SimpleDataContArrow : DATA_ARROW = struct
  type ('a, 'b) t =
    | Arr of ('a -> 'b)
    | Comp of ('a, 'b) comp
    | App of ('a, 'b) app

  and ('a, 'b) comp =
    {
      comp_open : 'z. ('a, 'b, 'z) comp_scope -> 'z
    }
  and ('a, 'b, 'z) comp_scope =
    {
      comp_bind : 'c. ('a, 'c) t -> ('c, 'b) t -> 'z
    }

  and ('a, 'b) app =
    {
      app_open : 'z. ('a, 'b, 'z) app_scope -> 'z
    }
  and ('a, 'b, 'z) app_scope =
    {
      app_bind :
        'c. ('a -> ('c, 'b) t * 'c) -> (('c, 'b) t * 'c, 'b) t -> 'z
    }

  let arr f = Arr f

  let (>>>) af ag = Comp { comp_open = fun scope -> scope.comp_bind af ag }

  let rec run_cont a x ~cont =
    match a with
    | Arr f -> cont (f x)
    | Comp comp ->
        comp.comp_open
          {
            comp_bind = fun af ag ->
              SimpleDataContArrow.run_cont af x
                ~cont:(SimpleDataContArrow.run_cont ag ~cont)
          }
    | App app ->
        app.app_open
          {
            app_bind = fun unpack af ->
              SimpleDataContArrow.run_cont af (unpack x) ~cont
          }

  let app () =
    App
      {
        app_open = fun scope ->
          let f (af, x) = SimpleDataContArrow.run_cont af x ~cont:id in
          scope.app_bind id (Arr f)
      }

  let run a x = run_cont a x ~cont:id
end

(* Fully-featured arrows with many more operators *)
module type ARROW = sig
  include SIMPLE_ARROW

  val first : ('a, 'b) t -> ('a * 'c, 'b * 'c) t
  (* [first af] takes a computation [af] accepting argument [a].
     @return a computation, which takes a pair [(a, c)], and returns the pair
     [(b, c)], where [b] is the result of running computation [ag] on [a],
     and [c] is a passed-through variable. *)

  val second : ('a, 'b) t -> ('c * 'a, 'c * 'b) t
  (* [second af] is a dual of [first], and passes the constant variable
     as first argument. *)

  val ( *** ) : ('a, 'b) t -> ('c, 'd) t -> ('a * 'c, 'b * 'd) t
  (* [af *** ag] @return computation that performs computation [af] and
     [ag] on the first and respectively second argument of the input pair,
     returning the two results as a pair. *)

  val (&&&) : ('a, 'b) t -> ('a, 'c) t -> ('a, 'b * 'c) t
  (* [af &&& ag] @return computation that passes its input to two
     computations [af] and [ag] and returns the pair of the results. *)

  val liftA2 : ('a -> 'b -> 'c) -> ('d, 'a) t -> ('d, 'b) t -> ('d, 'c) t
  (* [liftA2 f af ag] @return computation that applies the function [f]
     to the results of [af] and [ag], which both receive the input. *)

  type ('a, 'b) either = Left of 'a | Right of 'b

  val left : ('a, 'b) t -> (('a, 'c) either, ('b, 'c) either) t
  (* [left af] @return computation that applies computation [af] to
     [l] if the input is [Left l], returning [Left result] and otherwise
     passes [Right r] through unchanged. *)

  val right : ('a, 'b) t -> (('c, 'a) either, ('c, 'b) either) t
  (* [right af] is the dual of [left]. *)

  val (<+>) : ('a, 'c) t -> ('b, 'd) t -> (('a, 'b) either, ('c, 'd) either) t
  (* [af <+> ag] @return a computation that either performs [af] or
     [ag] depending on its input, returning either [Left res_af] or
     [Right res_ag] respectively. *)

  val (|||) : ('a, 'c) t -> ('b, 'c) t -> (('a, 'b) either, 'c) t
  (* [af ||| ag] @return a computation that either performs [af] or [ag]
     depending on input. *)

  val test : ('a, bool) t -> ('a, ('a, 'a) either) t
  (* [test acond] @return a computation that tests its input with [acond]
     and returns either [Left res] if the predicate is true or [Right res]
     otherwise. *)
end

(* Functor from simple arrows with "apply" to fully-featured arrows *)
module MkArrow (SA : SIMPLE_ARROW)
  : ARROW with type ('a, 'b) t = ('a, 'b) SA.t =
struct
  include SA

  let swap (x, y) = y, x
  let first af = arr (fun (a, c) -> af >>> arr (fun b -> b, c), a) >>> app ()
  let second af = arr swap >>> first af >>> arr swap
  let ( *** ) af ag = first af >>> second ag
  let ( &&& ) af ag = arr (fun x -> x, x) >>> af *** ag
  let liftA2 f af ag = af &&& ag >>> arr (fun (b, c) -> f b c)

  type ('a, 'b) either = Left of 'a | Right of 'b

  let left af =
    arr (function
      | Left l -> arr (fun () -> l) >>> af >>> arr (fun x -> Left x), ()
      | Right _ as right -> arr (fun () -> right), ())
    >>> app ()

  let mirror = function Left x -> Right x | Right x -> Left x
  let right af = arr mirror >>> left af >>> arr mirror
  let (<+>) af ag = left af >>> right ag
  let (|||) af ag = af <+> ag >>> arr (function Left x | Right x -> x)

  let test acond =
    acond &&& arr id >>> arr (fun (b, x) -> if b then Left x else Right x)
end

(* Instantiations of fully-featured arrows *)
module Arrow = MkArrow (SimpleArrow)
module ContArrow = MkArrow (SimpleContArrow)
module DataContArrow = MkArrow (SimpleDataContArrow)


(* Some silly fun with Kleisli categories *)

(* Monad specification *)
module type MONAD = sig
  type 'a t

  val return : 'a -> 'a t
  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t

  val run : 'a t -> 'a
end

(* Functor from arrow with apply operator to monad *)
module MkArrowMonad (SA : SIMPLE_ARROW)
  : MONAD with type 'a t = (unit, 'a) SA.t =
struct
  open SA

  type 'a t = (unit, 'a) SA.t

  let return x = arr (fun () -> x)
  let (>>=) af g = af >>> arr (fun x -> g x, ()) >>> app ()
  let run af = SA.run af ()
end

(* Functor from monads to their Kleisli category *)
module MkKleisli (M : MONAD) : ARROW with type ('a, 'b) t = 'a -> 'b M.t =
  MkArrow (struct
    open M

    type ('a, 'b) t = 'a -> 'b M.t

    let arr f x = return (f x)
    let (>>>) f g x = f x >>= g
    let app () (f, x) = f x
    let run f x = M.run (f x)
  end)

(* Example instantiation of a monad made from DataContArrows *)
module MonadFromArrow = MkArrowMonad (DataContArrow)

(* And now going back from monads to arrows *)
module ArrowFromMonad = MkKleisli (MonadFromArrow)


(* Some test code *)

open DataContArrow

let bump = arr succ

let bump_n_times n =
  let rec loop n arrow =
    if n <= 0 then arrow
    else loop (n - 1) (arrow >>> bump)
  in
  loop n (arr id)

let () =
  let n = 424242 in
  let arrow = bump_n_times n in
  let result = run arrow 0 in
  Printf.printf "%d\n" result
---------

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com