[Agda] another possible without-K problem

[drl at cs.cmu.edu]

If you make S1 and base abstract, then the example is not accepted.  

However, the current implementation of HITs uses private, not abstract,
and in this case the example is accepted (private is what gives you the
definitional behavior).  Unless you use the unit->unit
trick, so that base is no longer a constructor applied to variables.

What would happen if without-K restricted matching to only distinct
variables, not constructors applied to variables?  This would seem to
rule out the examples below, including disjointness.  

However, what I'd really like is:

- parameters can be anything
- indices must be distinct variables
- unless the index type is an hset, in which case indices can be
  anything

Assuming the identity type is defined in the Paulin-Mohring style, this
would allow Paulin-Mohring pattern matching (e.g. you can split on 
M == x for any term M), and let you mix in the usual with-K
Agda programming.

I remember an issue with parameters from the bug you noticed a while
ago.  Would my proposal above run afoul of that?  

-Dan

On Jul10, Altenkirch Thorsten 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
> >>
>