Why dependent types

Posted on January 16, 2016

Tags: types

in accordance with the propositions-as-types paradigm. Thus, filling in the details of a function definition and ensuring it is type correct is no different from filling in the details of a proof and checking that it establishes the desired conclusion.

This post discuss why I care about dependent-types.

module whydp where

Types give us a notion of possible values. Polymorphic types are types that are indexed by other types; they are functions from types to types. Dependent types are types that are indexed by values; they are functions from values to types. Since types themselves are values of a higher type, the distinction between types and values is erased in dependently-typed theories: they are both values of specific types! –this is very different from many conventional programming languages. Alternatively, one may say ‘types are first-class citizens’ in such a language and so can be manipulated like any other value.

Observe that dependent types encompass the other two notions. Since simple types are just polymorphic types that ignore the index-type, we regain simple types from polymorphic types. Since types are the values of the type of ‘small types’, we regain polymorphic types from dependent types.

A dependent (function) type is usually written π x ∶ A • B x or as (x : A) → B x. Agda gives us the latter, but we can mimic the former via syntax declarations:

π∶• : (A : Set) (B : A → Set) → Set
π∶• A B = (x : A) → B x

syntax π∶• A (λ x → B) = π x ∶ A • B -- `∶` is a ghost colon obtained by `slash :` in emacs

Why the bullet-notation? We cannot use a low dot . since it is one of the few reserved tokens in Agda; more importantly, I like Z-notation style quantification. Anyhow, this is why the main page of this blog contains a Π; the Σ is the notation for dependent product: Σ x ∶ A • B x has values being pairs denoted (a , b) with a : A and b : B a; note the dependence of the second component’s type on that of the first component. The dependent product type Σ x ∶ A • B x can be read as ‘the type of x : A satisfying B’; a sort of ‘sub-type’ of A.

A final notation for dependent function is ∀ (x : A) → B x. The reason for this notation is that a universal-quantification can be proved true by constructing a procedure that for any element x : A produces a proof of B x, i.e., an inhabitant of the type B x. This is the Curry-Howard Correspondence: it can be stated as saying propositions coincide with types, or that Gentzen’s natural deduction is identical to Church’s lambda calculus. Loosely put, logic and computation are flip-sides of the same coin. For more on this, see Proofs are programs: 19th century logic and 21st century computing

Basically, we can express a type which is inhabited precisely when the associated proposition is true: for a proposition p : X → 𝔹, we can construct a dependent type P : (X : x) → Set of ‘’proofs witnessing p(x), given x’’; we can construct a value of type P x precisely when p(x) holds. If p(x) does not hold, then we cannot construct a value of type P x and there is no run-time exception but a compile-time check.

Essentially, a type Q can be thought of as “the type of reasons, or proofs, that Q is true”.

Programming

Usually, a program that takes input satisfying a given Precondition and ensuring a given Postcondition is usually programmed, call it f, then is proven correct according to the aforementioned specification by ‘verifying’ ∀ x • x ∈ Pre ⇒ f x ∈ Post and if that is too difficult, tests are formed after-which f is written and checked to satisfy the given tests; so-called test-driven development. However, since types correspond to propositions, it suffices to ‘construct a correct program from its specification’ as f : Pre → Post; so-called type-driven programming. This is not a new idea; consider abs : ℤ → ℤ with a proof ∀ n : ℤ • abs b ≥ 0 versus the single program abs : ℤ → ℕ. However, dependent types allow us to put more complicated specification details into the types.

Similar examples include,

integer square root: isqrt : ℤ → ℤ with a proof of ∀ n : ℤ • let i = isqrt n • n ≥ 0 ⇒ i ≥ 0 ∧ i ² ≤ n < (1 + i)² versus the single type isqrt : (n : ℕ) → Σ i ∶ ℕ • i * i ≤ n ⋀ n < (i + 1) * (i + 1) —notice that the former specification says nothing about the case n < 0.
Exercise: transform type divrem : ℤ → ℤ → ℤ × ℤ with specification ∀ a, b : ℤ • let (q , r) = divrem a b • b > 0 ⇒ 0 ≤ r < b ∧ a = b * q + r into a single dependent-type that incorporates the specification.
Adding types removes issues.
‘Given a non-null non-empty array return its first element’. In an untyped language, we take input argument arr and return arr[0], all the while hoping the user only calls this operation on arrays; and still, we place the specification as a comment. We could place guards checking that the input is not-null, array-like, and not-empty; but that gets in the way of the purpose of the method. The simplest solution is to move to a typed language, where we can insist that arr : Array, all the while hoping the user only calls it with well-defined, non-null data. Then moving to a null-free language, such as Haskell, the issue of nullity disappears. All that remains in the non-empty constraint. Now we move to a dependently-typed setting where arrays are types indexed by numbers that represent their lengths, then our operation has input type ∀{n : ℕ} {X : Set} → Array (Suc n) X → X. Now the specification in in the type: given an array of length at-least one, we return an element of that type. (This example adapted from https://bimorphic.com/learning-idris-part-1/)
Some things can be misleading.
Consider zipWith : ∀ {k n} {A₁ … Aₖ B} → (A₁ → A₂ → ⋯ → Aₖ → B) → Vec n A₁ → Vec n A₂ → ⋯ → Vec n Aₖ → B. At a first glance it seems that the only way to write such a program is by using dependent types; however, if we use lists instead of vectors then it can actually be written without dependent types. Admittedly the solution is a bit clever.

The program-then-proof approach becomes simultaneously-program-and-prove, or test-driven becomes type-driven.

Dependent types can be used as specifications for programs that are a part of the programs themselves and not independently elsewhere, removed from the code. Then specification satisfiability is tantamount to type-checking!

Proving

I personally use the dependently-typed programming language Agda as a type checker for doing mathematics —manipulating symbols according to specified rules. Agda is used as just a mechanised mathematical notation that lets me write the mathematics in a natural way, and allows me to be confident about my proofs.

Theoretical developments can be fully mechanised and still be presented in readable calculational style, where writing is not significantly more effort than a conventional calculational presentation in LaTeX. – Wolfram Kahl

Moreover he goes on to say,

Agda permits readability and writiabiliy of mathematics as it is traditionally done by paper-and-pencil —this is accomplished by unicode and mixfix operators. See the bottom of the previous post for an example of this.
Since a proof is just a formal term, we can nest calculational proofs –compare this with page 2 of Fokkinga’s LaTeX calculation environment.
the use of Agda enables a completely natural mathematical treatment of theories, with nested calculational proofs, and their direct use as modules of executable programs.
formalisations in Agda have the advantage that they can be used both for theoretical reasoning and for executable implementations (by instantiating module parameters with appropriate choices of concrete structures).

Finally, proofs in Agda are fool-proof! Mechanised approaches do not allow us to leave anything as ‘an exercise to the reader’ –to the extent that we always have type-checking— and check every step of our proof. Sometime we may apply a lemma is a proof-step incorrectly on paper-and-pencil proofs and it might not at all be that obvious that we failed to meet some proviso, whereas in a mechanised setting, we can rest assured that such did not occur.

That is, the extra work of using a real language rather than pseudo-code is the type-checking: we can make sure all the i’s are dotted and t’s crossed.

A more personal reason is that mathematics is a hobby for me and there’s a proverb ‘I hear and forget, I see and remember, I do and understand’, so formalising the math I do is to ensure my comprehension —also it’s addictive fun :-)

Why dependent types

Programming

Proving

Further Reading