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
> [email protected]
> http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
