© 2021 Steven Obua

Practical Types

by Steven Obua
Cite as: https://doi.org/10.47757/practical.types.1
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:
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
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:
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: conceptconcrete syntaxabstract syntax \begin{array}{c||c|c} \text{concept} & \text{concrete syntax} & \text{abstract syntax} \\ \hline {\includegraphics[height=0.5em]{32041C4F-3CBF-4E52-9EF5-B52C847F57CD}} & {\includegraphics[height=0.5em]{05DF480E-1973-4DE7-914A-8B70E56CF11C}} & {\includegraphics[height=0.5em]{CB19EC3E-989E-40AB-B7C8-1EE0F117FD22}} \\ {\includegraphics[height=0.5em]{21705554-047F-495A-80E0-F86ED9696635}} & {\includegraphics[height=0.5em]{68748805-8D4C-46F4-BBA9-4EFE9E0E37EA}} & {\includegraphics[height=0.5em]{DFE2C24E-1C19-4487-93A9-6338D63E01E6}} \\ {\includegraphics[height=0.5em]{7D2A5F3C-C058-4CDD-BF27-A5ECAD27F4BD}} & {\includegraphics[height=0.5em]{4865DFE6-454E-4FD0-9A11-127D3F2B3A79}} & {\includegraphics[height=0.5em]{807B8600-1B50-4684-8A44-BD83593B7C11}} \\ {\includegraphics[height=0.5em]{A8601889-FC1E-468F-A066-047B75153490}} & {\includegraphics[height=0.5em]{2BEDF05B-0D74-4FA2-8CD7-86DE967C3774}} & {\includegraphics[height=0.5em]{9A26DFBD-5426-4C89-9F69-698E6AA21075}} \\ {\includegraphics[height=0.5em]{79672DD9-D649-4400-B67F-8BE2A14BE42A}} & {\includegraphics[height=0.5em]{552ED394-C43C-45BE-8638-2A4D9FFC228E}} & {\includegraphics[height=0.5em]{6FF8B99A-CCAE-4F75-9B9D-BAA4964F0CE7}} \\ {\includegraphics[height=0.5em]{DBBB6966-92B3-434C-B640-63EF02B23591}} & {\includegraphics[height=0.5em]{236B4CBC-C897-40BF-9520-A6C35F64D505}} & {\includegraphics[height=0.5em]{D563EF4B-0D5B-454B-B2E6-7B2C3A6883B5}} \\ {\includegraphics[height=0.5em]{00D383D0-865E-48B7-BF44-25D7C28FF116}} & {\includegraphics[height=0.5em]{7BC178B6-9163-44C3-9810-6FE036AECA2A}} & {\includegraphics[height=0.5em]{F8572C14-05BB-4E1E-8921-D308EB9AADE6}} \\ \hline {\includegraphics[height=0.5em]{C2F9DCA5-0BED-4C03-90E8-0426D8C1CDCD}} & {\includegraphics[height=0.5em]{0E31E269-9392-4CB0-A767-B4E0918BE68B}} & {\includegraphics[height=0.5em]{0415B1D4-A70D-4B02-A782-018633B50F01}} \\ {\includegraphics[height=0.5em]{0494D510-156B-4146-A729-997F55FA6C82}} & {\includegraphics[height=0.5em]{E1882D7A-55A3-4BC4-8DC7-597BA50D5716}} & {\includegraphics[height=0.5em]{E2EC19C3-715E-41A0-B685-52012219439F}} \\ {\includegraphics[height=0.5em]{455EEAD9-EC12-41B6-956F-3C8646A9F0F2}} & {\includegraphics[height=0.5em]{123FC04D-34D4-4239-B2BC-480199FDD613}} & {\includegraphics[height=0.5em]{BA3F0630-568B-4F74-B8FD-3DD1D43021EA}} \\ \hline {\includegraphics[height=0.5em]{0A7D7DED-8069-4676-A4B6-4483A0358629}} & {\includegraphics[height=0.5em]{E37C5891-88DC-487C-9F03-97A101A1EC2B}} & {\includegraphics[height=0.5em]{365971AE-22E3-40E0-B1DC-CC42762E6297}} \\ {\includegraphics[height=0.5em]{F342D793-2813-4A95-91C5-6719D18DD55F}} & {\includegraphics[height=0.5em]{9ECAD747-5992-41B0-955F-6ACF3B2F85A5}} & {\includegraphics[height=0.5em]{726C7144-30AA-4B0C-A808-B5B50FC1E855}} \\ {\includegraphics[height=0.5em]{E2430E13-915E-42A0-9001-25DD91E61F5A}} & {\includegraphics[height=0.5em]{1346B3F6-6FE3-4897-B965-D2D17194551C}} & {\includegraphics[height=0.5em]{BAAF63EF-7A30-4FD4-9779-0CA7CE87708C}} \\ \hline {\includegraphics[height=0.5em]{91551A0D-54FC-4EB0-85EF-56179B2255DD}} & {\includegraphics[height=0.5em]{60502242-2EFB-4069-ABE5-CCDB9BE13B2E}} & {\includegraphics[height=0.5em]{7B79ED15-CD5E-4FB3-B361-7BA379B7AFB2}} \\ {\includegraphics[height=0.5em]{596B3760-F4EF-4B35-8636-156A0F2822BC}} & {\includegraphics[height=0.5em]{FD50014A-0017-4458-A0E9-74FCF32472D1}} & {\includegraphics[height=0.5em]{BC22142F-B909-4668-B109-CA7CAC0DB968}} \\ {\includegraphics[height=0.5em]{133F1938-FCA9-4D82-B701-77263EB2D3CD}} & {\includegraphics[height=0.5em]{8EA4ECF6-B948-4DAF-BA4D-C8E272B11E86}} & {\includegraphics[height=0.5em]{8AD209B7-1D2C-4D42-996C-F9A70ED8C223}} \\ \end{array}

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, α\alpha-equivalence, β\beta-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: conceptconcrete syntaxlhsrhs \begin{array}{c||c|c|c} \text{concept} & \text{concrete syntax} & \text{lhs} & \text{rhs}\\ \hline {\includegraphics[height=0.5em]{F4D1DA34-D211-4AED-BDEC-138F36CA1F2B}} & {\includegraphics[height=0.5em]{8F93A553-3A4F-47C2-9BB1-4D85FEC7A0D2}} & {\includegraphics[height=0.5em]{908289B3-3A04-4EE9-B8F9-450C42167B66}} & {\includegraphics[height=0.5em]{A0F78D86-7D58-4963-8399-825ECEBDC74F}} \\ {\includegraphics[height=0.5em]{058A0982-AA69-438C-A40A-8606E1CB38A0}} & {\includegraphics[height=0.5em]{656B2B73-777A-483E-8845-D307FE188858}} & {\includegraphics[height=0.5em]{F86F0942-D537-4DBD-8020-4FEEAB996FE3}} & {\includegraphics[height=0.5em]{991B7F3C-2E4D-4546-B7ED-6001924E7B37}} \\ {\includegraphics[height=0.5em]{6D66B78A-EFFF-4B63-89B6-C381A80ECAC6}} & {\includegraphics[height=0.5em]{A8007AA1-8682-427D-987C-FD960591F219}} & {\includegraphics[height=0.5em]{8207F7B7-0CD0-428C-BF9F-0C63E5060D93}} & {\includegraphics[height=0.5em]{E72DBFC8-F83D-4E7B-B61E-BFDCCF0DA393}} \\ {\includegraphics[height=0.5em]{BFA79927-2381-47A6-87BD-943EEDFF4716}} & {\includegraphics[height=0.5em]{B7ADEC66-33F3-4D2F-A85B-492C9C3A8C44}} & {\includegraphics[height=0.5em]{FE71BB34-0BCB-4450-8F9F-8D29DDA16FF8}} & {\includegraphics[height=0.5em]{84C47B10-0379-4E73-90BC-263182EBA4E9}} \\ {\includegraphics[height=0.5em]{5924EEB3-B26F-4E9E-9768-408E4E1BD6C2}} & {\includegraphics[height=0.5em]{2CED1911-22F2-43BC-AA56-801DC49001AC}} & {\includegraphics[height=0.5em]{2310C970-2E60-44F1-8E02-E01B7857F6AA}} & {\includegraphics[height=0.5em]{B3129A1B-1502-42A8-9810-6B398CE027D1}} \\ {\includegraphics[height=0.5em]{62FBCB54-A600-4C15-9BD1-E7212576CE53}} & {\includegraphics[height=0.5em]{71A39495-04C5-4FC6-87F4-8BFA3D21D231}} & {\includegraphics[height=0.5em]{46CFDF2A-EBC6-4EDC-B525-7F97ECFE1A29}} & {\includegraphics[height=0.5em]{3022CFFD-59CC-4883-AC32-889794AE45E1}} \\ {\includegraphics[height=0.5em]{CDE234EB-D2EC-4A54-A062-A3464C3B3BAC}} & {\includegraphics[height=0.5em]{BA12582D-402C-4A34-AC26-3FDC8056B4CE}} & {\includegraphics[height=0.5em]{98C36BD9-3E37-482C-8B07-8B5ACB230267}} & {\includegraphics[height=0.5em]{84741954-6019-4E1C-850D-C5B6673B8DA0}} \\ {\includegraphics[height=0.5em]{24682E05-E7D6-47CB-BC2E-3B1ACA11F9EC}} & {\includegraphics[height=0.5em]{7C0497F2-78BE-4922-ACCE-600B8A9D1C67}} & {\includegraphics[height=0.5em]{7FD49FDC-C5C8-4C3A-AE48-55F2C51B292C}} & {\includegraphics[height=0.5em]{86CA6A18-9A66-4ED9-9B48-CE3B8ECF636E}} \\ {\includegraphics[height=0.5em]{8A5C916A-4F06-48A6-9F8C-F1AC3B2FAA2F}} & {\includegraphics[height=0.5em]{4F2CCB2B-12E5-406C-B080-4453F63C4A60}} & {\includegraphics[height=0.5em]{6D138FDB-422E-4A8B-A118-CE8BC42CB754}} & {\includegraphics[height=0.5em]{8B3A2306-B131-4E94-AC4E-91A8450A87F9}} \\ \end{array}
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:

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:

Conclusion

What just happened here? I am actually not quite sure. I really see only two possibilities:
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

[1]Steven Obua. (2021). Practal — Practical Logic: A Bicycle for Your Mathematical Mind, https://doi.org/10.47757/practal.1.
[2]Z. Luo, S. Soloviev, T. Xue. (2013). Coercive Subtyping: Theory and Implementation, https://doi.org/10.1016/j.ic.2012.10.020.
[3]Steven Obua. (2021). A New Semantics for Local Lexing, https://doi.org/10.47757/obua.ll.1.
[4]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel. (2019). From LCF to Isabelle/HOL, https://doi.org/10.1007/s00165-019-00492-1.