[Haskell-cafe] irrefutable patterns for existential types / GADTs
ctm at cs.nott.ac.uk
Fri Sep 29 10:39:32 EDT 2006
apfelmus at quantentunnel.de wrote:
> Ross Paterson wrote:
>> The story so far:
>> apfelmus: why are there no irrefutable patterns for GADTs?
>> Conor: because you could use them to write unsafeCoerce
>> Ross: how about irrefutable patterns (or newtypes) for existential types?
>> Simon: Try giving the translation into System F + (existential) data types
> I'd like to add that I see no problem with
> coerce :: Eq a b -> a -> b
> coerce ~Refl x = x
> as long as we have
> coerce _|_ x === _|_
But that makes it refutable! For the above, either
coerce _|_ x === x
or the notation is being abused.
The trouble is that GADT pattern matching has an impact on types, as
well as being a selector-destructor mechanism, and for the impact on
types to be safe, the match must be strict.
For existentials, I'm not sure, but it seems to me that there's not such
a serious issue. Isn't the only way you can use the type which allegedly
exists to project out some dictionary/other data which is packed inside
the existential? Won't this projection will cause a nice safe _|_
instead of a nasty unsafe segfault?
I think it's the extra power of GADTs to tell you more about type
variables already in play which does the damage.
All the best
More information about the Haskell-Cafe