<div dir="ltr"><div>If I replace the definition of S1 with</div><div><br></div><div>module S where</div><div> private</div><div> data #S1 : Set where</div><div> #base : #S1</div><div> #f : #S1 → #S1</div><div>
S1 : Set</div><div> S1 = #S1</div><div><br></div><div> base : S1</div><div> base = #base</div><div><br></div><div style>open S</div><div style><br></div><div style>it still checks for me in darcs-checked-out agda. Is this what you mean by hiding the fact that it's inductively defined?</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jul 10, 2013 at 11:01 AM, Altenkirch Thorsten <span dir="ltr"><<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br>
<br>
On 10/07/2013 15:52, "Dan Licata" <<a href="mailto:drl@cs.cmu.edu">drl@cs.cmu.edu</a>> wrote:<br>
<br>
>Is this a bug or a design decision? It seems like this example is in<br>
>accord with the description of without-K in the release notes, but<br>
>that allowing matching when the indices are constructors has some<br>
>interesting consequences.<br>
<br>
</div>You are right since in the example S1 is just an inductive type this isn't<br>
really a problem.<br>
<br>
Is this still possible if one "hides" the fact that S1 is inductively<br>
defined?<br>
I guess this is more the problem that the current implementation of HITs<br>
is a bit of a hack.<br>
<br>
Disjointness was always built into pattern matching and it is hard to see<br>
how to avoid this.<br>
One only needs a microscopic universe, Bool with T : Bool -> Type to<br>
justify this.<br>
<span class="HOEnZb"><font color="#888888"><br>
Thorsten<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
> In particular, it means that, in a core<br>
>theory without universes, without-K pattern matching cannot be<br>
>compiled to J, because you can prove disjointness (and injectivity) of<br>
>constructors, and that bool is an hset (code below), just using<br>
>pattern matching on the identity type. As far as I know, disjointness<br>
>and the hset-ness of bool require a universe/large elims to prove. Of<br>
>course, Agda has universes, and it is possible that without-K pattern<br>
>matching could be compiled to J + uses of large elims to code up these<br>
>constructions on constructors. But I would personally prefer it if<br>
>without-K pattern matching did not build these things in, because it<br>
>means we need to use two hacks (rather than just one :) ) to implement<br>
>higher inductives.<br>
><br>
>-Dan<br>
><br>
>-- checks in Agda 2.3.2.1<br>
>{-# OPTIONS --without-K #-}<br>
><br>
>module WithoutK where<br>
><br>
> data Nat : Set where<br>
> Z : Nat<br>
> S : Nat -> Nat<br>
><br>
> data Bool : Set where<br>
> True : Bool<br>
> False : Bool<br>
><br>
> data Void : Set where<br>
><br>
> data _==_ {A : Set} (x : A) : A -> Set where<br>
> Refl : x == x<br>
><br>
> injective : {m n : Nat} -> S m == S n -> m == n<br>
> injective Refl = Refl<br>
><br>
> disjoint : {m : Nat} -> S m == Z -> Void<br>
> disjoint ()<br>
><br>
> bool-hset : (b : Bool) -> (p : b == b) -> p == Refl<br>
> bool-hset True Refl = Refl<br>
> bool-hset False Refl = Refl<br>
><br>
><br>
><br>
>On Wed, Jul 10, 2013 at 5:56 AM, Altenkirch Thorsten<br>
><<a href="mailto:psztxa@exmail.nottingham.ac.uk">psztxa@exmail.nottingham.ac.uk</a>> wrote:<br>
>> This looks like a bug – please add it to the bug tracker.<br>
>><br>
>> We really need to understand what we are doing when checking wether<br>
>>pattern<br>
>> satisfy the —without-K condition. It seems that Conor's work on<br>
>>translating<br>
>> pattern matching to eliminators (with J and K) would be a good starting<br>
>> point.<br>
>><br>
>> At the same time we know that many types support UIP by structure.<br>
>>Michael<br>
>> Hedberg showed that all types with a decidable equality support UIP and<br>
>>it<br>
>> is not hard to see that this can be extended to stable equality (non-not<br>
>> closed). (Little puzzle: without extensionality – are there any types<br>
>>which<br>
>> have stable but not decidable equality ?)<br>
>><br>
>> We also want to quantify over all HSets (I.e. types with UIP) and so on.<br>
>><br>
>> Thorsten<br>
>><br>
>> From: Jason Reed <<a href="mailto:jcreed@gmail.com">jcreed@gmail.com</a>><br>
>> Date: Tue, 9 Jul 2013 16:31:22 +0100<br>
>> To: "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>
>> Subject: [Agda] another possible without-K problem<br>
>><br>
>> I'm experiencing something that I think is a violation of the intent of<br>
>>the<br>
>> --without-K flag, similar to what Thorsten was talking about in<br>
>> <a href="https://lists.chalmers.se/pipermail/agda/2012/004104.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2012/004104.html</a>.<br>
>><br>
>> The following file checks fine for me under current darcs Agda:<br>
>><br>
>> <<<begin>>><br>
>> {-# OPTIONS --without-K #-}<br>
>><br>
>> module Test where<br>
>><br>
>> data S1 : Set where<br>
>> base : S1<br>
>><br>
>> module test where<br>
>> data _≡_ {A : Set} (a : A) : A → Set where<br>
>> refl : a ≡ a<br>
>><br>
>> bad : (p q : base ≡ base) -> p ≡ q<br>
>> bad refl refl = refl<br>
>><br>
>> module test2 where<br>
>> data _≡_ {A : Set} : A → A → Set where<br>
>> refl : {x : A} → x ≡ x<br>
>><br>
>> bad : (p q : base ≡ base) -> p ≡ q<br>
>> bad refl refl = refl<br>
>> <<<end>>><br>
>><br>
>> Note that this covers both the possible definitions of the identity type<br>
>> mentioned by Guillaume in<br>
>> <a href="https://lists.chalmers.se/pipermail/agda/2012/004105.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2012/004105.html</a><br>
>><br>
>> Any ideas what should be done here? Does the K-check need to be further<br>
>> strengthened when there aren't parameters around? Am I misunderstanding<br>
>> something trivial?<br>
>><br>
>><br>
>> This message and any attachment are intended solely for the addressee<br>
>>and<br>
>> may contain confidential information. If you have received this message<br>
>>in<br>
>> error, please send it back to me, and immediately delete it. Please<br>
>>do not<br>
>> use, copy or disclose the information contained in this message or in<br>
>>any<br>
>> attachment. Any views or opinions expressed by the author of this<br>
>>email do<br>
>> not necessarily reflect the views of the University of Nottingham.<br>
>><br>
>> This message has been checked for viruses but the contents of an<br>
>>attachment<br>
>> may still contain software viruses which could damage your computer<br>
>>system,<br>
>> you are advised to perform your own checks. Email communications with<br>
>>the<br>
>> University of Nottingham may be monitored as permitted by UK<br>
>>legislation.<br>
>><br>
>><br>
>><br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>><br>
<br>
</div></div></blockquote></div><br></div>