[Agda] Re: Syntax for anonymous functions

[Fredrik Nordvall Forsberg]

Hi,

Karim and I have been happily hacking away on the pattern matching 
lambda implementation when we have found the time. Last time you heard 
from us, we said that we would try to implement the syntax

    \ { true x -> x ; false _ -> false }

but this turned out to be harder than expected because of the way the 
parser is written: it is hard for the parser to distinguish an extended 
lambda expression from a good old lambda, but with an implicit argument:

    \ {x} {y} -> y

While waiting for extended and old lambdas to be merged in an utopian 
future, we instead settled on the syntax

    function { true x -> x ; false _ -> false }

similar to the syntax for records. (Without making function a layout 
keyword, as that interfered with the syntax above.)

This is a bit heavyweight for a small function, though, so we have also 
introduced the syntax

    (a , b) |-> a

for one clause functions. The Unicode-inclined can use \mapsto in the 
emacs mode. I like this, as it makes it possible for me to write

    record FamSet : Set1 where
      constructor _,_
      field
        A : Set
        B : A -> Set

    ΣFAM : (A : Set) ->
           (B : A -> Set) ->
           (P : A -> Set) ->
           (Q : (x : A) -> P x -> B x -> Set) ->
             -> FamSet
    ΣFAM A B P Q = (Σ A P , ( (a , p) ↦ Σ (B a) (Q a p) ))

pretty much what I write on a blackboard, instead of

    [...]
    ΣFAM A B P Q = (Σ A P , f)
       where f : Σ A P -> Set
             f (a , p) = Σ (B a) (Q a p)

which I did before. For consistency, we have also changed it so that |-> 
can be used everywhere where -> can be used in a "mapping context", that 
is in ordinary lambdas

    \ x {y} |-> y

and in the new 'function' anonymous pattern matching functions

  function { false false |-> false ; true true |-> false ; _ _ |-> true }

but not in function spaces

    (x : A) -> B

of course.

Comments on this syntax are welcome, and there is a patch for those who 
want to try it out at

http://www.cs.swan.ac.uk/~csfnf/misc/extlam.dpatch

The changes come with a small price to the standard library though: 
Data/Star/Decoration.agda uses the symbol ↦ as a constructor name (any 
name not *only* consisting of ↦ is okay, just as for ->), and the new 
Reflection.agda uses the constructor name 'function'. I have renamed 
these to a longer version of the \mapsto-arrow (and added the input 
\r--| for this in the Emacs mode in the above patch) and 'fundef' 
respectively. The changes are recorded in this patch:

http://www.cs.swan.ac.uk/~csfnf/misc/extlam-stdlib.dpatch


By the way, am I the only one for which test/interaction/Issue373.agda 
doesn't output

    [1 of 3] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
    [2 of 3] Compiling Imports.Nat      ( Imports/Nat.hs, Imports/Nat.o )
    [3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs,
                                               MAlonzo/Code/Issue373.o )

when running the test suite? Or who gets the error message

    Not implemented: primQNameType

when compiling std-lib/src/Reflection.agdai in the compiler tests?

-- 
Best regards,
Fredrik