Type classes in GADTs
C Rodrigues
red5_2 at hotmail.com
Thu Oct 30 01:20:43 EDT 2008
I discovered that closed type classes can be implicitly defined using GADTs. The GADT value itself acts like a class dictionary. However, GHC (6.8.3) doesn't know anything about these type classes, and it won't infer any class memberships. In the example below, an instance of Eq is not recognized.
So is this within the domain of GHC's type inference, not something it shoud infer, or a bug?
{-# OPTIONS_GHC -XTypeFamilies -XGADTs -XEmptyDataDecls #-}
module CaseAnalysisOnGADTs where
-- Commutative and associative operators.
data CAOp a where
Sum :: CAOp Int
Disj :: CAOp Bool
Concat :: CAOp String
{- For any non-bottom value of type 'CAOp a', the value will have type
-- CAOp Int, CAOp Bool, or CAOp String. Int, Bool, and String are all
-- members of Eq. Therefore, if we have a non-bottom value of type
-- 'CAOp a' then 'a' is a member of Eq.
-}
data D a = D !(CAOp a) (a, a)
-- However, GHC won't figure this out.
noEvidenceOfEq :: D a -> Bool
noEvidenceOfEq (D op (e1, e2)) = e1 == e2 -- Error, no instance (Eq a)
-- Unless you force it to do case analysis on constructors.
evidenceOfEq :: CAOp a -> a -> a -> Bool
evidenceOfEq Sum = (==)
evidenceOfEq Disj = (==)
evidenceOfEq Concat = (==)
-- Then you can use the result from that, but GHC still won't
-- recognize it as an Eq instance.
useEvidenceOfEq :: D a -> Bool
useEvidenceOfEq (D op (e1, e2)) = evidenceOfEq op e1 e2
_________________________________________________________________
You live life beyond your PC. So now Windows goes beyond your PC.
http://clk.atdmt.com/MRT/go/115298556/direct/01/
More information about the Glasgow-haskell-users
mailing list