A Vatful of Fluid

A Distributed Object-Oriented Language with Session Types

2008-02-12T13:56:00.000+02:00

Abstract:

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such as ensuring the correct composition of communication behaviours and guaranteeing deadlock-freedom
of their protocols.
This paper proposes the language L_doos, a simple distributed object-oriented language augmented with session communication primitives and types. L_doos provides a flexible object-oriented programming style for structural interaction protocols by prescribing channel usages within signatures of distributed classes.
We develop a typing system for L_doos and prove its soundness with respect to the operational semantics. We also show that in a well-typed L_doos program, there will never be a connection error, a communication error, nor an incorrect completion between server-client interactions. These results demonstrate that a consistent integration of object-oriented language features and session types offers a compositional method to statically check safety of communication protocols.

Ticket-passing style?

2008-01-02T15:28:00.000+02:00

Upon further reflection, I think it does not make sense for application programmer to control CPU distribution down to the ticks.
This would over-specify the scheduling requirements, which often are quite lax.
Presence of multiple physical processors makes the situation even worse.

What probably makes sense is to allow the application developer to explicitly track the separate computation parts, assigning to them various properties, and enabling two-way reflective link between the programmer and the real scheduler.

Think of this as a task management system, e.g., Jira.
Persons acting in one role can create tasks, manage their dependencies, deadlines, estimates and priorities, while persons in another role execute the project making sure the tasks are completed at a satisfactory time.
The first role is like one for the application developer, the second one is for the scheduler of the language's runtime.

Manticore

2007-12-28T11:10:00.000+02:00

naasking mentioned that Manticore has nested schedulers - sounds very interesting, and similar to what I want to achieve in Fluid. Must read that.

Fluid preManifesto

2007-12-27T11:55:00.000+02:00

At this point of my life I don't have much time to actively pursue the research I would like to. I decided to make an overview of what is envisioned, so that at least I do not forget that myself when I have spare minute or two.

Fluid is a codename for programming language/framework/calculus/tool that should enable experiments with and teaching of various approaches to concurrency and possibly parallelism.
During my initial experiments with join calculus I decided that a lot of interesting stuff is being swept under the carpet. For one thing, scheduling of reactions is implicit on one hand, and rigid on the other. What if one had a language in which diving into the gory details of scheduling would be a matter of using some operator, like call/cc is being used to dive into underlying continuations? No scheduling would be left implicit, all interleaving would be deterministic and controlled - mostly using popular constructs from the library in a very lean syntactic way (monadic reflection?), but occasionally giving possibility to do exactly what is needed. At runtime, something similar to engines looks promising.

The language would follow the maxim Algorithm = Logic + Control, separating declarative part of the solution from the control of when to pursue which way and for how long. It must be possible to ration CPU cycles and other resources based on the perceived relative utility of the computations, as well as to prune the computations that are believed to have too few value to be worth any future resources. This utility-aware side of the research might come close to the mechanism design (most probably the algorithmic branch of it).

Having outsourced the scheduling to the user code, the next question is how to express the declarative part of the solution. After playing with various alternatives (promises, MVars, channels) I decided that concurrent constraint programming looks most general of them all. But which constraint system to choose? Or should I choose some specific system at all? As control part is very customizable, why not follow the same path in the logical part? I don't yet know the details, or whether it is possible at all, but the idea is to allow user code to define the constraint system as well.

To put it all in one line: Program = Logic + Control, Your Way, Best Value for Resources!

I would like to write much more, but my margin (of time) is too small, so I finish here.

A Software Architecture for Distributed Control Systems and Its Transition System Semantics

2007-12-11T13:28:00.000+02:00

A software architecture for distributed control systems is presented that is based on a shared data space coordination model. The architecture, named SPLICE, is introduced in two steps.First we give the general structure of the coordination model including the shared data space and the basic operations and we define its semantics by means of a transition system. Second we present a transition system for a refinement of the coordination model: data is distributed and replicated across a communication network using a publication-subscription protocol. We also discuss methods in SPLICE for fault-tolerance and the possibility for on-line system modification and extensions.

Similar to Linda, JavaSpaces, and other paradigms of communication via shared store.

SOA kills ORM?

2007-11-22T10:24:00.000+02:00

Recently I participated in several projects that heavily utilized services (message-based, shared-nothing, over-the-wire thingies). What I noticed is that object/relational mapping (ORM) tools are virtually useless for such projects. Indeed, significant, if not most value of ORM comes from ability to modify values in memory, using OO language constructs for that, and then just synchronize the memory with the database. This functionality goes completely unutilized in typical SOA application, where reads and writes are separated in time, use different objects and acces paths, and in fact can be performed from different machines. E.g., one service can read a list of tasks from the DB and return them as a message to the network peer. After traveling between peers this information (but not this specific object or message) in combination with information from other sources (e.g., user input) can be used to update a specific property of a specific task (written back to the DB). Has need for service/relational (or message/relational) mapping indeed arrived?

JoinJavaScript

2007-11-21T10:16:00.000+02:00

Sometimes I have to use JavaScript for my daily programming, and while it takes some time to switch to it, it has certain beauty and allows some expressivity missing in "bigger" languages like Java or C#.

I tried to identify, what features make it shine, and what features might add even more to the mix.

So great and already present:

Free extension of any object with properties ("every object is a dictionary").
(Limited) introspection ("for in").
Closures as first-class values ("closure is a value", and even "closure is an object").
Prototypes for ad hoc extensibility, e.g., interception of closure invocation at prototype level.

Potentially great, but missing:

Ergonomic way to qualify property names (a la XML or RDF).
More and deeper interception - e.g., access to properties (get/put/foreach).
More advanced control operators - e.g., co-routines and generators.
Concurrency at language level.
More like a constraint on other features - capability-based security.

I see certain synergy among proposed features, so adding them may not automatically turn the language into a kitchen sink.

I would try to approach features 3 to 5 via join calculus. Now, if I only had time.

A Methodology and Tool for Top-down Relational Database Design

2007-11-18T12:52:00.000+02:00

This paper presents a methodology for logical design of relational schemas and integrity constraints
using semantic binary schemas. This is a top-down methodology. In this methodology,
a conceptual description of an enterprise is designed using a semantic binary model.
Then, this description is converted into the relational database design.

THE HISTORICAL RELATIONAL DATA MODEL (HRDM) AND ALGEBRA BASED ON LIFESPANS

2007-11-18T12:05:00.000+02:00

Critical to the design of an historical database model is the representation of the existence of objects across the temporal dimension — for example, the "birth," "death," or "rebirth" of an individual, or the establishment or dis-establishment of a relationship. The notion of the "lifespan" of a database object is proposed as a simple framework for epressing these concepts. An object's lifespan is simply those periods of time during which the database models the properties of that object. In this paper we propose the historical relational data model (HRDM) and algebra that is based upon lifespans and that views the values of all attributes as functions from time points to simple domains. The model that we obtain is a consistent extension of the relational data model, and provides a simple mechanism for providing both time-varying data and time-varying schemes.

Reducibility Between Classes of Port Graph Grammar

2007-09-03T10:12:00.000+03:00

... by Charles Stewart (a.k.a. cas).

It is interesting to compare reducability results for PGGs with those for JCs (especially general SPGG in basic SPGG to general JC in core JC).

As a side note, I start to become uneasy with too complicated encodings... There should be some more fine-grained equivalence than an ability to encode one transformation system in another (something along the lines of expressivity).

For example, the standard encoding of general JC in core JC is not homomorphic in constructs of core JC - implying it is not identity on core JC terms - so this encoding does not prove expressibility of general JC in core JC Felleisen-wise.

PS: linearity.org seems to be down for some reason.

Core Join Calculus - too hardcore?

2007-09-01T10:38:00.000+03:00

After looking closely at core JC, and the proposed encoding of full JC in it, I found it unsatisfactory for my taste.
One problem is that the encoding results in "busy-wait" (stuttering non-termination), even if the original term was "normalizing", which makes the chosen notion of equivalence suspicious. Also, the encoding is sufficiently complicated to ask whether analysis of the resulting terms will be not harder than that of original ones (I recognize that analysis of core JC as a language is easier than of full JC, though - that's the usual trade-off between complexity of a language and its terms, sometimes exemplified by English vs. Chinese, or binary vs. hex).

So maybe I want to take a step back, and pick some variant of JC that is not as spartan as core JC. At the moment I see 3 differences between full and core JCs:
1. Polyadic vs. monadic messages (tuples of channels vs. single channels as payload).
2. N joins per definition vs. 1 join per definition.
3. M patterns per join vs. 2 pattern per join.

I am considering to look closer at the "monadic N M" variant, though in theory one could analyse all combinations, and how they can be encoded in each other (could make a PhD thesis :) ). If one adds to these 3 dimensions another one for allowing or disallowing free names in definitions, this yields 2⁴ = 16 variants. I suspect, though, that one does not need to define encoding for each pair of combinations separately - they all could be factored via few "encoding patterns" (e.g., encoding of N-M JC in 1-2 JC, polyadic JC in monadic JC, and "higher order/closured" JC in "first order/closureless" JC).

Defunc'ed Join Calculus, now in Haskell

2007-08-30T11:32:00.000+03:00


>module J where

This module defines alternative semantics for join calculus (JC) by means of providing an interpreter.

Major differences from standard semantics are:
1. "Kinda closure-converted/defunctionalized" form of object program
- we do not have nested definitions defining scope of names, all pieces of code are "kinda combinators".
2. Making code closed required introducing notion of object instances (data Obj).
- these objects are just identities (plus "vtable"), and could have been defined as just (Int, Code).
- however, this module models identity of the object as history of reactions (joins) that lead to its creation.
3. As all state is carried by messages, the history must be carried by them, as well.
- as a side-effect, we get unlimited stack-, err, graph-trace of the executed program!
- not that this is practical :)

>import Data.List as List
>import Data.Maybe (listToMaybe)

Let us model monadic JC, i.e., messages carrying just one channel as their body.
(see http://citeseer.ist.psu.edu/fournet95reflexive.html, Chapter 5).

Messages are the main part of the system, carrying all its mutable state.

"cause" is Nothing for primordial messages.

>data Msg = Msg {to::Channel, body::Channel, cause::Maybe Join} -- ("from" is redundant, as both causes have it as their "to")
>  deriving (Eq, Ord)
>instance Show(Msg) where
>  show (Msg t b Nothing) = (show t)++"("++(show b)++")"
>  show (Msg t b (Just j)) = (show j)++" -> "++(show t)++"("++(show b)++")"

Join is just a couple of messages that reacted.

Forward reference: Messages of Join have equal "to", left one has L port id, right one has R.

>data Join = Join Msg Msg
>  deriving (Eq, Ord)
>instance Show(Join) where
>  show (Join m1 m2) = "<"++(show m1)++", "++(show m2)++">"

Channels are destinations of messages (and in standard monadic JC the only payload of messages).
Channels are identified by a pair of object identity and a port.

>data Channel = Ch {obj::Obj, port::PortId}
>  deriving (Eq, Ord)
>instance Show(Channel) where
>  show (Ch o p) = (show o)++""++(show p)

As this is core JC, each definition/code/object has just two channels, identified by their port ids - Left or Right.

>data PortId = L | R
>  deriving (Show, Eq, Ord)

Obj is in fact a pair of object identity and procedure for handling messages ("kinda vtable").
Identity is formed by NewId qualified by birthjoin (think birthday).

"birthjoin" is Nothing for primordial objects.
TODO: "code" should not be a part of Eq's "key"

>data Obj = Obj {id::NewId, code::Code, birthjoin::Maybe Join}
>  deriving (Eq, Ord)
>instance Show(Obj) where
>  show (Obj i _ (Just j)) = (show j)++"->"++i
>  show (Obj i _ Nothing) = i

NewId differentiates multiple objects created during reaction to the same join.
In more bytecode-like implementation this would be integer.

>type NewId = String

Code is the procedure to react to a join by creating new objects and sending new messages.
Code is closed, and the only input (capabilities!) it has are:
1. Its left and right channels - via ThisChannel
2. Messages in them (parts of the join causing the reaction) - via ThisMsg
3. Channels in newly created objects - via NewChannel

The reaction is a list of codes for new objects, keyed by their NewIds,
and a list of to/body references for new messages.
TODO: introduce datatypes for these pairs.

>data Code = Code [(NewId, Code)] [(Ref, Ref)]
>  deriving (Show, Eq, Ord)

Reference - means for constructing capabilities.

>data Ref = ThisChannel PortId
>  | ThisMsg PortId
>  | NewChannel NewId PortId
>  deriving (Show, Eq, Ord)

Config of the system is currently just a list of messages (order is important to define deterministic scheduling).

>type Config = [Msg]

Context is "a config with a hole". It is assumed that in this implementation hole is at the end of list.

>type Context = [Msg]

We follow the usual practice:
1. Find in the config a redex and its surrounding context.
2. Reduce redex.
3. Plug the result back.

One might use Danvy's refocusing here (link?),
but I am reluctant to optimize for speed just right now.

Just find the first(!) pair of messages having the same object and having left and right channels as destinations:

>findRedex :: Config -> Maybe (Join, Context)
>findRedex ms = listToMaybe $ [(Join m1 m2, ms \\ [m1, m2])| m1 <- ms, m2 <- ms, (obj $ to m1) == (obj $ to m2), (port $ to m1) == L, (port $ to m2) == R]

Basically translate capabilities to channels:

>reduce :: Join -> [Msg]
>reduce j@(Join l r) = (List.map s2m) sends where
>  Code news sends = code this
>  this = obj $ to l
>  s2m (to, body) = Msg (r2c to) (r2c body) $ Just j
>  r2c (ThisChannel p) = Ch this p
>  r2c (ThisMsg L) = body l
>  r2c (ThisMsg R) = body r
>  r2c (NewChannel i p) = Ch (i2o i) p
>  i2o i = case lookup i news of
>    Just c -> Obj i c $ Just j
>    Nothing -> error ("broken ref "++(show i))

Put result back into the hole:

>plugBack :: Context -> [Msg] -> Config
>plugBack c ms = c ++ ms

TODO: externalise scheduling out of findRedex/plugBack (probably use lazy evaluation - link?).

Now combine all three functions to make a single step:

>step :: Config -> Maybe Config
>step c = case findRedex c of
>  Nothing -> Nothing
>  Just (j@(Join l r), c2) -> Just $ plugBack c2 $ reduce j

And now the most dangerous part, as it is potentially non-terminating (unlike step):

>run :: Config -> Config
>run c = case step c of
>  Nothing -> c
>  Just c2 -> run c2

A few examples:

>c1 = Code [] [(ThisMsg L, ThisMsg R)]
>c2 = Code [] [(ThisMsg L, ThisChannel R), (ThisChannel L, ThisMsg R)]
>--c3 = Code [("x", c2)] [(ThisMsg L, NewChannel "x" L), (ThisMsg R, NewChannel "x" R)]

>ms1 = [Msg (Ch o1 L) (Ch o2 R) Nothing, Msg (Ch o1 R) (Ch o2 R) Nothing, Msg (Ch o2 L) (Ch o1 L) Nothing]
>  where o1 = Obj "a" c1 Nothing ; o2 = Obj "b" c2 Nothing

Try "step ms1" and "run ms1" to get an idea.

The next installment should probably include a little compiler from LC terms to Config.

Programming Languages: Application and Interpretation

2007-08-27T21:16:00.000+03:00

I have to find time to read this textbook - if only to verify my background.

"Defunctionalization" of Join Calculus

2007-08-24T12:06:00.000+03:00

(See Defunctionalization at Work for a background on the defunctionalization technique, The reflexive CHAM and the join-calculus for a background on join calculus.) What I do is not really defunctionalization, but I miss the right term for that.

Lambda calculus can be encoded in join calculus (JC). Algebraic datatypes can be encoded in either. A decent functional PL (think ML) can be encoded in JC. Yesterday I had an idea of looking at the reversal of this encoding - take a JC term, and tell if it is an image of ML term under this encoding (similar in spirit to recovering user-lambdas from brutally CPSed terms). Better yet, take a JC term and split it into functional and (emmm...) superfunctional pieces.
Then I wandered into implementation ideas, and suddenly decided I need to explore some kind of first order JC. I mean, definitions in JC nest and form structures very similar in spirit to closures. What if I closure-convert JC semantics, tinker it a bit, and them put closures back?

I analyzed pages 5-6 of the JC paper, and started scribbling. Spoiled by UML, I didn't use sets or functions, only informal diagrams. "I'll validate it later", thought I.

Everything went fine, until I stumbled upon necessity to construct new instances. Need for elegant generation of fresh names and manifestedly safe references to them was what stopped me... Will have to check literature for inspiration.

An Accidental Simula User: Luca Cardelli

2007-08-24T12:03:00.000+03:00

A personal view of the history behind the calculus of objects!

Accidentally, just last night I considered playing with defunctionalized Join Calculus (a good topic for the next post).

Analyzing the Environment Structure of Higher-Order Languages using Frame Strings

2007-08-18T15:04:00.000+03:00

Besides tackling a really fundamental issue, the paper has an interesting preface.

Abstract And-Parallel Machines

2007-07-13T19:35:00.000+03:00

I will have to persuade myself I never read this paper before, as reading it induces a deja vu in me.

Excellent stuff!

Multiscale Scheduling: Integrating Competitive and Cooperative Scheduling in Theory and in Practice

2007-07-09T22:35:00.000+03:00

They touch a lot of ideas I was vaguely exploring on this blog (hierarchical scheduling, scheduling as game, utility-driven scheduling).

E.g., DAG models are superficially similar to cobs (though cobs are not sequential tasks, they are atomic units of rewriting).

Hope this program will succeed!

Graph Rewriting Semantics for Functional Programming Languages

2007-07-03T20:46:00.000+03:00

Something I should have read before pontificating on cobs :)

Preventing Internet Denial-of-Service with Capabilities

2007-06-24T20:50:00.000+03:00

A topic of DoS attacks has surfaced recently on LtU, so this paper may be relevant to PLs design enough.

Imagine combining Trickles with this scheme...

Trickles - Stateless High Performance Networking

2007-06-24T20:36:00.000+03:00

The Trickles network stack is a stateless replacement for TCP and the Berkeley sockets interface. It removes all per-connection state from one endpoint, typically the server, while providing important features such as congestion control, security of server-side state, and support for dynamic content.

In addition to markedly reduced memory overhead, our server-side stateless stack allows increased flexibility in redirecting network traffic at packet-level granularity, since any server can service any request regardless of past communications history. This enables new functionality in the network layer, such as transparent failover, load balancing, anycast services, and striped download.

I wonder, how well this can be bent to work with multicast.

Work, work

2007-04-05T13:39:00.000+03:00

This message is just to make sure Blogger does not write me off as MIA :)

My family and job responsibilities withdrew my attention from research and blogging, hope I will find some time soon to post some findings/ideas I had since January.

Punctuated Data Streams

2007-01-25T15:35:00.000+02:00

We explore a kind of stream semantics called punctuated
streams. Punctuations in a stream mark the end of substreams, allowing us to view a
non-terminating stream as a mixture of terminating streams. We introduce three kinds of
invariants to specify the proper behavior of query operators in the presence of punctuation.
Pass invariants unblock blocking operators by defining when such an operator can pass
results on. Keep invariants define what must be kept in local state to continue successful
operation. Propagation invariants define when an operator can pass punctuation on. We
then present a strategy for proving that implementations of these invariants are faithful
to their finite table counterparts.

Some definitions could be streamlined, and typos corrected, but otherwise looks interesting.
I also suspect reformulating the definitions in terms of domain theory might have benefited both reader and writer (less implementation-specific details).
On the other hand, category theory might be an overkill for this...

Also, can this be seen as a good application for concurrent constraint programming?
On the first glance punctuations look just like constraints.

Comonadic functional attribute evaluation

2007-01-24T10:50:00.001+02:00

They relate zippers to comonads. Wow!

CoKleisli categories make comonads relevant for analyzing notions of context-dependent
function. If the object D A is viewed as the type of contextually situated
values of A, a context-dependent function from A to B is a map D A -> B in the base
category, i.e., a map from A to B in the coKleisli category. The counit eA : D A -> A
discards the context of its input whereas the coextension k† : D A -> D B of a function k : D A -> B essentially duplicates it (to feed it to k and still have a copy left).

No wonder processes looked like zippers to me - they are about contextually situated values (err, actually computations :( ).

Monads, Kleisli Arrows, Comonads and other Rambling Thoughts

2007-01-24T10:02:00.000+02:00

Simple, and to the point.

Now I wonder how to generalize this result to stream processors that do not preserve rate (i.e., produce a list to an output stream for each history of the input stream). Generalization to multiple inputs is next.

The Theory of Timed I/O Automata

2007-01-23T13:30:00.000+02:00

Especially note receptiveness.

What kind of logic is “Independence Friendly” logic?

2007-01-23T12:51:00.000+02:00

In a series of singular, thought-provoking publications in recent years, Jaakko
Hintikka has vigorously promoted consideration of an extension of first-order logic called
IF logic, along with claims that its adoption promises to have revolutionary
consequences. My main purpose here is to examine in what sense it deserves to be called
a logic.

Uh-oh.

A REVOLUTION IN LOGIC?

2007-01-19T21:54:00.000+02:00

I wanted to compare IF logic to computability logic for a long time. Must find time to do that soon.

Payment as part of game semantics

2007-01-19T18:44:00.000+02:00

In CL, a semantical object maps each run to a set of possible moves for both players and a currently winning player. One idea would be to replace the latter by payments. I mean, if one uses games as contracts, it makes more sense saying that as a result of our interaction I owe you 10 euro by the end of the year than to say that I lost my contract. As a side effect, it makes possible win/win (or lose/lose) outcomes - I owe you 10 euro by the end of the year, but you owe me 10 dollars by the end of the month. Then again, how to enforce these payments? Sooner or later we must reach some escape hatch for extra-logical enforcement (court?). But I still believe that it may be more useful to come to court asking for 10 euro than asking to make false true.

Also, when going to court, you want to bring some evidence, or witness. So the outcome is not a boolean, but a scheduled flow of expected payments, each annotated with a witness (a non-repudiable pointer to a move that decided this payment). Note that missing a payment must be interpreted as a move as well - and thus modify the outcome. I wonder, if this can be implemented at least in theory, or there is some metacircular recursion ("it's moves all the way down").

PS: http://dsns.csie.nctu.edu.tw/research/crypto/HTML/PDF/C82/199.PDF

Untangling conditions from responsibility

2007-01-18T13:01:00.000+02:00

I've re-read the introduction to computability logic, and found that I might want to define my own version of it (or at least to try that).
For example, in CL it is not possible to define arbitrary predicates for branching - only those that can be assembled from conjunction and negation. It may sound funny at the first glance (and/not is a sufficient set of operations, as is Sheffer stroke, for example, right?), but this only holds in classical logic - as games are stateful in a way, one should not duplicate them lightheartedly, so some kind of linearity is needed. For example, XOR or EQ cannot be defined using AND and NOT without duplicating the parameters (A XOR B is !(!A & !B) & !(A & B)).

To overcome this problem, I prospose to replace conjunction and negation in the logic by a branching operator with attached truth table. So NOT A becomes BRANCH(a:A; not a), AND A B - BRANCH(a:A, b:B; a and b), XOR A B - BRANCH(a:A, b:B; a xor b) - where I write truth tables as classical logic formulas for brevity. Note that each subgame is mentioned by branch exactly once.

I have to explore the issues raised by the fact that now it becomes possible to define branches with not monotonically non-decreasing condition. The previous encoding elegantly combined conditions with switching responsibility. I would like to untangle one from another if only to prove that it was unnecessary. So in addition to replacing and/not by branch, I would like to explicitly annotate choices and quantifications by the party responsible for them, and make this annotation unaffected by branching conditions. This will yield more verbose formulas, but has potential of uncovering some independence between features that were coupled.

Also, for various reasons, I will use game variables instead of predicates as a base case.

All in all, game language could be defined as:
G = branch (Seq n G) satisfying (Seq n Bool -> Bool)
| hide x in G by Bool
| choose (Seq n G) by Bool -- in future also dependently-typed version of this
| let x = G in G -- recursion definition
| x -- recursion backlink
| v -- external game variable
| replicate G by Bool -- replication, may add some constraints on cardinality later

I may want to drop recursion and move to representing games as directed graphs at some point. ATM, textual representation is more handy, though.

The next installment will probably discuss terms (err, runs) for these types (games) or theories and models of this language.

Hard-play model

2007-01-16T11:21:00.000+02:00

See section 15.

The type of the process I described previously is similar to hard-play model by Giorgi Japaridze.
In terms of game semantics, the environment can make as many moves as it wants (and as is possible in the current state) by filling the holes and only then to give an opportunity to make a move to the process (by forcing it).

Hard-play and easy-play models intersect on a practical class of problems, so it might be enough to support only one of them. However, human factors might require suppporting both (or a more general model).

E.g. (piohiho process):


class Process p i o hi ho where
 schedule :: (p, Map hi i, Set ho) -> (p, Map ho o, Set hi)

The environment passes to a process some of the previously requested inputs, and requests some outputs. The process responds by some outputs, and requests some inputs.
Note that while values of both ho and hi must be used linearly, it is allowed to postpone their fullfilment by several steps.

PS: alterrnatively, to make justification structure more obvious:


class Process p i o hi ho where
 schedule :: (p, Map hi (i, Set ho)) -> (p, Map ho (o, Set hi))

Indexed Containers

2007-01-15T16:21:00.000+02:00

Two news. Good one - Conor McBride shows how to type interactive processes (section 7.3: Imperative Interfaces and Container Drivers).
Bad one - the type system involved is quite involved.

PS: also, I am not yet sure his idea indeed covers non-alternating games, so to say.

Weakly-typed processes

2007-01-15T15:17:00.000+02:00

To give a better idea of the process type I mentioned in the previous post, here is its weakly-typed variant:


class Process p o i h | p -> o i h where
 force :: p -> (o, Maybe h, p)
 fill :: (p, h, i) -> p
 runnable :: p -> Bool

Method force obtains an output, a potential hole, and a (new state of the) process.
Method fill fills a hole of the process with an input, obtaining a process.
Method runnable checks whether the process can be forced (at least once).

I call this variant weakly-typed because it permits various run-time errors (which are type errors for the tiny process language being interpreted). Examples are: forcing unrunnable process, filling a hole that does not belong to a process, filling a hole with a value of wrong type.

An encoding of the same functionality that statically catches these three errors is left as an exercise for the reader (the first one is easy, while the remaining require either dependent types or unwieldy tricks, I believe - one approach would be to carry in type of a process a boolean representing runnability and a map from holes represented as Peano numbers to their types - and I do not see how to make types that differ only by order of holes to be equal).

PS: idea, instead of Map Nat Type I can have [Maybe Type], which has simpler equality. However, the latter type either grows unboundedly as process evolves, or requires reuse of garbage (i.e, Nothing) slots. GC at type level, anyone? :)

Number-parameterized types

2007-01-15T11:07:00.000+02:00

Yesterday I played with number-parameterized types in Haskell (actually, GHC).
The ultimate goal was to create a type for a process, that when forced, pops out an output and another process, which can be forced again, etc. The environment can later graft inputs at the places in the process that popped outputs (not necessarily in the order of outputs, but keeping correspondence between inputs and outputs). E.g., process can request an input from a file, then from a keyboard, then environment will provide it with input from a keyboard, and then from file. To complicate the issue even more, different choices of outputs have different options for inputs (so types of inputs are indexed by values of outputs).

I started from more modest types to make sure I understand what I am doing.
First I needed a couple of phantom types to build arithmetic on types:


data Z -- 0 inhabitants
data S a = L a -- as much inhabitants as in a

class Sum a b c  a b -> c
instance Sum Z a a
instance Sum a (S b) c => Sum (S a) b c

Among other things, this enabled me to build sequences parameterized by their size:


data Seq a s = Seq [a]
 deriving Show

nil :: Seq a Z
nil = Seq []

cons :: a -> Seq a m -> Seq a (S m)
cons h (Seq t) = Seq (h:t)

app :: Sum m n s => Seq a m -> Seq a n -> Seq a s
app (Seq m) (Seq n) = Seq (m ++ n)

Note that I use ordinary lists inside Seq, so I can reuse all their operations (e.g., ++).

Next step would be to convert ordinary lists to sequences.
For that, I choose to bundle sequences with their lenght representation in an existential package. First, I define a type for representation of naturals:


data NatRep s = NatRep Int
 deriving Show

z :: NatRep Z
z = NatRep 0

s :: NatRep a -> NatRep (S a)
s (NatRep n) = NatRep $ n+1

I could have done the following:


data Nat = Zero | Succ Nat
 deriving Show

data NatRep s = NatRep Nat
 deriving Show

z :: NatRep Z
z = NatRep Zero

s :: NatRep a -> NatRep (S a)
s (NatRep n) = NatRep $ Succ n

, but decided to keep Peano arithmetic restricted to types.

Now I am equipped with tools to create dynamically typed sequences parameterized by their size (quite a mouthful):


data DynSeq a = forall m . DynSeq (NatRep m) (Seq a m)
instance Show a => Show (DynSeq a) where
 show (DynSeq n sq) = "(DynSeq " ++ (show n) ++ " " ++ (show sq) ++ ")"

toDynSeq :: [a] -> DynSeq a
toDynSeq [] = DynSeq z nil
toDynSeq (a:as) = case toDynSeq as of DynSeq n sq -> DynSeq (s n) $ cons a sq

A couple of surprizes notwithstanding (inability to derive Show for DynSeq, or to use pattern with DynSeq in either let or where), it was quite easy (if not optimal, should I have used GADTs?). Also, I suspect that the decision to use lists inside Seq and Int inside DynSeq will bite me more than once. Also, I am not comfortable with the approach of using functions like nil and cons instead of constructors, this may hinder compiler to help me.

Will have to think about ways to reach the ultimate goal now...

See also http://okmij.org.

PS: I am using the following options:
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances #-}

Helping in a multiprocessor environment

2007-01-13T19:02:00.000+02:00

Helping occurs when a thread A wants to lock an object that is already locked by another thread B. Instead of blocking, A donates time to B, helping it to finish its critical section. Helping is an implementation of priority inheritance.

So I learned that the idea I use in my interpreter is in fact widely known and used. No wonder.

Will have to add this line of research to my reading list.

Extending the Multilisp Sponsor Model

2007-01-08T12:39:00.000+02:00

That's the paper I should have read a long time ago!
It would give me the use cases to test my ideas against.
Now, I hope I will have more motivation to hack up some running code.

Design of the Kernel Language for the Parallel Inference Machine

2006-12-31T19:20:00.000+02:00

Looks like all my fooling around with cobs and application-level scheduling is very similar to Flat GHC/KL1 from the Japanese Fifth Generation Computer Systems project.
They were doing this stuff when I was learning my first programming lessons :)

PS: actually, http://citeseer.ist.psu.edu/ueda94moded.html is closer to my ideas.

Simultaneousity induced by causality

2006-12-19T15:50:00.000+02:00

A really quick note - when lifting functions to event processing, their inputs must happen simultaneously. One idea for simultaneosity in absence of global clocks is to define events as simultaneous iff their causes are equal.

More generally, all uses of timestamps might be replaced by causes. All these partial orders start looking similar to domain theory...

I will need to check how far this can get me.

Unitstreams

2006-12-13T12:41:00.000+02:00

Another random thought:

I got curious, what would be the minimum abstraction needed to describe communication between agents. One obvious solution would be bitstreams (streams of booleans). On the other hand, it is not the minimal one - if one thinks about computer networks, at the electrical level they do not use streams of bits. Superficially, setting potential on the line to either low or high can be thought as sending a bit, but actually the bitstreams sent this way are very limited - namely only streams with alternating bits can be encoded this way. And informational difference between all streams of units and those streams of bits where bits alternate is very small - just one bit per whole stream! By that I mean that a timestamped sequence of units [(), (), ()] corresponds to one of the two timestamped sequences of bits: either [0, 1, 0] or [1, 0, 1]. This difference is so negligeble, I believe it can be ignored, so we can pretend that computers communicate to each other using unitstreams (at least at some level). It is very crucial that units in these streams are timestamped, otherwise they cannot carry enough information. Networks rely on the fact that peers are usually not moving fast enough relatively to each other, so their local clocks are good enough to recover timestamps that are not sent explicitly. An interesting question would be whether it is beneficial to model clocks as unitstreams as well, then instead of timestamping units in the stream we instead relate them to units in some other stream (but probably need to ground this induction somewhere - or make it coinduction :) ).

Causality

2006-09-18T15:26:00.000+03:00

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)

2006-09-17T12:35:00.000+03:00

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

2006-09-09T17:20:00.000+03:00

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

2006-08-18T16:38:00.000+03:00

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

2006-07-29T22:26:00.000+03:00

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

2006-07-11T14:01:00.000+03:00

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

2006-06-16T13:51:00.000+03:00

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

2006-06-07T16:03:00.000+03:00

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

2006-05-19T10:56:00.000+03:00

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?

2006-05-09T11:05:00.000+03:00

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.

2006-05-08T09:53:00.000+03:00

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:

Fix implementation of variables in PVM (this is currently a strange hybrid of de Bruijn indices and dynamic scoping).
Express PAL statements in monadic form to simplify writing compiler(s).
Express PVM in monadic form to simplify experimenting with it.
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.
Explore possibilities for a type system for PAL (A Functional Abstraction of Typed Contexts?).

Typed Concurrent Programming with Logic Variables

2006-05-05T17:31:00.000+03:00

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:

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

Logical variables?

2006-05-03T16:08:00.000+03:00

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

2006-05-03T11:15:00.000+03:00

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?

2006-05-03T09:37:00.000+03:00

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

2006-05-02T12:02:00.000+03:00

I am away reading Maude 2.0 Primer.

A Language-Based Approach to Unifying Events and Threads

2006-04-28T21:35:00.000+03:00

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

Some examples from E

2006-04-28T12:37:00.000+03:00

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

2006-04-27T11:52:00.000+03:00

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

2006-04-26T10:48:00.000+03:00

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 :-)

Devices/distribution = chicken/egg?

2006-04-25T17:07:00.000+03:00

Obviously, I/O devices and distribution (multiple vats) can be expressed using each other.
For various reasons I prefer to view devices as primitive, and implement distribution via stubs/scions (this is consistent with E paradigm).

What is not consistent with E paradigm, though, is that a vat ceases to be a single thread - it is a family of threads, namely one thread for (transactional) instances, and one thread for each device. I cannot understand the implications at the moment (mostly for robustness), but this is something to keep an eye on. OTOH, I can always bind this family to a single OS thread, which means I will match E perfectly, right? Must ensure this way of running vats is enforced, though.

Some code functions+devices

2006-04-25T16:05:00.000+03:00

Here is some Haskell code to illustrate my previous post (I cheat a bit with tuples in unary cases):


-- AND join in workflow terminology.
binaryJoin :: (STM a, STM b) -> STM (a, b)
binaryJoin (sa, sb) = do
  a <- sa
  b <- sb
  return (a, b)

-- Very simple code function.
inc :: Num a => STM a -> STM a
inc sa = do
  a <- sa
  return (a+1)

-- Code that delegates to other code.
add :: Num a => (STM a, STM a) -> STM a
add inputs = do
  (a, b) <- binaryJoin inputs
  return (a+b)

This code covers so called instances in terminology of Mark's thesis.
What about devices? For output the answer looks simple: code for output devices has type:
(STM i1, ..., STM im) -> IO (), but such object would probably require a separate thread to run (can we say that's because, unlike STM, IO is not composable?). Thus, I suggest splitting (code for) output devices into a transactional matcher part (if needed at all) of type (STM i1, ..., STM im) -> STM a and a reactive handler part of type a -> IO (). This gives the framework runtime a chance to run matchers transactionally, and only when one of them matches, run the handler.
So, we have (pseudo-Haskell):
data OutputDevice = forall a . OutputDevice ((STM i1, ..., STM im) -> STM a) (a -> IO ())

What about input devices? The first idea is to type them:
(a -> STM ()) -> IO ()
with the contract that the device performs some input, then applies the (parameterised) transaction to it, then runs it.
Why not just IO a? Deal, I can minimize input device's responsibility by saying the framework will "apply and run", while the device will just read and return, so the type is:
IO a

Well, by its nature (blocking input) each input device will be run on a separate thread, injecting its values into the transactional thread via TChan'nels. I don't like this (especially when we dealt with multithreading issues of output devices), but currently see no other alternative. I have to explore the Haskell standard library to see, whether the input is mostly blocking.
If nothing better can be done with input devices, then maybe it makes sense to run output device on separate threads as well, and let STM runtime to handle blocking (so output devices will be typed (STM i1, ..., STM im) -> IO (), or even a -> IO ())...

Some thoughts

2006-04-25T15:37:00.000+03:00

Ok, I decided to stop fighting Haskell on the particular technical issues, and instead sit back and think a little.

What is an object? From the implementors point of view, of course :-)
Let's assume in E tradition that this is something that upon receiving a message can change its state and post a set of messages along the references it holds.

Nothing interesting so far. It becomes better when we notice that multiple objects often share some logic, which we might call "code" or "class" or "prototype". Let's call it code. What is this code? In Haskell, I postulate, it is natural to see this code as a function from message and object state to set of deliveries and new state. But what is the exact type of this function? Here some experience with join calculus suggest a nice trick: both the state and the messages can be modeled uniformly!
My current proposal is to say that object code is a function of type:
(STM i1, ..., STM im) -> (STM o1, ..., STM on)
The inputs are transactions that represent reading either public "facets" or private "state", and the outputs are transactions that represent either sending messages to other objects or updating private state (in a roundabout way - the transaction must be executed to obtain the "written" value - this simplifies composability of multiple code functions).
(Of course this type can be curried, but I like its simmetry).
is and os stand for (possibly polymorphic) types (not sure yet how to better handle multiple messages on the same ouput - and then, maybe on the same input, as well?).
Note that none of the output types mention the identity of the receiver - they are indeed types of messages, not of deliveries.

So how and who attaches the receivers to the messages? I say it is responsibility of (the instance of) the object that uses this "code". Note that I ended up with three parties: authors of the code, users of the code, and authors of the framework (that's me!) that are responsible for helping users to use the code easier. Now if only this third party knew how to achieve that :-)

No Data.Typeable for polymorphic types :(

2006-04-24T13:33:00.000+03:00

Alas, after spending some time with Data.Typeable I understood it is (for some reason) limited to monomorphic types.
Thus I hesitate to use it as a way to glue (user) delivery handling functions to the (system) framework.
Hmm, should I invert the logic, and instead of functions from (reading) STMs to Effect use tuples of (writing) STMs and Effect?

Probably I will get smarter after lunch :)

The first problem

2006-04-21T17:45:00.000+03:00

Well, I have the first subset of runtime working - objects with a single facet (so state or concurrency are not possible).
That was surprisingly easy, despite I needed to understand existential types.

Now I have the first problem - to introduce multi-faceted lexical compounds I need to write a function taking a function from several (let's say n) STM Delivery to Effect and returning exactly n TChan Delivery and an Effect...
A wrong type:
close :: ([STM Delivery] -> Effect) -> ([TChan Delivery], Effect)
as it does not constrain the lengths of the lists to be equal (and worse, operationally close does not know how many channels to create given just a function from a list to effect).

When I figure out how to do this (either by adding explicit n to the left side of the type, or by some GADT trick), I will generalize the problem to parametric (Delivery o a)...

Kick-off

2006-04-21T11:50:00.000+03:00

Ok, I said I will "try and create a toy implementation of E-like system", and so I started this blog to document my thinking and its changes.

First of all, I am happy to start working on this, as my previous experience with Haskell was limited to school assignments - now I can finally use all the cool features, including type classes, existential types, composable transactions, and more :-)

I quickly rolled a parser for join calculus using Parsec, not that this was needed at the moment, but it was fun and a good warm-up.

Now I am pondering over the ways to skin... err, to modularize the runtime.
One idea is to have multiple languages interoperating in my vats (word "vat" is used without permission of E authors :-) ), so I want to separate semantics of the process definition language from that of the "robustness framework".

I will start from defining the notions of delivery (or message), object (the target of deliveries), and effect - what happens upon delivery. I need at least IO effects to model output devices (in terms of E thesis), and also (STM [Delivery]) effects to allow objects send messages to other objects (transactionally - in the same vat). I think I will need forall to allow multiple implementations of objects to cooperate... Time to learn some Haskell-fu :-)

BTW, if you wonder: Fluid is the code name of this project.