Two months have pasted since the last update. If you are still here, it's probably to complain about the dependent type system infrastructure that doesn't support dependent types. No more, because here it comes → Π. et le but! Follow along by downloading the latest files, vouivre/misc.scm, vouivre/system.scm, and vouivre/rules.scm, from the wip branch. You will see the following new types: dependent functions `Π', dependent pairs `Σ', identities `=', natural numbers `ℕ', generalized booleans `Bool', lists `List', and vectors/arrays `Vector'. It also includes derivations for: the ordinary function type `→' (yes, that's right, it's now derivable), the constant function `constant', the identity type inverse operation `=-inverse', the addition function on natural numbers `add', and the length of lists `length'. Below, we provide an overview of the salient features.
Maybe (sometimes?) after a long night of programming you start having dreams about functions with types that check although the elements don't... like a function to add two vectors, but no matter how hard you try, the type can't make the difference if the two inputs have the same length or not... the stuff of nightmares, really. Ordinary function sleep is a serious condition, and here's what can be done about it.
The formation, introduction, and elimination rules for dependent functions are given by:
scheme@(guile-user)> (define-rule Π
(Γ ⊢ (type (Π (: x A) (B x))))
(Γ (: x A) ⊢ (type (B x))))
scheme@(guile-user)> (define-rule λ
(Γ ⊢ (: (λ x (b x))
(Π (: x A) (B x))))
(Γ (: x A) ⊢ (: (b x) (B x))))
scheme@(guile-user)> (define-rule evaluation
(Γ (: x A) ⊢ (: (f x) (B x)))
(Γ ⊢ (: f (Π (: x A) (B x)))))
What was the codomain for ordinary function is now a type (B x) dependent on the element x of A.
TIP: The "literals" argument to `define-rule' was removed, and judgments are no longer nested in a superfluous nesting level.
The corresponding `define-rule' for ordinary functions is no longer needed, and instead we derive:
scheme@(guile-user)> (define-derivation →
((Γ ⊢ (:= (→ A B)
(type (Π (: x A) B))))
(Γ ⊢ (type A))
(Γ ⊢ (type B)))
(Π)
(weakening)
(exact)
(exact))
scheme@(guile-user)> (define-derivation →-λ
((Γ ⊢ (: (λ x (b x))
(→ A B)))
(Γ (: x A) ⊢ (: (b x) B))
(Γ ⊢ (type A))
(Γ ⊢ (type B)))
(element-conversion A (Π (: x A) B))
(λ)
(exact)
(type-symmetric)
(definition)
(exact)
(exact))
scheme@(guile-user)> (define-derivation →-evaluation
((Γ (: x A) ⊢ (: (f x) B))
(Γ ⊢ (: f (→ A B)))
(Γ ⊢ (type A))
(Γ ⊢ (type B)))
(evaluation f f)
(element-conversion A (→ A B))
(exact)
(definition)
(exact)
(exact))
TIP: To evaluate along, derivations like `weakening' and other rules/derivations we talked about in the previous post need to be declared. Therefore, whenever you get an error like "parsing error: define-derivation: rule RULE is undefined." Simply copy the corresponding RULE from rules.scm into the REPL.
The new syntax `(:= X Y)' tells the system that, upon successful derivation of Y, X should be defined to be judgmentally equal to Y. Effectively, the system adds for us the formation rule for `→' with the same name and a judgmental type equality rule available at appropriate points under the name "definition", as you will see shortly.
TIP: The same syntax can be used to define named constants as elements of a type. See rules.scm for an example.
While the natural numbers don't form a dependent type, the induction principle does, and thus many familiar functions involving the natural numbers are derived using all the notions we want to talk about today: dependent types, derived (ordinary function) types, and proof by induction. Follows the formation, introduction, elimination, and computation rules for ℕ.
scheme@(guile-user)> (define-rule ℕ-formation
(⊢ (type ℕ)))
scheme@(guile-user)> (define-rule ℕ-introduction-1
(⊢ (: 0 ℕ)))
scheme@(guile-user)> (define-rule ℕ-introduction-2
(⊢ (: succ (→ ℕ ℕ))))
scheme@(guile-user)> (define-rule ℕ-elimination
(Γ ⊢ (: (ind-ℕ p0 ps)
(Π (: n ℕ) (P n))))
(Γ (: n ℕ) ⊢ (type (P n)))
(Γ ⊢ (: p0 (P 0)))
(Γ ⊢ (: ps (Π (: n ℕ)
(→ (P n)
(P (succ n)))))))
scheme@(guile-user)> (define-rule ℕ-computation-1
(Γ ⊢ (≐ ((ind-ℕ p0 ps) 0)
p0 (P 0)))
(Γ (: n ℕ) ⊢ (type (P n)))
(Γ ⊢ (: p0 (P 0)))
(Γ ⊢ (: ps (Π (: n ℕ)
(→ (P n)
(P (succ n)))))))
scheme@(guile-user)> (define-rule ℕ-computation-2
(Γ (: n ℕ) ⊢ (≐ ((ind-ℕ p0 ps)
(succ n))
(ps n ((ind-ℕ p0 ps)
n))
(P (succ n))))
(Γ (: n ℕ) ⊢ (type (P n)))
(Γ ⊢ (: p0 (P 0)))
(Γ ⊢ (: ps (Π (: n ℕ)
(→ (P n)
(P (succ n)))))))
The formation rule says that ℕ is a type without artifice. Then, we introduce zero, and the successor function, which takes a natural number to the next. In the last sentence, the wording is indicative of intention only. That is, we state what these constructors turn out to be. That zero has no predecessor or that all natural numbers have a successor needs to be derived. Next, we have the elimination rule stated in terms of a type family over the natural numbers. A property of the natural numbers, for short. It says that if we have a witness of the given property on zero and a function that, for all natural numbers, takes a witness of the property on that number to a witness on its successor, then we have a witness of the property for all naturals, a.k.a. induction. The computation rules state that induction gives the expected results on zero and on a successor. We have everything we need to derive the addition on natural numbers. Hold on to your sombrero.
scheme@(guile-user)> (define-derivation add
(((: m ℕ) ⊢ (: (ind-ℕ m ((λ n succ)
m))
(→ ℕ ℕ))))
(element-conversion #:start 1
A (Π (: x ℕ) ℕ))
(ℕ-elimination #:start 1
(P 0) ℕ
(P n) ℕ
(P (succ n)) ℕ)
(weakening #:start 1)
(weakening)
(ℕ-formation)
(ℕ-formation)
(weakening)
(ℕ-formation)
(ℕ-formation)
(generic-element)
(ℕ-formation)
(element-conversion #:start 1
A (→ ℕ ℕ))
(→-evaluation f (λ n succ))
(→-λ)
(weakening)
(ℕ-formation)
(ℕ-introduction-2)
(ℕ-formation)
(→)
(ℕ-formation)
(ℕ-formation)
(ℕ-formation)
(→)
(ℕ-formation)
(ℕ-formation)
(definition #:start 1)
(weakening)
(ℕ-formation)
(ℕ-formation)
(weakening)
(ℕ-formation)
(ℕ-formation)
(weakening)
(ℕ-formation)
(type-symmetric)
(definition)
(ℕ-formation)
(ℕ-formation))
Element conversion is used to change between → and Π types. This works as long as we can prove that these two types are judgmentally equal (a hypothesis of element conversion). This is the case by definition! Remember earlier when we used the symbol `:=' in `(:= (→ A B) (type (Π (: x A) B)))'? The system created a new rule for `(≐ (→ A B) (Π (: x A) B))' and we invoke it in this derivation with "definition". The system will know what to do based on the type or throw an error if the judgmental equality doesn't exist. For the first use of "definition", the types come out in the right order, but for the second one, we need to use `type-symmetric'. `ℕ-elimination', induction on ℕ, is the other novel aspect of this derivation.
The formation and introduction rules for vectors of verifiable lengths are:
scheme@(guile-user)> (define-rule vector-formation
(Γ ⊢ (type (Vector A n)))
(Γ ⊢ (type A))
(Γ ⊢ (: n ℕ)))
scheme@(guile-user)> (define-rule vector-introduction-1
(Γ ⊢ (: #() (Vector A 0)))
(Γ ⊢ (type A)))
scheme@(guile-user)> (define-rule vector-introduction-2
(Γ ⊢ (: ::
(Π (: n ℕ)
(→ A
(→ (Vector A n)
(Vector
A
(succ n)))))))
(Γ ⊢ (type A)))
as you can see, things are really coming together in the last rule with a dependent function on the natural numbers, a polymorphic type, and types for vectors of different lengths.