From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2M9OqMK025046 for ; Thu, 22 Mar 2012 10:24:55 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ag4BAE/vak9KfVK0kGdsb2JhbABEtxgIIgEBAQEJCQ0HFAQjgiICExMGARQlAw0FQB8gAQUBATQJGYdoC5gKgl0KjwSFF4k1AQULCIpQhR5jBJVeizODFz2BV4IzgVs X-IronPort-AV: E=Sophos;i="4.73,629,1325458800"; d="scan'208";a="137221117" Received: from mail-we0-f180.google.com ([74.125.82.180]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Mar 2012 10:24:50 +0100 Received: by werf3 with SMTP id f3so2634248wer.39 for ; Thu, 22 Mar 2012 02:24:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:subject:message-id:mime-version:content-type :content-disposition:user-agent; bh=m4kFDtxhtVO/HJiDDXEX7MzonEXnRANID/VQIRZfz6I=; b=sEAvOVAQntFqLNEZSFaeJI2kXW2bJMJA7QAAuINrU+AUzvfGi4tfzJDa3YSMhNHEej VbllZnjjMFxAtXdwP2Or+ciu22hArsS7FkM175z3lnR267ymT3Dt6zB1IALmOFfcCuqP VkalJfAuwXzy9NYEJQEHSZyEubbgdALWu+K5C975dAaaApDc2KiaC2bTvAy8BJ4isNHc BCMjkOWANWxutLEWM2MpSicMhRA71LOroYphAFcNu87qIzpD9SE9ZvRsRtJ6o3E1wevV wNx5758U423wuV5aEKAGzUzZkeQzeS8fO/9bkfP1POEQZO0ppKLwscrllXOSnqh3WLBw oRKg== Received: by 10.216.205.93 with SMTP id i71mr4103899weo.51.1332408290483; Thu, 22 Mar 2012 02:24:50 -0700 (PDT) Received: from voyager (knopper.inria.fr. [128.93.60.80]) by mx.google.com with ESMTPS id gg2sm6542177wib.7.2012.03.22.02.24.49 (version=TLSv1/SSLv3 cipher=OTHER); Thu, 22 Mar 2012 02:24:49 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by voyager with local (Exim 4.72) (envelope-from ) id 1SAeJS-0007kL-S4 for caml-list@yquem.inria.fr; Thu, 22 Mar 2012 10:28:06 +0100 Date: Thu, 22 Mar 2012 10:28:06 +0100 From: Roberto Di Cosmo To: caml-list@yquem.inria.fr Message-ID: <20120322092806.GA29219@voyager> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Subject: GADT examples: composable functions list (Was: Re: [Caml-list] Wanted: GADT examples: string length, counting module x) 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 ------------------------------------------------------------------