Sources, sinks, and unbound parameter types

Dario Teixeira
 Daniel_Bünzli
 Christopher L Conway
 Jeremy Yallop
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20080324 (23:06) 
From:  Jeremy Yallop <jeremy.yallop@e...> 
Subject:  Re: [Camllist] Sources, sinks, and unbound parameter types 
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 MLstyle 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": welltyped evaluators, datatypegeneric 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.