Jim
| 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.
Simon
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
