[Agda] heterogeneous equality

[Conor McBride]

Hi

Just to note that there's more lurking under
the surface here. Sorry. Old war stories ahead.

On 3 Mar 2008, at 10:44, Ulf Norell wrote:

>
>
> On Mon, Mar 3, 2008 at 4:02 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> Is it possible to define heterogeneous equality in Agda?  I tried:
>
>  data HId {A : Set} : {B : Set} -> A -> B -> Set where
>    HRefl : {a : A} -> HId {A} {A} a a
>
> but I can't figure out how to use it.

Back when I was mucking about with this type,
my answer was "homogeneously"! That's to say,
rather than interpreting heterogeneous equality
as "the types are equal and the terms are equal",
it's "if the types are equal, the terms are equal".

So, the omission in this ...

>
>
> E.g., for a context- and object-language-type-indexed expression type
> Tm, I want a congruence for the successor constructor:
>
>  help : { G G' : Ctx} {e : Tm G nat} {e' : Tm G' nat}
>       -> HId e e' -> HId (Succ e) (Succ e')
>  help {G} {.G} {e} {.e} HRefl = ?

... is an extra hypothesis (HId G G'). See below

module HId where

data HId {A : Set} : {B : Set} -> A -> B -> Set where
    HRefl : {a : A} -> HId {A} {A} a a

data Nat : Set where
   zero : Nat
   suc : Nat -> Nat

data Vec (X : Set) : Nat -> Set where
   nil : Vec X zero
   cons : {n : Nat} -> X -> Vec X n -> Vec X (suc n)

{-
boo : {X : Set}{m n : Nat}
       {xs : Vec X m}{ys : Vec X n}{x : X} ->
       HId xs ys ->
       HId (cons x xs) (cons x ys)
boo HRefl = ?
-}

woohoo : {X : Set}{m n : Nat}
          {xs : Vec X m}{ys : Vec X n}{x : X} ->
          HId m n -> HId xs ys ->
          HId (cons x xs) (cons x ys)
woohoo HRefl HRefl = HRefl

> darcs pull :-)
>
> The unification performed when pattern matching only handled data  
> constructors (not type constructors), so Tm G nat and Tm G' nat  
> didn't unify (with G' := G). Fixed now.

Remember that the equality used in pattern matching
becomes your notion of propositional equality. So
this is a significant step with potentially interesting
consequences. It makes type theory just a bit more
intensional and a bit more reflective, in that type
constructors become provably injective and disjoint.
I don't consider that a crime, but it rules out some
kinds of "up to isomorphism" thinking. It also allows
you to define equality of Sets in Set

record TT : Set where

SetEq : Set -> Set -> Set
SetEq A B = HId {A -> TT} {B -> TT} _ _

which is, again, not necessarily a crime. In the OTT
paper, we have Prop a subuniverse of Set and Set
equations in Prop. Type constructors are injective
and disjoint: the intuition for set equality is that
it induces a representation-preserving coercion
from one side to the other, erasable at run-time.
That's certainly a more intensional notion than
isomorphism, but with quite a practical motivation.

In Coq, you can prove that Bool isn't Nat by
considering the predicate "has three distinct elements"
but you can't prove Nat isn't BTree in the same way.
My point is that this isn't so much a "fix" as a
distinct *choice*, of which I happen to be in favour.
There's more where that came from: "what is the
notion of equality hidden in pattern matching?" is
the key issue of pattern matching. It needs to pulled
out into the open.

Note, however, that making type constructors injective
only solves Dan's problem because he's lucky enough to
have a type constructor in the right place at the right
time. With the new type unification, my "boo" above
becomes ok, but if I switch to using recursively
computed vectors, it breaks again, because we are
unifying the application of a less special function.
The "woohoo" version is completely agnostic in this
respect: the right to treat the vectors as equal is
bought and paid for by the equation on their lengths.

The only effective general way to work with
heterogeneous equations is to ensure that you always
carry enough assumptions to explain why the
intensionally distinct types can be treated the same.
Het-eq is what lets you shift from working within one
given type to working within one given *telescope*:
equations between elements of arbitrary pairs of types
may be stated, but are not especially useful. There
used to be a metaphor about compassionate conservatism
which brought out this characteristic more clearly: I
think this is the first time that I regret its loss.

Funny old world

Conor