<p>Some would say type theory is fundamental to programming.
A programming language implementation typically expresses a single type theory through its type system.</p>
<p>Are there any specific features a language can provide to support expressing a type theory directly or to help implement a type checker or some other useful aspect of a type system?</p>
<p>For example you might provide a unification operator and logic primitves to implement Hindley-Milner.</p>
<p>How does a particular set of features limit or enhance you ability to express different kinds of type system?</p>
<p>Note: I am more interested in the semantics of these features than in any given syntax.
The semantics can be expressed informally. Suggestions on how they might be implemented are welcome but not required.
If you want to express the semantics formally please try to also include a less formal explanation (something like <a href="https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html" rel="nofollow noreferrer">https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html</a> or just think &quot;explain like I'm 5&quot;)</p>

<type-checker><type-theory>
How can we express type theory in a programming language?
CC BY-SA 4.0
2023-06-26T02:49:46.307Z
Explain like I'm a 5 year old coder?
Seggan
<p>Supporting this or that specific algorithm or feature (unification, &quot;logic primitives&quot; – whatever that is) that is used in a typical proof assistant is just a minor convenience. It's quite unlikely it would provide it precisely in the form needed, so you'd end up implementing your own anyhow.</p>
<p>To my mind, a more relevant question is how the <em>design</em> of a language can support type theory in a deeper way. There has been quite a bit of research in this direction, which can hardly be summarized in an SE answer, so I just going to give you some pointers:</p>
<ol>
<li><p><a href="https://en.wikipedia.org/wiki/Logic_for_Computable_Functions" rel="noreferrer">LCF</a> was an early proof checker/assistant that seriously addressed the question of a programming meta-language. In fact, its meta-language was so successful that it spawned the entire family of ML langauges (Standard ML, OCaml, etc.) You can see a modern incarnation in <a href="https://isabelle.in.tum.de" rel="noreferrer">Isabelle</a> which relies on ML-style features quite heavily (parametric polymorphism, abstract data types, etc.) An interesting variant is <a href="http://cristal.inria.fr/%7Efpottier/alphaCaml/" rel="noreferrer">Cαml</a> which has built in support for variable binding.</p>
</li>
<li><p>There are specialized langauges based on logical frameworks, such as <a href="http://twelf.org/wiki/LF" rel="noreferrer">Twelf</a> and <a href="https://www.cs.mcgill.ca/%7Ecomplogic/beluga/" rel="noreferrer">Beluga</a>, while <a href="http://abella-prover.org" rel="noreferrer">Abella</a> is more in the tradition of logic programming languages.</p>
</li>
<li><p>Closer to my home, <a href="https://haselwarter.org" rel="noreferrer">Philipp Haselwarter</a> in his <a href="https://haselwarter.org/assets/pdfs/effective-metatheory-for-type-theory.pdf" rel="noreferrer">PhD thesis</a> studied how computational effects can support a proof assistant (in particular I refer you to Chapter 4 &quot;An effectful metalanguage for type theories&quot;). Some of his work was implemented in <a href="http://www.andromeda-prover.org" rel="noreferrer">Andromeda</a>.</p>
</li>
</ol>

CC BY-SA 4.0
2023-06-25T20:35:18.443Z
2023-06-25T20:35:18.443Z
Andrej Bauer
# How can we express type theory in a programming language?
Posted by: username_0 on 2023-06-25
Some would say type theory is fundamental to programming.
A programming language implementation typically expresses a single type theory through its type system.

Are there any specific features a language can provide to support expressing a type theory directly or to help implement a type checker or some other useful aspect of a type system?

For example you might provide a unification operator and logic primitves to implement Hindley-Milner.

How does a particular set of features limit or enhance you ability to express different kinds of type system?

Note: I am more interested in the semantics of these features than in any given syntax.
The semantics can be expressed informally. Suggestions on how they might be implemented are welcome but not required.
If you want to express the semantics formally please try to also include a less formal explanation (something like <https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html> or just think "explain like I'm 5")
**Tags:** type-checker type-theory
> **Comments:**
> **username_1**: Explain like I'm a 5 year old coder?  
---
## 1 answers
### Answer by username_2 on 2023-06-25. Score: 9
Supporting this or that specific algorithm or feature (unification, "logic primitives" – whatever that is) that is used in a typical proof assistant is just a minor convenience. It's quite unlikely it would provide it precisely in the form needed, so you'd end up implementing your own anyhow.

To my mind, a more relevant question is how the *design* of a language can support type theory in a deeper way. There has been quite a bit of research in this direction, which can hardly be summarized in an SE answer, so I just going to give you some pointers:

1. [LCF](https://en.wikipedia.org/wiki/Logic_for_Computable_Functions) was an early proof checker/assistant that seriously addressed the question of a programming meta-language. In fact, its meta-language was so successful that it spawned the entire family of ML langauges (Standard ML, OCaml, etc.) You can see a modern incarnation in [Isabelle](https://isabelle.in.tum.de) which relies on ML-style features quite heavily (parametric polymorphism, abstract data types, etc.) An interesting variant is [Cαml](http://cristal.inria.fr/%7Efpottier/alphaCaml/) which has built in support for variable binding.
2. There are specialized langauges based on logical frameworks, such as [Twelf](http://twelf.org/wiki/LF) and [Beluga](https://www.cs.mcgill.ca/%7Ecomplogic/beluga/), while [Abella](http://abella-prover.org) is more in the tradition of logic programming languages.
3. Closer to my home, [Philipp Haselwarter](https://haselwarter.org) in his [PhD thesis](https://haselwarter.org/assets/pdfs/effective-metatheory-for-type-theory.pdf) studied how computational effects can support a proof assistant (in particular I refer you to Chapter 4 "An effectful metalanguage for type theories"). Some of his work was implemented in [Andromeda](http://www.andromeda-prover.org).
---
