[Haskell-cafe] Re: Optimization problem

[Robert Dockins]

On Sep 19, 2006, at 8:52 AM, Conor McBride wrote:

> Hi folks
>
> apfelmus at quantentunnel.de wrote:
>> Btw, why are there no irrefutable patterns for GADTs? I mean, such  
>> a sin
>> should be shame for a non-strict language...
>>
>
>
> Just imagine
>
> > data Eq a b where Refl :: Eq a a
>
> > coerce :: Eq a b -> a -> b
> > coerce ~Refl a = b


I think you mean:

 > coerce ~Refl x = x


> coerce undefined True :: String
>
> Bang you're dead. Or rather... Twiddle you're dead.
>
> Moral: in a non-total language, if you're using indexing to act as  
> evidence for something, you need to be strict about checking the  
> evidence before you act on it, or you will be vulnerable to the  
> blandishments of the most appalling liars.
>
> As Randy Pollack used to say to us when we were children, the best  
> thing about working in a strongly normalizing language is not  
> having to normalize things.
>
> All the best
>
> Conor


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG