Bidirectional Pure Type Systems
#Introduction
This are my notes, where I write things down to try to clarify my own thoughts. All the mistakes are my own.
I try to show show the rules for Pure Type Systems in a bidirectional type-checking style.
This post was motivated by me thinking why Conor McBride has sorts and function types as checkable types in his systems. For example look at I Got Plenty o’ Nuttin’ paper (definition 4 for syntax, and definition 17 for typing judgements in the linked version).
I present two variants of bidirectional pure type systems. In the first variant type formers are inferrable terms. It's slightly different then one used in Lambda Pi: A tutorial implementation of a dependently typed lambda calculus, and generalized to arbitrary (single sorted) PTS.
Type formers in the second system are checkable. This is requirement for cumulative universes, where types of types are not unique.
#Pure Type Systems
This is the review of Barendregt (Lambda calculi with types, 1992).
A Pure Type System (PTS) is a type system with following syntax
The type judgement of PTS is parameterized by a specification
- is a subset of constants, called sorts
- is a set of axioms in the form , with constant and
- is a set of rules of the form with .
Typical examples are simply typed lambda calculus (without products or sums),
or a predicative system with an infinite hierarchy of sorts (like in Agda), which some call :
Barendregt shows a lot of properties for pure type systems, One important result is that if PTS is single sorted:
in other words and are partial functions, then terms have unique types
A corollary of that property, is that beta-reduction preserves types.
and systems are single sorted.
Barendregt gives declarative typing judgements for the PTS. Here I omit writing context in every rule, and only show how contexts are extended. Reverse is used to lookup in the context.
#Bidirectional Systems
Bidirectional systems have two syntactical groups, which McBride calls terms and elimination. I choose to call them check terms and synth terms, as I find the name elimination somewhat misleading.
There are three groups of terms: there are introduction and elimination forms, but also type formations, because types appear in terms.
One valid approach is to divide introduction, elimination and type formers arbitrarily into check and synth terms, trying to minimize the need for the type-annotations.
Example: Booleans We know that and , thus introduction forms can be synth terms. In the boolean elimination (if expression) scrutinee have to be Boolean, so we can check that. As we don't know anything about the type of branches, we can decide to avoid type annotation for the result type and ask it to be provided.
Here I use the Conor's notation to make type judgments be "executable" in the clockwise order. is read as "check that has type ", and as "infer (or synthesize) a type of which will be ".
These are the rules you will find in David Christiansen tutorial.
As said, this is a valid design strategy.
Another approach is to take normal forms, which are divided into neutral and normal terms, and add double agent, cut as a type annotation construct to normal forms.
Frank Pfenning in his lectures talks about natural deduction and verifications (and sequent calculus and cut elimination. I haven't been in his class, but have watched his and Brigitte Pientka's OPLSS lectures on Proof Theory. The atomic proposition are allowed to meet
which is restricted version of conversion rule we will have. (Restricting to atomic propositions means that you need to -expand everything in normal forms). The opposite rule
is analogous to cut rule in sequent calculus, i.e. shows where the derivation can be simplified. This rule is admissible.
We can design bidirectional systems so the cut-rule has second purpose as type-annotation rule. This way, we know precisely where we need to perform reductions to normalize terms. As far as I understand, this is the design principle Conor McBride advocates for.
As a consequence, all introduction forms have to be checkable terms. This is natural for function abstraction (which is introduction form for function types), but feels less natural for "data". With these design principles, rules for Booleans are:
Now we cannot write
as is check term, but the scrutinee of if have to be synth term. If we want to write such redundant program, it have to be written as
Notice, as there is a type annotation, we know that expression can be reduced:
Exercises
Does if expression itself have to be checkable term, can't we have it as inferrable?
What problems will occur? Hint: Nest things.
This is an example why I don't think that calling inferrable terms eliminations is good idea. Some elimination forms have to be checkable.
The sum types, even Boolean, are however quite challenging.
#Bidirectional PTS
In this section I will describe a bidirectional pure type system. I have proved nothing about this system, but I have implemented it. I relies on PTS specification to be single sorted.
It is fun to instantiate the implementation to different specifications and see what is possible or not. A specific highlight is to see Hurkens Paradox to fail to type-check in one system, and fail to terminate in other.
Check and synth terms. We have the same five syntactical forms as previously, and two new ones to allow conversions between check and synth terms. Unlike McBride, type formation forms are synth terms. Also type in type annotation have to be synth term. Notice that lambda term don't have argument type annotation.
The typing rules are syntax directed, we have one rule for each syntactic form.
The rules are not showing the evaluation steps. We could write the rules in more explicit way
but I find it nicer to avoid these extra steps.
In these rules we rely on and to be (partial) functions. Otherwise the type-checking algorithm won't work.
The final missing bit is to specify the process. As already pointed out, one need to look for type annotations, and try to remove them.
If we forget the type of synth term, and then annotate it, this can be simplified. Also if you have checkable term which is annotated, but then coerced back can also be simplified:
Function beta-redexes are more complicated than what you are probably used to:
As function application is an inferrable, synth term, it have to reduce to a synth term, thus we annotate the result. In the substitutions, we cannot substitute just as variables are also synth terms, so we substitute annotated terms . But this all is a good thing. In function beta redex we replace big redex at big type, with smaller redexes at smaller types. Type annotations tell where redexes are.
You should be now be able to see how Lambda Pi paper is crucially relying on axiom of its system, and how relatively easy it is to "fix" by changing Star constructor to Star Natural to implement the system, for example.
#Internalizing Axiom and Rule, universe polymorphism
In as systems were and are (non-partial) functions, we can try to internalize them.
Internalizing means introducing them into the system itself, so they can be used from the inside. This way we can add universe polymorphism to the system. That is (almost) possible in but isn't in (not that it makes any sense to do so in the latter).
Agda does that, there are lsuc and _\sqcup_ functions on Levels.
We then can write universe polymorphic identity function
If we want to type-check the type of that term, we need to add an axiom to (it is so in Agda, Level : Set), then we'll need to synthesize the following:
That matches the product rule again, and we need to check that is a valid sort:
We can modify the axiom rule to match on this, and then we would need to make compute symbolically: .
Then we'll need to compute . What could it be?
Exercises
- Check what Agda returns for the type of universe polymorphic identity function. Hint:
C-c C-dinfers (deduces) type of the term. Types are terms. - Based on the previous answer, how do you think could be modified to support universe polymorphism (Answer to Agda's approach is on https://agda.readthedocs.io/en/latest/language/sort-system.html#agda-s-sort-system).
Another possible type to universe polymorphic identity function would be
If you have done the exercises, you know what the should be in the place of the question mark .
#Cumulatative universes
In the previous section we assumed that the system is single sorted. But what if it isn't. Instead of universe polymorphism we might want to have system with cumulative universes.
A rule we might want to have is
for some well founded ordering . If we do so, we are required to make all type formation terms to be checkable, as they don't know a sort they have as their type.
Because type formers are now checkable, also type annotation rule have to change.
and I don't exactly understand how this could work, as the level is not specified anywhere. There is some missing bit I cannot figure out.
My best understanding that Coq (and Idris?), for example, collect constraints which occur during the type-checking process, and then tries to solve them. Yet I don't know how (and when) that work is done. When is , figuring out whether a solution exists is not hard (essentially, you need to check that there are no loops in the graph, topological ordering will give you that, and a way to assign levels).
#Challenges with sums
Before I conclude, let me briefly mention problem with sums.
Consider a type
If types are checkable, and Boolean-elimination is checkable or if types are inferrable and Boolean-elimination is inferrable, the above type type-checks.
If types are checkable, and eliminations are inferrable, like in Conor system, we need to add a conversion
to make the term to type check.
In the last case, when types are inferrable, but Boolean elimination is checkable, we have to annotate the type of if expression.
Here we have an annotation. This is problematic.
In the meantime, consider nested if expressions
If Boolean elimination is inferrable, then this is normal form. If it isn't, we have to add type annotation
And this can be reduced with case-of-case transformation to
Similarly, we can "reduce' a type example to
From this point of view, we can try to check the in and have checkable Boolean elimination.
In cumulative universes system, we can probably check with . This variant is new to me, and I haven't tried to implement it.
We will run into similar problem if we add dependent sum, i.e. types. (I use instead of and therefore will use instead of ). If we use projections as eliminators, we will avoid problems as these eliminations can (should) be inferrable:
But if we will add match (or split or case) elimination rule, it will be the same problem, as with Booleans.
#Conclusion
I see the niceties of cumulative universes (in Coq you just write Type), especially compared to uglyness of universe polymorphism details business in Agda (see link in exercises).
I think that the bidirectional PTS I presented, with inferrable type formers, is simpler system and is good basis for considering extensions. However there are problems with finite sets (like Boolean) and dependendent sums.
- 2024-04-18 – What makes a good compiler warning?
- 2024-04-12 – Core Inspection
- 2024-04-01 – Implicit arguments
- 2024-03-17 – ST with an early exit
- 2024-02-27 – More QualifiedDo examples
This work is licensed under a “CC BY SA 4.0” license.