[Haskell] "Never" GADT Function?

[Martin Sulzmann]

You should be able to even write

neverT (BoolT x) = x
neverT (IntT x) = False
-- neverT = undefined -- also possible

cause as a temporary type assumptions we'll add in Bool=Char
(or Int=Char in case of the second clause which effectively
equals False, the always false constraint.
Note that under the False assumption we can give any type
to the result expression.

I don't know whether this is supported in GHC, at least,
it works in Chameleon (which also supports GADTs and a bit more).

Here's the Chameleon code.

data T a = (a=Bool) => BoolT a
         | (a=Int)  => IntT a

neverT :: T Char -> x
neverT (BoolT x) = x
neverT (IntT x) = False

Chameleon is available via
http://www.comp.nus.edu.sg/~sulzmann/chameleon
(look for Existentially Quantified Type Classes)
A new update is coming soon.

Martin



Ashley Yakeley writes:
 > OK, so I've been playing around with GADTs in the CVS GHC. Consider this:
 > 
 >   data T a where
 >     BoolT :: T Bool
 >     IntT :: T Int
 > 
 >   neverT :: T Char -> x
 > 
 > Is it possible to write neverT without using undefined? Such functions 
 > are occasionally useful, especially when GADTs are being used as type 
 > witnesses.
 > 
 > Then again, I suppose it's the same situation for types with no 
 > constructors.
 > 
 > -- 
 > Ashley Yakeley, Seattle WA
 > 
 > _______________________________________________
 > Haskell mailing list
 > Haskell at haskell.org
 > http://www.haskell.org/mailman/listinfo/haskell