[Agda] another possible without-K problem

[Dan Doel]

(If I'm not mistaken) way back in Eliminating Dependent Pattern Matching
(at least), it is remarked that the translation relies on both K (or, an
appropriate heterogeneous equality) and disjointness and injectivity of
constructors. So it would not be a surprise that removing K does not remove
disjointness of constructors.

It's pretty easy to see that this is not going to work if the 'data'
construct that allows for pattern matching does some form of quotienting,
though. And higher inductive types allow you to assert that something is a
(normal) quotient, among other things.

Getting rid of this is a big deal, though. If you just throw it away, then
I don't think definitions like the following work:

    zip : {A B : Set} {n : ℕ} -> Vec A n -> Vec B n -> Vec (A × B) n
    zip [] [] = []
    zip (x :: xs) (y :: ys) = (x , y) :: zip xs ys

The ability to elide the two other cases relies on the fact that they cause
unification errors, zero ≠ suc n. But, this presumes disjointness of the
natural numbers. If we aren't allowed that, then we must write these cases,
and explicitly appeal to disjointness proofs. Except, Agda (for instance)
isn't equipped for such a thing; we have no way of accessing a
propositional 'zero = suc n' in those cases to hand off to a lemma.

Also, you presumably lose the ability to write things like:

    foo : ∀ n -> Fin n -> ...
    foo zero () ...
    ...

and similarly have no real recourse for that case in Agda.



On Wed, Jul 10, 2013 at 10:52 AM, Dan Licata <drl at cs.cmu.edu> wrote:

> Is this a bug or a design decision?  It seems like this example is in
> accord with the description of without-K in the release notes, but
> that allowing matching when the indices are constructors has some
> interesting consequences.  In particular, it means that, in a core
> theory without universes, without-K pattern matching cannot be
> compiled to J, because you can prove disjointness (and injectivity) of
> constructors, and that bool is an hset (code below), just using
> pattern matching on the identity type.  As far as I know, disjointness
> and the hset-ness of bool require a universe/large elims to prove.  Of
> course, Agda has universes, and it is possible that without-K pattern
> matching could be compiled to J + uses of large elims to code up these
> constructions on constructors.  But I would personally prefer it if
> without-K pattern matching did not build these things in, because it
> means we need to use two hacks (rather than just one :) ) to implement
> higher inductives.
>
> -Dan
>
> -- checks in Agda 2.3.2.1
> {-# OPTIONS --without-K #-}
>
> module WithoutK where
>
>   data Nat : Set where
>     Z : Nat
>     S : Nat -> Nat
>
>   data Bool : Set where
>     True : Bool
>     False : Bool
>
>   data Void : Set where
>
>   data _==_ {A : Set} (x : A) : A -> Set where
>     Refl : x == x
>
>   injective : {m n : Nat} -> S m == S n -> m == n
>   injective Refl = Refl
>
>   disjoint : {m : Nat} -> S m == Z -> Void
>   disjoint ()
>
>   bool-hset : (b : Bool) -> (p : b == b) -> p == Refl
>   bool-hset True Refl = Refl
>   bool-hset False Refl = Refl
>
>
>
> On Wed, Jul 10, 2013 at 5:56 AM, Altenkirch Thorsten
> <psztxa at exmail.nottingham.ac.uk> wrote:
> > This looks like a bug – please add it to the bug tracker.
> >
> > We really need to understand what we are doing when checking wether
> pattern
> > satisfy the —without-K condition. It seems that Conor's work on
> translating
> > pattern matching to eliminators (with J and K) would be a good starting
> > point.
> >
> > At the same time we know that many types support UIP by structure.
> Michael
> > Hedberg showed that all types with a decidable equality support UIP and
> it
> > is not hard to see that this can be extended to stable equality (non-not
> > closed). (Little puzzle: without extensionality – are there any types
> which
> > have stable but not decidable equality ?)
> >
> > We also want to quantify over all HSets (I.e. types with UIP) and so on.
> >
> > Thorsten
> >
> > From: Jason Reed <jcreed at gmail.com>
> > Date: Tue, 9 Jul 2013 16:31:22 +0100
> > To: "agda at lists.chalmers.se" <agda at lists.chalmers.se>
> > Subject: [Agda] another possible without-K problem
> >
> > 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?
> >
> >
> > This message and any attachment are intended solely for the addressee and
> > may contain confidential information. If you have received this message
> in
> > error, please send it back to me, and immediately delete it.   Please do
> not
> > use, copy or disclose the information contained in this message or in any
> > attachment.  Any views or opinions expressed by the author of this email
> do
> > not necessarily reflect the views of the University of Nottingham.
> >
> > This message has been checked for viruses but the contents of an
> attachment
> > may still contain software viruses which could damage your computer
> system,
> > you are advised to perform your own checks. Email communications with the
> > University of Nottingham may be monitored as permitted by UK legislation.
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130710/65ec64b2/attachment-0001.html