[Agda] Re: wait whaaat
Dan Licata
drl at cs.cmu.edu
Tue Jul 9 18:04:05 CEST 2013
I think the relevant question is "what should without-K do when the indices are
constructors?". Note that Agda won't accept "bad" if you replace S1 and
base with a postulate or variable or make them abstract.
However, this is an important question, since we use (private) constructors to
implement higher inductive types with definitional computation rules.
I would prefer that without-K did not allow this match.
However, even at present, a workaround is to implement higher inductives
using the "pair with (unit -> unit)"
trick that I proposed when Nisse noticed that Agda still lets you do
an absurd match on private datatypes. This also blocks your example.
I've attached a sample below.
BTW, did --without-K always allow matching on constructors?
I've been using an old version of Agda (2.3.0 I think) until just this week, but I
no longer have the old version or the ghc that it compiled on to test.
-Dan
{-# OPTIONS --without-K #-}
module Test where
record Unit : Set where
constructor <>
data Void : Set where
data _≡_ {A : Set} (a : A) : A → Set where
refl : a ≡ a
-- simplification of how we implement HITs
module Interval where
private
data I' : Set where
zero' : I'
one' : I'
I : Set
I = I'
zero : I
zero = zero'
one : I
one = one'
module Bad where
open Interval
-- Agda allows a disjointness match, even though I don't want it.
bad1 : (zero ≡ one) → Void
bad1 ()
-- Agda allows UIP, even though I don't want it.
bad2 : (p : one ≡ one) → p ≡ refl
bad2 refl = refl
module IntervalFn where
private
data I' : Set where
zero' : I'
one' : I'
data I'' : Set where
i'' : I' -> (Unit -> Unit) -> I''
I : Set
I = I''
zero : I
zero = i'' zero' _
one : I
one = i'' one' _
module Good where
-- The presence of the function defeats the "constructors (or
-- literals) applied to variables" check:
open IntervalFn
{-
good1 : (zero ≡ one) → Void
good1 ()
Fails with error message
/Users/drl/tmp/Test.agda:63,3-11
The indices
.Test.IntervalFn.I''.i'' .Test.IntervalFn.I'.one' (λ _ → <>)
are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the clause good1 () has type zero ≡ one → Void
-}
{-
good2 : (p : one ≡ one) → p ≡ refl
good2 refl = refl
Fails with error message
/Users/drl/tmp/Test.agda:75,9-13
The indices
.Test.IntervalFn.I''.i'' .Test.IntervalFn.I'.one' (λ _ → <>)
are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the pattern refl has type one ≡ one
-}
On Jul09, Jason Reed wrote:
> I'm experiencing something that I think is a violation of the intent of the
> --without-K flag, similar to what Thorsten was talking about in
> https://lists.chalmers.se/pipermail/agda/2012/004104.html.
>
> The following file checks fine for me under current darcs Agda:
>
> <<<begin>>>
> {-# OPTIONS --without-K #-}
>
> module Test where
>
> data S1 : Set where
> base : S1
>
> module test where
> data _≡_ {A : Set} (a : A) : A → Set where
> refl : a ≡ a
>
> bad : (p q : base ≡ base) -> p ≡ q
> bad refl refl = refl
>
> module test2 where
> data _≡_ {A : Set} : A → A → Set where
> refl : {x : A} → x ≡ x
>
> bad : (p q : base ≡ base) -> p ≡ q
> bad refl refl = refl
> <<<End>>>
>
> Note that this covers both the possible definitions of the identity type
> mentioned by Guillaume in
> https://lists.chalmers.se/pipermail/agda/2012/004105.html
>
> Any ideas what should be done here? Does the K-check need to be further
> strengthened when there aren't parameters around? Am I misunderstanding
> something trivial?
>
>
> On Tue, Jul 9, 2013 at 11:06 AM, Jason Reed <jcreed at gmail.com> wrote:
>
> > Nope, that doesn't help me.
> >
> > The following checks for me in fresh-from-darcs Agda 2.3.3, I'd be curious
> > if you observe anything different:
> >
> > {-# OPTIONS --without-K #-}
> >
> > module Test where
> >
> > data S1 : Set where
> > base : S1
> >
> > module test where
> > data _≡_ {A : Set} (a : A) : A → Set where
> > refl : a ≡ a
> >
> > bad : (p q : base ≡ base) -> p ≡ q
> > bad refl refl = refl
> >
> > module test2 where
> > data _≡_ {A : Set} : A → A → Set where
> > refl : {x : A} → x ≡ x
> >
> > bad : (p q : base ≡ base) -> p ≡ q
> > bad refl refl = refl
> >
> >
> >
> > On Tue, Jul 9, 2013 at 11:01 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> >
> >> Also, IIRC, if you use the
> >>
> >> data Id {A : Set} (a : A) : A -> Set where
> >> refl : Id a a
> >>
> >> definition, no one was able to trip this bug. It was related to
> >> the parameter/index disctinction.
> >>
> >> -Dan
> >>
> >
> >
More information about the Agda
mailing list