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
14(5):547-587.

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

}