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 q2MEVdXs009987 for ; Thu, 22 Mar 2012 15:31:39 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlkBAA03a09KfVK0kGdsb2JhbABEtzIIIgEBAQEJCQ0HFAQjggkBAQEEEgITGQEUBx0BAwwGBQsNIwshAQERAQUBHAYTCBqHaAuaegqMFoJxhSM/iHYBBQuJYoZ3BJVfiy+DGj2EJQ X-IronPort-AV: E=Sophos;i="4.73,630,1325458800"; d="scan'208";a="137274482" 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 15:31:34 +0100 Received: by werf3 with SMTP id f3so3021936wer.39 for ; Thu, 22 Mar 2012 07:31:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=jjXPuF4q6HEVFXNcVU9GbZt4z8/SNlyxxc1KtlGKwZw=; b=kbMSVccSp+gsKU3ECmBuNbESpqLrvHOr60it7wuinMPDoAolG3eX8+lb0XQG7o90hf riqxJgt4cBFjdFptGBLNG3/rGAv8LucvYBCx8iyz7xtsizlHBgH9UNpVMYocnDArrdEj YTGe6oprkrexmtHllugvN6c/9u92OEQmwAmrQSWun8MyFtlePxRyagBeS8Mv6qZ/LcSd wEY22oU5TlaPNe6Q0ky9yFl5U1O8MlVWTgvKoKnj9LgZyGP7iIXU9V/BpwABD73xA9py xRirWemPsHFIFBKTzrd8RkoncijwQ78shya5ylJD42J30ZxbOnPYa5RoAIaOaVYwdSlT F2qg== MIME-Version: 1.0 Received: by 10.180.102.101 with SMTP id fn5mr98298wib.6.1332426693891; Thu, 22 Mar 2012 07:31:33 -0700 (PDT) Received: by 10.180.78.102 with HTTP; Thu, 22 Mar 2012 07:31:33 -0700 (PDT) In-Reply-To: <062C697B60F0423CBF94220A63C44633@erratique.ch> References: <20120322092806.GA29219@voyager> <062C697B60F0423CBF94220A63C44633@erratique.ch> Date: Thu, 22 Mar 2012 10:31:33 -0400 Message-ID: From: Markus Mottl To: =?ISO-8859-1?Q?Daniel_B=FCnzli?= Cc: Roberto Di Cosmo , caml-list@yquem.inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q2MEVdXs009987 Subject: Re: GADT examples: composable functions list (Was: Re: [Caml-list] Wanted: GADT examples: string length, counting module x) On Thu, Mar 22, 2012 at 05:46, Daniel Bünzli 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