Re: [Haskell-cafe] irrefutable patterns for existential types / GADTs
On Sat, Sep 30, 2006 at 01:38:28AM -0700, [EMAIL PROTECTED] wrote: It seems that irrefutable pattern match with existentials is safe. The fact that irrefutable pattern match with GADT is unsafe has been demonstrated back in September 2004. it is safe in that you can't express coerce, but irrefutable pattern matching on existentials has other practical issues for an implementation. namely, even though you may not ever evaluate the irrefutable pattern, its type is probably used in the underlying translation somewhere like. if you happen to use any polymorphic functions. for instance data Foo = exists a . Foo a f ~(Foo x) = const 4 (id x) now, you would think that f _|_ would evaluate to 4, but (depending on your translation) it might evaluate to _|_. the reason being that id translates internally to id = /\a . \x::a . x since you cannot pull out an appropriate type to pass to id without evaluating the 'irrefutable' pattern, you end up with _|_ instead of 4. basically, allowing irrefutable matching on existentials would expose whether the underlying implementation performs type-erasure. even if an implementation does type erasure like ghc. suddenly odd things occur, like adding an unusned class constraint to a type signature might change the behavior of a program. (since it will suddenly have to pull out a dictionary) All in all, even though type-safety is not broken, irrefutable patterns should not be allowed for existentials. John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] irrefutable patterns for existential types / GADTs
It seems that irrefutable pattern match with existentials is safe. The
fact that irrefutable pattern match with GADT is unsafe has been
demonstrated back in September 2004.
Let us consider the following regular existential data type
data TFoo where
Foo :: Show a = a - TFoo
Bar :: Int - TFoo
Despite the 'where' syntax, it is NOT GADT; it is just a regular data
type. We can write
test_foo vf = case vf of ~(Foo x) - body
Now, if 'x' does not occur in `body', we could have just as well written
test_foo vf = body
If `x' does occur in body and the scrutinee is not of the form `Foo',
then 'x' is undefined, and so 'body' bottoms out when it demands the
value of 'x'. No surprise, and no concern here.
Let is now consider a GADT
data GTFoo a where
GFoo :: GTFoo Int
GBar :: GTFoo Bool
test_gfoo :: GTFoo a - a
test_gfoo vf = case vf of GFoo - (1::Int)
It can be faithfully emulated as follows
-- the data constructors Em_GFoo and Em_GBar must be hidden!
data EmulateGTFoo a = Em_GFoo | Em_GBar
em_gfoo :: EmulateGTFoo Int
em_gfoo = Em_GFoo
em_gbar :: EmulateGTFoo Bool
em_gbar = Em_GBar
The constructors Em_GFoo and Em_GBar should be hidden. The user should
use `smart' constructors em_gfoo and em_gbar, which not only set the
correct type (Int vs Bool) but also produce the witness, viz. Em_GFoo
or Em_GBar.
Now, the test_gfoo function should be written as
tesd_emulate_gfoo :: EmulateGTFoo a - a
tesd_emulate_gfoo vf = case vf of Em_GFoo - unsafeCoerce (1::Int)
So, we test for evidence, Em_GFoo, and if it is presented, we proceed
with unsafeCoerce, which generalizes Int to the desired type 'a'. We
know this generalization is safe because the evidence Em_GFoo told us
that 'a' was really Int. The similarity with Dynamics is uncanny.
Now, had we used an irrefutable match instead, we would have
proceeded with unsafeCoerce without checking for the evidence.
The following code, written back in Sep 13, 2004, shows that the above
is not an empty concern. The code did indeed typecheck, with the
version of GHC (tidt-branch CVS branch) that existed at that
time. Running the code produced the result one'd expect when reading
an Int as a Bool. I think the code below was the reason GHC prohibited
irrefutable GADT pattern matching since.
{-# OPTIONS -fglasgow-exts #-}
module Main where
import Data.IORef
data T a where
Li:: Int - T Int
Lb:: Bool - T Bool
La:: a - T a
writeInt:: T a - IORef a - IO ()
writeInt v ref = case v of
~(Li x) - writeIORef ref (1::Int)
readBool:: T a - IORef a - IO ()
readBool v ref = case v of
~(Lb x) -
readIORef ref = (print . not)
tt::T a - IO ()
tt v = case v of
~(Li x) - print OK
main = do
tt (La undefined)
ref - newIORef undefined
writeInt (La undefined) ref
readBool (La undefined) ref
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] irrefutable patterns for existential types / GADTs
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 === _|_ The wish is that f = \refl - Just . coerce refl = \~Refl x - Just x should satisfy f _|_ x === Just _|_ f _|_ x =/= _|_ and likewise for any other constructor than Just. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] irrefutable patterns for existential types / GADTs
[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
