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.
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:
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: 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: 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.
[1]: http://bondi.it.uts.edu.au/
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.
[2]: http://www.springerlink.com/content/978-3-540-89184-0