# 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:

• Linear context-free rewriting systems
• Indexed grammars

So my questions are:

• 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?

• In computational linguistics, there has been research on “mildly context-sensitive grammars”, which (in theory) describe the context-sensitivity of natural languages, without running into the tractability issues of general context-sensitive (never mind unrestricted) grammars. In type theory, would it be equally viable to study “mildly dependently typed languages”, with the goal to describe the invariants that appear in real-world programs, without running into the usability issues of full-blown dependently typed languages? To what extent can we reuse the results already obtained by the formal languages and automata theory communities, in the design of type checkers for mildly dependently typed languages?

• IIUC, algebraic datatypes represent a strict superset of the class of context free grammars, because a constructor can carry elements of function type which don't seem to have any equivalent on the CFG side. – Stefan Jul 10 '16 at 0:09
• @Stefan: I see first-class functions as being orthogonal to algebraic data types. And I made it explicit that, by “algebraic data types”, I meant exclusively sums of products (of primitive types). – pyon Jul 10 '16 at 0:50