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