From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 7DC9DBBC1 for ; Tue, 25 Mar 2008 00:06:51 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjgKAC7R50dT9QHmYGdsb2JhbACBW48yFwQICBeWXw X-IronPort-AV: E=Sophos;i="4.25,549,1199660400"; d="scan'208";a="24135723" Received: from pop.bulldoghome.com (HELO bdmail1.accesst.com) ([83.245.1.230]) by mail4-smtp-sop.national.inria.fr with ESMTP; 25 Mar 2008 00:06:36 +0100 Received: from host-84-9-233-154.dslgb.com ([84.9.233.154] helo=[192.168.123.191]) by bdmail1.accesst.com with esmtpa (Exim 4.50) id 1Jdvi2-0007uU-1V; Mon, 24 Mar 2008 23:04:06 +0000 Message-ID: <47E8332E.9090602@ed.ac.uk> Date: Mon, 24 Mar 2008 23:03:10 +0000 From: Jeremy Yallop User-Agent: Mozilla-Thunderbird 2.0.0.9 (X11/20080110) MIME-Version: 1.0 To: Dario Teixeira Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Sources, sinks, and unbound parameter types References: <535050.42465.qm@web54603.mail.re2.yahoo.com> In-Reply-To: <535050.42465.qm@web54603.mail.re2.yahoo.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; constructors:01 constructors:01 datatypes:01 datatype:01 datatypes:01 val:01 semantics:01 datatype:01 val:01 node:01 well-typed:01 combinators:01 transforming:01 corresponds:01 combinator:01 One useful way to attack this sort of problem (wiring things together in a way that hides the intermediate types) is to use functions in place of constructors. The problem with constructors in ML-style datatypes is that every type variable that appears in the arguments must also appear as a parameter to the datatype, so the intermediate types "leak out". GADTs lift this restriction, but we can achieve a large part of what GADTs offer by moving from a datatypes and a set of constructors to an abstract type and a set of functions which construct values of the type. That is, instead of encoding "pipe" as a constructor type ('a, 'b) tree_t = ... | Pipe of ('a, 'c) tree_t * ('c, 'b) tree_t ... (which is not allowed, because 'c is not a type parameter) we can encode it as a function: type ('a, 'b) tree_t = val pipe : ('a, 'c) tree_t * ('c, 'b) tree_t -> ('a, 'b) tree_t and similarly for the other constructors. Instead of having a separate interpreter function that walks the tree, inspecting each constructor, we can then encode the semantics of each constructor directly, using these functions. (One way to view this is as a sort of Church encoding of the original datatype; another is as a dualization, using a product (the module containing the abstract type and its operations) in place of a sum). This encoding also avoids the problem you raised at the beginning of your mail, since the type of "source" becomes val source : (unit -> 'b) -> (unit, 'b) node_t This trick has been used to good effect in the ML community to do the sort of things that are often assumed to require GADTs or other "fancy types": well-typed evaluators, datatype-generic programming, etc. Your plumbing primitives seem quite reminiscent of the combinators used in the "arrows" approach to effectful combination. An arrow is a type constructor with two parameters, representing input and output: type ('i, 'o) arr together with primitives for constructing an arrow from a function val arr : ('i -> 'o) -> ('i, 'o) arr composing two arrows val (>>>) : ('i, 'j) arr -> ('j, 'o) arr -> ('i, 'o) arr and transforming an arrow into another arrow that threads additional data val first : ('i, 'o) arr -> (('i*'d), ('o*'d)) arr Your source, sink and processor primitives are all particular instances of "arr"; your "pipe" directly corresponds to the composition operator (>>>), and your splitter can be written using "first", although you may like to consider the arrow combinator val (&&&) : ('i,'o) arr -> ('i,'p) arr -> ('i, ('o*'p)) arr (also expressible using the primitives) which provides a way to pipe the same input into two arrows and collect both the outputs. Here's an example implementation: module type ARROW = sig type ('i,'o) arr val arr : ('i -> 'o) -> ('i, 'o) arr val (>>>) : ('i, 'j) arr -> ('j, 'o) arr -> ('i, 'o) arr val first : ('i, 'o) arr -> (('i*'d), ('o*'d)) arr val run : ('i,'o) arr -> ('i -> 'o) end module Arrow : ARROW = struct type ('i,'o) arr = 'i -> 'o let arr f = f let (>>>) f g x = g (f x) let first f (x,y) = (f x, y) let run f = f end module Composable : sig type ('a,'b) tree = ('a,'b) Arrow.arr val source : (unit -> 'b) -> (unit, 'b) tree val sink : ('a -> unit) -> ('a, unit) tree val processor : ('a -> 'b) -> ('a, 'b) tree val pipe : ('a, 'c) tree -> ('c, 'b) tree -> ('a, 'b) tree val split : ('a, 'b) tree -> ('a, 'c) tree -> ('a, ('b*'c)) tree end = struct open Arrow type ('a,'b) tree = ('a,'b) arr let source = arr let sink = arr let processor = arr let pipe = (>>>) let split f g = let dup x = (x,x) and swap (x,y) = (y,x) in arr dup >>> first f >>> arr swap >>> first g >>> arr swap end (Actually, "arr" is supposed to be for pure functions only; it'd be better to have a separate operation for introducing effectful operations into the arrow.) The computation given in your diagram might then be expressed as follows: pipe (pipe (source source1) (processor process1)) (split (sink sink1) (sink sink2)) or, using the arrow combinator syntax: source source1 >>> processor process1 >>> (sink sink1 &&& sink sink2) Jeremy.