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:
- Tree-adjoining grammars
- 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?