lambda-match vs PMC

[kahl at cas.mcmaster.ca]

After a particularly bad week in a very busy term
I am just now getting around to have a first look
at Claus Reinke's <claus.reinke at talk21.com> lambda-match proposal
and at his message from 29 Oct 2006:
 > 
 > - matchings are not first-class expressions in PMC
 > 
 > the only syntactically correct way to mention a matching in an expression
 > is inside a splice ( {| match |} ).
 > this is fairly surprising given the aims of PMC,

The most important aim of the original PMC
was to be a confluent rewriting system
that emulates Haskell pattern matching
(also known as the ``functional rewriting strategy'').
This makes equational reasoning much easier
since you don't have to take a very complex evaluation strategy
into account.
(Isabell proof of confluence described in FLOPS 2004.)

 > as one would expect operations on matchings, matchings as 
 > parameters and results of functions, etc. .. 

So I needed only those operations on matchings
that are ``somehow implicit'' in Haskell pattern matching,
and I did not need matching variables etc.


 > application exists, but is not needed,
 > because [corrected version]  {| e |> ^f^ |} --> {| ^f e^ |} --> f e

I haven't tried yet whether the corresponding adaptation of the rules
still keeps the system confluent (I suspect it does),
but my original motivation was to deviate from Haskell as little as
possible, so you can have lambda-abstraction as syntactic sugar,
and the only real changes are matching groups without case-argument,
and the addition of argument supply for matchings.

 > and the separation of 
 > expressions and matchings seems needed only to support 
 > conversions between the two:
 > 
 > {| _ |} :: Match -> Expression
 > ^ _ ^ :: Expression -> Match 

Which are handled as separate syntactic categories,
just like matching alternatives and expressions are separate
syntactic categories in Haskell.

 > in spite of the monadic semantics, there are no monads in the type
 > system,

Just like in ML.

In fact, just like in pure expression Haskell, which,
from the point of view taken in the MPC2006 paper,
still relies on a lifting monad to add undefined to constructed types.

 > <interactive>:1:0:-)
 >     Couldn't match `Categories' against `Haskell'
 >         Expected type: Haskell
 >         Inferred type: Categories

The problem with a Haskell translation of PMC
(I do have a prototype implementation like that)
is that too much is implicit in the Haskell semantics
that needs to be made explicit, and making it explicit in Haskell notation
does not make it more readable than the category notation.

 > A "running commentary"
 >     in computational lambda-calculus,

The main problem I see with that
is that the computational lambda-calculus only sugars away ONE monad,
while, in the MPC paper, we are dealing with TWO monads.

In fact, for our two-monad setting, I suspect that if we want
to get close in spirit to the computational lambda-calculus,
it is going to look pretty much like PMC again...
perhaps that's why the original description of the 
computational lambda-calculus is using categories ;-)


In the lambda-match proposal there is the remark:
 > 
 > -- we use Maybe as the default matching monad, but [] can be fun, too..

In PMC (see the MPC paper)
you can change not only the matching monad,
but also the expression monad, for example:
 * the lifting monad in standard Haskell
 * a Maybe monad in the ``matching failure as exceptions'' view
    of the pattern guards paper [Erwig-PeytonJones-2001],
 *  a list monad in functional-logic programming.


To me, it looks like the main difference between the lambda-match library
and Tullsen's pattern matching combinators [PADL 2000] is
that the lambda-match library also includes
the same ``pointwise lifting'' of the monadic operations into function types
that we use in the MPC paper.

Since PMC handles this as a language extension,
it only concerns the semantics, not the type system.

Since the lambda-match proposal does it as a library,
it has to be done inside the language,
leading to the type-class artistry involving declarations like the
following:

 > -- extract (with function) from inner match monad
 > -- (extraction is lifted over lambda-match parameters;
 > --  we cannot express all functional dependencies,
 > --  because the inner c could be a function type)
 > class Ex a c da dc | da -> a, dc da -> c, da c -> dc {- , dc a c -> da -} where
 >   ex :: (a -> c) -> da -> dc 

So probably this is a seemingly innocuous extension to do notation
with the potential for some quite spectacular type error messages...

And, from my point of view,
all it achieves over my tentative PMC proposal
is to avoid the two language extensions of
alternatives inside lambda abstractions,
and argument supply (match ... with ...),
at the cost of a different language extension.

(I am also afraid that the ``|'' notation might be dangerous.
 To emphasise its character as a ``monadic lambda'',
 I would rather consider something like ``\>'', to be typeset $\lambda_{>}$.
)


Wolfram