[Haskell] Implicit parameters redux

[Ben Rudiak-Gould]

This article attempts to describe in more detail the implicit-parameter-
based sequencing model that I was trying to develop in a recent thread. I
am getting more and more excited about this idea, and after reading this I
hope you'll understand why. Any comments are greatly appreciated.
(Especially if there's a fatal flaw -- you'd better tell me now and get it
over with.)


Review of implicit return values
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

In the syntax I proposed a few days ago, implicit values are attached to
ordinary values like this:

  (123, %x = "foo", %y = 99)

(I now write %x instead of ^x for a reason described in the next section.)

The syntax resembles a tuple, and they are in fact tuples behind the
scenes (unlifted, and probably unboxed). But the semantics is not quite
the same: the example above is equivalent to the same example with %x and
%y reversed, and also to

  ((123, %y = 99), %x = "foo")

These implicit return values propagate upward through expressions in the
same way that implicit parameters propagate downward. They can be "caught"
at the root of an expression by matching against a similar syntax:

  case expr of
    (a, %x = b) -> ...

Implicit return values are merged by name as they propagate upward, using
mappend. It is a compile-time error if two values to be merged have
different types, or a single type that is not an instance of Monoid.

Another extension I proposed is that the "name" of an implicit return
value can include type parameters: thus %foo Int and %foo Char would be
treated as though they had different names.


Threading and branching implicit values
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Implicit values fall into two categories which I'll call "threading" and
"branching".

Linear implicit parameters (%name) are branching if they have a type which
is an instance of the class Splittable, and threading otherwise.

Ordinary implicit parameters (?name) are always branching: they behave as
though their types were trivial instances of Splittable, where split x =
(x,x).

Implicit return values are like linear implicit parameters: they're
branching or threading depending on whether their types are or are not
instances of Monoid. There is no trivial instance of Monoid for arbitrary
types, so implicit return values have no variant analogous to ?name. For
this reason I will write them %name (abandoning the ^name convention I
used before).

The intuition behind the terminology is this: if you've programmed in both
procedural and functional languages (and who here hasn't?) you know that
procedural code tends to have a sequential structure, and functional code
tends to be hierarchical. Threading parameters mirror procedural
code: because they cannot be split or merged, they are passed along in
sequential fashion from a single point of production to a single point of
consumption. Branching parameters mirror functional code: they either
percolate down the expression tree, splitting as they go, or they
percolate up, merging as they go.


Branching implicit parameters render the Reader monad obsolete
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

It has been noticed already that ordinary implicit parameters provide
essentially the same functionality as the Reader monad, but in a more
convenient and versatile way. The main advantages are:

  * Different pieces of state are distinguished by descriptive names,
    instead of by depth in the monad stack.

  * Code need not be rewritten in monadic style.

These are big advantages. There's no point using Reader if you have
implicit parameters.


Branching implicit return values render the Writer monad obsolete
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

It's not hard to see that implicit return values provide a replacement for
Writer with the same advantages.


Threading implicit values render IO, ST, and State obsolete
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

I'll be arguing for the rest of this article that threading implicit
values can replace all state-threading monads, and provide advantages
similar to those above. In the case of IO and ST the advantage is even
greater. IO and (forall s . ST s) form a mutually exclusive infinite
family of monads: any piece of code can operate on at most one at a
time. My proposal has (or seems to have) no similar restriction. This
opens the door to fine-grained fragmentation of mutable state, something
people have wanted since the earliest days of monads in Haskell.


Input and output threads
~~~~~~~~~~~~~~~~~~~~~~~~

Along with its other arguments and return value, any function takes zero
or more threading implicit arguments and returns zero or more threading
implicit return values. I'll call the former "input threads" and the
latter "output threads".

These threads represent bits of mutable state. For example, corresponding
to the IO monad there is an implicit value %io :: RealWorld, and any
function which interacts with the world will have an input and output
thread of this name and type.


Example: polymorphic cells
~~~~~~~~~~~~~~~~~~~~~~~~~~

Using this system we can implement a form of polymorphic "mutable cell" in
Haskell. We want an interface something like this:

  beginRef :: a -> (exists s . (Ref s, %refState s a :: State a))

  readRef  :: (%refState s a :: State a) =>
                Ref s -> (a, %refState s a :: State a)

  writeRef :: (%refState s a :: State a) =>
                Ref s -> b -> ((), %refState s b :: State b)

  endRef   :: (%refState s a :: State a) => Ref s -> a

The purpose of the "exists s" in the first type is to express the idea
that different cells get different state types s, and hence that the
threaded states for different cells remain separate for merge-by-name
purposes. It's not clear what Haskell's current type inference algorithm
would make of this, however. (Question: is there a deep reason that
anonymous existentials like this are not allowed in Haskell?)

Other than that, the most interesting type is that of writeRef, which is
more polymorphic than might be expected. This is a kind of flexibility not
offered by monads: the input and output threads of a function need not
match. These cells can be safely "overwritten" with a value of a totally
new type.

This interface is easily implemented in Haskell (for a sufficiently
flexible definition of "Haskell"):

  newtype State a = State a
  newtype Ref s   = Ref

  beginRef val =
    (Ref, %refState s a = State val)

  readRef { %refState s a = State val } Ref =
    (val, %refState s a = State val)

  writeRef { %refState s a = State _ } Ref val =
    ((), %refState s b = State val)

  endRef { %refState s a = State val } Ref =
    val

Notice that the Ref doesn't actually hold any information: it's just there
to pull in the appropriate state. This is only useful if we don't have to
pass that state in explicitly, which is what the next section is about.

The above implementation (if it indeed typechecks) is a proof that this
style of ref is type-safe. Once we know that, we can implement it using
low-level mutability instead. In this implementation the State parameter
holds no information, and exists only to enforce sequencing. The value is
actually held in the Ref, and it's updated by a genuine mutation.

Refs of this kind are not sufficient, however: we must have an analogue of
STRefs also. The reason is that it can't always be determined at
typechecking time which cell is used by a particular piece of code. Any
cells which can't be distinguished by the typechecker must be placed in a
common state space, a la STRef. It's not clear that it needs to be
possible to place cells of different value types ("a" above) in the same
space, though, since they can always be distinguished by that type. If
it's not necessary, then this style of "parallel ref" can also be
implemented in Haskell (in terms of the above ref type, in fact), which
solves a long-standing theoretical difficulty with the ST monad.

Oleg's polymorphic heap also fits into this model. It doesn't seem to be
needed here, but it might be helpful in thinking about the Tieable class
described below.

Haskell's pure functional style and its monadic style can be thought of as
special cases of this threading model. The pure functional style is the
case of no input or output threads, and the monadic style is the case of
all threads passing through all expressions in sequence, with the same
names and types throughout.


Hiding the plumbing
~~~~~~~~~~~~~~~~~~~

I introduce an operator =<>=, called "tie", which causes the output
threads of its left argument to be passed as input threads to its right
argument. Matching of threads is done by name. Any threads left untied
become input or output threads of the full expression.

This operator presents a serious problem for the design of the system
since it cannot be implemented in Haskell, and cannot even be given a
type. Worse, generic functions which use it are also untypable. I think
this problem can't be avoided -- it's inseparable from the benefits of
this system. I'll come back to this later and describe a possible
solution. For now I'll assume that there's a solution and we have =<>=.

I'll assume =<>= returns the (explicit) values of its arguments as a pair
(though this may be needlessly inefficient). We should be able to get the
>>= behavior of passing the value of the first expression on to the next
by writing "let (a,b) = (expr1 =<>= expr2 a) in b".

I next introduce some sugar called "thread" which takes a list of
expressions and glues them together using =<>=. The "var <- expr" syntax
is also available to bind the explicit value of any expression except the
last. I can see no reason why this can't be recursive -- i.e. all bound
variables are in scope throughout the thread expression -- but I could be
missing something.

"thread" takes a sequence of expressions, but in contrast to "do" -- where
expressions really do form a linear sequence -- the expressions passed to
"thread" have dependencies forming an arbitrary dag, and any topo-sorted
order within the thread expression is equivalent. The sorting is necessary
only because of the linear nature of source code.

In fact, if there are no dependencies at all, we needn't thread the
expressions at all. If the cells r and s live in separate state spaces, we
can simply write

  readRef r + readRef s

instead of something analogous to "liftM2 (+) (readRef r) (readRef s)",
since the type system knows that the refs are independent and needn't be
ordered relative to each other. This is the key to safe declarative
concurrency, which I'll return to later.


Breaking up the IO cartel
~~~~~~~~~~~~~~~~~~~~~~~~~

Since we're no longer limited to one thread at a time, there's no reason
that IO need consist of a single thread. We could have separate threads
for stdin, stdout, and stderr, for example, and code which only outputs
could safely run in parallel with code which only inputs.

However, it's difficult to see what divisions can be made safely, since
pretty much anything goes in the RealWorld. Sometimes stdin and stdout are
independent, but sometimes they're not. The solution is to leave this up
to the programmer.

We provide (among other things) a function (unsafe)detachHandle, which
takes a handle and the world, and returns two worlds, one containing only
that handle and one containing everything else. The proof obligation is
simply that the two worlds don't interact outside the Haskell
program. (The implementation guarantees that they don't interact inside.)

The first of these worlds should be parameterized by a state variable. A
new handle, also so parameterized, will have to be returned as well. I
don't think there's a way to statically prevent reuse of the old handle --
this must be checked at runtime. This check corresponds to the current
"half-closed" state of handles.

There should also be a sledgehammer function unsafeForkWorld, for cases
when the more precise functions aren't versatile enough. This is analogous
to unsafeInterleaveIO. I think that everyone's favorite sledgehammer,
unsafePerformIO, will also still be useful.


Declarative concurrency
~~~~~~~~~~~~~~~~~~~~~~~

This system is a natural fit with concurrency. To spawn concurrent
threads, a program divides up the IO world as it sees fit, then gives each
thread its own independent piece. Provided the proof obligation is met,
these threads cannot interfere with each other. MVar state must be shared,
of course, but needn't be tied to IO: MVars should exist in state-thread
families like STRefs.


The need for boxing
~~~~~~~~~~~~~~~~~~~

Aside from untypability, the present system has another serious flaw: a
function like

  performTwice foo = thread { foo; foo }

will in fact perform foo's side effects only once! The reason is that
implicit values are not passed into functions along with arguments. Foo
will do its thing at the call point, and inside performTwice it will just
be an unthreaded value.

The core reason for this is that we don't explicitly specify when thread
parameters get applied to actual values. The monad system does not suffer
from this problem because you must explicitly place values in the monad
(with return) and explicitly extract them (with runX). We can solve the
analogous problem for threads by boxing the return value and its
associated threads into a single abstract entity, and making =<>= operate
on that.

Once we have a box, we can make that box an instance of a type class,
which suggests a solution to the problem of typing =<>=. We introduce a
class which for lack of a better idea I'll call "Tieable":

  class Tieable a b c | a b -> c where
    (=<>=) :: a x -> b y -> c (x,y)

Instances of Tieable must be automatically derived by the compiler. It's
not clear to me how the actual boxing and unboxing should take place, or
how the boxes should be named in the type language.


The ties that bind
~~~~~~~~~~~~~~~~~~

Can we derive an implementation of monadic bind from an implementation of
tie? In general no, but in certain cases yes.

The cases are those in which the types a and b in the definition of
Tieable are the same. That is, we have something like

  instance (Tieable a a a) => Monad a where
    m >> n    = snd (m =<>= n)
    m >>= f   = let (a,b) = (m =<>= f a) in b
    return    = box

This is fortunate, since it means that IO and ST can continue to exist for
compatibility, and that flow-control transformers like ContT can be
applied to threaded values.


Arrows?
~~~~~~~

Question: how does the class Tieable compare to the class Arrow?


-- Ben