[Agda] change in handling of irrelevant parameters (bug?)

[Andreas Abel]

A bug. Should be fixed in the darcs version now.

On 3/15/11 9:20 AM, Darin Morrison wrote:
>
> On 15 Mar 2011, at 12:35, Nils Anders Danielsson wrote:
>
>> On 2011-03-15 12:02, Darin Morrison wrote:
>>> I noticed a change in the handling of irrelevant parameters between
>>> 2.2.9 and 2.2.10 which I think is beyond having irrelevant projections
>>> enabled by default. [...]
>>
>> I don't know too much about irrelevance, but this doesn't look good.
>
>  From the 2.2.8 release notes, it says:
>
>>      Irrelevant arguments can only be used in irrelevant contexts.
>>      Consider the following subset type:
>>
>>        data Subset (A : Set) (P : A → Set) : Set where
>>          _#_ : (elem : A) → .(P elem) → Subset A P
>>
>>      The following two uses are fine:
>>
>>        elimSubset : ∀ {A C : Set} {P} →
>>                     Subset A P → ((a : A) → .(P a) → C) → C
>>        elimSubset (a # p) k = k a p
>>
>>        elem : {A : Set} {P : A → Set} → Subset A P → A
>>        elem (x # p) = x
>>
>>      However, if we try to project out the proof component, then Agda
>>      complains that “variable p is declared irrelevant, so it cannot be
>>      used here”:
>>
>>        prjProof : ∀ {A P} (x : Subset A P) → P (elem x)
>>        prjProof (a # p) = p
>
> This restriction to using irrelevant arguments in irrelevant contexts is what I would expect and that is what seems to have been changed in the most recent release.
>
> However, in the 2.2.10 release notes, it states the following:
>
>>     Postulates and functions can be marked as irrelevant by prefixing
>>     the name with a dot when the name is declared. Example:
>>
>>       postulate
>>         .irrelevant : {A : Set} → .A → A
>>
>>     Irrelevant names may only be used in irrelevant positions or in
>>     definitions of things which have been declared irrelevant.
>>
>>     The axiom irrelevant above can be used to define a projection from
>>     an irrelevant record field:
>>
>>       data Subset (A : Set) (P : A → Set) : Set where
>>         _#_ : (a : A) → .(P a) → Subset A P
>>
>>       elem : ∀ {A P} → Subset A P → A
>>       elem (a # p) = a
>>
>>       .certificate : ∀ {A P} (x : Subset A P) → P (elem x)
>>       certificate (a # p) = irrelevant p
>>
>>     The right-hand side of certificate is relevant, so we cannot define
>>
>>       certificate (a # p) = p
>>
>>     (because p is irrelevant). However, certificate is declared to be
>>     irrelevant, so it can use the axiom irrelevant. Furthermore the
>>     first argument of the axiom is irrelevant, which means that
>>     irrelevant p is well-formed.
>
> This makes me think that in the code you posted, 'proj' should have to be marked as irrelevant to typecheck, e.g.,
>
>    data Bool : Set where
>      true : Bool
>      false : Bool
>
>    data _≡_ {A} (x : A) : A → Set where
>      refl : x ≡ x
>
>    resp : ∀ {A₁ A₂ x₁ x₂} (f : A₁ → A₂) → x₁ ≡ x₂ → f x₁ ≡ f x₂
>    resp f refl = refl
>
>    data D : Set where
>      c : .Bool → D
>
>    irr : c true ≡ c false
>    irr = refl
>
>    .proj : D → Bool
>    proj (c x) = x
>
>    bad : proj (c true) ≡ proj (c false)
>    bad = resp proj irr
>
> In this case, 'bad' would fail to type check for a more expected reason, namely that 'proj' is being used in a non-relevant position.
>
> So maybe the problem is just that the condition mentioned in the 2.2.10 release notes is not properly enforced?
>
> This is pretty important for me as I have a large development that relies on irrelevant fields quite heavily.  Without them, the code type-checks far too slowly to be usable.  I don't think I'm unintentionally relying on bugs in the implementation in my proofs but now I'm a little bit worried...
>
> Cheers,
> Darin
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
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/