Causality

Denotational semantics of processes is often though of as functions from input stream to output stream.
I already argued that streams are not general enough to represent communication between processes, but let's keep the model simple.

Function from stream to stream fails to represent one crucial property of the process - which input message must have been fed to the process in order to observe a specific output message. I do not mean data dependency here, but something like control dependency, or causality. Streams (or full orders) are a special case of partial orders that can be used to model causality, so there seems everything is ok - except there is no ordering between elements of input stream and output stream.
Imagine a function from stream of unit to stream of unit:

data Stream a = Message a (Stream a)
type X = (Stream ()) -> (Stream ())

There is just one function of type X - identity (non-termination is out of equation as we are talking math functions, not Haskell functions).
On the other hand, there are multiple different behaviors that accept empty messages and output empty messages.
One would be an identity behavior - for each input message send one output message. Another would be a counter - for nth input message send n output messages. By applying a function from Nat to Nat to the definition of the counter, one obtains a new behavior: for nth input message send f(n) output messages. Thus there are infinitely many observably different behaviors of this type, and trying to denote them by a single function is unsatisfactory at least.

So, the quick solution seems to define a process as a function from input list (a prefix of stream) to a list of outputs produced after receiving the last input (so the whole output list is obtained by concatenating output lists for all prefixes of the input). This may work for a single input stream, but for multiple streams we need to encode which stream received the last message.

A more general way to look onto this is to say that a process extends a partially ordered set of input messages to a partially ordered set of both input and output messages, with a constraint that it does not introduce PO links to an input message (but obviously is allowed to introduce such links from an input to an output, or between two outputs).
Need to think of a formal (and elegant) way for saying this.

Agents as frontiers of futures (or arachnoagents)

Imagine truly concurrent constraint programming, but without entailment, or any other appeal to logic. In fact, let's try to separate causality from mechanism of specification of interaction.

It may be easier to approach this task from FSM angle, or more precisely, ISM - interacting state machines.
Unlike ISM, our machines (cobs?) do not communicate via FIFO streams of messages - to model causality fairfully, a more rich structure is needed (a cobweb).
Each machine can be thought as crowling along links of immutable network of message nodes, producing another network as its output (to be traversed by other machines). Traversion is not destructive - network nodes not referenced by any machine operatonally are GCed, while denotationally they have infinite lifetime.
FIFO streams are a special case of network with strictly linear links.
To support growth, immutable networks have future nodes (promises) at their frontier - and exactly these nodes are referred (and fulfilled) by the owner machine (hind legs of the cob). Readers of the network cannot get past these growth points (with their front legs) until creator resolves them - a typical future/promise, but probably with more low-level operations than usual.
A machine is a unit of authority, while execution as such can have finer grained units.

Marshalling as a game

Investigate the problem of what to put on wire when marshalling (serializing) objects.
Some runtime environments force this decision, at least when it comes to data/code dichotomy.
When it comes to code-is-data view, it becomes very unclear, what should be transferred - think of the reflexive tower - should it be unraveled to its (infinite) roots, or at least down to the fixpoint? What if the receiver of the stream already shares some part of the tower with the sender?
In general, how can they engage in a negotiation that minimizes not only the size of the stream, but also the size of negotiation itself?

It looks it is not really about streams (that's why I do not really like the term serialization), but about identifying the part of the object that needs to be copied, and then grafting that part onto the receiver's view of world).

"It's machines all the way down" language

Seeing how concurrency support steadily becomes a must-have for a programming language, it's very sad to observe that details of scheduling concurrent processes are almost always hidden from the programmer.

{Rant about resource-aware programs}.

Would not it be good to allow the programmer to explicitly provide schedulers when needed? And resource management in general.

The idea of what I am thinking about goes as follows:

Execution history of the program forms a tree, where root represents start of the execution (initiated "supernaturally"), edges represent causality, branching represents concurrent execution, some leaves are final and represent completed (quescent??) execution, while other leaves are "growing points" and represent schedulable resumptions or input requests (there is actually not much difference between these later two, you can think about them as tokens in Petri nets). The tree is unfolded by executing resumptions by (potentially) multiple evaluators (machines?), guided by program-provided schedulers (constraints?). Each resumption is a function from evaluator's input to a tree (which can be a final leaf, an input request or a new resumption (growing point leaves), or a more complicated structure). Whenever an evaluator chooses to execute a resumption, it runs it on an input determined by the resumption's position in the tree, and then grafts the resulting tree under the resumption (probably recording the input as well, which may be useful when input is not _uniquely_ determined by the path).

Virtual machines
To make execution concurrent, resumption may return a "VM" node containing a virtual machine - with its own execution tree and a scheduler. The key is to be able to define the scheduler in the same way as "user" programs.

Another option is to return a "conc" node containing multiple resumptions - these will merge into the pool (err, tree) of resumptions controlled by the current (virtual) machine, and, respectively, scheduled using its scheduler.

Schedulers control only fairness of resource consumption, while all synchronisation issues must be dealt with by using "promise".

Issue: in this design, program is able to consume only one resource at a time - namely, the machine that executes it. How to model multiple resources? And why?
Also: explore potential for join of multiple resumptions - it's dual to the previous - one resource is simultaneously (and even atomically) consumed by multiple processes.
Also: where trust/ownership/responsibility comes into picture?

Also: vau?

Membrane contest

I am sure there will be enough people knowing the languages mentioned by Paul, and willing to participate.
I wonder, whether I'd better follow a different way, and design a language specifically for implementing membranes... But that would be E.

Another idea is to explore membrane as a game. 3-player game. A good reason to criticise theories that emphasise 2-player games?

Socially Responsive, Environmentally Friendly Logic

This logic looks very interesting, as it covers multiple players.
I still have to understand whether it also supports true concurrency in the sense used in CCP.

Away for a week

I am away for a week to a sea-side, may spend some of this time thinking about Goedel's incompleteness theorem.

A Hyperdoctrinal View of Constraint Systems

The title sounds scary, but this paper is quite thoughtful and looks crucial to understand the importance and beauty of concurrent constraint programming.

Intuitively, CCP is good because it is so easy and natural to define a denotational semantics for it. This naturality stems from the fact that closure operators are completely defined by sets of their fixpoints, so all combinators on them can be defined in terms of this sets, not functions themselves. And ability to limit attention to closure operators follows from informational approach to computation.

Internal Type Theory

In a previous paper I introduced a general notion of simultaneous inductive-recursive definition in intuitionistic type theory. This notion subsumes various reflection principles and seems to pave the way for a natural development of what could be called ``internal type theory'', that is, the construction of models of (fragments of) type theory in type theory, and more generally, the formalization of the metatheory of type theory in type theory.
The present paper is a first investigation of such an internal type theory.

I am currently reading this paper (when not working on my day job), so the interpreter has to wait.

Open scheduler. Or open language?

I just wanted to add yet another feature to PAL - fairness for units bigger than a single continuation.
Round-robin for continuations is simple, but it does not take into account the creators of continuations (cause/effect tree). As always, it is possible to construct a use case where right scheduling means not only difference in performance, but also in termination; but I will not do that.
Basically, PAL needs a construct to give a programmer control over dividing "CPU time" between sets of continuations. This could be done, for example, by a statement (SplitCPU PerCent Statement Statement) that reduces two statements in parallel by allocating PerCent "CPU cycles" to the first one, and 100-PerCent to the second one. These statements compose with other statements and each other in an obvious way (children sharing percantage of their parent, not the whole 100%).
This looks cool, but what if I want to introduce more constructs? Already I need cancellation of a branch and scheduling of non-CPU resources ("oracles", more on this later). And I see no easy way to implement these constructs via compilation to PAL.
At this moment I decided - why not make PAL user-extendable? It already supports user-extended terms, I plan to support user-provided scheduler, then why not user-provided statements (op-codes)?
In fact, the whole PAL can be just a composition of a set of "features", where each feature is a set of statements, terms, and scheduling rules. The current PAL can be split into three features - promises, cells, and atomic execution.
I already compose terms using a fixpoint of multiple term functors (actually I mix one functor into a base term, but maybe there ways to do that for any number of functors), I hope the same can be done for statements, but composition of schedulers (reduction strategies) looks a bit less clear at the moment.
If this indeed works, I believe it's time to either create a SourceForge project, or write a paper, or both :)

PS: I have to remember to document my thoughts on efficient implementation of the execution trace tree in the light of composable features.

Plain interpreter. No, compiler.

I was a bit ill during the weekend, so instead of going to seashore played with Haskell.
I shot for an interpreter of Plain in Haskell, but ended with a compiler from Plain to a STM-like intermediate language (promises and atomic execution - let's call it PAL) and an interpreter for PAL in Haskell (let's call it PVM). This looks promising (pun intended).

What I need to do before going further is:

1. Fix implementation of variables in PVM (this is currently a strange hybrid of de Bruijn indices and dynamic scoping).
   
2. Express PAL statements in monadic form to simplify writing compiler(s).
   
3. Express PVM in monadic form to simplify experimenting with it.
   
4. Externalize scheduling (probably in a way of A Language-Based Approach to Unifying Events and Threads). Amusingly, an atomic execution could be elegantly expressed as a strict node in the trace tree.
   
5. Explore possibilities for a type system for PAL (A Functional Abstraction of Typed Contexts?).
   

Typed Concurrent Programming with Logic Variables

We present a concurrent higher-order programming language called Plain and a
concomitant static type system. Plain is based on logic variables and computes
with possibly partial data structures. The data structures of Plain are procedures, cells, and records. Plain's type system features record-based subtyping, bounded existential polymorphism, and access modalities distinguishing between reading and writing.

You may want to compare this with The Oz Programming Model (OPM), which

... is a concurrent programming model subsuming higher-order functional and object-oriented programming as facets of a general model. This is particularly interesting for concurrent object-oriented programming, for which no comprehensive formal model existed until now. The model can be extended so that it can express encapsulated problem solvers generalizing the problem solving capabilities of constraint logic programming.

Another paper on OPM is The Operational Semantics of Oz.

In short, the model of Plain is based on that of Oz with the main differences being:

1. Plain statically types programs using a type system with subtyping, while Oz is latently typed.
   
2. Therefore Plain chooses to drop support for unification in favor of a single-assignment operation.
   

Logical variables?

After all, it looks like old good logical variables may be the best solution for a communication between objects.
See, for example, An introduction to AKL (a precursor of Oz).

Typed Logical Variables in Haskell looks like a good introduction to typed logical variables in Haskell (hey, that's written in the title :) ).

Backtracking

Well, STM's retry is so to say pessimistic - it restarts the whole transaction (up to "atomically" or "orElse") instead of backtracking a single step (one "bind").

Using (simple) backtracking can be inefficient. As an example, consider again a binary join, which succeeds if both its inputs succeed:

join [([], []), ([1], []), ([1], [2]), ([1, 3], [2, 4])] = [([1],[2]),([1],[2]),([1],[4]),([3],[2]),([3],[4])]

It can be implemented for any MonadPlus, but there is some inefficiency there:

join :: MonadPlus m => m (m a, m b) -> m (m a, m b)
join sab = do
  (sa, sb) <- sab
  a <- sa
  b <- sb -- failure on this unneccesary retries sa, should retry sab
  return (return a, return b)

What's worse, there is also a difference in semantics. Consider a shocking example, which fails to terminate:

join [(repeat 1, []), (repeat 1, [2])] = ⊥

This would produce a single answer, and THEN fail to terminate, if it retried sab after failing to read sb:

join [(repeat 1, []), (repeat 1, [2])] = [(1, 2), ⊥]

Note that I cannot fix join by simple moving b <- sb before a <- sa, as they are fully symmetric. What I need is a combinator, which unlike bind would execute actions in parallel, and fail AS SOON as any of them fails. Let's say I need a parallel and - pand. Can I code it in terms of MonadPlus? Let us see...
Aha, a quick googling got me A Monadic Semantics for Core Curry.

Software transactional memory = optimistic transaction isolation + backtracking?

While playing with STM, it occurred to me that it actually combines two features: optimistic transaction isolation (OTI), which allows transactions to execute seemingly independently of each other, and backtracking (BT, implemented via retry/orElse/bind in place of fail/or/and), which ensures atomicity.
If one takes care when designing a concurrent language, then OTI becomes unnecessary. For that, it is sufficient to have:
NDW: non-destructive writes - the source of communication cannot undo previous actions, it can only "append" to them.
LRD: localised read and destroy - access to read/destroy operations on communication media is tightly controlled and in some sense local (like a single thread).
MB: monotonic behaviors - behavior cannot fail on an input bigger than one which made it succeed.
Join calculus enjoys all these properties. Indeed, NDW is ensured by writes appending to a multiset of messages, LRD is ensured syntactically by coupling creation of channels with specifying reactions to them, and MB is trivial as well - join calculus behaviors can only fail (which means - block) because of lack of a message, not because of an extra message.

Why do I think that NDW+LRD+MB obviate OTI?
Because MB ensures it's ok to schedule producer a bit sooner, BT ensures it is ok to schedule consumer a bit sooner, and NDW+LRD+MB ensure it is ok to run producer and consumer in parallel.
One still has to be careful at a very low level of operations - e.g., the multi-processor implementation must ensure atomicity of single writes and reads, but this is easier then full OTI.

If I am right with this conjecture, it would be cool to try and split STM into two facets, OTI and BT, and see, what happens.

BTW, isn't BT just a fancy name for Control.Monad.List? :)

Maude

I am away reading Maude 2.0 Primer.

A Language-Based Approach to Unifying Events and Threads

Looks like great minds think alike :-)
I have to read this paper to see if I am reinventing a wheel.

Some examples from E

I had ten minutes before lunch, and decided to code up a couple of examples from E in Haskell:

type Cont a = a -> STM ()

-- Blocking caretaker - requests are blocked until the gate is open
-- Note that the gate can be opened/closed repeatedly.
makeCaretaker :: Cont a -> STM (Cont a, Cont Bool)
makeCaretaker target = do 
  enabled <- newTVar True
  return (\m -> do {e <- readTVar enabled ; if e then target m else retry}, writeTVar enabled)
  
-- Overwritable promise.
makePromise :: STM (Cont a, Cont (Cont a))
makePromise = do
  queue <- newTChan
  target <- newTVar Nothing
  return (\m -> do
    t <- readTVar target
    case t of
      Nothing -> writeTChan queue m
      Just r -> r m
    , writeTVar target . Just)

Note that both caretaker and promise allow the controller to change its mind - either by repeatedly opening/closing the gate, or by re-resolving the reference. Also, when closed, the caretaker does not signal errors or swallow messages - it keeps the senders blocked. OTOH, promise stores messages in a queue.
Of course, this can be changed (I leave this as an exercise for readers :-) ).
I may consider creating a small library of such patterns and see whether something DSLish comes of it...
But before that I must decide on verification procedure - should I use unit tests or proofs...

STM for CPS

I am trying to manually code up some simple programs using a -> STM () as a continuation type...
And, well, I've stumbled upon some problem with types. Consider a type for a cons list expressed in CPS:

type List a = ((STM (), (a, List a) -> STM ()) -> STM ())

The first STM () gets executed in case of Nil, the second in case of Cons (getting a pair of car and cdr).

Unfortunately, this type fails to check in Haskell. I have to grok yet why, and how to work around it. I would hate to use data:

data List a = List ((STM (), (a, List a) -> STM ()) -> STM ())

as this would reduce clarity by boxing unboxing. Compare:

makeNil :: List a
makeNil (caseNil, _) = caseNil

and

makeNil :: List a
makeNil = List $ \(caseNil, _)->caseNil

Then again, if I shoot for terseness, then nothing beats:

makeNil :: List a
makeNil = List fst

Envisioning code generation for algebraic data types, I arrive to:

type Cont a = a -> STM ()

type CaseNil = Cont ()
type CaseCons a = Cont (a, List a)
data List a = List {unList :: Cont (CaseNil, CaseCons a)}

makeNil :: () -> List a
makeNil payLoad = List  $ \(caseNil, _) -> caseNil payLoad

makeCons :: (a, List a) -> List a
makeCons payLoad = List $ \(_, caseCons) -> caseCons payLoad

Hmm, I should consider using currying, after all...

Critique

The ideas presented so far are not even close to supporting join calculus (however simple it is).
Fluid still falls short in several areas: it is (practically) first-order (so messages do not carry references), it does not support creaition of objects at runtime, it is data flow driven (call it pull-only, or lazy, if you please).
The first problem is caused by the third, which is caused by input devices being the only active sources of messages.
This was caused by the decision to represent outputs of instances as transactionally lazy (STM a)'s, which promised better composability.
Basically, the choice (for a very simple case with one input and one output) is between:
STM i -> STM o -- transaction transformer paradigm, precludes "push", as only the receiving side of the reference is active
and
STM i -> (o -> STM ()) -> STM () -- hey, looks like monadic bind!

BTW, I suspect that relationship between these two types can be seen as expression of some property of negation in some logic :-)