<p>It's well-known that a formal grammar (a formal description of a language's syntax) can be used to programmatically generate a parser (an algorithm which analyses that syntax); tools which do this are called &quot;parser generators&quot; or &quot;<a href="https://en.wikipedia.org/wiki/Compiler-compiler" rel="noreferrer">compiler-compilers</a>&quot;. A parser generator may impose some constraints on the grammars it accepts (e.g. no left-recursion).</p>
<p>To what extent can the same be done for type systems? That is, given a formal description of a language's typing rules, is it practical to programmatically generate a type-checking algorithm, or a type-inference algorithm? If so, does this require any constraints on the type systems that the type-checker-generator accepts?</p>
<p>There are some academic publications on the topic of type-checker-generators, but I am interested to know if such generators are or would be useful in practice; or if they are only of academic interest, why?</p>
<ul>
<li><a href="https://www.semanticscholar.org/paper/A-generator-for-type-checkers-Gast/a91e189079a8ec0ac22cc944c2cbcd567caa2c26" rel="noreferrer"><em>A generator for type checkers</em></a>, Holger Gast, 2004 (thesis)</li>
<li><a href="https://2018.splashcon.org/details/splash-2018-Posters/37/METACO-a-Type-Checker-Generator" rel="noreferrer"><em>METACO, a Type Checker Generator</em></a>, Haochen Xie, 2018 (poster presentation)</li>
<li><a href="https://digitalscholarship.unlv.edu/thesesdissertations/4579/" rel="noreferrer"><em>Jiapi: A Type Checker Generator for Statically Typed Languages</em></a>, Benjamin Cisneros Merino, 2022 (thesis)</li>
</ul>

<compilers><type-systems>
Can type-checking algorithms be practically generated from formal descriptions of type systems?
<h1>For general-purpose languages, probably not</h1>
<p>In theory, it is possible. In practice, it is currently essentially never done in “real” languages, for a set of related reasons.</p>
<h2>Formally defined type systems are almost always <em>models</em></h2>
<p>The primary purposes of typing rules, as they appear in programming languages papers, are twofold:</p>
<ol>
<li><p><strong>To serve as a communication tool for humans.</strong> They distill how the type system works down to its essence, which allows ideas and innovations to be shared without needing to read the source code for an industrial-strength typechecker.</p>
</li>
<li><p><strong>To formalize a system enough to prove things about it.</strong> Proving anything formally about a language is difficult enough as it is, so this necessarily optimizes for a certain simplicity and economy in the statement of the language and its rules.</p>
</li>
</ol>
<p>Both these goals incentivize formalizing <em>models</em> of languages rather than full languages. The model serves as an explanatory tool and a tool of thought for language implementors, but there is only an informal argument made that the model adequately captures the complexity of the real thing.</p>
<h2>Implementations have practical concerns not handled well by formal specifications</h2>
<p>Real implementations of typecheckers care about many things that most formal models do not, such as providing quality error diagnostics, handling real programs efficiently, and supporting incremental recompilation. Many of these concerns are essentially programming concerns, and they can easily result in a typechecker that takes tens of thousands of lines of code.</p>
<p>Some of this massive expansion in verbosity is due to the relative concision of formal type system notation, but plenty of it is inherent in the fact that real implementations just do more stuff. Since those things are intentionally left absent from models, the formal notation is not optimized for expressing them, and extending the notation to be able to support it would be a serious language design undertaking in and of itself.</p>
<h2>The “PL notation metalanguage” is itself an open language</h2>
<p>Parser generators have the benefit of well-understood classes of grammars with well-understood properties, such as LR(1) and LL(k), which can be expressed in well-known ways. In contrast, the notation of type systems is not nearly so fixed, and although the <em>foundations</em> are shared between different presentations, it is extremely common to extend the notation as needed to most usefully model a given language.</p>
<p>For this reason, even ignoring the practical concerns not captured by the notation, developing a system to mechanize typing rules in the first place is more difficult than you might think! <a href="https://www.youtube.com/watch?v=7HKbjYqqPPQ" rel="noreferrer">Guy Steele’s 2017 talk “It’s Time for a New Old Language”</a> discusses some of this dramatic variation, and it can provide some perspective on just how challenging this problem is. It can also be quite illuminating to work within a system explicitly designed to mechanize PL notation, such as <a href="https://docs.racket-lang.org/redex/" rel="noreferrer">PLT Redex</a>—you may find that mechanizing many of the type systems you find in the wild is substantially more challenging you’d expect.</p>
<p>One way to think about this is that the role of mathematical notation in many papers is essentially to define a bespoke domain-specific language <em>specifically for the purpose</em> of expressing the concepts in the paper. Obviously, if the entire notation were bespoke, this would not be very useful, but the shared foundation provides a common vocabulary that allows researchers to add extensions as necessary to best communicate their ideas. Of course, one can easily make the case that some of these notational innovations are more successful (and perhaps more necessary) than others, but the fact remains that it is done, and this poses an obstacle to mechanization.</p>
<h2>Reuse in type systems is surprisingly hard</h2>
<p>Type systems are fundamentally “global” analyses. In order for a type system to usefully function, it must guarantee a lengthy set of invariants <em>everywhere</em>. How exactly this is done can vary substantially depending on the features the type system supports, and often the very structure of the system is designed around supporting a particular feature.</p>
<p>For this reason, two type systems that share a feature from a user’s point of view cannot necessarily implement that feature in the same way. Every feature of a type system interacts to some degree with other features of the type system, and those interactions may need to be handled explicitly on a case-by-case basis. This requirement means that the algorithms and data structures used to implement type systems are often tailored to each individual implementation, from the representation of syntax to the strategy used to implement constraint solvers.</p>
<p>In models, these things can often be handwaved to some degree. Lots of type system papers don’t even discuss the algorithmic details of constraint solving at all, and in some cases, the systems are even <em>parameterized over</em> the choice of constraint solver! But in a real system, all of these things must be implemented carefully and precisely, and this requires weighing the language’s individual requirements and designing something with them in mind.</p>
<h1>Type system generators could be useful for DSLs</h1>
<p><a href="https://en.wikipedia.org/wiki/Domain-specific_language" rel="noreferrer">Domain-specific languages</a> are something of a darling idea within much of the PL community, and reducing the amount of effort it takes to produce them is a subject of a great deal of active research. Though the results of this research are still not used in practice particularly often, so-called <a href="https://en.wikipedia.org/wiki/Language_workbench" rel="noreferrer">language workbenches</a> continue to mature.</p>
<p>In projects like <a href="https://docs.racket-lang.org/turnstile/index.html" rel="noreferrer">Turnstile</a>, typing rules are mechanized using a notation that very closely resembles standard PL notation, and the tool is intended to be useful for practical DSL engineering. In other systems, like <a href="https://www.jetbrains.com/help/mps/typesystem.html" rel="noreferrer">JetBrains MPS</a> and <a href="https://spoofax.dev/references/statix/rules/" rel="noreferrer">Spoofax</a>, the notation is quite different, but many of the same concepts are represented in some way.</p>
<p>These systems are still relatively young, and the design space is rather vast, so it remains to be seen how much adoption they will receive. Still, they do demonstrate that “type system generators” almost certainly do have a practical niche, even if they never end up being used for the implementations of type systems in general-purpose languages. And given enough time, who knows? Maybe someday they will develop to the point that even general-purpose languages’ type systems can be implemented that way. But that future, if it exists, seems like probably a distant one.</p>

CC BY-SA 4.0
2023-08-15T16:12:13.230Z
2023-08-15T16:12:13.230Z
Alexis King
CC BY-SA 4.0
2023-08-29T20:04:57.470Z
One could argue this is also not done for grammars, but it does seem more feasible.
cody
# Can type-checking algorithms be practically generated from formal descriptions of type systems?
Posted by: username_0 on 2023-08-15
It's well-known that a formal grammar (a formal description of a language's syntax) can be used to programmatically generate a parser (an algorithm which analyses that syntax); tools which do this are called "parser generators" or "[compiler-compilers](https://en.wikipedia.org/wiki/Compiler-compiler)". A parser generator may impose some constraints on the grammars it accepts (e.g. no left-recursion).

To what extent can the same be done for type systems? That is, given a formal description of a language's typing rules, is it practical to programmatically generate a type-checking algorithm, or a type-inference algorithm? If so, does this require any constraints on the type systems that the type-checker-generator accepts?

There are some academic publications on the topic of type-checker-generators, but I am interested to know if such generators are or would be useful in practice; or if they are only of academic interest, why?

* [*A generator for type checkers*](https://www.semanticscholar.org/paper/A-generator-for-type-checkers-Gast/a91e189079a8ec0ac22cc944c2cbcd567caa2c26), Holger Gast, 2004 (thesis)
* [*METACO, a Type Checker Generator*](https://2018.splashcon.org/details/splash-2018-Posters/37/METACO-a-Type-Checker-Generator), Haochen Xie, 2018 (poster presentation)
* [*Jiapi: A Type Checker Generator for Statically Typed Languages*](https://digitalscholarship.unlv.edu/thesesdissertations/4579/), Benjamin Cisneros Merino, 2022 (thesis)
**Tags:** compilers type-systems
---
## 1 answers
### Answer by username_1 on 2023-08-15. Score: 9 | Accepted answer
# For general-purpose languages, probably not

In theory, it is possible. In practice, it is currently essentially never done in “real” languages, for a set of related reasons.

## Formally defined type systems are almost always *models*

The primary purposes of typing rules, as they appear in programming languages papers, are twofold:

1. **To serve as a communication tool for humans.** They distill how the type system works down to its essence, which allows ideas and innovations to be shared without needing to read the source code for an industrial-strength typechecker.
2. **To formalize a system enough to prove things about it.** Proving anything formally about a language is difficult enough as it is, so this necessarily optimizes for a certain simplicity and economy in the statement of the language and its rules.

Both these goals incentivize formalizing *models* of languages rather than full languages. The model serves as an explanatory tool and a tool of thought for language implementors, but there is only an informal argument made that the model adequately captures the complexity of the real thing.

## Implementations have practical concerns not handled well by formal specifications

Real implementations of typecheckers care about many things that most formal models do not, such as providing quality error diagnostics, handling real programs efficiently, and supporting incremental recompilation. Many of these concerns are essentially programming concerns, and they can easily result in a typechecker that takes tens of thousands of lines of code.

Some of this massive expansion in verbosity is due to the relative concision of formal type system notation, but plenty of it is inherent in the fact that real implementations just do more stuff. Since those things are intentionally left absent from models, the formal notation is not optimized for expressing them, and extending the notation to be able to support it would be a serious language design undertaking in and of itself.

## The “PL notation metalanguage” is itself an open language

Parser generators have the benefit of well-understood classes of grammars with well-understood properties, such as LR(1) and LL(k), which can be expressed in well-known ways. In contrast, the notation of type systems is not nearly so fixed, and although the *foundations* are shared between different presentations, it is extremely common to extend the notation as needed to most usefully model a given language.

For this reason, even ignoring the practical concerns not captured by the notation, developing a system to mechanize typing rules in the first place is more difficult than you might think! [Guy Steele’s 2017 talk “It’s Time for a New Old Language”](https://www.youtube.com/watch?v=7HKbjYqqPPQ) discusses some of this dramatic variation, and it can provide some perspective on just how challenging this problem is. It can also be quite illuminating to work within a system explicitly designed to mechanize PL notation, such as [PLT Redex](https://docs.racket-lang.org/redex/)—you may find that mechanizing many of the type systems you find in the wild is substantially more challenging you’d expect.

One way to think about this is that the role of mathematical notation in many papers is essentially to define a bespoke domain-specific language *specifically for the purpose* of expressing the concepts in the paper. Obviously, if the entire notation were bespoke, this would not be very useful, but the shared foundation provides a common vocabulary that allows researchers to add extensions as necessary to best communicate their ideas. Of course, one can easily make the case that some of these notational innovations are more successful (and perhaps more necessary) than others, but the fact remains that it is done, and this poses an obstacle to mechanization.

## Reuse in type systems is surprisingly hard

Type systems are fundamentally “global” analyses. In order for a type system to usefully function, it must guarantee a lengthy set of invariants *everywhere*. How exactly this is done can vary substantially depending on the features the type system supports, and often the very structure of the system is designed around supporting a particular feature.

For this reason, two type systems that share a feature from a user’s point of view cannot necessarily implement that feature in the same way. Every feature of a type system interacts to some degree with other features of the type system, and those interactions may need to be handled explicitly on a case-by-case basis. This requirement means that the algorithms and data structures used to implement type systems are often tailored to each individual implementation, from the representation of syntax to the strategy used to implement constraint solvers.

In models, these things can often be handwaved to some degree. Lots of type system papers don’t even discuss the algorithmic details of constraint solving at all, and in some cases, the systems are even *parameterized over* the choice of constraint solver! But in a real system, all of these things must be implemented carefully and precisely, and this requires weighing the language’s individual requirements and designing something with them in mind.

# Type system generators could be useful for DSLs

[Domain-specific languages](https://en.wikipedia.org/wiki/Domain-specific_language) are something of a darling idea within much of the PL community, and reducing the amount of effort it takes to produce them is a subject of a great deal of active research. Though the results of this research are still not used in practice particularly often, so-called [language workbenches](https://en.wikipedia.org/wiki/Language_workbench) continue to mature.

In projects like [Turnstile](https://docs.racket-lang.org/turnstile/index.html), typing rules are mechanized using a notation that very closely resembles standard PL notation, and the tool is intended to be useful for practical DSL engineering. In other systems, like [JetBrains MPS](https://www.jetbrains.com/help/mps/typesystem.html) and [Spoofax](https://spoofax.dev/references/statix/rules/), the notation is quite different, but many of the same concepts are represented in some way.

These systems are still relatively young, and the design space is rather vast, so it remains to be seen how much adoption they will receive. Still, they do demonstrate that “type system generators” almost certainly do have a practical niche, even if they never end up being used for the implementations of type systems in general-purpose languages. And given enough time, who knows? Maybe someday they will develop to the point that even general-purpose languages’ type systems can be implemented that way. But that future, if it exists, seems like probably a distant one.
> **Comments:**
> **username_2** (2023-08-29): One could argue this is also not done for grammars, but it does seem more feasible.  
---
