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 <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime