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

[Wolfram Kahl]

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 expression``p -> 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},
  SpringerURL = {http://www.springerlink.com/content/3jet4qgw1q2nu0a8/},
  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},
  SpringerURL = {http://www.springerlink.com/content/2715070606u63648/}
}