Practical Types
July 29th, 2021
Abstract
These are preliminary notes about
Practal’s logic and its system of
practical types. This is ongoing research, and I expect updates to this document over time.
Practal Light is a research prototype implementing (part of) what is presented in this document.
Introduction
I have outlined in the
initial design document for Practal [1] how I expect
types to work in Practal. The basic idea is that they should be similar to sets; but unlike sets, they should support data abstraction.
Types in Practal are designed to be extensional. That is, two types are the same if they have the same members. This is the same as in set theory. But unlike in standard set theory, the members of a type do not need to be sets or types themselves, and do not expose structure beyond what is required to make them proper citizens of their type.
Subtyping can be seen as a direct consequence of type extensionality. We write x : A to denote that x has type A. In this case we also say that x is a member of A. We say that A is a subtype of B, in symbols A ⊆ B, if for all members x of A we also have that x is a member of B. That means that for all types A and B the following is a theorem:
(A ⊆ B) = (∀ x : A. x : B)
Equality between two types A and B is thus characterized by
(A = B) = (A ⊆ B ∧ B ⊆ A)
An often posed question is, what is wrong with
coercions [2]? Why not just use
them instead of subtyping? There is a simple argument
for subtyping, and another simple argument
against coercions:
- Firstly, subtyping is just a natural consequence of type extensionality, and it would be strange to have type extensionality, but not subtypes.
- Secondly, the basic idea of coercions is that in a function application f u, where f is a function from V to W, u an argument of type U, and U ≠ V, we can replace the illtyped term f u by the welltyped term f (c u), where c is a coercion from U to V. But in Practal, f u is not an illtyped term, but will have either type W in case of u : U ∩ V, or type Nil if ¬(u : V).
The system of practical types I propose for Practal is not a type system in the conventional sense. In fact, there are no illtyped terms in Practal, just illformed terms and wellformed terms. All wellformed terms have a type, although you might not be able to determine or prove what it is.
Practal Light
Practal’s logic is new territory for me, and
Practal Light is an ITP prototype I am implementing in
Swift to test ideas. I will use source code excerpts from Practal Light to introduce and explain concepts. The full source code of Practal Light is available at
https://github.com/practal/practal-light under an MIT license.
Terms
An important choice is to decide what the terms of Practal’s logic look like. I have finally arrived at the following design I am very pleased with:
enum Term {
case variable(Var, params: [Term])
case constant(Const, binders: [Var], params: [Term])
}
Here Var represents variable names, and Const constant names. A Term is either
- a variable; if it is free, it may depend on parameters;
- a constant binding variables and being applied to parameters.
For example, a lambda term is represented as
.constant("abs", binders: ["x"],
params: [.variable("T", params: []), .variable("P", params: ["x"])])
We use the more concise abstract syntax (abs x. T P[x]) instead, or rather the concrete syntax λ x : T. P[x].
Every term, type or formula is represented in Practal Light via this minimalistic Term data structure. I call this way of representing terms first-order abstract syntax.
A term is wellformed if the following conditions are true:
- All constants appearing in the term conform to their introduced abstract syntax.
- Each free variable has a fixed arity of parameters throughout the term.
- Only bound variables in scope are accessed.
A wellformedness check has been implemented in Practal Light and can be examined for more detailed information.
The following code in Practal Light introduces all primitive constants that all other constants will be defined in terms of:
introduce("(eq. A B)", syntax: "A = B", priority: REL_PRIO)
introduce("(abs x. T B[x])", syntax: "λ x : T. `B", priority: BINDER_PRIO)
introduce("(app. A B)", syntax: "`A B", priority: APP_PRIO)
introduce("(in. A T)", syntax: "A : T", priority: REL_PRIO)
introduce("(all x. P[x])", syntax: "∀ x. `P", priority: BINDER_PRIO)
introduce("(choose x. P[x])", syntax: "ε x. `P", priority: BINDER_PRIO)
introduce("(imp. A B)", syntax: "A ⟶ `B", priority: LOGIC_PRIO + IMP_RPRIO)
introduce("(false.)", syntax: "⊥")
introduce("(Prop.)", syntax: "ℙ")
introduce("(Fun. U V)", syntax: "U → `V", priority: TYPE_PRIO + FUN_RPRIO)
introduce("(Pred x. T P[x])", syntax: "{ x : T | P }")
introduce("(Type. i)", syntax: "Type i", priority: TYPE_PRIO + TYPE_RPRIO)
introduce("(Union i. I T[i])", syntax: "⋃ i : I. `T", priority: TYPE_PRIO + UNION_RPRIO)
introduce("(Nat.)", syntax: "ℕ")
introduce("(Nat-zero.)", syntax: "0")
introduce("(Nat-succ.)", syntax: "succ")
The constants are introduced by specifying their abstract and their concrete syntax. The concrete syntax can have optional priority and associativity annotations. From these, a
pyramid grammar [3] is constructed for parsing both abstract and concrete syntax simultaneously. As an example for how this works, consider the case
theory.introduce("(app. A B)", syntax: "`A B", priority: APP_PRIO)
The priority is given as a floating point value APP_PRIO. This means that the expression A B is understood to be an expression of that priority. Without any further annotation the default assumption is that A and B are themselves expressions of the next-higher priority compared to APP_PRIO. But that would rule out an expression like A B C. Therefore, the actual syntax given is
`A B
where the tick in front of A signifies that A has priority APP_PRIO as well. Therefore the expression A B C is parsed as (A B) C. Note that A (B C) is ruled out, because B C has priority APP_PRIO, but is required to have a priority just higher than APP_PRIO. So effectively the tick in front of A specifies left associativity.
The following table summarizes the introduced primitive constants:
conceptType Membership
Type of Propositions
Equality
Universal Quantification
Hilbert Choice
Implication
Falsity
Types of Functions
Function Abstraction
Function Application
Predicate Subtypes
Types of Types
Union of Types
Type of Natural Numbers
Zero
Successor
concrete syntaxA : T
ℙ
A = B
∀ x. P[x]
ε x. P[x]
A ⟶ B
⊥
U → V
λ x : T. B[x]
A B
{ x : T | P[x] }
Type i
⋃ i : I. T[i]
ℕ
0
succ n
abstract syntax(in. A T)
(Prop.)
(eq. A B)
(all x. P[x])
(choose x. P[x])
(imp. A B)
(false.)
(Fun. U V)
(abs x. T B[x])
(app. A B)
(Pred x. T P[x])
(Type. i)
(Union i. I T[i])
(Nat.)
(Nat-zero.)
(Nat-succ. n)
Theorems
Practal Light has no theorems or rules of inference implemented yet. There will be basic axioms like
⊢ a = a
and
⊢ (a = b) : ℙ
and primitive inference rules like modus ponens,
α-equivalence,
β-reduction, and instantiation of free variables.
Note that practical types are completely governed by theorems, i.e. a typing judgement is a normal theorem. That means that initially, type checking will possibly be harder compared to other ITP systems, as there is no built-in automation for proving typing judgements. But it also means that practical types have unparalleled flexibility. Furthermore, as the general support for automation in Practal gradually increases, this wave of automation will also lift type checking.
Definitions
Practal Light follows the
LCF approach [4]. After initial primitive constants and axioms have been introduced, all other theory development occurs by consistency-preserving definitions only.
One basic definition mechanism has already been implemented in Practal Light: Given two terms lhs and rhs, where lhs describes the abstract syntax of the new constant to be defined, and rhs is the right hand side of the defining equality, a new constant is defined if certain side-conditions are met, such as the wellformedness of rhs, and that all free variables of rhs are among the free variables of lhs.
Using this definition mechanism, we can already define many important derived notions:
define("(not. P)", "P ⟶ ⊥", syntax: "¬`P", priority: LOGIC_PRIO + NOT_RPRIO)
define("(true.)", "¬ ⊥", syntax: "⊤")
define("(or. P Q)", "¬P ⟶ Q", syntax: "`P ∨ Q", priority: LOGIC_PRIO + OR_RPRIO)
define("(and. P Q)", "¬(¬P ∨ ¬Q)", syntax: "`P ∧ Q", priority: LOGIC_PRIO + AND_RPRIO)
define("(equiv. P Q)", "(P ⟶ Q) ∧ (Q ⟶ P)", syntax: "P ≡ Q", priority: REL_PRIO)
define("(neq. P Q)", "¬(P = Q)", syntax: "P ≠ Q", priority: REL_PRIO)
define("(ex x. P[x])", "¬(∀ x. ¬P[x])", syntax: "∃ x. `P", priority: BINDER_PRIO)
define("(all-in x. T P[x])", "∀ x. x : T ⟶ P[x]", syntax: "∀ x : T. `P", priority: BINDER_PRIO)
define("(ex-in x. T P[x])", "∃ x. x : T ∧ P[x]", syntax: "∃ x : T. `P", priority: BINDER_PRIO)
CONTROL_PRIO)
The above definitions are summarized in the following table:
conceptNegation
Truth
Disjunction
Conjunction
Equivalence
Inequality
Existential Q.
Bounded U. Q.
Bounded E. Q.
concrete syntax¬P
⊤
P ∨ Q
P ∧ Q
P ≡ Q
P ≠ Q
∃ x. P[x]
∀ x : T. P[x]
∃ x : T. P[x]
lhs(not. P)
(true.)
(or. P Q)
(and. P Q)
(equiv. P Q)
(neq. P Q)
(ex x. P[x])
(all-in x. T P[x])
(ex-in x. T P[x])
rhsP ⟶ ⊥
¬ ⊥
¬P ⟶ Q
¬(¬P ∨ ¬Q)
(P ⟶ Q) ∧ (Q ⟶ P)
¬(P = Q)
¬(∀ x. ¬P[x])
∀ x. x : T ⟶ P[x]
∃ x. x : T ∧ P[x]
In the following we write definitions in an abbreviated notation, for example:
all-in: ⊢ ∀ x : T. P[x] ≝ ∀ x. x : T ⟶ P[x]
Practical Types
The following is a blueprint for the development of practical types in Practal Light. For each type, the following questions need to be answered:
- What are the elements of the type?
- When do we consider two elements of the type to be equal?
- Are elements of the type equal to elements of some other type?
The Type of Propositions
Practal uses classical logic, and therefore the type ℙ of propositions consists of exactly two elements, ⊤, which denotes truth, and ⊥, which denotes falsity:
⊢ ∀ p : ℙ. p = ⊥ ∨ p = ⊤
⊢ ⊤ ≠ ⊥
The Empty Type
The empty type ∅ is the simplest possible type, as it has no members at all. It is characterized by
⊢ ∀ x : ∅. ⊥
We can actually define the empty type using predicate subtypes as
Empty: ⊢ ∅ ≝ { p : ℙ | ⊥ }
Types of Functions
Given two types A and B, the type of total functions with domain A and codomain B is denoted by A → B. Therefore the following axiom holds:
⊢ f : A → B ⟶ (∀ a : A. f x : B)
A function is only equal to other functions. Furthermore for a function f : A → B and g : C → D to be equal, they need to be defined on the same domain, i.e. A = C.
⊢ ∀ f : A → B. ∀ g : C → D. (f = g) = (A = C ∧ (∀ x : A. f x = g x))
It should therefore be possible to prove the following subtype relationship between function types for types A, B, C and D:
(A → B ⊆ C → D) = (A = C ∧ (A = ∅ ∨ B ⊆ D))
We will define the meaning of
⊆ itself
later →.
We can define in our logic the property of being a function, in code:
define("(is-Fun. f)", "∃ U. ∃ V. f : U → V", syntax: "f : Fun", priority: REL_PRIO)
In our abbreviated notation this reads
is-Fun: ⊢ f : Fun ≝ ∃ U. ∃ V. f : U → V
Note that Fun is not a type. It is just notation that allows us to pretend so in many situtations. We can extend notation for universal and existential quantification accordingly:
all-fun: ⊢ ∀ f : Fun. P[f] ≝ ∀ f. f : Fun ⟶ P[f]
ex-fun: ⊢ ∃ f : Fun. P[f] ≝ ∃ f. f : Fun ∧ P[f]
The Nil Type
Note that for any type A ≠ ∅ we have
(A → ∅) = ∅
On the other hand, for any type B, we have
(∅ → B) = (∅ → ∅)
We therefore define
Nil: ⊢ Nil ≝ ∅ → ∅
The type Nil has exactly one element, namely the unique function nil : Nil with empty domain:
nil: ⊢ nil ≝ λ x : ∅. ⊥
We use nil to deal with undefinedness. In particular, we postulate the following axiom:
⊢ f : A → B ⟶ ¬ (x : A) ⟶ f x = nil
In other words, if we apply a function to an argument outside of its domain, the result is nil. Because nil itself is a function with empty domain, we also have
⊢ nil x = nil
What does A B mean if A is not a function? The following axiom handles this case:
⊢ ¬(A : Fun) ⟶ A B = nil
Furthermore, we introduce the following notions that simplify working with undefinedness:
defined: ⊢ x↓ ≝ x ≠ nil
undefined: ⊢ x↑ ≝ x = nil
defined-eq: ⊢ x =↓ y ≝ (x↓ ∨ y↓) ∧ x = y
undefined-eq: ⊢ x =↑ y ≝ x↑ ∨ y↑ ∨ x = y
The Hilbert choice operator obeys the following axioms:
⊢ (∃ x. P[x]) ⟶ P[ε x. P[x]]
⊢ ¬(∃ x. P[x]) ⟶ (ε x. P[x]) = nil
Predicate Subtypes
The expression
{ a : A | P[a] }
denotes the subtype of A consisting of exactly those elements a : A for which P[a] is true.
Consequently, we postulate the following axiom:
⊢ (a : { a : A | P[a] }) = (a : A ∧ P[a])
Of course, for any type A this implies
{ a : A | P[a] } ⊆ A
The Type of Natural Numbers
We also postulate the existence of a type ℕ which represents the natural numbers. We assume the Peano axioms, adapted to our setting:
⊢ 0 : ℕ
⊢ succ : ℕ → ℕ
⊢ succ n ≠ 0
⊢ succ(m) =↓ succ(n) ⟶ m = n
⊢ 0 : N ⟶ (∀ n : N. succ n : N) ⟶ ℕ ⊆ N
Types of Types
Given a type
A, what type does
A have? It would be convenient if there could be a single type
Type of types, but using
Russell’s paradox it is easy to see that this leads to inconsistency. Because let the type
R be defined via
R = { T : Type | ¬(T : T) }
Assuming R : R, it follows that ¬(R : R). On the other hand, assuming ¬(R : R) implies R : R. Thus (R : R) = ¬(R : R), an inconsistency.
We take the same way out of this dilemma as
Lean does: There is not just a single type
Type of types, but an infinite family
Type i of types of types such that
(Type 0 : Type 1) ∧ (Type 1 : Type 2) ∧ (Type 2 : Type 3) ∧ ...
We furthermore require a nesting of types such that
(Type 0 ⊆ Type 1) ∧ (Type 1 ⊆ Type 2) ∧ (Type 2 ⊆ Type 3) ∧ ...
We use 𝕋 as an abbreviation for Type 0:
Type-0: ⊢ 𝕋 ≝ Type 0
Membership to Type i is governed by the following axioms:
⊢ ℙ : 𝕋
⊢ ℕ : 𝕋
⊢ A : Type i ⟶ B : Type i ⟶ A → B : Type i
⊢ A : Type i ⟶ P : A → ℙ ⟶ { a : A | P a } : Type i
⊢ i : ℕ ⟶ Type i : Type (succ i)
⊢ i : ℕ ⟶ Type i ⊆ Type (succ i)
Let’s try to apply Russell’s paradox again, and form for example
S = { T : 𝕋 | ¬(T : T) }
From S : S we can still derive ¬(S : S). But the other direction doesn’t work anymore, because the assumption ¬ (S : S) is not enough to prove S : S. We also need to show S : 𝕋, but we can only prove S : Type 1. So there is no paradox here anymore, just a proof of ¬ (S : S).
Although there is no universal type of types, we can nevertheless introduce notation that emulates it in certain situations, just like we did for Fun:
is-Type: ⊢ T : Type ≝ ∃ i. T : Type i
all-type: ⊢ ∀ T : Type. P[T] ≝ ∀ T. T : Type ⟶ P[T]
ex-type: ⊢ ∃ T : Type. P[T] ≝ ∃ T. T : Type ∧ P[T]
We can now give the definition of
⊆:
sub-type: ⊢ U ⊆ V ≝ U : Type ∧ V : Type ∧ (∀ u : U. u : V)
Singleton Types
Given x : T we could define the singleton type { x } as
{ x } = { y : T | y = x }
But what if we don’t know which type x has? Could it be that x has no type? That doesn’t seem to make sense, so we introduce the following axiom:
⊢ ¬ (x : Type) ⟶ (∃ T : 𝕋. x : T)
This makes sure that x : { x } actually holds, where we define { x } by
Singleton: ⊢ { x } ≝ { y : (ε T. x : T) | x = y }
Union of Types
We want the expression
⋃ a : A. T[a]
to denote the type formed by the union of T[a] over all a : A.
But this is a powerful operation, and we need to be careful for it not to lead to inconsistency. For example, if we allow
⋃ i : ℕ. Type i
then we have effectively constructed our type of all types, which we know leads to inconsistency.
We try to tame the union operator by defining it only when all T[a] are members of Type i for some fixed i. This leads to the following axioms:
⊢ (∀ a : A. T[a] : Type i) ⟶ (x : ⋃ a : A. T[a]) = (∃ a : A. x : T[a])
⊢ (∀ a : A. T[a] : Type i) ⟶ (⋃ a : A. T[a]) : Type i
⊢ ¬(∃ i : ℕ. ∀ a : A. T[a] : Type i) ⟶ (⋃ a : A. T[a]) = nil
This still allows us to construct huge types like
⋃ T : 𝕋. T
The Intersection Type
We define the intersection of types by
Intersection: ⊢ ⋂ a : A. T[a] ≝ { x : ⋃ a : A. T[a] | ∀ a : A. x : T[a] }
The Binary Union and Intersection Types
We define A ∪ B and A ∩ B via
Binary-Union: ⊢ A ∪ B ≝ ⋃ p : ℙ. (if p then A else B)
Binary-Intersection: ⊢ A ∩ B ≝ ⋂ p : ℙ. (if p then A else B)
The if-then-else construct is defined by
if-then-else: ⊢ if p then A else B ≝ ε x. (p ⟶ x = A) ∧ (¬ p ⟶ x = B)
Function Abstraction
The lambda expression
λ x : T. B[x]
is only defined if its type
T → ⋃ x : T. {B[x]}
is defined:
⊢ T → (⋃ x : T. {B[x]}) ↓ ⟶ (λ x : T. B[x]) : T → (⋃ x : T. {B[x]})
⊢ T → (⋃ x : T. {B[x]}) ↑ ⟶ (λ x : T. B[x]) = nil
Application of a lambda expression to an argument is defined accordingly:
⊢ T → (⋃ x : T. {B[x]}) ↓ ⟶ x : T ⟶ (λ x : T. B[x]) x = B[x]
The Type of Pairs
There is no mechanism for defining new types implemented yet in Practal Light. Let us assume it would allow a type definition of pairs somewhat like this:
typedef Pair: A ⨯ B ⇄ { f : ℙ → A ∪ B | f ⊥ : A ∧ f ⊤ : B }
A member e of A ⨯ B is written (a, b) if it is represented by an f such that f ⊥ = a and f ⊤ = b. In this case we also define fst e = a, and snd e = b.
Why do we need a new type definition mechanism? Could we not just define it as:
Pair: ⊢ A ⨯ B ≝ { f : ℙ → A ∪ B | f ⊥ : A ∧ f ⊤ : B }
That would certainly be possible, but then A ⨯ B would consist of functions. We want pairs not to be equal to anything than other pairs, and thus the new mechanism is needed.
Dependent Functions and Pairs
The dependent function type [a : A] → B[a] is defined as
D-Fun: ⊢ [a : A] → B[a] ≝ { f : A → (⋃ a : A. B[a]) | ∀ a : A. f a : B[a] }
Dependent pair types are defined likewise:
D-Pair: ⊢ [a : A] ⨯ B[a] ≝ { p : A ⨯ (⋃ a : A. B[a]) | snd p : B[fst p] }
Cleaning Up
There have been a few assumptions left unsaid and implicit, and it is now time to spell them out explicitly.
Propositions, natural numbers, functions, pairs and types are disjoint:
⊢ ℙ ∩ ℕ = ∅
⊢ ℙ ∩ (A → B) =↑ ∅
⊢ ℙ ∩ (A ⨯ B) =↑ ∅
⊢ ℙ ∩ Type i =↑ ∅
⊢ ℕ ∩ (A → B) =↑ ∅
⊢ ℕ ∩ (A ⨯ B) =↑ ∅
⊢ ℕ ∩ Type i =↑ ∅
⊢ (A → B) ∩ (A ⨯ B) =↑ ∅
⊢ (A → B) ∩ Type i =↑ ∅
⊢ (A ⨯ B) ∩ Type i =↑ ∅
The =↑ operator is used instead of just = because operands might be undefined:
⊢ ¬ (A : Type) ∨ ¬ (B : Type) ⟶ (A → B) = nil
⊢ ¬ (A : Type) ∨ ¬ (B : Type) ⟶ (A ⨯ B) = nil
⊢ ¬ (i : ℕ) ⟶ Type i = nil
Similarly, we need to be clear for all remaining primitive constants when they are defined or otherwise undefined. This will then ripple through derived notions, often without any further need to specify definedness / undefinedness.
⊢ ¬ (T : Type) ⟶ (x : T) = ⊥
⊢ ¬ (T : Type) ⟶ { x : T | P[x] } = nil
Logical operators are defined on ℙ ∪ Nil, and the nil value is taken to mean false:
¬ (P : ℙ ∪ Nil) ⊢ (¬ P)↑
¬ (P : ℙ ∪ Nil) ⊢ (P ⟶ Q)↑
¬ (Q : ℙ ∪ Nil) ⊢ (P ⟶ Q)↑
⊢ ¬ nil
⊢ (¬ ⊤) = ⊥
P : ℙ ∪ Nil ⊢ nil ⟶ A
P : ℙ ∪ Nil ⊢ ⊥ ⟶ A
⊢ ⊤ ⟶ ⊤
⊢ (⊤ ⟶ ⊥) = ⊥
⊢ (⊤ ⟶ nil) = ⊥
Universal quantification ∀ x. P[x] is defined as follows:
- If there is an a such that ¬ (P[a] : ℙ ∪ Nil), then (∀ x. P[x]) = nil.
- If P[x] = ⊤ for all x, then (∀ x. P[x]) = ⊤.
- If P[x] : ℙ ∪ Nil for all x, but there is an a with ¬ P[a], then (∀ x. P[x]) = ⊥.
Conclusion
What just happened here? I am actually not quite sure. I really see only two possibilities:
- This is all some inconsistent bullshit.
- Practical Types can serve as the new and improved foundations of interactive theorem proving, and mathematics in general.
Maybe you have an opinion which one of the two it is, or want to offer a third option? If you have any comments, questions, and/or want to share your ideas for Practal, please visit
Practal’s discussion forum!
References
