> But that makes it refutable! For the above, either > > coerce _|_ x === x > > or the notation is being abused.
Making a pattern irrefutable does not mean that the function in question will become lazy: fromJust (~Just x) = x fromJust _|_ === _|_ The point with coerce is that it looks very much like being lazy in its first argument but in fact it is not. > 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. > > I think it's the extra power of GADTs to tell you more about type > variables already in play which does the damage. But I think that something still can be squeezed out, strictness is not absolutely necessary. I thought something along the lines of f :: Eq a b -> a -> Maybe b f ~Refl x = Just x with f _|_ x === Just _|_ The point is one can always output the constructor Just, it does not inspect the type of x. Now, I don't think anymore that this is feasible as the type of (Just x) still depends on the type of x (even if the constructor Just does not mention it). Nevertheless, I still want to remove strictness, see my next mail in this thread. > 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 agree. The only practical problem I can imagine is that GHC internally treats existentials as GADTs. Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
