<div dir="ltr"><div><div>All,<br><br></div>The blog post I promised: <a href="http://serendependy.blogspot.com/2014/11/with-great-power-great-intractibility.html">http://serendependy.blogspot.com/2014/11/with-great-power-great-intractibility.html</a><br><br></div>Feel free to add comments or suggestions on the blog itself or here.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 6, 2014 at 3:39 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Note that I am in the process of outlawing `with` on variables bound by module telescopes (because of the issue 1342 that came up during this discussion).<br>
<br>
Cheers,<br>
Andreas<span class=""><br>
<br>
On 05.11.2014 23:53, Christopher Jenkins wrote:<br>
</span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
Alright, two people is enough to motivate me. I will try to have a first<br>
blog post out this weekend, mostly dealing with pattern-matching after a<br>
rewrite and the basic concept of `with', with more to follow.<br>
<br>
On Wed, Nov 5, 2014 at 2:21 AM, Arseniy Alekseyev<br></span><span class="">
<<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a> <mailto:<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@<u></u>gmail.com</a>>> wrote:<br>
<br>
  Oh wow, I should have tried that. I don't understand why this works at<br>
  all. Note that none of these compile for me:<br>
<br>
    y | true  = id {A = (q : Bool) → x ≡ z q} (λ { true → refl ; false<br>
  → refl }) -- x != true of type Bool<br>
<br>
    y | true  = id {A = (q : Bool) → true ≡ z q} (λ { true → refl ;<br>
  false → refl }) -- true != x of type Bool<br>
<br>
  However, even more confusingly, this one does work:<br>
<br>
    y | true  = id {A = _} (λ { true → refl ; false → refl })<br>
<br>
  So what's the value of underscore it infers then?<br>
  Can anybody explain what's going on?<br>
<br>
  As for the code smell part, I think you can only smell it on toy<br>
  examples, not on the "real" ones.<br>
<br>
  On 5 November 2014 01:28, Christopher Jenkins <<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a><br></span><span class="">
  <mailto:<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a>>> wrote:<br>
   ><br>
   ><br>
   > On Tue, Nov 4, 2014 at 5:18 PM, Arseniy Alekseyev<br>
   > <<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a><br></span><span class="">
  <mailto:<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@<u></u>gmail.com</a>>> wrote:<br>
   >><br>
   >> That was not a genuine attempt to prove `y : ∀ q → x ≡ z q`. Instead<br>
   >> that was an example of `with` rewriting the goal from (as you<br>
   >> demonstrated!) provable one into (as I assert) non-provable one. I<br>
   >> think that's the property of `with` that's causing you grief<br>
  when you<br>
   >> re-order or nest them in a bad way.<br>
   >><br>
   > Ah, makes sense. Though of course you could probably continue on<br>
  to prove<br>
   > the goal by pattern-matching on a lambda argument introduced in<br>
  both cases,<br>
   > but by that point hopefully someone would see the code smell.<br>
   ><br>
   > Actually, decided to include it anyway, so you could smell the<br>
  smelly code<br>
   > smell:<br>
   ><br>
   >  y : ∀ q → x ≡ z q<br>
   >  y with x<br>
   >  y | true  = λ { true → refl ; false → refl }<br>
   >  y | false = λ { true → refl ; false → refl }<br>
   ><br>
   >><br>
   >> On 4 November 2014 22:43, Christopher Jenkins<br></span>
  <<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a> <mailto:<a href="mailto:cjenkin1@trinity.edu" target="_blank">cjenkin1@trinity.edu</a>>><span class=""><br>
   >> wrote:<br>
   >> ><br>
   >> ><br>
   >> > On Mon, Nov 3, 2014 at 2:38 PM, Arseniy Alekseyev<br>
   >> > <<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a><br></span><div><div class="h5">
  <mailto:<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@<u></u>gmail.com</a>>> wrote:<br>
   >> >><br>
   >> >> You are right, there is not much point. I was trying to point<br>
  out that<br>
   >> >> it's the "proper expression" part that makes `with` complicated.<br>
   >> >><br>
   >> >> Unfortunately, that's not even true. In the following<br>
  example, I don't<br>
   >> >> think you can fill the holes.<br>
   >> >><br>
   >> >> f : Bool → Bool<br>
   >> >> f x = true where<br>
   >> >><br>
   >> >>  z : Bool → Bool<br>
   >> >>  z true = x<br>
   >> >>  z false = x<br>
   >> >><br>
   >> >>  y : ∀ q → x ≡ z q<br>
   >> >>  y with x<br>
   >> >>  y | true = {!!}<br>
   >> >>  y | false = {!!}<br>
   >> >><br>
   >> >><br>
   >> ><br>
   >> > I'm not entirely sure why you would expect that approach to be<br>
  fruitful.<br>
   >> > Essentially, what you're trying to do is unwind the<br>
  computational nature<br>
   >> > of<br>
   >> > `z', which is defined by case analysis on its argument (in<br>
  this case q).<br>
   >> > To<br>
   >> > trigger the rules, you would have to bring q into scope and<br>
  inspect q,<br>
   >> > which<br>
   >> > would then lead to `z true' and `z false' in the equations,<br>
   >> > respectively,<br>
   >> > and Agda will then go on to normalize the goals as `x \== x'<br>
   >> ><br>
   >> > f : Bool → Bool<br>
   >> > f x = true where<br>
   >> >  z : Bool → Bool<br>
   >> >  z true = x<br>
   >> >  z false = x<br>
   >> ><br>
   >> >  y : ∀ q → x ≡ z q<br>
   >> >  y true = {!!} -- Goal: x ≡ x<br>
   >> >  y false = {!!} -- Goal: x ≡ x<br>
   >> ><br>
   >> > I have actually been thinking about writing a blog post<br>
  targeted at<br>
   >> > newbies<br>
   >> > (such as myself) on the sometimes unintuitive behaviour of<br>
  `with' (and<br>
   >> > in<br>
   >> > particular, `rewrite'). Should anyone be interested I can send<br>
  a link on<br>
   >> > this email chain once I have written it.<br>
   >> ><br>
   >> ><br>
   >> >><br>
   >> >> On 3 November 2014 10:59, Andreas Abel<br></div></div><div><div class="h5">
  <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a> <mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.<u></u>de</a>>> wrote:<br>
   >> >> > On 03.11.2014 09:47, Arseniy Alekseyev wrote:<br>
   >> >> >> I think the problem goes away if you<br>
   >> >> >> only use `with x` where `x` is a variable.<br>
   >> >> ><br>
   >> >> > Mmh, why use `with` at all then? You could directly split<br>
  on the<br>
   >> >> > variable<br>
   >> >> > `x`. I thought the only reason to use `with` was when you<br>
  wanted to<br>
   >> >> > case on<br>
   >> >> > a proper expression and refine your type in the<br>
  with-branches...<br>
   >> >> ><br>
   >> >> ><br>
   >> >> ><br>
   >> >> > On 03.11.2014 09:47, Arseniy Alekseyev wrote:<br>
   >> >> >><br>
   >> >> >> Indeed that's the usual Agda behaviour.<br>
   >> >> >> Here the reason seems to be an additional occurrence of<br>
  `lookup k<br>
   >> >> >> ps`<br>
   >> >> >> in the context produced by pattern-match on `no`.<br>
   >> >> >> You see, `with expr` only rewrites the occurrences of<br>
  `expr` present<br>
   >> >> >> in the enclosing context, so the new occurrences inside<br>
  the body of<br>
   >> >> >> `with` don't get rewritten (and you do want it rewritten<br>
  in this<br>
   >> >> >> case).<br>
   >> >> >><br>
   >> >> >> I do agree this is confusing. I think the problem goes<br>
  away if you<br>
   >> >> >> only use `with x` where `x` is a variable. That makes<br>
  `with` much<br>
   >> >> >> less<br>
   >> >> >> useful though. You can also avoid `with` altogether and<br>
  write the<br>
   >> >> >> helper functions by hand (that's what `with` is doing<br>
  after all!).<br>
   >> >> >><br>
   >> >> >> On 2 November 2014 17:14, <<a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a><br></div></div><div><div class="h5">
  <mailto:<a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a><u></u>>> wrote:<br>
   >> >> >>><br>
   >> >> >>> People,<br>
   >> >> >>><br>
   >> >> >>> Having the proof<br>
   >> >> >>><br>
   >> >> >>>  prove : (k∈ks : k ∈ ks) → proj₂ (lookupIf∈ k (p ∷ ps)<br>
  k∈k':ks) ≡<br>
   >> >> >>>               proj₂ (lookupIf∈ k ps k∈ks)<br>
   >> >> >>>  prove k∈ks with k ≟ k'<br>
   >> >> >>> --<br>
   >> >> >>> (I)<br>
   >> >> >>><br>
   >> >> >>>  ... | yes k≡k' = ⊥-elim $ k≉k' k≡k'<br>
   >> >> >>>  ... | no _   with lookup k ps<br>
   >> >> >>>  ...        | inj₠_  = PE.refl<br>
   >> >> >>>  ...        | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks<br>
   >> >> >>><br>
   >> >> >>><br>
   >> >> >>> (I do not give the complete code),<br>
   >> >> >>><br>
   >> >> >>> I try to rewrite it in a bit simpler way by joining it<br>
  into one<br>
   >> >> >>> `with'<br>
   >> >> >>> clause:<br>
   >> >> >>><br>
   >> >> >>><br>
   >> >> >>>  prove k∈ks with k ≟ k' | lookup k ps<br>
   >> >> >>> --<br>
   >> >> >>> (II)<br>
   >> >> >>><br>
   >> >> >>>  ... | yes k≡k' | _     = ⊥-elim $ k≉k' k≡k'<br>
   >> >> >>>  ... | no _   | inj₠_  = PE.refl<br>
   >> >> >>>  ... | no _   | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks<br>
   >> >> >>><br>
   >> >> >>><br>
   >> >> >>> (I) is type-checked, and (II) is not.<br>
   >> >> >>><br>
   >> >> >>> Is this natural for Agda to decide so?<br>
   >> >> >>><br>
   >> >> >>> (I have spent 4 hours trying to prove a similar real and<br>
  evident<br>
   >> >> >>> example.<br>
   >> >> >>> Then tried to split `with' into two, and this has succeeded).<br>
   >> >> >>><br>
   >> >> >>> Thanks,<br>
   >> >> >>><br>
   >> >> >>> ------<br>
   >> >> >>> Sergei<br>
   >> >> >>> ______________________________<u></u>_________________<br>
   >> >> >>> Agda mailing list<br></div></div>
   >> >> >>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><span class=""><br>
   >> >> >>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
   >> >> >><br>
   >> >> >> ______________________________<u></u>_________________<br>
   >> >> >> Agda mailing list<br></span>
   >> >> >> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><span class=""><br>
   >> >> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
   >> >> >><br>
   >> >> ><br>
   >> >> ><br>
   >> >> > --<br>
   >> >> > Andreas Abel <><   Du bist der geliebte Mensch.<br>
   >> >> ><br>
   >> >> > Department of Computer Science and Engineering<br>
   >> >> > Chalmers and Gothenburg University, Sweden<br>
   >> >> ><br></span>
   >> >> > <a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a> <mailto:<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a>><span class=""><br>
   >> >> > <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
   >> >> ______________________________<u></u>_________________<br>
   >> >> Agda mailing list<br></span>
   >> >> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><span class=""><br>
   >> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
   >> ><br>
   >> ><br>
   >> ><br>
   >> ><br>
   >> > --<br>
   >> > Christopher Jenkins<br>
   >> > Computer Science 2013<br>
   >> > Trinity University<br>
   ><br>
   ><br>
   ><br>
   ><br>
   > --<br>
   > Christopher Jenkins<br>
   > Computer Science 2013<br>
   > Trinity University<br>
<br>
<br>
<br>
<br>
--<br>
Christopher Jenkins<br>
Computer Science 2013<br>
Trinity University<br>
</span></blockquote>
<br><div class="HOEnZb"><div class="h5">
<br>
-- <br>
Andreas Abel <><   Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</div></div></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div>Christopher Jenkins<br>Computer Science 2013<br>Trinity University</div></div></div>
</div>