1{-# LANGUAGE CPP #-} 2{-# LANGUAGE DeriveDataTypeable #-} 3{-# LANGUAGE GADTs #-} 4{-# LANGUAGE RankNTypes #-} 5{-# LANGUAGE ScopedTypeVariables #-} 6{-# LANGUAGE TypeOperators #-} 7#if __GLASGOW_HASKELL__ >= 706 8{-# LANGUAGE PolyKinds #-} 9#endif 10#if __GLASGOW_HASKELL__ >= 704 11#define GHC __GLASGOW_HASKELL__ 12#if (GHC >= 704 && GHC <707) || GHC >= 801 13{-# LANGUAGE Safe #-} 14#else 15{-# LANGUAGE Trustworthy #-} 16#endif 17#undef GHC 18#endif 19module Data.GADT.Internal where 20 21import Control.Applicative (Applicative (..)) 22import Data.Functor.Product (Product (..)) 23import Data.Functor.Sum (Sum (..)) 24import Data.Maybe (isJust, isNothing) 25import Data.Monoid (Monoid (..)) 26import Data.Semigroup (Semigroup (..)) 27import Data.Type.Equality ((:~:) (..)) 28 29#if __GLASGOW_HASKELL__ >=708 30import Data.Typeable (Typeable) 31#endif 32 33#if MIN_VERSION_base(4,10,0) 34import Data.Type.Equality (testEquality) 35import qualified Type.Reflection as TR 36#endif 37 38-- $setup 39-- >>> :set -XKindSignatures -XGADTs 40 41-- |'Show'-like class for 1-type-parameter GADTs. @GShow t => ...@ is equivalent to something 42-- like @(forall a. Show (t a)) => ...@. The easiest way to create instances would probably be 43-- to write (or derive) an @instance Show (T a)@, and then simply say: 44-- 45-- > instance GShow t where gshowsPrec = showsPrec 46class GShow t where 47 gshowsPrec :: Int -> t a -> ShowS 48 49gshows :: GShow t => t a -> ShowS 50gshows = gshowsPrec (-1) 51 52gshow :: (GShow t) => t a -> String 53gshow x = gshows x "" 54 55instance GShow ((:~:) a) where 56 gshowsPrec _ Refl = showString "Refl" 57 58#if MIN_VERSION_base(4,10,0) 59instance GShow TR.TypeRep where 60 gshowsPrec = showsPrec 61#endif 62 63-- 64-- | >>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int) 65-- "InL Refl" 66instance (GShow a, GShow b) => GShow (Sum a b) where 67 gshowsPrec d = \s -> case s of 68 InL x -> showParen (d > 10) (showString "InL " . gshowsPrec 11 x) 69 InR x -> showParen (d > 10) (showString "InR " . gshowsPrec 11 x) 70 71-- | >>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int) 72-- "Pair Refl Refl" 73instance (GShow a, GShow b) => GShow (Product a b) where 74 gshowsPrec d (Pair x y) = showParen (d > 10) 75 $ showString "Pair " 76 . gshowsPrec 11 x 77 . showChar ' ' 78 . gshowsPrec 11 y 79 80-- |@GReadS t@ is equivalent to @ReadS (forall b. (forall a. t a -> b) -> b)@, which is 81-- in turn equivalent to @ReadS (Exists t)@ (with @data Exists t where Exists :: t a -> Exists t@) 82type GReadS t = String -> [(Some t, String)] 83 84getGReadResult :: Some tag -> (forall a. tag a -> b) -> b 85getGReadResult t k = withSome t k 86 87mkGReadResult :: tag a -> Some tag 88mkGReadResult = mkSome 89 90-- |'Read'-like class for 1-type-parameter GADTs. Unlike 'GShow', this one cannot be 91-- mechanically derived from a 'Read' instance because 'greadsPrec' must choose the phantom 92-- type based on the 'String' being parsed. 93class GRead t where 94 greadsPrec :: Int -> GReadS t 95 96greads :: GRead t => GReadS t 97greads = greadsPrec (-1) 98 99gread :: GRead t => String -> (forall a. t a -> b) -> b 100gread s g = withSome (hd [f | (f, "") <- greads s]) g where 101 hd (x:_) = x 102 hd _ = error "gread: no parse" 103 104-- | 105-- 106-- >>> greadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool))) 107-- Just (mkSome (InL Refl)) 108-- 109-- >>> greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int)) 110-- Nothing 111-- 112greadMaybe :: GRead t => String -> (forall a. t a -> b) -> Maybe b 113greadMaybe s g = case [f | (f, "") <- greads s] of 114 (x : _) -> Just (withSome x g) 115 _ -> Nothing 116 117instance GRead ((:~:) a) where 118 greadsPrec p s = readsPrec p s >>= f 119 where 120 f :: forall x. (x :~: x, String) -> [(Some ((:~:) x), String)] 121 f (Refl, rest) = return (mkSome Refl, rest) 122 123instance (GRead a, GRead b) => GRead (Sum a b) where 124 greadsPrec d s = 125 readParen (d > 10) 126 (\s1 -> [ (S $ \k -> withSome r (k . InL), t) 127 | ("InL", s2) <- lex s1 128 , (r, t) <- greadsPrec 11 s2 ]) s 129 ++ 130 readParen (d > 10) 131 (\s1 -> [ (S $ \k -> withSome r (k . InR), t) 132 | ("InR", s2) <- lex s1 133 , (r, t) <- greadsPrec 11 s2 ]) s 134 135------------------------------------------------------------------------------- 136-- GEq 137------------------------------------------------------------------------------- 138 139-- |A class for type-contexts which contain enough information 140-- to (at least in some cases) decide the equality of types 141-- occurring within them. 142class GEq f where 143 -- |Produce a witness of type-equality, if one exists. 144 -- 145 -- A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.: 146 -- 147 -- > extract :: GEq tag => tag a -> DSum tag -> Maybe a 148 -- > extract t1 (t2 :=> x) = do 149 -- > Refl <- geq t1 t2 150 -- > return x 151 -- 152 -- Or in a list comprehension: 153 -- 154 -- > extractMany :: GEq tag => tag a -> [DSum tag] -> [a] 155 -- > extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)] 156 -- 157 -- (Making use of the 'DSum' type from <https://hackage.haskell.org/package/dependent-sum/docs/Data-Dependent-Sum.html Data.Dependent.Sum> in both examples) 158 geq :: f a -> f b -> Maybe (a :~: b) 159 160-- |If 'f' has a 'GEq' instance, this function makes a suitable default 161-- implementation of '(==)'. 162defaultEq :: GEq f => f a -> f b -> Bool 163defaultEq x y = isJust (geq x y) 164 165-- |If 'f' has a 'GEq' instance, this function makes a suitable default 166-- implementation of '(/=)'. 167defaultNeq :: GEq f => f a -> f b -> Bool 168defaultNeq x y = isNothing (geq x y) 169 170instance GEq ((:~:) a) where 171 geq (Refl :: a :~: b) (Refl :: a :~: c) = Just (Refl :: b :~: c) 172 173instance (GEq a, GEq b) => GEq (Sum a b) where 174 geq (InL x) (InL y) = geq x y 175 geq (InR x) (InR y) = geq x y 176 geq _ _ = Nothing 177 178instance (GEq a, GEq b) => GEq (Product a b) where 179 geq (Pair x y) (Pair x' y') = do 180 Refl <- geq x x' 181 Refl <- geq y y' 182 return Refl 183 184#if MIN_VERSION_base(4,10,0) 185instance GEq TR.TypeRep where 186 geq = testEquality 187#endif 188 189------------------------------------------------------------------------------- 190-- GCompare 191------------------------------------------------------------------------------- 192 193-- This instance seems nice, but it's simply not right: 194-- 195-- > instance GEq StableName where 196-- > geq sn1 sn2 197-- > | sn1 == unsafeCoerce sn2 198-- > = Just (unsafeCoerce Refl) 199-- > | otherwise = Nothing 200-- 201-- Proof: 202-- 203-- > x <- makeStableName id :: IO (StableName (Int -> Int)) 204-- > y <- makeStableName id :: IO (StableName ((Int -> Int) -> Int -> Int)) 205-- > 206-- > let Just boom = geq x y 207-- > let coerce :: (a :~: b) -> a -> b; coerce Refl = id 208-- > 209-- > coerce boom (const 0) id 0 210-- > let "Illegal Instruction" = "QED." 211-- 212-- The core of the problem is that 'makeStableName' only knows the closure 213-- it is passed to, not any type information. Together with the fact that 214-- the same closure has the same StableName each time 'makeStableName' is 215-- called on it, there is serious potential for abuse when a closure can 216-- be given many incompatible types. 217 218 219-- |A type for the result of comparing GADT constructors; the type parameters 220-- of the GADT values being compared are included so that in the case where 221-- they are equal their parameter types can be unified. 222data GOrdering a b where 223 GLT :: GOrdering a b 224 GEQ :: GOrdering t t 225 GGT :: GOrdering a b 226#if __GLASGOW_HASKELL__ >=708 227 deriving Typeable 228#endif 229 230-- |TODO: Think of a better name 231-- 232-- This operation forgets the phantom types of a 'GOrdering' value. 233weakenOrdering :: GOrdering a b -> Ordering 234weakenOrdering GLT = LT 235weakenOrdering GEQ = EQ 236weakenOrdering GGT = GT 237 238instance Eq (GOrdering a b) where 239 x == y = weakenOrdering x == weakenOrdering y 240 241instance Ord (GOrdering a b) where 242 compare x y = compare (weakenOrdering x) (weakenOrdering y) 243 244instance Show (GOrdering a b) where 245 showsPrec _ GGT = showString "GGT" 246 showsPrec _ GEQ = showString "GEQ" 247 showsPrec _ GLT = showString "GLT" 248 249instance GShow (GOrdering a) where 250 gshowsPrec = showsPrec 251 252instance GRead (GOrdering a) where 253 greadsPrec _ s = case con of 254 "GGT" -> [(mkSome GGT, rest)] 255 "GEQ" -> [(mkSome GEQ, rest)] 256 "GLT" -> [(mkSome GLT, rest)] 257 _ -> [] 258 where (con, rest) = splitAt 3 s 259 260-- |Type class for comparable GADT-like structures. When 2 things are equal, 261-- must return a witness that their parameter types are equal as well ('GEQ'). 262class GEq f => GCompare f where 263 gcompare :: f a -> f b -> GOrdering a b 264 265instance GCompare ((:~:) a) where 266 gcompare Refl Refl = GEQ 267 268#if MIN_VERSION_base(4,10,0) 269instance GCompare TR.TypeRep where 270 gcompare t1 t2 = 271 case testEquality t1 t2 of 272 Just Refl -> GEQ 273 Nothing -> 274 case compare (TR.SomeTypeRep t1) (TR.SomeTypeRep t2) of 275 LT -> GLT 276 GT -> GGT 277 EQ -> error "impossible: 'testEquality' and 'compare' \ 278 \are inconsistent for TypeRep; report this \ 279 \as a GHC bug" 280#endif 281 282defaultCompare :: GCompare f => f a -> f b -> Ordering 283defaultCompare x y = weakenOrdering (gcompare x y) 284 285instance (GCompare a, GCompare b) => GCompare (Sum a b) where 286 gcompare (InL x) (InL y) = gcompare x y 287 gcompare (InL _) (InR _) = GLT 288 gcompare (InR _) (InL _) = GGT 289 gcompare (InR x) (InR y) = gcompare x y 290 291instance (GCompare a, GCompare b) => GCompare (Product a b) where 292 gcompare (Pair x y) (Pair x' y') = case gcompare x x' of 293 GLT -> GLT 294 GGT -> GGT 295 GEQ -> case gcompare y y' of 296 GLT -> GLT 297 GEQ -> GEQ 298 GGT -> GGT 299 300------------------------------------------------------------------------------- 301-- Some 302------------------------------------------------------------------------------- 303 304-- | Existential. This is type is useful to hide GADTs' parameters. 305-- 306-- >>> data Tag :: * -> * where TagInt :: Tag Int; TagBool :: Tag Bool 307-- >>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool" 308-- >>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> [] 309-- >>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <- lex s, r <- classify con ] 310-- 311-- With Church-encoding youcan only use a functions: 312-- 313-- >>> let y = mkSome TagBool 314-- >>> y 315-- mkSome TagBool 316-- 317-- >>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String 318-- "B" 319-- 320-- or explicitly work with 'S' 321-- 322-- >>> let x = S $ \f -> f TagInt 323-- >>> x 324-- mkSome TagInt 325-- 326-- >>> case x of S f -> f $ \x' -> case x' of { TagInt -> "I"; TagBool -> "B" } :: String 327-- "I" 328-- 329-- The implementation of 'mapSome' is /safe/. 330-- 331-- >>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool 332-- >>> mapSome f y 333-- mkSome TagBool 334-- 335-- but you can also use: 336-- 337-- >>> withSome y (mkSome . f) 338-- mkSome TagBool 339-- 340-- >>> read "Some TagBool" :: Some Tag 341-- mkSome TagBool 342-- 343-- >>> read "mkSome TagInt" :: Some Tag 344-- mkSome TagInt 345-- 346newtype Some tag = S 347 { -- | Eliminator. 348 withSome :: forall r. (forall a. tag a -> r) -> r 349 } 350 351-- | Constructor. 352mkSome :: tag a -> Some tag 353mkSome t = S (\f -> f t) 354 355-- | Map over argument. 356mapSome :: (forall x. f x -> g x) -> Some f -> Some g 357mapSome nt (S fx) = S (\f -> fx (f . nt)) 358 359-- | @'flip' 'withSome'@ 360foldSome :: (forall a. tag a -> b) -> Some tag -> b 361foldSome some (S thing) = thing some 362 363-- | Traverse over argument. 364traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g) 365traverseSome f x = withSome x $ \x' -> fmap mkSome (f x') 366 367-- | Monadic 'withSome'. 368-- 369-- @since 1.0.1 370withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r 371withSomeM m k = m >>= \s -> withSome s k 372 373------------------------------------------------------------------------------- 374-- Church Some instances 375------------------------------------------------------------------------------- 376 377instance GShow tag => Show (Some tag) where 378 showsPrec p some = withSome some $ \thing -> showParen (p > 10) 379 ( showString "mkSome " 380 . gshowsPrec 11 thing 381 ) 382 383instance GRead f => Read (Some f) where 384 readsPrec p = readParen (p>10) $ \s -> 385 [ (withSome withTag mkSome, rest') 386 | (con, rest) <- lex s 387 , con == "Some" || con == "mkSome" 388 , (withTag, rest') <- greadsPrec 11 rest 389 ] 390 391instance GEq tag => Eq (Some tag) where 392 x == y = 393 withSome x $ \x' -> 394 withSome y $ \y' -> defaultEq x' y' 395 396instance GCompare tag => Ord (Some tag) where 397 compare x y = 398 withSome x $ \x' -> 399 withSome y $ \y' -> defaultCompare x' y' 400 401instance Control.Applicative.Applicative m => Data.Semigroup.Semigroup (Some m) where 402 m <> n = 403 withSome m $ \m' -> 404 withSome n $ \n' -> 405 mkSome (m' *> n') 406 407instance Applicative m => Data.Monoid.Monoid (Some m) where 408 mempty = mkSome (pure ()) 409 mappend = (<>) 410