Sources, sinks, and unbound parameter types

Sources, sinks, and unbound parameter types

[Dario Teixeira]

Hi,

I'm looking for a way to express the composition of functional components
in a tree-like data structure.  Each node in the tree is either:

  a) a Source, producing values "out of nowhere": unit -> 'a
  b) a Sink, end point of the tree: 'b -> unit
  c) a Processor, transforming values from one type to another: 'c -> 'd


The Ocaml type that represents a node is as follows: (pretty
straightforward, though I wonder if there's a way to explicitly
say that "Source is of 'a -> 'b where 'a must be of type unit")

type ('a, 'b) node_t =
        | Source of (unit -> 'b)
        | Sink of ('a -> unit)
        | Processor of ('a -> 'b)


In addition, there are two types of connectors linking these nodes in the tree:

  a) a Pipe, connecting one node that outputs a value of type 'a into
     another that inputs an 'a.
  b) a Splitter, essentially like a Pipe, but able to feed the same
     value into multiple inputs.


If you'll pardon the ASCII art, here's a diagram of one such simple tree:


|                        ===========
|                        | source1 | 
|                        ===========
|                             |
|                             |
|                             O Pipe
|                             |
|                             |
|                        ============
|                        | process1 |
|                        ============
|                             |
|                             |
|             ----------------O----------------
|             |           Splitter            |
|             |                               |
|        ===========                     ===========
|        |  sink1  |                     |  sink2  |
|        ===========                     ===========


Where each component node can, for example, be defined as follows:

let source1 () = 10
let process1 n = 2.0 *. (float_of_int n)
let sink1 x = Printf.printf "Sink1: %f\n" x
let sink2 x = Printf.printf "Sink2: %f\n" x


To define the tree type, I would like to express something like the code
below.  Note that I am trying to get to the compiler to statically enforce
that outputs and inputs are correctly matched type-wise.

type ('a, 'b) tree_t =
        | Node of ('a, 'b) node_t
        | Pipe of ('a, 'c) tree_t * ('c, 'b) tree_t
        | Splitter of ('a, 'c) tree_t * ('c, 'b) tree_t list


The code above obviously won't work because of the unbound type parameter 'c.
(Also, please ignore for now the fact it allows splitters with an empty
output list -- that can easily be circumvented).

So, my question is if there is any way to express what I want?  I guess there
is a solution involving the creation of a syntax extension, but I'm looking
for a pure Ocaml way.

Thanks in advance for your time!
Best regards,
Dario Teixeira





      ___________________________________________________________ 
Rise to the challenge for Sport Relief with Yahoo! For Good  

http://uk.promotions.yahoo.com/forgood/

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

[Daniel Bünzli]

It seems what you want is existential types, see the example with  
lists of composable functions here [1,2].

Best,

Daniel

[1] http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f55650778d883ae5e9.fr.html
[2] http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/470ee4e9fe63cf36e1bc477980b102e2.fr.html

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

[Christopher L Conway]

This looks a lot like the "Lists of Composable Functions" example
using existentials cited here last week [1].

Your comment about the type of Source and Sink being too general is
interesting. In general, you're asking for GADTs [2], though this
instance is simple enough you could possibly hack up a solution
without them.

Chris

[1] http://groups.google.com/group/fa.caml/msg/8f11bc7839aac98f
[2] http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype

On Mon, Mar 24, 2008 at 5:56 PM, Dario Teixeira <darioteixeira@yahoo.com> wrote:
> Hi,
>
>  I'm looking for a way to express the composition of functional components
>  in a tree-like data structure.  Each node in the tree is either:
>
>   a) a Source, producing values "out of nowhere": unit -> 'a
>   b) a Sink, end point of the tree: 'b -> unit
>   c) a Processor, transforming values from one type to another: 'c -> 'd
>
>
>  The Ocaml type that represents a node is as follows: (pretty
>  straightforward, though I wonder if there's a way to explicitly
>  say that "Source is of 'a -> 'b where 'a must be of type unit")
>
>  type ('a, 'b) node_t =
>         | Source of (unit -> 'b)
>         | Sink of ('a -> unit)
>         | Processor of ('a -> 'b)
>
>
>  In addition, there are two types of connectors linking these nodes in the tree:
>
>   a) a Pipe, connecting one node that outputs a value of type 'a into
>      another that inputs an 'a.
>   b) a Splitter, essentially like a Pipe, but able to feed the same
>      value into multiple inputs.
>
>
>  If you'll pardon the ASCII art, here's a diagram of one such simple tree:
>
>
>  |                        ===========
>  |                        | source1 |
>  |                        ===========
>  |                             |
>  |                             |
>  |                             O Pipe
>  |                             |
>  |                             |
>  |                        ============
>  |                        | process1 |
>  |                        ============
>  |                             |
>  |                             |
>  |             ----------------O----------------
>  |             |           Splitter            |
>  |             |                               |
>  |        ===========                     ===========
>  |        |  sink1  |                     |  sink2  |
>  |        ===========                     ===========
>
>
>  Where each component node can, for example, be defined as follows:
>
>  let source1 () = 10
>  let process1 n = 2.0 *. (float_of_int n)
>  let sink1 x = Printf.printf "Sink1: %f\n" x
>  let sink2 x = Printf.printf "Sink2: %f\n" x
>
>
>  To define the tree type, I would like to express something like the code
>  below.  Note that I am trying to get to the compiler to statically enforce
>  that outputs and inputs are correctly matched type-wise.
>
>  type ('a, 'b) tree_t =
>         | Node of ('a, 'b) node_t
>         | Pipe of ('a, 'c) tree_t * ('c, 'b) tree_t
>         | Splitter of ('a, 'c) tree_t * ('c, 'b) tree_t list
>
>
>  The code above obviously won't work because of the unbound type parameter 'c.
>  (Also, please ignore for now the fact it allows splitters with an empty
>  output list -- that can easily be circumvented).
>
>  So, my question is if there is any way to express what I want?  I guess there
>  is a solution involving the creation of a syntax extension, but I'm looking
>  for a pure Ocaml way.
>
>  Thanks in advance for your time!
>  Best regards,
>  Dario Teixeira
>
>
>
>
>
>
>       ___________________________________________________________
>  Rise to the challenge for Sport Relief with Yahoo! For Good
>
>  http://uk.promotions.yahoo.com/forgood/
>
>  _______________________________________________
>  Caml-list mailing list. Subscription management:
>  http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>  Archives: http://caml.inria.fr
>  Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>  Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

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

[Jeremy Yallop]

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.