It is encouraging that separate groups have come to similar approaches wrt to more modular pattern match facilities (though perhaps it isn't all that surprising, eg, my own musings on this topic started after one of the early functional logic programming high periods, in the early 1990s, and have since been shaped by the developments in monadic and type class programming in Haskell; PMC seems to have come from a rewriting background, shaped by monadic semantics and type theory; these would imply the same influences, moderated via different communities?). There are, however, some differences that might be worth further inspection. Referring to http://www.cas.mcmaster.ca/~kahl/PMC/ , and especially to the MPC 2006 paper, in no particular order, with no claim to completeness (and please read comments like "odd" as purely subjective, reflecting only my personal reactions as I'm trying to figure out the relation!-): - 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, as one would expect operations on matchings, matchings as parameters and results of functions, etc. .. until one notices that not only the operations on matchings, but - *all* the interesting action in PMC is at the level of matchings, not at the level of expressions lambda-abstraction doesn't even exist at expression level, but is replaced by spliced matching; application exists, but is not needed, because (f e) = {| e |> {| f |} |} (unless I'm mistaken?) if one eliminated the oddity of having two applications, but only one abstraction, the category of expressions would be nearly empty, apart from constructor terms, and the separation of expressions and matchings seems needed only to support conversions between the two: {| _ |} :: Match -> Expression ^ _ ^ :: Expression -> Match which directly brings up the next oddity, in that there are no such types in PMC: - the difference between matchings and expressions is maintained in the typing contexts/labels, not in the types in spite of the monadic semantics, there are no monads in the type system, and instead of .. |- pattern |> match :: a -> m b (as Haskellers might expect to see), one has .. |M- pattern |> match :: a -> b I was looking into these details because I was trying to compare lambda-match and PMC, and while most of the differences seemed merely cosmetic at first, the one difference I couldn't account for was that PMC examples seemed to imply an implicit flattening of the monadic type structure, whereas I had to join nested lambda-matches explicitly (I would find the ability to join nested matchings quite useful on occasion, but I fail to see how this could be done implicitly/ automatically, unless by giving up the ability to express nested matches). if I now understand all these items correctly in combination, PMC is a flattened monadic framework, ie., one cannot even construct the equivalent of a ( <nested> :: m (m a))? or am I missing the obvious?-) cheers, claus ps. after reading the MPC 2006 paper, I have to support the referees' recommendation: as one of many who only occasionally dive into the most shallow parts of category theory, I don't find the monadic semantics in its current presentation helpful. A "running commentary" in computational lambda-calculus, as apparently suggested by the referees, would have made all the difference (I think, because that kind of presentation usually translates easily into Haskell;-). As it stands, I fear you are limiting your audience needlessly. -- <interactive>:1:0:-) Couldn't match `Categories' against `Haskell' Expected type: Haskell Inferred type: Categories In the first argument of `readPaper', namely `PMC_MPC2006' In the definition of `it' : it = readPaper PMC_MPC2006
lambda-abstraction doesn't even exist at expression level, but is replaced by spliced matching; application exists, but is not needed, because (f e) = {| e |> {| f |} |} (unless I'm mistaken?)
oops, wrong brackets around f - should be: {| e |> ^f^ |} --> {| ^f e^ |} --> f e with f supposedly being a lambda abstraction ( \v.b ) represented as a match ( {| v => ^b^ |} ), we get: f e = {| v => ^b^ |} e --> {| e |> v => ^b^ |} --> {| ^b^[ v\a ] |} --> b[ v\a ] as seen on page 3 of the MPC2006 paper, also showing that application reduces to argument supply, which provides beta reduction. claus
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
- 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
Hi Wolfram,
- matchings are not first-class expressions in PMC
The most important aim of the original PMC was to be a confluent rewriting system that emulates Haskell pattern matching .. So I needed only those operations on matchings that are ``somehow implicit'' in Haskell pattern matching, and I did not need matching variables etc.
understood. sorry if my message suggested that our aims were the same!-) and as your earlier message indicated, one could nevertheless use PMC-inspired constructs to replace Haskell pattern matching with something more modular. btw, while my proposal ticket does link to your email, it doesn't make your alternative proposal explicit - would you mind elaborating your proposal into a separate Haskell' ticket, so that Haskellers and committee could compare the two alternative proposals and their pros & cons (I have been told that my current ticket is already rather long, so it will be better to have two separate, but cross-linked proposal tickets)?
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.
unlike ML, pure expression Haskell only provides an implicit identity monad, where fail raises an exception, so you might want to be explicit about both the expression and the matching monad. which would mean to have these monads reflected in the types.
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.
interesting, I hadn't thought about that at all - so we Haskellers routinely use several instances of computational lambda-calculus in our code, and while each of those instances could be explained through one such calculus, one calculus (at least in original form) wouldn't be sufficient to cover current practice.
In the lambda-match proposal there is the remark:
-- we use Maybe as the default matching monad, but [] can be fun, too..
the code carefully leaves open which matching monad to choose, but provides some help for common default choices, such as Maybe, Either String, and []. I'm tempted to make (Either String) the default, as it makes it easy to preserve error messages (although I should use a newtype, to avoid instance conflicts).
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.
we can still do most of that, we just have to be explicit about both monads. as one example, the function "ok", used to define match-failure in do-notation, merges the match monad and the monad of the do-block. another example is "nest", which merges two nested match-monads. using lists of successes should also work, although we don't have logic variables (not unless we use non-standard data structures that allow for them). propagating match failure through exceptions probably suffers from similar problems (need to use monadic rather than pure code).
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.
that is strange - if you re-read that paper (I did after your email), I think you'll find very little actual overlap with the lambda-match proposal. of course, both start from the same idea, namely to replace pattern matching with "monadic data parsing", but most of the details are rather different. one might also say that Tullsen's work is more ambitious, in making not only match failure and fall-through explicit in a MonadPlus, but also matching itself (through various pattern combinators and syntactic sugar). this is the main reason I did not mention his paper as related work in the proposal - it would only confuse the issues. of course, I have been working on my own versions of first class patterns, based on the lambda-match proposal, and -so far- no further syntax extensions, but that isn't part of the lambda-match proposal. so, lambda-match is a smaller step, both syntactically and semantically, and has been specifically targetted to be suited for Haskell'. it also aims to lay the groundwork for refactoring Haskell pattern matching into something simpler, more compositional, and more expressive (first-class patterns tend to include pattern abstractions and views), after Haskell'. Henrik has pointed out to me that I should make these aims and expected advantages more explicit in my proposal ticket, which I'll try when I next update it (I'm recompiling ghc and libraries to check whether I've missed any syntax conflicts, updates after that..).
Since PMC handles this as a language extension, it only concerns the semantics, not the type system.
(this referred to the lifting of lambda-matches to multiple parameters) I could be wrong, but when you elaborate your own proposal, I think you'll find that both n-ary patterns and the choice of monads will need to be reflected in the type system, as most other properties of interest in Haskell. once we start to distinguish nested match monads, "curried" matches are no longer as easy to use as n-ary matches, so while you may say that this is merely a convenience, I think it is of practical importance. and I've tried to be careful not to use disputed features such as overlapping instances, etc., which led to the pedestrian approach of wrapping matches in Match constructors. this is nothing but a tag to serve as a base-case for any type-level recursions over the parameters of n-ary matches, which therefore are straightforward.
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:
hmm. speaking for myself, I wouldn't be interested in Haskell's design if I didn't want to use it. and if I want to use Haskell, it would seem odd to handle parts of my proposal as language extensions unless Haskell is not expressive enough to handle those parts as libraries. I don't claim that it was straightforward to come up with the type classes (separating Lift and MonadPlus, separating Ex from Lift, and the details of Nest, all took some work), but apart from Nest, the results are not difficult to read or use, and even nest does seem to pose few problems in use. in fact, I put a lot of work into trying to achieve the latter, by reducing the potential for ambiguities (hence the functional dependencies that make Ex look more complicated), and by keeping to the common subset of Hugs/GHC. there are a few cases where things could be easier, eg, kind annotations (scheduled for Haskell', I think) in MatchMonad, or type patterns in class declarations (which would permit me to make the purpose of Ex more obvious -as it is from the type of ex- while still being able to express the functional dependencies). As for all embedded DSLs, I would like to be able to add syntax transformations without changing the Haskell implementation, and I would like to add error message postprocessing the same way (so that I could define DSL- specific syntax and error messages as part of a library), but I have to make do with what Haskell provides..
-- 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...
we are not talking about an extension to do notation. we are trying to expose a language feature that was previously only available implicitly, via do notation or case. yes, the type errors messages can be formidable, but mostly due to our old enemy, the monomorphism restriction (how an implementation issue that should at best result in a performance warning was ever permitted to enter the language definition, let alone be such an annoying obstacle to *programming with functions*, is beyond me - I do hope this mistake will finally be corrected in Haskell'!!). having said that, I would again point out that I've tried to make the library useable, and while I haven't been entirely successful wrt to ease of use, the type errors do seem to be helpful most of the time (translating missing constraints into the class members helps), and explicit type declarations do not seem to be needed as often as one might fear for this kind of type-class programming (ymmv, of course, so you'll have to try for yourself, and let me know!-).
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.
as I mentioned, the monads will need to be explicit in Haskell, which throws into doubt the idea of not having n-ary matches, as well as raising all the problems of how to handle nested monads, and how to reduce ambiguities while still allowing the monads to be chosen as needed. keeping alternatives inside lambda abstractions as anything other than syntactic sugar does not seem to make the main impact of the suggested change as clear as providing for single alternatives plus composition: pattern match failure and fall-through have become programmable, no longer tied to a language construct. my proposal tries to be a compromise, by providing most (all?) features of PMC, as well as foundations for monadic data parsing in general, using syntactic sugar only where absolutely necessary, and library support everywhere else. please do pursue your own proposal through to a prototypical implementation and Haskell' ticket, though - if you can come up with something that does provide the same features as lambda-match, without its difficulties, I'd like to know about it!
(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_{>}$. )
I chose the '|' because it is already reserved, but cannot be used in that position (*), and because it is already associated with alternatives in data types. the notation needs to be very lightweight, because several lambda-matches will be normally be used together with (+++) and parenthesis, to cover alternative cases, and the '|' does provide a nice visual aid in connecting these separate cases by layout. I'm not completely tied to this syntax, but anything else I've tried so far seems unable to provide similar benefits in practice (including your \>, which neither aligns well, nor suggests the case alternatives - even if you meant \>>; and we are concerned more with MonadPlus than with Monad here) and might steal another operator/keyword (like "proc" for arrows). note also that this is *not* the "monadic lambda" one might expect, because it embeds the body of the lambda-match in a return. one might want to add a lambda-do as well: [| '\>' <patterns> 'do' <statements> |] ==> \ <variables> -> do {<patterns> <- return (<variables>) ; <statements> } or, using lambda-match to define lambda-do: \> <patterns> do <statements> = ok $ (| <patterns> -> do <statements>) but I decided not to make that part of the present proposal. Thank you for your comments, Claus (*) actually, when recompiling ghc and libraries from scratch, I found one conflict that I hadn't anticipated: if, within the head of a list comprehension, one uses a do-block with more than one statement, and layout instead of explicit {}, then it is not clear whether one sees the last expression in the do-block or the first qualifier of the list comprehension.. (don't laugh, that actually occurs, in Data/Array/Base;-). to avoid complications, and because lambda-matches are meant to be passed as parameters to higher-order functions such as splice and (+++) anyway, I've now changed the patch to require parens around all lambda-matches, and from this safe position I'm looking for places where the parens are not needed (the way the grammar is organised does not always make it easy to differentiate these places).
participants (2)
-
Claus Reinke -
kahl＠cas.mcmaster.ca