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