[Agda] another possible without-K problem

[Dan Licata]

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
>