[Agda] AIM XIII code sprints

[karim kanso]

On 4 May 2011 16:57, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> Hi Karim,
>
> thanks for your message.
>
>
> On 5/4/11 5:02 PM, karim kanso wrote:
>
>> On behalf of Noam and Fredrick.
>>
>> We have spend some more time working on an extended syntax for lambda
>> expressions. It is currently
>> at status 3. The use of with and where clauses have issues, the where
>> clauses have lambda lifting
>> issues, with clauses have scoping issues.
>>
>> We could submit a beta patch that will allow for anonymous case
>> distinctions, but disable the use of with
>> and where clauses inside the lambda terms for now?
>>
>
> That is already something!
>
> Could you explain what the syntax now is for the lambda with matching?
>
>
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:

and : Bool -> Bool -> Bool
and = \ ( true x = x ; false _ = false )

which is internally translated into

.extlam0 : Bool -> Bool -> Bool
.extlam0 true x = x
.extlam0 false _ = false

and : Bool -> Bool -> Bool
and = .extlam0

The dot being used to keep the namespace hygienic.

.extlam0 is lambda lifted so we can write:

or : Bool -> Bool -> Bool
or x = \ ( true = true ; false = x )

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.

g : Bool -> Bool -> Bool
g = \ ( x y with (and x y) ; ... | z = ?)

The where statements have an issue when nested under other where statements,
 causes extra lambda lifting (appears to be done twice).

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.

Best,
Karim Kanso







Cheers,
> Andreas
>
>  On 28 April 2011 15:30, Andreas Abel <andreas.abel at ifi.lmu.de
>> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>>
>>    Hi AIM XIII participants,
>>
>>    two weeks after the end of this very successful meeting, I would
>>    like to know the status of the code sprints which were continued
>>    after the meeting.
>>
>>    @Makoto: I do not remember all the sprints, can I find the notes
>>    online somewhere?
>>
>>    Status:
>>      1 = finished
>>      2 = almost finished
>>      3 = still working, might take some more time
>>      4 = indefinitely postponed
>>      5 = abandoned
>>
>>    Sprint                           Leader            Status
>>
>>      clean up builtins              Simon             1?
>>      unquote                        Nicolas           3?
>>      first class lambda syntax      Noam               ?
>>      mutual blocks                  James             3?
>>      installer                      Makoto             ?
>>      meta variables                 Andreas           3
>>
>>      what else?
>>
>>    Cheers,
>>    Andreas
>>
>>    --
>>    Andreas Abel <><      Du bist der geliebte Mensch.
>>
>>    Theoretical Computer Science, University of Munich
>>    Oettingenstr. 67, D-80538 Munich, GERMANY
>>
>>    andreas.abel at ifi.lmu.de <mailto:andreas.abel at ifi.lmu.de>
>>    http://www2.tcs.ifi.lmu.de/~abel/ <http://www2.tcs.ifi.lmu.de/%7Eabel/
>> >
>>    _______________________________________________
>>    Agda mailing list
>>    Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>
>>    https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110504/184e1771/attachment.html