• Me
• Publications
• Teaching
• Software
• Blog

A type theory based on indexed equality - Implementation

In this post I would like to present the type theory I have been working on, where the usual equality is replaced by an equality type indexed by the homotopy interval. This results in ideas very similar to those from the cubical system. I have a prototype implementation of this system in Haskell, which you can find on github. The system is unimaginatively called TTIE, a type theory with indexed equality. In this post I will focus on the introducing the type system and its implementation. I save the technical details for another post.

To recap: I have previously written about the 'indexed equality' type. The idea is that if we have the homotopy interval type with two points and a path between them,

-- Pseudo Agda notation
data Interval : Type where
  0 : Interval
  1 : Interval
  01 : Eq _ 0 1

then we can then define a type of equality, 'indexed' by the interval:

data Eq (A : Interval → Type) : A 0 → A 1 → Type where
  refl : (x : (i : Interval) → A i) → Eq A (x 0) (x 1)

Rather than using lambdas all the time in the argument of Eq and refl, in TTIE I write the bound variable in a subscript. So refl_i (x i) means refl (\i → x i) and Eq_i (A i) x y means Eq (\i → A i) x y. If we represent all paths with this indexed equality type, then we can actually take 01 = refl_i i.

Now the (dependent) eliminator for the interval is

iv : ∀ {A} → {x : A 0} → {y : A 1} → (xy : Eqi (A i) x y) → (i : Interval) → A i
iv {A} {x} {y} xy 0 = x
iv {A} {x} {y} xy 1 = y
iv {A} {x} {y} (refli (xy i)) i = xy i
refli (iv {A} {x} {y} xy i) = xy

For readability, I write iv xy i as xyⁱ. This combination already makes it possible to prove, for instance, congruence of functions without needing to use substitution (the J rule):

cong : ∀ {A B x y} → (f : A → B) → Eqi A x y → Eqi B (f x) (f y)
cong f xy = refli (f xyi)

this can be generalized to dependent types

cong : ∀ {A B x y} → (f : (x : A) → B x) → (xy : Eqi A x y) → Eqi (B xyi) (f x) (f y)
cong f xy = refli (f xyi)

And we also get extensionality up to eta equality:

ext : ∀ {A B f g} → ((x : A) → Eqi (B x) (f x) (g x)) → Eqi ((x : A) → B x) (\x → f x) (\x → g x)
ext fg = refli (\x → (fg x)i)

So far, however, we can not yet represent general substitution. I have found that the most convenient primitive is

cast : (A : I → Type) → (i : Interval) → (j : Interval) → A i → A j

where cast_i A 0 0 x = x and cast_i A 1 1 x = x.

This generalized cast makes all kinds of proofs really convenient. For instance, we would like that cast A 1 0 ∘ cast A 0 1 = id. But it is already the case that cast A 0 0 ∘ cast A 0 0 = id. So we just have to change some of those 0s to 1s,

lemma : ∀ {A : Type} {x} → Eq _ (casti A 1 0 (casti A 0 1 x)) x
lemma {A} {x} = castj (Eq _ (casti A j 0 (casti A 0 j x)) x) 0 1 (refli x)

As another example, most type theories don't come with a built in dependent or indexed equalty type. Instead, a common approach is to take

Eqi (A i) x y = Eq (A 0) x (casti (A i) 1 0 y)

or

Eqi (A i) x y = Eq (A 1) (casti (A i) 0 1 x) y

We can prove that these are equivalent:

lemma' : ∀ {A} {x y} → Eq Type (Eq (A 0) x (casti (A i) 1 0 y)) (Eqi (A i) x y)
lemma' {A} {x} {y} = reflj (Eqk (A (j && k)) x (casti (A i) 1 j y))

where i && j is the and operator on intervals, i.e.

_&&_ : Interval → Interval → Interval
0 && j = 0
1 && j = j
i && 0 = 0
i && 1 = i

We can even go one step further to derive the ultimate in substitution, the J axiom:

J : ∀ {A : Type} {x : A} → (P : (y : A) → Eq A x y → Type)
  → (y : A) → (xy : Eq A x y) → P x (refl x) → P y xy
J P y xy pxy = casti (P xyi (reflj (xy^(j && i)))) 0 1 pxy

With the TTIE implementation, you can type check the all of the above examples. The implementation comes with a REPL, where you can ask for types, evaluate expressions, and so on. Expressions and types can have holes, which will be inferred by unification, like in Agda.

On the other hand, this is by no means a complete programming language. For example, there are no inductive data types. You will instead have to work with product types (x , y : A * B) and sum types (value foo x : data {foo : A; bar : B}). See the readme for a full description of the syntax.

Comments

Andrej BauerDate: 2017-04-07T09:46Zx

I find this a bit strange. With equality types it should be possible to state that true and false are not equal. In ordinary type theory this would be the type Id bool true false -> empty, and this type is indeed inhabited. How do you do the same thing in your approach?

What I find odd is that normally the equality type on A is dependent over A * A, but here it is dependent over I -> A. Since there is no map from I to bool that would take 0 to false and 1 to true, I do not see how to form the type Id bool false true.

Twan van LaarhovenDate: 2017-04-07T10:22Zx

In TTIE you can prove that false is not equal to true in much the same way as other dependent type theories. That is, by substitution into a function that gives the empty type for one case and the unit type for another case:

Bool : Type
Bool = data {false : Unit; true : Unit}

false : Bool
false = value false tt

true : Bool
true = value true tt

false≠true : Eq _ false true → data{}
false≠true eq = cast_i (case eq^i of {false _ → data{}; true _ → Unit}) 1 0 tt

The indexed equality type is of the form Eq : (A : I → Type) → A 0 → A 1 → Type. This is a strict generalization of the usual equality type. When you take the first argument to be a constant function, you get back the non-indexed equality:

SimpleEq : {A : Type} → A → A → Type
SimpleEq A x y = Eq (\_ → A) x y

So you can still form Eq (\_ → Bool) false true just fine. The only 'inhabitants' of this type are functions that take 0 to false and 1 to true, of which there are none. So this equality type is uninhabited, as it should be, since false is not equal tot true.

Andrej BauerDate: 2017-04-07T10:56Zx

Oops, I totally misread the type of Eq! I read the first argument as I -> A instead of A : I -> Type. Never mind, sorry for the noise.

Reply