2015-08-06

A proof with intervals

One of the problems with homotopy type theory at the moment is that there are few uninformed hobbyists writing partially correct blog posts about it. More generally, it's hard to find examples of simple proofs that nonetheless make use of some of the tools HoTT gives us above the intensional type theories used by most theorem provers and dependently typed programming languages today. This is my attempt to improve (or worsen) the situation.

For this post, I will use the programming language Hoq. I use this for two reasons:
  • I like the functional (Agda/Idris) style of proving, particularly when exploring the possibilities of the type system. Tactics-based provers seem too removed from the underlying mathematics to give me a clear picture of what's going on.
  • I wanted to use a language built for HoTT, rather than one that has been modified to use it. Idris is incompatible with HoTT due to the K axiom, and, though it can be run K-less these days, I don't know whether there are other things missing from Agda (my guess being that there are).
My only other options were the mutually related cubical and cubicaltt. Though these are well documented, lack of comfort features like implicit arguments and LHS pattern matching makes them rather painful to work in. Hoq has barely any documentation (examples/basics.hoq is all I can find), so this post should help with that.

The objective of this exercise is to prove right distributivity of boolean or over and by first proving left distributivity and commutativity, then combining them in the obvious way. The fact that we can combine them in the obvious way is the focus of this post. This contrasts with what we'd do in an intensional language, as we will see.

First, we define some basic things, which should really be in some prelude module. This will hopefully give an introduction to the syntax, which is similar to that of Idris and Adga. I've refrained from defining the most general versions of ext and flip for simplicity (and to help Hoq infer implicit arguments).
-- Booleans
data Bool = False | True

or : Bool -> Bool -> Bool
or False False = False
or _ _ = True

and : Bool -> Bool -> Bool
and True True = True
and _ _ = False

-- Convenient alias: at p = \i -> p @ i
at : {A : Type} -> {x y : A} -> x = y -> I -> A
at _ _ _ p i = p @ i

-- Equality proofs
ext : {A B : Type} -> {f g : A -> B} -> ((a : A) -> f a = g a) -> f = g
ext _ _ _ _ p = path (\i a -> p a @ i)

idp : {A : Type} -> {a : A} -> a = a
idp _ a = path (\_ -> a)

-- Combinator
flip : {A B C : Type} -> (A -> B -> C) -> B -> A -> C
flip _ _ _ f y x = f x y
Also introduced implicitly is the interval type I, as seen in lambda variable i. An equality proof p for terms of type A is basically a wrapper around a function of type A -> I, and the underlying function is accessed using p @ i. I is supposed to be analogous to \({\leq}|0,1|{\geq}\) (written by people other than me as \([0,1]\)), with end points left and right which, crucially, we can't pattern match with. If p : x = y, p @ left is x and p @ right is y.

In order to proceed, we prove the required facts about or in the standard way:
orCommutative : (x y : Bool) -> or x y = or y x
orCommutative False False = idp
orCommutative _ _ = idp

orLeftDistr : (x y z : Bool) -> or x (and y z) = and (or x y) (or x z)
orLeftDistr False False _ = idp
orLeftDistr False _ False = idp
orLeftDistr False True True = idp
orLeftDistr True _ _ = idp
As you can see, we use idp (the identity path) where we might expect Refl on the right-hand side.

We could just prove right distributivity in the same way, but that would be terribly boring. The point of this article is really to introduce a method that can be used in more complex situations, where we want to avoid code duplication. In intensional type theory, the proof we want might look something like this (using equational reasoning syntax from examples/Paths.hoq):
orDistrRight' : (x y z : Bool) -> or (and x y) z = and (or x z) (or y z)
orDistrRight' x y z =
  or (and x y) z
    ==< orCommutative (and x y) z >==
  or z (and x y)
    ==< orLeftDistr z x y >==
  and (or z x) (or z y)
    ==< pmap (\w -> and w (or z y)) (orCommutative z x) >==
  and (or x z) (or z y)
    ==< pmap (and (or x z)) (orCommutative z y) >==
  and (or x z) (or y z)
    !qed
This is rather repetitive, though. Each time we want to apply orCommutative, we have to say exactly where to apply it in the expression, which involves writing out the expression over and over again.

We'll proceed with the main proof in small steps. To put us on steady ground, we prove or = flip or:
orFlippedEq : or = flip or
orFlippedEq = ext (\x -> ext (\y -> orCommutative x y))
Now, at last, we get to a HoTT-specific part. Here, we prove that the identity we're trying to prove is equivalent to the type of orDistrLeft. Naturally, we produce an equivalence between equivalences:
orRightDistrEqOrLeftDistr : (x y z : Bool) ->
  (or x (and y z) = and (or x y) (or x z)) =
    (or (and y z) x = and (or y x) (or z x))
orRightDistrEqOrLeftDistr x y z =
  path (\i -> (orFlippedEq @ i) x (and y z) =
                and ((orFlippedEq @ i) x y) ((orFlippedEq @ i) x z))
The expression inside the lambda abstraction is simply the left side of the required equality, but with or replaced by orFlippedEq @ i. orFlippedEq @ left is or and orFlippedEq @ right is flip or, which give us the required end points.

The final thing we need to introduce is coe (short for “coerce”, presumably). Its type is (A : I -> Type) -> (i : I) -> A i -> (j : I) -> A j, meaning that it takes a type equality and moves the given value along it from i to j. Here, we use it to simply transport our proof of left distributivity into a proof of right distributivity:
orRightDistr : (x y z : Bool) -> or (and x y) z = and (or x z) (or y z)
orRightDistr x y z =
  coe (at (orRightDistrEqOrLeftDistr z x y)) left (orLeftDistr z x y) right
And that's the result we wanted.

2015-04-08

The language of types

It's been a while since I posted here. That can be attributed partially to the increased workload I had after starting university, and partially to the fact that most of my ideas had reached either a conclusion or a dead end by the end of summer. But now it's revision time, and I've been able to think about the things I wrote here. Since last post, I've learnt a lot about type theory via Idris. In this post, I apply some of that knowledge.

My aim is to present a type-theoretic interpretation of spoken language, taking advantage of the Curry-Howard correspondence. On the one hand, type theory lends itself very well to the declarative claims of spoken language. It's possible to define predicates as types, with the claim the predicate is making visible to the outside world. Also, it's well documented that logical connectives are easily defined as type families. However, the somehow closed nature of types, in comparison to sets, makes it difficult to work out what types there should be, and how they should be used.

My main idea is to encode verbs as type families and nouns as values. For now, we'll consider all nouns to be of a single, simple type. Notionally, every noun we could want to talk about is specified as its own value constructor, which takes no arguments. Constructors of most real-world verb types are specified similarly, but construct values only of a specific type. For example, taking Lojban's {ciska} (“write”), we make the type family:\[
\begin{align}
\mathbf{data}\ &\mathrm{Ciska} : \mathrm{Noun}\to\mathrm{Noun}\to\mathrm{Noun}\to\mathrm{Noun}\to\mathrm{Type}\ \mathbf{where}\\
&\mathrm{MkCiska0} : \mathrm{Ciska}\ \mathit{me}\ \mathit{this\_post}\ \mathit{my\_blog}\ \mathit{keyboard}\\
&\mathrm{MkCiska1} : \mathrm{Ciska}\ \mathit{me}\ \mathit{a\_tweet}\ \mathit{Twitter}\ \mathit{keyboard}\\
&\dots
\end{align}
\]Notice that these simple value constructors essentially correspond to events. It has happened that I have written a tweet on Twitter using a keyboard, so the event of that happening constitutes a proof. In this way, we can consider Lojban's {nu} as a wrapper over the contained bridi (type), fixing the type parameters. Of course, we already know that {ka} is used for creating functions resulting in types, and many type constructors take this kind of argument. I'm not sure yet about {du'u} and {si'o}, and {ni} is probably something different again.

Since we now have a reïfied view of statements, it makes sense to quantify them. This is in fact what we are doing with dependently typed Πs and Σs. In implication statements, for example, we are saying that for all proofs of the hypothesis, there exists a proof of the conclusion using that proof. “every time A, B” is logically equivalent to “A ⇒ B”, and is proven using a function of type \(A\to B\). We can similarly use dependent pairs for existential quantification, just as in dependently typed programming.

Quantifiers like “almost all” and “almost always when”, naturally, are more difficult to handle, and types don't particularly help us with that. They're probably best dealt with theoretically by having a function of type \(A\to\mathrm{Maybe}\ B\) mapping this over a list of inhabitants of A, then interpreting the output list (in some context-sensitive way). How useful this notion is, I don't know.

Anyway, the main point of the latter part of this post was that type families, as opposed to my previous idea of referent sets, are the things that should be quantified over. This becomes apparent when we have polyadic verbs. In my new language, it used to be the case that I'd express “a dog catches a ball” as something like “gerku fasu'o fasu'o kavbu fesu'o fasu'o bolci” (with all those “su'o” usually being implicit). This would literally be read as “a dog is a catching thing; a caught thing is a ball”. However, the problem is that the dog and the ball aren't obviously involved in the same event, and the symmetry of the sentence structure means that we can't make “kavbu” be the main verb. Now, I propose to say “gerku su'o fafa kavbu su'o fefa bolci su'o”, literally “a dog is the catcher in at least one catching event in which a ball is caught”.