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.
>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?