[Agda] another possible without-K problem

[Jason Reed]

If I replace the definition of S1 with

module S where
 private
  data #S1 : Set where
       #base : #S1
       #f : #S1 → #S1
 S1 : Set
 S1 = #S1

 base : S1
 base = #base

open S

it still checks for me in darcs-checked-out agda. Is this what you mean by
hiding the fact that it's inductively defined?


On Wed, Jul 10, 2013 at 11:01 AM, Altenkirch Thorsten <
psztxa at exmail.nottingham.ac.uk> wrote:

>
>
> On 10/07/2013 15:52, "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.
>
> You are right since in the example S1 is just an inductive type this isn't
> really a problem.
>
> Is this still possible if one "hides" the fact that S1 is inductively
> defined?
> I guess this is more the problem that the current implementation of HITs
> is a bit of a hack.
>
> Disjointness was always built into pattern matching and it is hard to see
> how to avoid this.
> One only needs a microscopic universe, Bool with T : Bool -> Type to
> justify this.
>
> Thorsten
>
> > 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
> >>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130710/e51a174a/attachment.html