3 applications of "indexed composition" as a language design principle

Here are links to 3 toy language specs (as webapps) for manipulating and computing with

• typed sets of tuples (naturalselection)
• graphs (GraphL)
• processes (parallelOgram)

i have included below a short exegesis of the strategy for generating these languages and some examples from each language.

Building the examples

To build these examples on a *nix box you need at a minimum

• svn client installed
• mvn (2.x) installed
• for GraphL you also need graphviz installed and its dot utility on your execution path

The steps to build any one of these is the same, but for purposes of discussion let's use naturalselection

> svn co http://svn.biosimilarity.com/src/open/naturalselection/trunk naturalselection
...
> cd naturalselection
> mvn compile
> mvn jetty:run

point your browser at localhost:8080 and play around.


A brief explanation of how this stuff works

In essence the idea can be explained in terms of a data structure that supports a some form of composition. The simplest of these (with identity and an associative notion of composition) is a monoid. An instance of such a data type is freely generated from

m,n ::= e | g1 | ... | gN | m*n

and cut to order with the identities, e*m = m = m*e, m1*(m2*m3) = (m1*m2)*m3, together with any identities a specific monoid might require.

This is all well and good, but many times we want to provide a form of indexed composition. We are familiar with this in arithmetic where we want indexed sums or indexed products. These are usually written as expressions of the forms

• ∑_{i ∈ S} t(i)

• ∏_{i ∈ S} t(i)

However, it is clear that such expressions can really be expressed as a kind of comprehension

• {+ t(i) | i <- S +} // we move from ∑ summation to "braced-summation"

• {* t(i) | i <- S *} // we move from ∏ product to "braced-product"

Again, there is not much to this than a shift in syntax. However, there is a question about the language for

• generators, e.g. i <- S, and
• conditions, e.g. p(i), where p is some predicate on i

Here, we can use two monads to generate the language for predicates and patterns (the source and target of substitutions). For this we only need to provide as input a 'notion of collection' and then both the predicate and pattern language fall out.
Suppose our 'notion of collection' is set. Then the logic language for the predicates is given by

k,l ::= true | ~k | k&l | e | g₁ | ... | g_N | k*l | \forall x in k.l | rec x.k | x

with semantics as discussed, for example, here.

The pattern language is given by

p,q ::= _ | v | e | g₁ | ... | g_N | p*q

Finally, our indexed composition is given by

{* p | q₁ <- m₁, ..., q_N <- mN, q_i1 in k₁, ..., q_iM in k_M *}

Pragmatically, a term of this form of this will evaluate to

(p s₁) * (p s₂) * ... * (p s_N) * ...

where s_i are substitutions generated from the generators that simultaneously satisfy the constraints. In fact, there is a nice 'evaluation' theorem which says that every term in Q m c evaluates to a (possibly lazy) extensional form. This is essentially a generalization of (the construction underlying) Codd's theorem.

If you recognize that a monad is really a monoid in disguise (or the other way around depending on which side of the mirror you live on), you will see that this is really just Oleg's LogicT monad transformer generalized with a 'notion of collection'.

More specifically, given a data type, like m above, that supports some composition we can generate a new data type Q m c, (where c is the 'notion of collection'). In the case that c is set, then QSet m = Q m set is given by

m,n ::= e | g1 | ... | gN | m*n | {* p | q1 <- m1, ..., qN <- mN, qi1 in k1, ..., qiM in kM *}
k,l ::= true | ~k | k&l | e | g1 | ... | gN | k*l | \forall x in k.l | rec x.k | x
p,q ::= _ | v | e | g1 | ... | gN | p*q

In the code at the links above i'm still writing the evaluators. The one for GraphL is filled in enough that the REPL doesn't just print out the parse tree for the expression but actually generates an svg image using GraphViz magic.

The others are still in progress, so check back at the repo occasionally, as there will be updates to the source. A final comment regarding the generality of this approach. The examples were chosen for a reason.

• In the case of naturalselection, we have essentially autogenerated a pretty compelling version of SQL.
• In the case of graphs not only have we given an algebra of graphs with nice properties we have also autogenerated a query language for graphs.
• In the case of processes you will note that processes have execution semantics. They evolve in time. The logic that is autogenerated allows constraints that govern the execution semantics of processes. The constraint solver is essentially a model-checker. There's an older codebase written in OCaml instead of Scala+Lift where the REPL and model-checker considerably more developed, here. This codebase does not explore the idea of indexed composition, however.
  

The point of this is that the approach is extremely general and yet effective and realizable with tools that are freely available on the web.

Examples of the toy language naturalselection

• The empty record and a synonym
  

Nil
record () { }

• An extensionally described dataset -- this is the equivalent of dump from an sql table
  

record (F1,F2,F3){ (1,2.0,"three"), (4,5.0,"six") }

• An intensionally described dataset -- describing a dataset in terms of a composition of some given datasets R1, R2, R3
  

record (F1,F2,F3) { (x,y,z) | (x,u,w) <- R1, (v,y,a) <- R2, (t,s,z) <- R3, u == v, a > w }

this returns all the triples (x,y,z) the 1st column of which comes from the first column of R1, the 2nd column of which comes from the second column of R2, and the 3rd column comes from the 3rd column of R3; the dataset only contains those triples for which the 2nd column of R1 equals the 1st column of R2 and the 3rd column of R2 is greater than the 3rd column of R1

• Another few examples of intensionally described datasets

let {: (a,b,c) ; R1 :} = R in record (F1,F2,F3) { (x,y,z) | (x,u,w) <- R1, (v,y,a) <- R2, (t,s,z) <- R3, u == v, a > w }

let {: (a,b,c) ; R1 :} = R in record (F1,F2,F3) { (x,y,z) | (x,u,w) <- R1, (v,y,a) <- R2, (t,s,z) <- R3, u == v, a > w, (u,v,w) in (~null,~null,~null) }

let {: (a,b,c) ; R1 :} = R in record (F1,F2,F3) { (x,y,z) | (x,u,w) <- R1, (v,y,a) <- R2, (t,s,z) <- R3, u == v, a > w, (u,v,w) in (~null,~null,~0) }

These three illustrate 'destructuring' a given dataset in a let binding. This particular binding picks off the first triple from R and uses the 'rest' as the value R1. These examples extend the previous one by adding structural logical conditions. The middle one requires that we don't pick out tuples with null values for u,v and w. The last one requires that we don't pick out null values for u and v and that w is non-zero.

• Operations on dataset expressions 'in place'

(2,3,5) :: record (F1,F2,F3) { (x,y,z) | (x,u,w) <- R1, (v,y,a) <- R2, (t,s,z) <- R3, u == v, a > w }

This example 'conses' a triple onto a dataset containing triples

• This one illustrates the creation of 'infinite' datasets using lazy semantics

let R = (( (2,3,5) :: record (F1,F2,F3){ (x*x,y*y,z*z) | (x,y,z) <- R } )) in R

The first 5 triples of this dataset are

{(2,3,5),(4,9,25),(16,81,625),(256,6561,390625),(65536,43046721,152587890625)}

Examples of the toy language GraphL

• The discrete graph with 3 vertices
  

<[[1]]> | <[[2]]> | <[[3]]>

• The graph with two vertices and an edge between them

(("phred"))(let x = [[1]] in <[[1]]>, let y = [[2]] in <[[2]]>)

• Two copies of the previous example laid side-by-side

(("phred"))(let x = [[1]] in <[[1]]>, let y = [[2]] in <[[2]]>) | (("jorge"))(let u = [[3]] in <[[3]]>, let v = [[4]] in <[[4]]>)

• Lest you think these examples verbose, check out the docs (with pictures) in the doc directory of the GraphL project to see examples for where the programmatic language starts to pay off; but please note the documents are slightly out of date with respect to the running application and i haven't taken the time to update them.

Examples of the toy language parallelOgram

• The stopped process

0

• A process waiting on input at channel x, only to terminate immediately after

x?(y)0

• The process that will deliver the code for the stopped process to some lucky process waiting on input at channel x

x!('0)

• The process that will wait for input on channel x or channel u and then terminate

switch { x?(y)0, u?(v)0 }

• The process that runs the process that outputs on channel x the code for the stopped process in parallel with a process waiting for input on channel x (and then terminates)

{ x?(y)0, x!('0) }

• The classic race -- the switched process will wait for input on x or u and is running in parallel with two processes, one that outputs on x and one that outputs on u

{ u!('0), x!('0), switch { x?(y)0, u?(v)0 } }

• This one is pretty cool -- it's a parallel version of the paradoxical combinator -- essentially it implements (a much too eager form of) Milner's replication, !P

{ x?(y){*y, x!(y)}, x!('{ P, x?(y){*y, x!(y)} }) }

• Our first example of a comprehension in processes this will generate an (output x on running in parallel with the switch) running in parallel with (output on u running in parallel with the switch)

{ {: P, 'switch { x?(y)0, u?(v)0 } :} | P <- { x!('0), u!('0) } }

• Another example of a comprehension -- this generates a switch with branch continuations taken from the outputting processes

{ :switch: { x:?(@X)P, u:?(@Y)P } | P <- { x!('0), u!('0) } }