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

[apfelmus at quantentunnel.de]

> 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