Re: [Caml-list] Sources, sinks, and unbound parameter types

[Jeremy Yallop <jeremy.yallop@ed.ac.uk>]

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.