I’ll give it a try. The main idea is to treat a programming language not based on its advertised type system, but on its actual computational rules. Because all programming languages must have such rules, the derived type theory must be a valid logic for reasoning about the behavior of programs, even if the language is traditionally considered untyped.
For example, let’s take a snippet of Python 3.
x = 1; x + 2
This snippet is closed; it doesn’t refer to any outer names. By the rules of Python, we could remove the first statement and put x into an outer scope with the primitive value 1 already assigned. So, assuming that x = 1 already, we have:
x + 2
Now, again by the rules of Python, we can substitute 1 for x in our snippet, rewriting the syntax:
1 + 2
This might seem like ordinary big-step semantics. But we also inherit type information from the term constructors of the language. For Python 3, we know that 1 is not just a value, but has a type int of integers. This applies to operators, too; we know that if x and y are of type int, then so is x + y. Or, in a phrasing closer to type theory:
x :int, y :int |- x + y :int
The paper’s main contribution is a seamless synthesis of these two ways of approaching the behaviors of programming languages.
Also see the comment (use case) from Mike Stay: https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html#c059431
This looks interesting, but it’s a bit beyond me. Any chance we could get a slightly dumbed-down explanation, with a bit less category theory jargon?
I’ll give it a try. The main idea is to treat a programming language not based on its advertised type system, but on its actual computational rules. Because all programming languages must have such rules, the derived type theory must be a valid logic for reasoning about the behavior of programs, even if the language is traditionally considered untyped.
For example, let’s take a snippet of Python 3.
This snippet is closed; it doesn’t refer to any outer names. By the rules of Python, we could remove the first statement and put
xinto an outer scope with the primitive value1already assigned. So, assuming thatx = 1already, we have:Now, again by the rules of Python, we can substitute
1forxin our snippet, rewriting the syntax:This might seem like ordinary big-step semantics. But we also inherit type information from the term constructors of the language. For Python 3, we know that
1is not just a value, but has a typeintof integers. This applies to operators, too; we know that ifxandyare of typeint, then so isx + y. Or, in a phrasing closer to type theory:The paper’s main contribution is a seamless synthesis of these two ways of approaching the behaviors of programming languages.