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

[Roberto Di Cosmo <roberto@dicosmo.org>]

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
------------------------------------------------------------------