Search code examples
idrisdependent-type

Working with types up to a certain equivalence

Suppose we'd like to represent (signed) integers as the Grothendieck group over naturals (or, in other words, as a pair (m, n), where the integer that's understood is m - n):

data ZTy : Type where
  MkZ : (m, n : Nat) -> ZTy

Now the (structural) equality that the language gives us for free is no longer what we want: instead, we only care about a certain equivalence relation (namely, (m1, n1) ~ (m2, n2) iff m1 + n2 = m2 + n1). No biggie, let's write this down!

data Equiv : ZTy -> ZTy -> Type where
  MkEquiv : (prf : m1 + n2  = m2 + n1) -> Equiv (MkZ m1 n1) (MkZ m2 n2)

But working with this gets messy really quickly. Any argument of type prop Const (for prop : ZTy -> Type) is replaced with (k : ZTy) -> (k `EqZ` Const) -> prop k, to say the least (as a more applied example, I'm struggling with writing down the two-sided induction proof for this type, and I'm still not sure I got even the signature of that term right).

Moreover, a function like replaceZ : {P : ZTy -> Type} -> (k1 `Equiv` k2) -> P k1 -> P k2 (obviously) does not exist, but I cannot find a better candidate. As an interesting side note/observation, if we don't export the definition of ZTy, no client-code P can observe it, and this function would make sense for any P defined in any other module, but looks like we cannot internalize this within the language.

Another thing I have in mind is to limit the set of predicates to the ones that hold under equivalence relations. That is, replacing P : ZTy -> Type with something like P : ZTy -> Type, pAdmissible : ZPred P where ZPred carries along a proof of its invariance under the equivalence relation:

data ZPred : Type -> Type where
  MkZPred : {P : ZTy -> Type} ->
            (preservesEquiv : {k1, k2 : ZTy} -> (k1 `Equiv` k2) -> P k1 -> P k2) ->
            ZPred P

Anyway, what's the common approach to working with such types? Is there anything else that would work nicely?

I've also heard something about quotient types, but I don't know much.

Solution

  • Coq describes these situations with a rich language of "relation combinators", which is better version of your last idea. I'll translate it. You have

    ZTy : Type -- as yours

    And you proceed to define relations and functions on relations:

    -- if r : Relation t and x, y : t, we say x and y are related by r iff r x y is inhabited
Relation : Type -> Type
Relation t = t -> t -> Type

-- if x, y : ZTy, we say x and y are (Equiv)alent iff Equiv x y is inhabited, etc.
Equiv : Relation ZTy  -- as yours
(=)   : Relation a    -- standard
Iso   : Relation Type -- standard

-- f and f' are related by a ==> r if arguments related by a end up related by r
(==>) : Relation a -> Relation b -> Relation (a -> b)
(==>) xr fxr = \f, f' => (x x' : a) -> xr x x' -> fxr (f x) (f' x')
infixr 10 ==>

    The idea is that Equiv, (=), and Iso are all equality relations. Equiv and (=) are two different notions of equality on ZTy, and (=) and Iso are two notions of equality on Type. (==>) combines relations into new relations.

    If you have

    P : ZTy -> Type

    You would like to say that Equivalent arguments map to Isomorphic types. That is, you need

    replaceP : (x x' : ZTy) -> Equiv x x' -> Iso (P x) (P x')

    How can the language of relations help? Well, replaceP is essentially saying that P is "equal" to itself, under the relation Equiv ==> Iso (N.B. Equiv ==> Iso is not an equivalence, but the only thing it's missing is reflexivity.) If a function is not "equal" to itself under Equiv ==> Iso, then that's a little bit like a "contradiction", and that function "doesn't exist" in your universe. Or, rather, if you want to write a function

    f : (ZTy -> Type) -> ?whatever

    You can restrict yourself to the correct kind of functions by requiring a proof argument like so

    Proper : Relation a -> a -> Type
Proper r x = r x x

f : (P : ZTy -> Type) -> Proper (Equiv ==> Iso) P -> ?whatever

    Usually, though, you leave off the proof unless absolutely needed. In fact, the standard library already contains a lot of functions on ZTy, like

    concatMap : Monoid m => (ZTy -> m) -> List ZTy -> m

    Instead of writing a concatMap taking a proof argument, you really only have to write a proof about concatMap:

    concatMapProper : Proper ((Equiv ==> (=)) ==> Pairwise Equiv ==> (=))
-- you'd really abstract over Equiv and (=), but then you need classes for Relations
Pairwise : Relation a -> Relation [a] -- as you may guess

    I'm not sure what induction principle you want to write, so I'll just leave that alone. However, your concern that

    proof : Property Constant

    always needs to be replaced with

    proof : (k : ZTy) -> Equiv k Constant -> Property k

    is only partially well-founded. If you already have

    PropertyProper : Proper (Equiv ==> Iso) Property

    which you very likely should, then you can write proper : Property Constant, and just shove it through PropertyProper to generalize it when needed. (Or, write proper with the general signature by using the simple definition with PropertyProper on top). You can't get out of writing a proof somewhere though, because it simply isn't that trivial.

    It's also worth noting that (==>) has uses other than as the argument to Proper. It serves as a general purpose extensional equality:

    abs1 : ZTy -> Nat
abs1 (MkZ l r) = go l r
  where go (S n) (S m) = go n m
        go Z     m     = m
        go n     Z     = n
abs2 : ZTy -> Nat
abs2 (MkZ l r) = max l r - min l r

absEq : (Equiv ==> (=)) abs1 abs2
--    : (x x' : ZTy) -> Equiv x x' -> abs1 x = abs2 x'