[EMAIL PROTECTED] 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
Conor
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
