English version
Accueil     Ŕ propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis ŕ jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml ŕ l'adresse ocaml.org.

Browse thread
Sources, sinks, and unbound parameter types
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ 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 =
     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)

   module Arrow : ARROW =
     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

   module Composable :
     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 =
     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

(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

   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)