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: | -- (:) |
| 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.