CODEWITHSUNDEEP
agda
Beanandbean
Beanandbean

Reputation: 61

Rewrite with proof-irrelevant equivalence relations in Agda?

I am quite new to type theories and dependently typed programming and is recently experimenting with various features of Agda. The following is a very simplified example I wrote of a record type C which contains multiple component records and some constraints that we can prove things with.

open import Relation.Binary.PropositionalEquality 

module Sample (α : Set) where
  record A (type : α) : Set where

  record B : Set where
    field
      type : α

  record C : Set where
    field
      b₁ : B
      b₂ : B
      eq : B.type b₁ ≡ B.type b₂

    conv : A (B.type b₁) → A (B.type b₂)
    conv a rewrite eq = a

It seems appealing to me that the constraint eq : B.type b₁ ≡ B.type b₂ should be declared irrelevant by adding a . in the front (or, in the latest dev version 2.6.0, to replace by an equivalence relation of sort Prop, e.g.

data _≡_ {ℓ} {α : Set ℓ} (x : α) : α → Prop ℓ where
  refl : x ≡ x

), so that two instances of type C with the same components can be directly unified via refl regardless of different proofs eq. However, either way, the program stops to compile because I cannot pattern match on an irrelevant value / Prop.

I would like to know whether it is possible for the same functionality to be implemented in Agda in any way, or that in general why it is impossible to rewrite with proof-irrelevant equivalence relations in Agda (technical support difficulties, or this breaks some parts of Agda's type theory, etc.)?

Upvotes: 3

Views: 236

Answers (1)

Jesper
Jesper

Reputation: 2955

This is currently not yet possible in Agda due to technical limitations: 'rewrite' is just syntactic sugar for a pattern match on refl, and currently pattern matching on irrelevant arguments is not permitted. In our paper at POPL '19 we describe a criterion for which datatypes in Prop are 'natural' and can thus be pattern matched on. I hope to add this criterion to Agda before the release of 2.6.1, but I cannot make any promises (help on the development of Agda is always welcome).

Upvotes: 2

Related Questions