i am not a monad i am a free algebra! (Pt 3)

This post is a part of a series of posts attempting make explicit some folklore and wisdom of the commons that computer scientists enjoy but neither mainstream programmers nor mainstream mathematicians have exposure to. Both of these cultures would benefit from this common wisdom and so it feels like telling this story is of a certain utility. The caveat is that unlike the other posts the pay-off is cumulative not immediate. i'm not going to present some eye-catching bauble as with the post on Conway Games. Instead, you're going to have to steep in this stuff a bit before the goodness kicks in.

A short detour through LBNF

If we look at the LBNF grammar formalism, the correspondence to type construction in a functional language is very clear. The primary difference between LBNF and ordinary BNF is that each alternative or choice is given a label (hence the ‘L’ in LBNF). Thus, while an ordinary BNF rule is of the form

Cat "::=" Item* ;

where Cat is the syntactic category of the rule that corresponds to the expansion given by the list of elements in Item*, the body of the rule, an LBNF rule is of the form

Label "." Cat "::=" Item* ;

where the Label is added to disambiguate various alternatives. So, the heart of an LBNF grammar for LBNF grammars is given here.

--The rules of the grammar
Rule . Def ::= Label "." Cat "::=" [Item] ;

-- Items
Terminal . Item ::= String ;
NTerminal . Item ::= Cat ;

-- Categories
IdCat . Cat ::= Ident ;

Notice that the category Item has two different alternatives, conveniently labeled Terminal and NTerminal, illustrating the role of the label in disambiguating alternatives. In fact, it works just like a tag in a discriminated union, which is exactly the machinery in Scala's case classes.

From this we can relatively easily intuit a direct mapping from LBNF rules to type specifications in an (object-)functional language like Scala.

C1 "." T "::=" Item11, …, Item1M ;
C2 "." T "::=" Item21, …, Item2N ;

These rules correspond to

trait T
case C1( i11 : [| Item11 |], …, i1M : [| Item1M |] ) extends T
case C2( i21 : [| Item21 |], …, i2N : [| Item2N |] ) extends T

where [| Itemij |] denotes the trait to which the category Itemij has been translated.

Thus, if we write down our old friend, a basic grammar for the lambda calculus we have

Mention . LambdaTerm ::= Ident ;
Abstraction . LambdaTerm ::= "lambda" Ident* "." LambdaTerm ;
Application . LambdaTerm ::= LambdaTerm "(" LambdaTerm* ")" ;

this would result in

trait LambdaTerm

case class Mention( i : [| Ident |] ) extends LambdaTerm
case class Abstraction( fmls : List[Ident], body : LambdaTerm ) extends LambdaTerm
case class Application( op : LambdaTerm, actls : List[LambdaTerm] ) extends LambdaTerm

The correspondence to type construction in a language that supports a purer functional style such as Haskell, or even OCaml is even clearer. (The reader is encourage to compare the Haskell type definition (sub)language to LBNF. The main difference lies in type parameterization. i submit that this would be an excellent addition to the idea of grammars and language processing.) The crucial point, though, is that because type representation in an actual computer must effectively be symbolic, aka syntactic, grammars are simply an alternative mechanism for specifying type structure, and -- at least in the case of Scala -- they can constitute a significantly more compact notation (and have the side-effect of producing a parser!). Indeed, this is why many, many, many computer science papers use a grammar-like style for specifying abstract syntax as a way of representing type structure or domain models.

It is worth pointing out that though this understanding is common wisdom in computer science it is not common wisdom in either mainstream programming or in mainstream mathematics. In fact, it is not even common wisdom in branches and subcultures of mainstream mathematics in which Category Theory is a principal tool. For example, when i was presenting some results at GroupoidFest 2008 i made an assumption that my audience -- who were for the most part quite facile with Category Theory -- would understand the use of such a notation as a means of specifying algebraic structure -- as i've noted above, a very common practice in theoretical computer science papers. Sadly, my audience did not understand this use of notation. Indeed, it is very sad to me that these excellent and brilliant practitioners do not have the benefits of these tools because they allow for a highly structured and elegant presentation of a range of algebraic structures that are of significant interest.

So, the modern programmer should recognize that she is on much the same footing as the mainstream mathematician when it comes to acquiring this tool set.