<br><br><div class="gmail_quote">On 4 May 2011 16:57, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi Karim,<br>
<br>
thanks for your message.<div class="im"><br>
<br>
On 5/4/11 5:02 PM, karim kanso wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On behalf of Noam and Fredrick.<br>
<br>
We have spend some more time working on an extended syntax for lambda<br>
expressions. It is currently<br>
at status 3. The use of with and where clauses have issues, the where<br>
clauses have lambda lifting<br>
issues, with clauses have scoping issues.<br>
<br>
We could submit a beta patch that will allow for anonymous case<br>
distinctions, but disable the use of with<br>
and where clauses inside the lambda terms for now?<br>
</blockquote>
<br></div>
That is already something!<br><br></blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Could you explain what the syntax now is for the lambda with matching?<br>
<br></blockquote><div><br></div><div>The syntax, thanks to Noam and Fredrick whom tweaked the parser is essentially function clauses (omitting the name) delimited by semicolon&#39;s. So, one could define propositional conjunction as follows:</div>
<div><br></div><div>and : Bool -&gt; Bool -&gt; Bool</div><div>and = \ ( true x = x ; false _ = false )</div><div><br></div><div>which is internally translated into</div><div><br></div><div>.extlam0 : Bool -&gt; Bool -&gt; Bool</div>
<div>.extlam0 true x = x</div><div>.extlam0 false _ = false</div><meta http-equiv="content-type" content="text/html; charset=utf-8"><meta http-equiv="content-type" content="text/html; charset=utf-8"><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>
<br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>and : Bool -&gt; Bool -&gt; Bool</div><div>and = .extlam0</div></div><div><br></div><div>The dot being used to keep the namespace hygienic. </div>
<div> </div><div>.extlam0 is lambda lifted so we can write:</div><div><br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>or : Bool -&gt; Bool -&gt; Bool</div><div>or x = \ ( true = true ; false = x )</div>
</div><div><br></div><div>All the examples above work, now in the cases where we are having some difficulties. A with statement does not work at all, scope checking fails with the message &quot;...&quot; is out of scope.</div>
<div><br></div><div>g : Bool -&gt; Bool -&gt; Bool</div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>g = \ ( x y with (and x y) ; ... | z = ?)</div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>
<br></div><div>The where statements have an issue when nested under other where statements,  causes extra lambda lifting (appears to be done twice). </div><div><br></div><div>It is not currently clear if it even a significant advantage to have with and where statements inside the extended lambda notation as the main motivation as I understand it is to allow anonymous/in-situ case distinctions. Any other opinions would be welcome. </div>
<div><br></div><div>Best,</div><div>Karim Kanso</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

Cheers,<br>
Andreas<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
On 28 April 2011 15:30, Andreas Abel &lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br></div><div><div></div><div class="h5">
&lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;&gt; wrote:<br>
<br>
    Hi AIM XIII participants,<br>
<br>
    two weeks after the end of this very successful meeting, I would<br>
    like to know the status of the code sprints which were continued<br>
    after the meeting.<br>
<br>
    @Makoto: I do not remember all the sprints, can I find the notes<br>
    online somewhere?<br>
<br>
    Status:<br>
      1 = finished<br>
      2 = almost finished<br>
      3 = still working, might take some more time<br>
      4 = indefinitely postponed<br>
      5 = abandoned<br>
<br>
    Sprint                           Leader            Status<br>
<br>
      clean up builtins              Simon             1?<br>
      unquote                        Nicolas           3?<br>
      first class lambda syntax      Noam               ?<br>
      mutual blocks                  James             3?<br>
      installer                      Makoto             ?<br>
      meta variables                 Andreas           3<br>
<br>
      what else?<br>
<br>
    Cheers,<br>
    Andreas<br>
<br>
    --<br>
    Andreas Abel &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
    Theoretical Computer Science, University of Munich<br>
    Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br></div></div>
    <a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a> &lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;<br>
    <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a> &lt;<a href="http://www2.tcs.ifi.lmu.de/%7Eabel/" target="_blank">http://www2.tcs.ifi.lmu.de/%7Eabel/</a>&gt;<br>
    _______________________________________________<br>
    Agda mailing list<br>
    <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>&gt;<div class="im"><br>
    <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</div></blockquote><div><div></div><div class="h5">
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
</div></div></blockquote></div><br>