[Haskell-cafe] irrefutable patterns for existential types / GADTs

Conor McBride 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 mailing list