<br><br><div class="gmail_quote">On 4 May 2011 16:57, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">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;">
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's. So, one could define propositional conjunction as follows:</div>
<div><br></div><div>and : Bool -> Bool -> 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 -> Bool -> 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 -> Bool -> 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 -> Bool -> 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 "..." is out of scope.</div>
<div><br></div><div>g : Bool -> Bool -> 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 <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br></div><div><div></div><div class="h5">
<mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>>> 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 <>< 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> <mailto:<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> <<a href="http://www2.tcs.ifi.lmu.de/%7Eabel/" target="_blank">http://www2.tcs.ifi.lmu.de/%7Eabel/</a>><br>
_______________________________________________<br>
Agda mailing list<br>
<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>><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 <>< 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>