[Agda] Pattern matching on irrelevant data

[Dan Doel]

This change appears to have irrelevant equality elimination as a
special case. One has to be careful about this, because something like
the following can occur:

-- snip --

module EqIrr where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Relation.Unary
open import Relation.Nullary

open import Data.Empty

subst : ∀{i j} {A : Set i} (P : A → Set j) {x y : A} → .(x ≡ y) → P x → P y
subst P refl Px = Px

roll : .((¬ ⊥) ≡ ⊥)  → (⊥ → ⊥) → ⊥
roll eq = subst (λ T → T) eq

rick : .((¬ ⊥) ≡ ⊥) → ⊥ → ⊥ → ⊥
rick eq = subst (λ T → T) (sym eq)

rick-roll : .((¬ ⊥) ≡ ⊥) → ⊥
rick-roll eq = ω (roll eq ω)
 where
 ω : ⊥ → ⊥
 ω b = rick eq b b

-- rick-roll = λ. eq → ω (roll eq ω)
--   ⟨erase⟩
--           = ω (roll ω)
--           = rick (roll ω) (roll ω)
--           = rick (subst ω) (roll ω)
--           = subst (subst ω) (roll ω)
--           = subst ω (roll ω)
--           = ω (roll ω)

-- snip --

Since the equality argument is allegedly irrelevant to subst, it can
be erased, and subst just always computes. Currently this doesn't
happen, but it appears to be due to that version of subst simply
_never_ computing, even if refl is supplied directly (subst P refl Px
simply reduces to subst P _ Px).

This isn't a soundness issue, but it's a strong normalization issue,
as normalization may need to happen in inconsistent contexts, and
terms can loop if we don't get stuck on the neutral, false terms.

I'd also add: the irrelevance in Agda seems to be mixing two different
things. The reducing of irrelevant arguments to _ during type checking
seems motivated by the EPTS and similar stuff, which is tracking
parametricity of arguments, and supports checking-time erasure. The
matching-on-irrelevant stuff, including this new addition, but also on
⊤, ⊥, and the like, is motivated by proof irrelevance, though, which
supports only closed-term runtime erasure, hence the problem above.

In some cases, it seems safe to do the former's erasure for the latter
situation. But in general, they are different modalities, and if we
try to jam them all into one, I think we'll end up with ad-hoc rules
for how things work. For instance:

data ⊤ : Set where
  tt : ⊤

foo : .⊤ → ℕ
foo tt = 5

If I normalize 'foo tt', I get 'foo _'. We might decide that it should
evaluate to 5, and this is safe, but we cannot make a similar decision
for the identity type, because it will cause my listing above to
loop... unless we also keep track of what was 'erased' and use it to
decide whether the irrelevant match in fact matches, and so on.

On Mon, Oct 3, 2011 at 11:13 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hi folks,
>
> I just pushed a patch that allows one to match on an irrelevant argument,
> under the proviso that only one constructor matches.
>
> The reason why I implemented this feature is because I want to define
> functions by recursion on a deterministic termination predicate but not
> prove that its value does not depend on the derivation of that predicate.
>
> Please play around with this new feature and find bugs and inconsistencies.
> ;-)
>
> Here is an example (good old division, without sized types, but
> Bove-Capretta style):
>
> module Div where
>
> data _≡_ {A : Set}(a : A) : A → Set where
>  refl : a ≡ a
>
> data Nat : Set where
>  zero : Nat
>  suc  : Nat → Nat
>
> minus : Nat → Nat → Nat
> minus  zero    m      = zero
> minus (suc n)  zero   = suc n
> minus (suc n) (suc m) = minus n m
>
> {- definition we'd like to have, does not termination check
> div : Nat → Nat → Nat
> div zero    m = zero
> div (suc n) m = suc (div (minus n m) m)
> -}
>
> -- termination predicate
>
> data Div! (m : Nat) : Nat → Set where
>  zero : Div! m zero
>  suc  : ∀ {n} → Div! m (minus n m) → Div! m (suc n)
>
> div' : (n m : Nat) → .(Div! m n) → Nat
> div'  zero   m  zero   = zero
> div' (suc n) m (suc N) = suc (div' (minus n m) m N)
>
> -- irrelevance of termination argument
>
> irrDiv! : (n m : Nat)(d d' : Div! m n) → div' n m d ≡ div' n m d'
> irrDiv! n m d d' = refl
>
> Pay attention to the last line!
> We could have gotten the same result without irrelevance, but much more
> tedious.
>
> Here is another example, involving a universe definition:
> ( in test/succeed/)
>
> module TerminationOnIrrelevantArgument where
>
> data ⊥ : Set where
>
> data D : Set where
>  empty : D
>  pi    : D -> D -> D
>  other : D
>
> postulate
>  app : D -> D -> D
>
> mutual
>
>  data Ty : D -> Set where
>
>    Empty : Ty empty
>
>    Pi    : (a f : D) ->
>            (A : Ty a) ->
>            (F : (d : D) -> .(El a A d) -> Ty (app f d)) ->
>            Ty (pi a f)
>
>
>  El : (a : D) -> .(A : Ty a) -> D -> Set
>  El  empty    Empty         g = ⊥
>  El (pi a f) (Pi .a .f A F) g = (d : D) -> .(Ad : El a A d) ->
>                                 El (app f d) (F d Ad) (app g d)
>  El  other   ()             g
>
> -- Termination checking needs to look inside irrelevant arguments.
> -- This only works because the termination checker is syntactic
> -- and does not respect equality of irrelevant things!
>
> -- clearly, the derivation of Ty a does not matter when computing El
> cast : (a : D)(A A' : Ty a)(d : D) -> El a A d -> El a A' d
> cast a A A' d x = x
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>