# Mildly dependently-typed metalanguage for mildly context-sensitive object languages

This is almost certainly not a new idea, but I haven't seen it elaborated or discussed elsewhere. A very natural way to represent the abstract syntax of an object language in a typeful metalanguage is to define:

• A metalanguage equality type for every nonterminal in the object language's grammar.
• A metalanguage constructor for every production rule in the object language's grammar.

There is a direct and obvious correspondence between the expressive power of the metalanguage's type system and the classes of syntactic structures that can be represented accurately in it. For example:

• Algebraic data types (possibly recursive finite sums of finite products, as in ML, but without function types or reference cells) represent exactly the class of context-free grammars.
• Inductive type families can represent unrestricted grammars.

In formal language theory, there exist several classes strictly between context-free and unrestricted grammars. For example, in increasing order of expressive power:

• For every one of these classes, what kind of type system allows us to describe exactly the grammars that belong to it, and no others? For indexed grammars, I suspect the answer is something like “GADTs parameterized by SML-like eqtypes promoted to GHC-like DataKinds”, but what about the others?