Browse thread
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: | 2008-03-24 (23:06) |
From: | Jeremy Yallop <jeremy.yallop@e...> |
Subject: | Re: [Caml-list] 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 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.