Rank-2 polymorphism and pattern matching
simonpj at microsoft.com
Mon Jan 7 04:37:52 EST 2008
| My reason for wanting pattern matching on values of polymorphic types
| is a kind of first-level refinement types. I'm going to demonstrate
| using the "risers" function, as presented in Dana N. Xu's ESC/Haskell, which
| references Neil Mitchell's Catch.
I didn't follow all the details, but I think your main idea is to use the fact that  is the only value of type (forall a. [a]), and similarly for other polymorphic values, and use that to reason that certain branches are inaccessible.
Sadly, it's not true in Haskell, is it?
(error "urk") : 
also has type (forall a. [a]).
I don't know how to fix this, short of making the constructors strict.
Another less-than-satisfying aspect is that Nil has a real value argument (usually () I guess) which is there only to speak to the type system. It's nicer if static properties have static witnesses, and involve no runtime activity.
You have a type (NonEmpty (NonEmpty a)). If you expand that out, I think you get a
forall n1. List (forall n2. List a n2) n1
So you're instantiating the element type of the outer list with a polytype, which requires impredicativity too, not just existentials!
All that said, I never thought of using existentials this way. Ingenious.
More information about the Glasgow-haskell-users