<div dir="ltr"><div><div><div><div><div><div><div>(If I&#39;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.<br>


<br></div>It&#39;s pretty easy to see that this is not going to work if the &#39;data&#39; 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.<br>


<br></div>Getting rid of this is a big deal, though. If you just throw it away, then I don&#39;t think definitions like the following work:<br><br></div>    zip : {A B : Set} {n : ℕ} -&gt; Vec A n -&gt; Vec B n -&gt; Vec (A × B) n<br>


</div>    zip [] [] = []<br></div>    zip (x :: xs) (y :: ys) = (x , y) :: zip xs ys<br><br></div>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&#39;t allowed that, then we must write these cases, and explicitly appeal to disjointness proofs. Except, Agda (for instance) isn&#39;t equipped for such a thing; we have no way of accessing a propositional &#39;zero = suc n&#39; in those cases to hand off to a lemma.<br>


<br></div><div>Also, you presumably lose the ability to write things like:<br><br></div><div>    foo : ∀ n -&gt; Fin n -&gt; ...<br></div><div>    foo zero () ...<br>    ...</div><div><br></div><div>and similarly have no real recourse for that case in Agda.<br>
<br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jul 10, 2013 at 10:52 AM, Dan Licata <span dir="ltr">&lt;<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.  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 -&gt; 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 -&gt; Set where<br>
    Refl : x == x<br>
<br>
  injective : {m n : Nat} -&gt; S m == S n -&gt; m == n<br>
  injective Refl = Refl<br>
<br>
  disjoint : {m : Nat} -&gt; S m == Z -&gt; Void<br>
  disjoint ()<br>
<br>
  bool-hset : (b : Bool) -&gt; (p : b == b) -&gt; p == Refl<br>
  bool-hset True Refl = Refl<br>
  bool-hset False Refl = Refl<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
On Wed, Jul 10, 2013 at 5:56 AM, Altenkirch Thorsten<br>
&lt;<a href="mailto:psztxa@exmail.nottingham.ac.uk">psztxa@exmail.nottingham.ac.uk</a>&gt; wrote:<br>
&gt; This looks like a bug – please add it to the bug tracker.<br>
&gt;<br>
&gt; We really need to understand what we are doing when checking wether pattern<br>
&gt; satisfy the —without-K condition. It seems that Conor&#39;s work on translating<br>
&gt; pattern matching to eliminators (with J and K) would be a good starting<br>
&gt; point.<br>
&gt;<br>
&gt; At the same time we know that many types support UIP by structure. Michael<br>
&gt; Hedberg showed that all types with a decidable equality support UIP and it<br>
&gt; is not hard to see that this can be extended to stable equality (non-not<br>
&gt; closed). (Little puzzle: without extensionality – are there any types which<br>
&gt; have stable but not decidable equality ?)<br>
&gt;<br>
&gt; We also want to quantify over all HSets (I.e. types with UIP) and so on.<br>
&gt;<br>
&gt; Thorsten<br>
&gt;<br>
&gt; From: Jason Reed &lt;<a href="mailto:jcreed@gmail.com">jcreed@gmail.com</a>&gt;<br>
&gt; Date: Tue, 9 Jul 2013 16:31:22 +0100<br>
&gt; To: &quot;<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>&quot; &lt;<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>&gt;<br>
&gt; Subject: [Agda] another possible without-K problem<br>
&gt;<br>
&gt; I&#39;m experiencing something that I think is a violation of the intent of the<br>
&gt; --without-K flag, similar to what Thorsten was talking about in<br>
&gt; <a href="https://lists.chalmers.se/pipermail/agda/2012/004104.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2012/004104.html</a>.<br>
&gt;<br>
&gt; The following file checks fine for me under current darcs Agda:<br>
&gt;<br>
&gt; &lt;&lt;&lt;begin&gt;&gt;&gt;<br>
&gt; {-# OPTIONS --without-K #-}<br>
&gt;<br>
&gt; module Test where<br>
&gt;<br>
&gt; data S1 : Set where<br>
&gt;     base : S1<br>
&gt;<br>
&gt; module test where<br>
&gt;    data _≡_ {A : Set} (a : A) : A → Set where<br>
&gt;     refl : a ≡ a<br>
&gt;<br>
&gt;    bad : (p q : base ≡ base) -&gt; p ≡ q<br>
&gt;    bad refl refl = refl<br>
&gt;<br>
&gt; module test2 where<br>
&gt;    data _≡_ {A : Set} : A → A → Set where<br>
&gt;        refl : {x : A} → x ≡ x<br>
&gt;<br>
&gt;    bad : (p q : base ≡ base) -&gt; p ≡ q<br>
&gt;    bad refl refl = refl<br>
&gt; &lt;&lt;&lt;end&gt;&gt;&gt;<br>
&gt;<br>
&gt; Note that this covers both the possible definitions of the identity type<br>
&gt; mentioned by Guillaume in<br>
&gt; <a href="https://lists.chalmers.se/pipermail/agda/2012/004105.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2012/004105.html</a><br>
&gt;<br>
&gt; Any ideas what should be done here? Does the K-check need to be further<br>
&gt; strengthened when there aren&#39;t parameters around? Am I misunderstanding<br>
&gt; something trivial?<br>
&gt;<br>
&gt;<br>
&gt; This message and any attachment are intended solely for the addressee and<br>
&gt; may contain confidential information. If you have received this message in<br>
&gt; error, please send it back to me, and immediately delete it.   Please do not<br>
&gt; use, copy or disclose the information contained in this message or in any<br>
&gt; attachment.  Any views or opinions expressed by the author of this email do<br>
&gt; not necessarily reflect the views of the University of Nottingham.<br>
&gt;<br>
&gt; This message has been checked for viruses but the contents of an attachment<br>
&gt; may still contain software viruses which could damage your computer system,<br>
&gt; you are advised to perform your own checks. Email communications with the<br>
&gt; University of Nottingham may be monitored as permitted by UK legislation.<br>
&gt;<br>
&gt;<br>
&gt;<br>
</div></div><div class="HOEnZb"><div class="h5">&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<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>
</div></div></blockquote></div><br></div>