This is the first time I've encountered this and what you wrote packs a lot of ideas in a small space so forgive me if I have misunderstood.
What you write seems like an even more powerful version of the Active Patterns in F#, which are already really powerful. Active Patterns are the closest thing to First class patterns in a production language * .
Haskell has a similar thing in views. But I think another concept, unique to and playing better to its strengths, while attacking this level of problem are Generalized Algebraic Datatypes. I mentions GADTs because it deals specifically with "This is somewhat limited: you cannot easily write code that is generic over the constructor at the head of the pattern. " Like I said, I've never heard of the pattern calculus - is there any problem it solves that could not be solved with GADTs with a similar level of effort?
* certainly biased but I see active pattern use more than I see extractors or views
I'm afraid that I'm not too familiar with either active patterns or GADTs at the moment. However, given the understanding that I do have, I think they are both unrelated to the basic dynamic pattern matching that I was talking about.
As far as I can tell, active patterns only affect the constructor. They let a constructor like Even to run an arbitrary function when it's matched. This lets you customize what a constructor actually means, which seems very useful, but is orthogonal to dynamic patterns. Dynamic patterns affect the patterns and not the constructors, where a pattern is the expression that is actually matched. That is, given a function f (Foo a b) the pattern is Foo a b. Active patterns would let me customize how Foo works, but the full pattern (Foo a b) still looks and acts the same.
Given this meaning of "pattern", I think active patterns do not constitute first-class patterns. You can't take a pattern and pass it into a function or make up a pattern of variables that can be any pattern. With first-class patterns, you should be able to take the pattern (Foo a b) and pass it into a function as a pattern. So a function like
match pattern (pattern x̂) = x
would make sense in a system with first-class patterns. Here, a pattern is an argument to a function and then used to match against the next argument. Hopefully this clarifies the particular thing that dynamic patterns add to the language.
GADTs are also unrelated. For one, GADTs only affect the type of a constructor and not its behavior. I did not talk about types in my post at all--everything I talked about would make sense in a dynamically typed language that had pattern matching. It just so happens that dynamically typed languages tend not to have pattern matching like this, so it's associated with statically typed languages.
Also, GADTs, like active patterns, only affect the constructor. They do not change the actual patterns used to match against values (except by restricting possible types of the matched values).
So really both active patterns and GADTs are somewhat orthogonal to dynamic patterns. When I said a code that is generic over the head of the pattern, I meant a function like:
doFoo (a b) = b
where doFoo will match both Foo x and Bar x and Baz x and extract x in every case. This function is generic over the constructor in the sense that it matches regardless of what the constructor actually is--the constructor becomes just another matchable term.
This sort of function, which just uses static patterns, is already something that a GADT cannot do. Dynamic patterns are even more flexible. My match function above lets you take an arbitrary pattern like (Foo a b) and match (Foo a b x) against some value to get x. You're passing a pattern into a function which then uses that pattern to match against its next argument. This feature has nothing to do with the type of the constructor.
I hope this cleared things up for you. However, it's almost 4 in the morning and I'm not entirely coherent. If you're still confused, or if I made some glaring errors, feel free to email me about this when I'm more awake :P.
Excellent! Thank you, yes I am clearer, the concept is even more awesome than I thought .
>I think active patterns do not constitute first-class patterns.
I agree, but like I said, they are the closest thing in active use, they extend the type of structures one can deconstruct to encapsulated ones while being more flexible in implementation. They fall in the class of techniques which extend and make matching more flexible, other examples would be multimethods and predicate dispatch. So very much orthogonal to approaches in pattern calculi but I think in a subspace in terms of matching.
>GADTs are also unrelated. For one, GADTs only affect the type of a constructor
Yes they are unrelated that's why I focused on expressitivity, and you are right, I misconstrued what you meant by generalizes on constructors. But everything has a cost - runtime, learning, cognitive overhead - what I was curious of is: how much does the pattern calculus buy you? GADTs are another concept that allow one to elegantly tackle problems where it looks like the pattern calculus would help. I was just looking for an example where something like GADTs fumbles in comparison.
It's clearer to me now that the pattern calculus is definitely more flexible in terms of match semantics but I can't think of any situation in practice where this would give an added advantage.
Also, Is this typically done via term rewriting and is there anything on the decidability of this?
I think the main advantage is what I pointed out before--being able write functions that work on a wide variety of data types. I think my count example is something that could not be done with GADTS:
Keep in mind that this is pseudocode, so some of the semantics may not be perfect. The basic idea is this: the first argument count takes is a pattern, like a constructor. The second argument is matched against the dynamic pattern (constructor x̂). This pattern has one matchable variable x̂ and one free variable constructor. This free variable is bound in the previous argument to the function.
So this lets you use the count function to count any sort of sub-pattern in its argument. Let's imagine you have some hierarchy like (Book (Cons (Chapter stuff) (Cons (Chapter stuff) nil))). You could use the count function to count the number of chapters like this:
count Chapter book
Basically, you're parametrizing your count function on the pattern you want to count. So count can work on any data type and any pattern. If you wanted to count sections, you could:
count Section book
Now lets pretend that sections have numbers. Instead of (Section content) we have (Section number content). You can now count something like how many sections have the number 5:
count (Section 5) book
I think you could generalize this even further, but it would be more complicated.
I'm not sure how this is typically implemented, largely because it typically isn't :P. I think there's essentially one implementation in a language called bondi[1] but I don't know how it is implemented.
As for decidability, I'm not sure. The entire pattern calculus--that is, an extension of lambda calculus supporting this sort of pattern matching--is Turing-complete. I don't know if just the pattern matching part is undecidable though.
As I said in my original post, there is a nice book on this called Pattern Calculus. I think you can read it online[2], which is nice because it turns out to be fairly expensive on Amazon.
What you write seems like an even more powerful version of the Active Patterns in F#, which are already really powerful. Active Patterns are the closest thing to First class patterns in a production language * .
Haskell has a similar thing in views. But I think another concept, unique to and playing better to its strengths, while attacking this level of problem are Generalized Algebraic Datatypes. I mentions GADTs because it deals specifically with "This is somewhat limited: you cannot easily write code that is generic over the constructor at the head of the pattern. " Like I said, I've never heard of the pattern calculus - is there any problem it solves that could not be solved with GADTs with a similar level of effort?
* certainly biased but I see active pattern use more than I see extractors or views