Wednesday, December 12, 2007

Two-level types, grammars and pretty encodings

i recently ran into a little ugliness in a Scala -- which i have been finding generally very pleasant. i can illustrate the problem in terms of so-called two-level types and how they can be used to interpret ebnf grammars.

Two-level types and grammars

The problem can be understood in the following context. Consider the following grammar.

An example

N0 ::= T0 | T1 N1 | T2 N1 N0 | T3 N0 N0
N1 ::= T4 N0

where Ti (0 <= i < 4) are understood to be terminals.

Using generics we can translate each production independently of the others. Like so:

[| N0 ::= T0 N1 | T1 N1 N0 | T2 N0 N0 |]
data N0 n1 = T0 n1 | T1 n1 (N0 n1) | T2 (N0 n1) (N0 n1) deriving (Eq, Show)

[| N1 ::= T3 N0 |]
data N1 n0 = T3 n0 deriving (Eq, Show)

Then, we can compose the types to get the recursive grammar.

data G = N0 (N1 G) deriving (Eq, Show) -- this is the line that seems to be problematic for the obvious translation to Scala

This approach has the apparent advantage of treating each production independently and yet being compositional.

The significance of our example

Now, let me de-obfuscate the grammar above. The first production should be very familiar.

Term ::= I | Var Name | Abstraction Name Term | Application Term Term

(Ignore the pesky 0-ary constructor, I. It's to get the grammar "off the ground", i.e. generating. It turns out to be quite interesting, but it's not germane to the discussion.) The generics-based translation of this grammar yields something we already know: we can use lots of different types to work as identifiers. This is something that the nominal notions of Gabbay, Pitts, et al, have factored out nicely.

The second production can be treated independently, but composes well with the first.

Name ::= Quote Term

This illustrates that a particularly interesting class of names is one that requires we look no further than our original (parametric) data type.

Related work

While i had the two-level type idea independently (and about the same time), these guys [1] clearly wrote it up first. To the best of my knowledge, i am the only one who seems to have seen the application to reflection.

[1] Tim Sheard and Emir Pasalic. 2004. Two-level types and
parameterized modules. Journal of Functional Programming

Appendix: how to do this in Scala

trait Terms {
type TName

sealed trait Term
case class Var(name : TName) extends Term
case class Abs(name : TName, v2 : Term) extends Term
case class App(fun : Term, arg : Term) extends Term

trait Names {
type TTerm

sealed trait Name
case class Quote(v : TTerm) extends Name

trait Grammar extends Terms with Names {
type TName = Name
type TTerm = Term

No comments: