# Call to arms: lambda-case is stuck and needs your help

Wolfram Kahl kahl at cas.mcmaster.ca
Tue Jul 10 05:48:36 CEST 2012

On Mon, Jul 09, 2012 at 07:22:30PM +0300, Wolfgang Jeltsch wrote:
> Although I wasn’t asked, I want to express my opinion. I think, the use
> of the comma is strange. When declaring functions with multiple
> arguments, we don’t have commas:
>
>     f Nothing  y = y
>     f (Just x) y = x
>
> In lambda expressions for multi-argument functions, we also don’t have
> commas:
>
>     \x y -> x + y
>
> Why should we have them when using a case-lambda expression for a
> multi-argument function?

A variant of this question is easy to answer:
multi-case-multi-argument function expressions are conceptually obtained
as generalisation of sets of case bindings (the part after the of'')
instead of as a generalisation of lambda expressions.

This leads me to a first quick shot:

Proposal 1: caseof'':

Introduce a new layout keyword caseof'' to delimit (via layout or braces)
the case bindings, producing the function that currently would be
\ x -> case x of ...    (with fresh x).

Multi-case-multi-argument function definitions are currently translated into
multi-case-single-argument case expressions, with the arguments collected together
into tuples --- this might provide motivation for the commas.

This leads me to a second quick shot:

Proposal 2: no-multiple-argument-case'':

Make no further changes to the case bindings syntax.
Programmers who want multiple arguments can put them into tuples
and curry the whole caseof construct, which is reasonably cheap syntactically:

zip = curry $caseof ([] , ys ) -> [] (xs , [] ) -> [] (x : xs , y : ys) -> (x , y) : zip xs ys This has the advantage that no new rules need to be added to syntax or semantics. Side note (and shameless plug): The above is partially inspired by my work on the pattern matching calculus (PMC) where groups of case bindings form the second syntactic category of matchings'' (besides expressions). caseof'' then corresponds to the wrapping {| m |} that turns a matching into an expression, and Haskell's sequence of case bindings would be mapped to the monoid of matchings with with empty matching as unit and matching alternative as composition. PMC includes two additional features that allow equational reasoning with matchings (case binding groups): Argument supply: Applying a matching to an argument without first converting the matching into an expression. This feature can be seen as a generalisation of pattern guards. Nestable matching construction: Individual cases in PMC are of shape p -> m'' with a matching right-hand side instead of an expressionp -> e'' in Haskell. Nestable matching construction allows construction of multiple-argument pattern matching functions with more liberal shapes than the strict matrix shape required for function definitions, but with a different semantics. That more liberal shape can already be achieved with the tuple scheme of proposal 2 above: f = curry$ curry $caseof (p , []) -> ... ((xs, []) , z : zs) -> ... _ -> ... and zip = curry$ caseof
(x : xs , y : ys)  -> (x , y) : zip xs ys
_                  -> []

Integrating argument supply and nestable matching construction into Haskell
would be a more far-reaching change --- an easy'' attempt at nestable
matching construction alone would turn the -> of case bindings into a
layout keyword, and insert conversion of expressions into
zero-argument matchings (return'') automagically:

zip = caseof
[] -> []
x : xs ->
[] -> []
y : ys -> (x , y) : zip xs ys

The important aspect of considering the part after -> as a matching
instead of as an expression is fall-through --- the nested patterns
act somewhat like pattern guards:

zip = caseof
x : xs -> y : ys -> (x , y) : zip xs ys
_   ->   _  -> []

The two alternatives in this last example are intentionally not aligned
to emphasise the fact that the two 2-argument matchings are constructed
completely indepnedent from each other.

Automagical insertion of conversion of expressions into zero-argument
matchings depends on having no expressions that can legally be parsed
as matchings. With what I sketched above, this might actually work,
but I cannot claim that I have fully thought this through.
If it can be made to work, it could be called

Proposal 3: nestable case bindings''.

Generalising pattern guard syntax into argument supply requires a second
syntactic construct that contains a group of case bindings;
most easily this would be another layout keyword, say into''
(in the PMC papers, this is $\righttriangle$;
better keywords would be welcome; I guess |>'' is not a good idea...):

Pattern guards are of shape pat <- arg'' with the argument to the right,
as in SPJ's clunky'':

clunky env var1 var2
| Just val1 <- lookup env var1
, Just val2 <- lookup env var2
= val1 + val2
...other equations for clunky...

For argument supply and into'' we use the opposite sequence,
arg  into  pat'', and clunky could then become:

clunky = caseof
env ->
var1 ->
var2 ->
lookup env var1  into
Just val1 ->
lookup env var2  into
Just val2 -> val1 + val2
... other case bindings for clunky ....

(This runs into similar nested layout issues as discussed recently;
if we were to change the layout rule (perhaps only for the new keywords)
to not apply if the next token is separated from the layout keyword
by only a single space, we could turn this into a more compact shape:

clunky = caseof
env -> var1 -> var2 -> lookup env var1  into Just val1
-> lookup env var2  into Just val2 -> val1 + val2
... other case bindings for clunky ....

(The alignment of the two lookups and their preceding -> is irrelevant here.)
)

into'' would generalise pattern guards by allowing the same expression
to be matched against different patterns and still enable fall-through:

f = caseof
[x] -> g x  into  []         -> []
a : b : bs -> (a, b) : h bs
... other cases, including g returning a singleton ...

This could be:

Proposal 4: case-group argument supply'' or generalised pattern guards''

Best wishes,

Wolfram

---------------------------------------------

@InProceedings{Kahl-2004a,
author = 	 {Wolfram Kahl},
title = 	 {Basic Pattern Matching Calculi: A Fresh View on Matching Failure},
crossref =  {FLOPS2004},
pages = 	 {276--290},
DOI = {10.1007/978-3-540-24754-8_20},
abstract = {We propose pattern matching calculi as a refinement
of $\lambda$-calculus that integrates mechanisms appropriate for
fine-grained modelling of non-strict pattern matching.

Compared with the functional rewriting strategy
usually employed to define the operational semantics of
pattern matching in non-strict functional programming languages
like Haskell or Clean, our pattern matching calculi
achieve the same effects using simpler and more local rules.

The main device is to embed into expressions
the separate syntactic category of matchings;
the resulting language naturally encompasses
pattern guards and Boolean guards as special cases.

By allowing a confluent reduction system and a normalising strategy,
these pattern matching calculi provide a new basis for
operational semantics of non-strict programming languages
and also for implementations.}
}

@InProceedings{Kahl-Carette-Ji-2006a,
author = 	 {Wolfram Kahl and Jacques Carette and Xiaoheng Ji},
title = 	 {Bimonadic Semantics for Basic Pattern Matching Calculi},
crossref =  {MPC2006},
pages = 	 {253--273},
DOI = {10.1007/11783596_16},