This post intends to promote self types as a safer, simpler, and faster alternative to inductive types and dependent pattern matching at the core of programming languages.
In summary, it should go through the problems that self types try to solve, the problems that they introduce, and then a concrete solution proposed at the end, with a syntax-directed, bidirectional type system with decidable checking.
SYNTAX at the Syntax section.
So I heard that you may want to build a dependently typed language. The path is usually quite straightforward.
You usually start with a PTS like the Predicative Calculus of Constructions, whose rules look something like this.
Then you add dependent pattern matching, whose rules usually look something like this.
And that gets you all the way there. And don't you dare forget about the "guard condition".
The goal of adding dependent pattern matching is to get inductive types in the language which is effectively a requirement for anything where you would like to prove non-trivial theorems like forall n, n + 0 == n.
And while we call them inductive types, they describe effectively any ADT with the equivalent "induction principle". This includes many nice things like pairs and equalities.
// a dependent pair, also known as a module
data Sigma(A : Type, B : (a : A) -> Type) : Type =
| exist(a : A, b : B(a));
// the identity type, aka x is equal to y
data Id(A : Type, x : A, y : A) : Type =
| refl(x : A);
// but also the booleans
data Bool : Type =
| true
| false;
// and the natural numbers
data Nat : Type =
| zero
| succ(n : Nat);Additionally, inductive types cannot be "encoded" using functions, like we can usually do in non-dependent type theory, here it does requires additional properties. Meaning that it is usually assumed that you cannot avoid adding inductive types to the language.
In practice, implementing it is not even much harder, but it is clearly not what most people would describe as elegant.
Usually it also requires adding recursion to the language, this is done in a safe way, but it's still a bit of a pain and an another annoying feature to implement, the "guard condition" in the above image is written in English for a reason.
It also does not compose well. For example, it needs to be extended further to include quotient types and higher inductive types. And due to a common property called large elimination, it also increases the computational power of the system.
A naive solution is to remove dependent pattern matching by decomposing it a bit further, for example by adding Recursion + Sigma + Bool + Identity. This makes the guard condition a bit more annoying, but it does work. Potentially, even just Recursion + Sigma is enough, if that recursion allows you to describe "codata types".
A less naive decomposition was recently proven by Eduardo Rafael at Nat by J (yes, this is me; I'm still happy), it shows that given a powerful enough universe (like CoC), Sigma (with_eta) + Identity is enough to encode all inductive types. As far as I know, this is the simplest approach that preserves the computational content while still providing useful inductive types.
A similar and simpler encoding is possible by adding {axiom K,UIP} to the system, but those are not compatible with univalence and feel out of place. While it works, it is not especially nice, and it is not possible in a predicative type theory without adding an impredicative identity type, which is a common choice nowadays. The specific encoding above is also very slow.
A common advantage of a PTS, like System F and the Calculus of Constructions, is that they have a single way of computing, this is inherited from the untyped lambda calculus.
This is desirable because usually functions are universal and well-behaved, we use them for everything and we know how they work, meaning that if you need to think about something weird, you can think about it in terms of functions.
But in dependent type theories this is usually not enough. For example, it is known that you can describe the natural numbers using Church encodings, a way of describing data using only functions.
Bool = (C : Type, t : C, f : C) -> C;
Nat = (C : Type, z : C, s : (acc : C) -> C) -> C;Given that, it is weird that we're needing to add things like recursion to those systems, well, as shown by the above result, it is not truly needed, but there is still a problem, large elimination.
There is a problem when we stop using Type : Type, there is no way for a term in a lower universe, to branch on a term of a higher universe, this can be seen below.
Unit = (C : Type, r : C) -> C;
Bool = (C : Type, t : C, f : C) -> C;
// as in, if the boolean is true, x : Unit, if it's false, x : Bool
f = (b : Bool, x : b(Type, Unit, Bool)) => _;
// if we go with Set : Type, like the CoC
Unit : Set = (C : Set, r : C) -> C;
Bool : Set = (C : Set, t : C, f : C) -> C;
// this fails because, b(Set, _, _) is invalid
f = (b : Bool, x : b(Set, Unit, Bool)) => _;While Type : Type is really nice, it allows for paradoxes and does not lead to a logically consistent system without further restrictions.
While in impredicative type theory (like System F), we can work around it in many ways, this is not the case in predicative type theory (like Agda), where it cannot even be reliably simulated.
So inductive types come with a special property, eliminating from a universe to a "larger" universe, where you can have Bool : Set and still somehow branch on the type-level, this is known to work and be safe, but it's clearly adding something more in the system.
data Unit : Set = | unit;
data Bool : Set = | true | false;
// this works, even though b is producing something higher
f = (b : Bool, x : b ? Unit : Bool) => _;I do not attempt to propose an alternative to large elimination here. For the rest of the article, I will assume Type : Type as I consider these features orthogonal and best studied independently. I do propose some alternatives at the end tho.
Also maybe a better name would be "strong elimination", but I don't know if that is a common name.
The main issue is that any attempt seems to run into very dependent types, which are "subject-dependent": the type of a term depends on the term itself, and we lack the primitives to construct such types. I will argue that this is not an issue and that most dependent type theories already have them.
A naive attempt to apply the same technique that works for deriving Church encodings of non-dependent types fails.
// internalizing works for non-dependent eliminators
fold(n : Nat) : (C : Type, z : C, s : (acc : C) -> C) -> C;
Nat = (C : Type, z : C, s : (acc : C) -> C) -> C;
// fails for dependent eliminators, even unit lol
ind(u : Unit) : (C : (u : Unit) -> Type, r : C(unit)) -> C(u);
// at least inductive-recursion, but what about the u?
Unit = (C : (u : Unit) -> Type, r : C(unit)) -> C(u???);A similar problem also appears when trying to CPS-transform type theories with sigma types. In fact, it is known to be impossible without adding further primitives, as shown in Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible. Self types also solve this.
Anyway, given those problems, here I will be trying to show that dependent fixpoints, described by self types, are a better alternative, but first:
They are types that depend on the terms they themselves describe. This is often the case with mutual recursion; simple examples can be seen in inductive-recursive types.
A : Type;
x : A;
A = (C : (a : A) -> Type, r : C(x)) -> C(x);
x = (C, r) => r;
// the type of x is
(C, r) => r : (C : _, r : C(x)) -> C(x)
// which if you expand the x once
(C, r) => r : (C : _, r : C((C, r) => r)) -> C(x)
// so the type of the term includes the termWhile those may look like exotic types, they kind of appear everywhere recursive and inductive types are involved, like in the Church-encoding failure above.
Additionally, people accept inductive types. My intuition for why that is the case is simply that they are usually hidden: the actual inductive type is opaque, so we can only see it happening at elimination.
// even simple sigma types and identity types are subject-dependent
// M appears in it's own elimination
(M : sig(a : A) -> B).1 : B{a := M.0};
// M also appears in it's own elimination
(M : x == y).J : (C, r : C(refl(), x)) -> C(M, y);
// it's always something like the following
f(M : A) : B{x := M};We also know that it is possible to encode such types for all inductive types in the presence of Sigma and Identity. Potentially, it is even possible to encode all such types in the presence of {axiom K,UIP}.
Many years ago, Peng Fu and Aaron Stump proposed a type system that could encode inductive types using lambdas: Self Types for Dependently Typed Lambda Encodings. It did this by adding a type former for describing {subject,self}-dependent types, which they named Self Types.
This system was presented in Curry style and relied on hiding some infinite types in an implicit forall. Additionally, it was not syntax-directed, meaning that it is not clear how to implement it, and it did not appear to have decidable equality. However, termination and logical consistency were proven.
But the system provided us with an amazing primitive, theoretically much more elegant than dependent pattern matching, which could naturally describe all inductive types and after type erasure, it was just the untyped lambda calculus.
Naively, Self Types can be characterized by their eliminator. This is the workhorse and, in a certain way, what makes them self types.
Γ |- M : self(x) -> T
---------------------
Γ |- M.@ : T{x := M}Additionally, self types do not only allow for self-dependent types, but also unlock the possibility to quantify over all of them.
// I'm skipping MANY details here
true : (C, t : C(true), f : C(false)) -> C(true);
false : (C, t : C(true), f : C(false)) -> C(false);
Bool = self(b) -> (C, t : C(true), f : C(false)) -> C(b);This line of work was mostly discontinued by Stump, who switched to a dependent intersection approach that, for his purposes, seems better behaved. That project eventually led to the Cedille language.
Sadly, dependent intersections still rely on a Curry-style system, and they lead to a system where axiom K is provable. Again, this is not compatible with univalence, but it is still a very interesting line of work.
C_Eq(A, x, y) = (C : (a : A) -> Type, r : C(x)) -> C(y);
c_refl(A, x) : C_Eq(A, x, x) = (C, r) => r;
Eq(A, x, y) = (s : C_Eq(x, x)) & C_Eq(x, y) & C_Eq(_, s, c_refl(A, x));
// then when x is judgementally equal to y
K(A, x, eq) : C_Eq(_, eq, c_refl(A, x)) = eq.1;Given those shortcomings, people started working on many variants, notably Victor Taelin. Then, a couple of years later, when I started working on my own dependently typed language, I quickly stumbled on the same problem and decided to make my own attempts.
At some point, I arrived at a simple insight: the natural way to make it a Church-style system seems to be making the self type the type of the fixpoint. This is very intuitive, and many people arrived at this before me. You can verify this by simply trying to type a fixpoint in a dependent type theory, fix(x) : T => K. Ideally, you would want T to mention x; that would make it a dependently typed fixpoint.
But I did mention that fixpoints are bad, and yes, they are still the annoying bit of this proposal. However, those fixpoints are completely positive and erasable, meaning that while they enable induction, they do not extend the computational content of the system, even in a predicative type theory.
While this naively works, it still suffers from a major issue: while typing both the self and the fix, you need to assume that both are well typed. Even worse, inside the fixpoint, the fix case knows that it is the fixpoint itself.
Nonetheless, this system is still quite well behaved, potentially compatible with univalence, and perhaps even decidably type-checkable. It is especially elegant if you rely on unification for it.
// to type it, you need to assume that it is typed
Γ, a : self(a) -> T |- T : Type
-------------------------------
Γ |- self(a) -> T : Type
// usually you only add valid types to the context
// as in, the following would lead to cyclical derivations
Γ is Context Γ |- A : Type
---------------------------
(Γ, a : A) is Context
// you even need to use the fixpoint during equality check
Γ, (a : self(a) -> T) == (fix(a) => K) |- K : T
-----------------------------------------------
Γ |- fix(a) => K : self(a) -> T
// examples
Unit = fix(Unit) =>
// to type this, you need to expand both the Unit and the u
unit : Unit = fix(u) => (C, r) => r;
self(u) -> (C : (r : Unit) -> Type, r : C(unit)) -> C(u);The issue with the self type itself can be solved by requiring that the self type be under a fixpoint, so that there is a type describing the variable's type. This is a bit weird because, to type a fixpoint, you may need a self type; however, this does not solve the problem of eliminating the strong fixpoint, where it internally needs to expand.
Γ |- A : Type Γ, a : A |- B : Type
Γ |- A == self(x : A) -> B // this equality is okay
---------------------------------------------------
Γ |- self(a : A) -> B : Type
Γ, (a : A) == (fix(a) => K) |- K : B
------------------------------------
Γ |- fix(a) => K : self(a : A) -> B
// this example still works
Unit = fix(Unit) : Type =>
unit : Unit = fix(u) => (C, r) => r;
self(u : Unit) -> (C : (r : Unit) -> Type, r : C(unit)) -> C(u);You can see the system fully defined in the SYSTEM: Declarative Self Types.
But for a good foundational core, that is still not enough. It likely does not have decidable type checking, would require cyclical derivations, and uses untyped equality. While those properties could be accepted, we are looking for a better approach.
The approach below still mostly follows the idea that, to type a self type, you need something that allows you to reference the whole self type somehow. In particular, it extends the inference rules so that it carries a way of referencing itself.
// note that while typing B, there is no known self
Γ, a : A |- B : Type
--------------------------------
Γ | A |- self(a : A) -> B : Type
// this rule has some problems, try making Unit
Γ, a : A | a |- K ⇐ B
-----------------------------------
Γ |- fix(a) => K ⇐ self(a : A) -> B
// this is almost enough, it works for False
fix(False) : Type => self(f : False) ->
(C : (f : False) -> Type) -> C(f);
// note that this works with mutual recursion
Unit : Type;
unit : Unit;
Unit = self(u) -> (C, r : C(unit)) -> C(u);
// this technically fails, but I will explain later
unit = fix(u) => (C, r) => r;
// also works if you have pair that propagates self
Γ | S.0 |- M.0 ⇐ A Γ, S.0 == M | S.1 |- N ⇐ B
----------------------------------------------
Γ | S |- [M, N] ⇐ sig(a : A) -> B
P : sig(Unit : Type) -> Unit;
P = [
self(u) -> (C : (u : Unit) -> Type, r : C(P.1)) -> C(u),
// same issue, the fix needs to propagate through the self
fix(u) => (C, r) => r
];While this works, it requires adding either mutual recursion or pairs. Traditionally, the former is a major source of PAIN, and while the latter is well behaved, it is unfortunate that we need it as in the original system, where it could have been derived.
But the core idea is sound: propagate the self and update it after things finish typing. This can be done in more complete forms, but the main remaining issue is that we need to propagate through application or through a let to get it to type nicely.
// propagate through the fix
Γ, (a : A) == S | a |- K ⇐ B
---------------------------------------
Γ | S |- fix(a) => K ⇐ self(a : A) -> B
// this is okay because the S should always be a neutral
Γ |- M ⇒ (a : A) -> B Γ, a : A, S == M(a) | a |- N ⇐ A
-------------------------------------------------------
Γ | S |- M(N) ⇒ B{a := N}
// then you can do
fix(Unit) : Type =>
((unit : Unit) => self(u) -> (C, r : C(unit)) -> C(u))(
fix(u) => (C, r) => r);
// it is also nice to have another type of let
Γ, a : A |- K ⇒ B Γ, a : A, S == K | a |- N ⇐ A
------------------------------------------------
Γ | S |- a : A = N; K : B{a := N}
// or in a nicer syntax
fix(Unit) : Type =>
// this let is checked after the body finishes
unit : Unit = fix(u) => (C, r) => r;
self(u) -> (C , r : C(unit)) -> C(u);You can see the system fully defined in the SYSTEM: Bidirectional Self Types.
This system has the main properties we can hope for: it is Church-style, syntax-directed, and has decidable type checking. It is also very likely compatible with univalence and has a nice notion of equality.
But it lacks one property: it cannot directly "reify" normalized terms. We can always reify them by introducing the required additional lets. Alternatively, we can normalize modulo substitution so that the weird lets are preserved; this makes subject reduction especially annoying.
// cannot be typed
fix(Unit) : Type =>
self(u) -> (C , r : C(fix(u) => (C, r) => r)) -> C(u);
// introducing the let works, though
fix(Unit) : Type =>
unit : Unit = fix(u) => (C, r) => r;
self(u) -> (C , r : C(unit)) -> C(u);There is also a weird, partially related issue: there is no elegant way to construct a self type, because you need a self to create a fix and a fix to create a self. This is resolved in a slightly non-elegant way: the rule produces a self type during checking without a self, so all non-dependent self types get a fresh variable as their type.
// what is the type of x?
self(x) -> TypeOn the other hand, this does work in practice, and these rules can be managed in many ways. It still gives a syntax-directed bidirectional type system that supports NbE, and I believe it to be compatible with univalence.
I hope that, by checking the system at SYSTEM: Bidirectional Self Types, I was able to convince you that self types are not only nice to have, but are in fact simpler than the alternatives and hopefully better behaved.
Additionally, I showcase some of the additional power: extensionalities, additional inductive types, constructors that compute, and higher-inductive-recursive types, in the bonus section BONUS: Examples, also check BONUS: Free Mutual Recursion.
There are still many open problems. I do not yet have proofs for common properties of this system, but I believe they can be produced. The termination proof for CoC + Self Types, where the fix is allowed only in positive and erasable positions, still works, though. One central open question is: is it compatible with HoTT?
Additionally, there is the large elimination problem. While I believe these concerns are orthogonal, they need to be solved anyway. A naive approach that can work is an additional universe containing only simple types, which can be instantiated in any other universe; this seems to be folklore. I am also studying an approach with a {linear, affine, graded} universe at the "top" of a predicative tower, such that the top can safely be Type : Type.
----------------
Γ |- Type : Type
-----------------
Γ, a : A |- a : A
Γ |- A : Type Γ, a : A |- B : Type
-----------------------------------
Γ |- (a : A) -> B : Type
Γ, a : A |- K : B
----------------------------
Γ |- (a) => K : (a : A) -> B
Γ |- M : (a : A) -> B Γ |- N : A
---------------------------------
Γ |- M(N) : B{a := N}
Γ, a : self(a) -> T |- T : Type
-------------------------------
Γ |- self(a) -> T : Type
Γ, (a : self(a) -> T) == (fix(a) => K) |- K : T
-----------------------------------------------
Γ |- fix(a) => K : self(a) -> T
Γ |- M : self(a) -> T
---------------------
Γ |- M.@ : T{a := M}// format
Γ |- M ⇒ A // infer
Γ |- M ⇐ A // check
Γ | S |- M ⇒ A // infer-with-self
Γ | S |- M ⇐ A // check-with-self
// rules
----------------
Γ |- Type ⇒ Type
-----------------
Γ, a : A |- a ⇒ A
Γ, a : A | S |- K ⇒ B Γ, a : A, S == K | a |- N : A
---------------------------------------------------- // self-let
Γ | S |- a = N; K : B{a := N}
Γ |- A ⇐ Type Γ, a : A |- B ⇐ Type
-----------------------------------
Γ |- (a : A) -> B ⇒ Type
Γ, a : A | S(a) |- K ⇐ B
--------------------------------
Γ | S |- (a) => K ⇐ (a : A) -> B
// apply doesn't propagate to simplify things
Γ |- M ⇒ (a : A) -> B Γ |- N ⇐ A
---------------------------------
Γ |- M(N) ⇒ B{a := N}
Γ |- A ⇐ Type Γ, a : A |- B ⇐ Type
-----------------------------------
Γ | A |- self(a) -> B ⇒ Type
Γ, a : self(a) -> B == S | S.@ |- K ⇐ B
---------------------------------------
Γ | S |- fix(a) => K ⇐ self(a) -> B
Γ |- M ⇒ self(a) -> B
---------------------
Γ |- M.@ ⇒ B{a := M}
// rules about modes
Γ |- M ⇒ B Γ |- A == B
----------------------- // check-with-self-to-infer
Γ | S |- M ⇐ A
Γ | S |- M ⇒ A
-------------- // infer-with-self-to-check-with-self
Γ | S |- M ⇐ A
Γ, a : A | a |- M ⇐ A
--------------------- // check-to-check-with-self
Γ |- M ⇐ AType, A, B ::=
Term, M, N, K, A, B ::=
| Type // type of all types
| (M : A) // type annotation
| x // var
| x : A = N; K // let
| (a : A) -> B // pi type
| (a) => M // lambda
| M(N) // apply
| self(a : A) -> B // self type
| fix(a) => M // fixpoint
| M.@ // unfold
| sig(a : A) -> B // sigma type
| [M, N] // pair
| M.0 // pair fst proj
| M.1 // pair snd proj
| M == N // identity type
| refl() // identity refl
| M.J // identity eliminator
// I also often do hoisting, this is not a feature
// I show the erasure of that in the BONUS_SECTION
a : A;
b : B(a);
a = M[a, b];
// a == M[a, b] definitionally here
b = N[a, b];I will be using a bit more syntax here, also often using hoisting instead of fix, it's just nicer to define big blocks.
// should also be a self
ext(
x : self(a : A) -> B(a),
y : self(a : A) -> B(a),
// would fail because B(x) != B(y)
// m : x.@ == y.@
m : self(m) -> coe(ext(x, y, m), B, x.@) == y.@
) : a == b;
// often I use it implicitly, in an OTT style
Interval : Type;
left : Interval;
right : Interval;
seg : left == right;
Interval = self(i) ->
(
C : (i : Interval) -> Type,
l : C(left),
r : C(right),
// this is the magic
s : coe(seg, C, l) == r
) -> C(i);
left = (C, l, r, s) => l;
right = (C, l, r, s) => r;
// this works due to fun and self ext the goal is
seg = (C, l, r, s) => s
// the goal is the following,
seg.@ : coe(
seg,
(i) => (C : _, l : _, r : _, s : _) -> C(i),
left.@
) == right.@;
// which by pushing through
seg.@(C, l, r, s) : coe(seg, (i) => C(i), l) == r;// assuming impredicative Set
C_Bool : Set = (C : Set, t : C, f : C) -> C;
c_true : Bool = (C, t, f) => t;
c_false : Bool = (C, t, f) => f;
Bool : Set;
true : Bool;
false : Bool;
Bool = self(b) -> [
c : C_Bool,
p : c(Bool, true, false) == b
];
true = [c_true, refl()];
false = [c_false, refl()];
// this is inspired by dependent intersections work
ind(b : Bool, C, t, f) : C(b) =
[r, i] = b.@.c([b, i : C(b)], [true, t], [false, f]);
// works because r == b.@.c(true, false)
coe(b.@.p, C, i);
// this type can split all definitional idempotents
// you can also make the type that splits all coherent idempotents
// but that one requires too many lemmas
A : Set;
f : (a : A) -> A;
f_I(a) : f(f(a)) == f(a) = refl();
Fix : Set;
fix(a : A) : Fix;
mod(a) : fix(a) == fix(f(a));
Fix = self(x) -> [a : A, p : fix(a) == x];
fix(a) = [f(a), mod(a)];
// this may require a stronger fixpoint
mod(a) = refl();This is not ideal and it's still a WIP, but I have hope.
// sigma itself is already CPS
Sigma(A : Type, B : (a : A) -> Type) : Type;
exist(A, B, a : A, b : B(a)) : Sigma(A, B);
Sigma(A, B) = self(s) ->
(C, c : (a : A, b : B(a)) -> C(exist(A, B, a, b))) -> C(s);
exist(A, B, a, b) = (C, c) => c(a, b);
// CPS-former
CPS(A : Type) : Type;
ret(A, a : A) : CPS(A);
CPS(A) = self(c) ->
(C, k : (a : A) -> C(ret(A, a))) -> C(c);
ret(A, a) = (C, k) => k(a);
// this is not a complete transformation because I'm lazy
fst(A, B, s : Sigma(A, B)) : CPS(A);
mod_fst(A, B, a, b) : ret(A, a) == fst(A, B, exist(a, b));
fst(A, B, s) = (C, k) =>
// I'm assuming strong fix because I'm lazy
s.@((s) => C(fst(A, B, s)), (a, b) =>
coe(mod_fst(A, B, a, b), C, k(a)))
// strong fix because I'm lazy and this is work
mod_fst(A, B, a, b) = refl();
snd(A, B, s : Sigma(A, B)) : CPS(B(fst(A, B, s)));
mod_snd(A, B, a, b) : ret(B(a), b) == snd(A, B, exist(a, b));
snd(A, B, s) = (C, k) =>
s.@((s) => C(snd(A, B, s)), (a, b) =>
coe(mod_snd(A, B, a, b), C, k(b)));a : A;
b : B(a);
a = M{a, b};
b = N{a, b};
// becomes
a : A;
a =
b : B(a);
b = N{a, b};
M{a, b};
// which with explicit fix
a : A = fix(a) =>
b : B(a) = fix(b) => N{a, b};
M{a, b};
// you can even split them
m_a(b : B(m_a(b))) : A = M{m_a(b), b};
b : B(m_a(b)) = N{m_a(b), b};
// which without sugar is the monster below
T_m_a = fix(T_m_a) : Type =>
T_b : self(_) -> (m_a : T_m_a.@) -> Type =
fix(T_b) => (m_a) => self(b : T_b.@(m_a)) -> B(m_a.@(b));
self(m_a : T_m_a.@) -> (b : T_b.@(m_a)) -> A;
T_b : self(_) -> (m_a : T_m_a.@) -> Type =
fix(T_b) => (m_a) => self(b : T_b.@(m_a)) -> B(m_a.@(b));
m_a : T_m_a.@ = fix(m_a) => (b) => M{m_a.@(b), b.@};
b_w : T_b.@(m_a) = fix(b_w) => N{m_a.@(b_w), b_w.@};