dependent-sum 0.5 → 0.6

raw patch · 9 files changed

+271/−300 lines, 9 filesdep +constraints-extrasdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: constraints-extras

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +15/−0
• dependent-sum.cabal +8/−9
• examples/FooGADT.hs +23/−29
• src/Data/Dependent/Sum.hs +59/−156
• src/Data/Dependent/Sum.hs-boot +0/−5
• src/Data/Dependent/Sum/Typeable.hs +0/−26
• src/Data/GADT/Compare.hs +52/−63
• src/Data/GADT/Show.hs +66/−10
• src/Data/Some.hs +48/−2

@@ -1,5 +1,20 @@ # Revision history for dependent-sum +## 0.6 - 2019-03-21++* Use constraints-extras ArgDict/Has' to define the instances of Eq, Ord, Read and Show for DSum.+  This obviates the need for the EqTag, OrdTag, ReadTag and ShowTag classes.++## 0.5.1.0++* Add `mkSome` and `mapSome` to `Data.Some`.+* Add `GEq`, `GCompare`, `GShow,` and `GRead` instances for `Sum` and `Product` (Except `GRead (Product a b)`).+* Deprecate `(:=)` for `(:~:)` from `Data.Type.Equality`.+  In GHC 7.8 and above, this is the same as `(:~:)`.+  But now we no longer support earlier GHCs, so there's no point of the alias.+* Remove support for GHC 7.x.+* The git repositories for dependent-sum and dependent-sum-template are now the same, though the Haskell packages remain separate.+ ## 0.5.0.0  * Make `Some` a `newtype` with associated pattern synonyms using `unsafeCoerce`

@@ -1,5 +1,5 @@ name:                   dependent-sum-version:                0.5+version:                0.6 stability:              provisional  cabal-version:          >= 1.6@@ -26,10 +26,11 @@  tested-with:            GHC == 8.0.2,                         GHC == 8.2.2,-                        GHC == 8.4.4+                        GHC == 8.4.4,+                        GHC == 8.6.4 -extra-source-files:     examples/*.hs-                        ChangeLog.md+extra-source-files:     ChangeLog.md+                      , examples/*.hs  source-repository head   type:     git@@ -41,10 +42,8 @@                         Data.GADT.Compare                         Data.GADT.Show                         Data.Some-  -  if impl(ghc < 7.8)-    other-modules:      Data.Dependent.Sum.Typeable-  -  build-depends:        base >= 3 && <5+  other-extensions:     PatternSynonyms+  build-depends:        base >= 4.9 && <5+                      , constraints-extras >= 0.2 && < 0.4   if impl(ghc >= 7.2)     ghc-options:        -trust base

@@ -1,11 +1,17 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TemplateHaskell #-}+ module FooGADT where  import Data.Dependent.Sum import Data.Functor.Identity import Data.GADT.Show import Data.GADT.Compare+import Data.Constraint.Extras+import Data.Constraint.Extras.TH+import Data.List (sort)  data Foo a where     Foo :: Foo Double@@ -13,6 +19,20 @@     Baz :: Foo String     Qux :: Foo Double +deriveArgDict ''Foo++{-+-- NB: The instance for ArgDict could be manually written as:++instance ArgDict Foo where+    type ConstraintsFor Foo c = (c Double, c Int, c String)+    argDict x = case x of+        Foo -> Dict+        Bar -> Dict+        Baz -> Dict+        Qux -> Dict+-}+ instance Eq (Foo a) where     (==) = defaultEq @@ -23,13 +43,6 @@     geq Qux Qux = Just Refl     geq _   _   = Nothing -instance EqTag Foo Identity where-    eqTagged Foo Foo = (==)-    eqTagged Bar Bar = (==)-    eqTagged Baz Baz = (==)-    eqTagged Qux Qux = (==)-    eqTagged _   _   = const (const False)- instance GCompare Foo where     gcompare Foo Foo = GEQ     gcompare Foo _   = GLT@@ -45,14 +58,6 @@          gcompare Qux Qux = GEQ -instance OrdTag Foo Identity where-    compareTagged Foo Foo = compare-    compareTagged Bar Bar = compare-    compareTagged Baz Baz = compare-    compareTagged Qux Qux = compare-    -    compareTagged _   _   = error "OrdTag (Foo): bad case"- instance Show (Foo a) where     showsPrec _ Foo      = showString "Foo"     showsPrec _ Bar      = showString "Bar"@@ -62,13 +67,6 @@ instance GShow Foo where     gshowsPrec = showsPrec -instance ShowTag Foo Identity where-    showTaggedPrec Foo = showsPrec-    showTaggedPrec Bar = showsPrec-    showTaggedPrec Baz = showsPrec-    showTaggedPrec Qux = showsPrec-- instance GRead Foo where     greadsPrec _ str = case tag of         "Foo" -> [(GReadResult (\k -> k Foo), rest)]@@ -78,12 +76,6 @@         _     -> []         where (tag, rest) = splitAt 3 str -instance ReadTag Foo Identity where-    readTaggedPrec Foo = readsPrec-    readTaggedPrec Bar = readsPrec-    readTaggedPrec Baz = readsPrec-    readTaggedPrec Qux = readsPrec- foo :: Double -> DSum Foo Identity foo x = Foo ==> x @@ -96,5 +88,7 @@ qux :: Double -> DSum Foo Identity qux x = Qux ==> x -xs = [foo pi, bar 100, baz "hello world", qux (exp 1)]+xs, xs', xs'' :: [DSum Foo Identity]+xs = [bar 100, foo pi, qux (exp 1), baz "hello world"] xs' = read (show xs) `asTypeOf` xs+xs'' = sort xs

@@ -1,51 +1,49 @@-{-# LANGUAGE ExistentialQuantification, GADTs #-}-{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Safe #-}-#endif-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 {-# LANGUAGE PolyKinds #-}-#endif+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-} module Data.Dependent.Sum where  import Control.Applicative -#if MIN_VERSION_base(4,7,0)-import Data.Typeable (Typeable)-#else-import Data.Dependent.Sum.Typeable ({- instance Typeable ... -})-#endif+import Data.Constraint.Extras+import Data.Type.Equality ((:~:) (..))  import Data.GADT.Show import Data.GADT.Compare  import Data.Maybe (fromMaybe) --- |A basic dependent sum type; the first component is a tag that specifies +import Text.Read++-- |A basic dependent sum type; the first component is a tag that specifies -- the type of the second;  for example, think of a GADT such as:--- +-- -- > data Tag a where -- >    AString :: Tag String -- >    AnInt   :: Tag Int--- +-- -- Then, we have the following valid expressions of type @Applicative f => DSum Tag f@: -- -- > AString ==> "hello!" -- > AnInt   ==> 42--- --- And we can write functions that consume @DSum Tag f@ values by matching, +--+-- And we can write functions that consume @DSum Tag f@ values by matching, -- such as:--- +-- -- > toString :: DSum Tag Identity -> String -- > toString (AString :=> Identity str) = str -- > toString (AnInt   :=> Identity int) = show int--- +-- -- By analogy to the (key => value) construction for dictionary entries in -- many dynamic languages, we use (key :=> value) as the constructor for -- dependent sums.  The :=> and ==> operators have very low precedence and@@ -55,162 +53,67 @@ -- @DSum Identity Tag@.  Its precedence is just above that of '$', so -- @foo bar $ AString ==> "eep"@ is equivalent to @foo bar (AString ==> "eep")@. data DSum tag f = forall a. !(tag a) :=> f a-#if MIN_VERSION_base(4,7,0)-    deriving Typeable-#endif+ infixr 1 :=>, ==>  (==>) :: Applicative f => tag a -> a -> DSum tag f k ==> v = k :=> pure v --- |In order to make a 'Show' instance for @DSum tag f@, @tag@ must be able--- to show itself as well as any value of the tagged type.  'GShow' together--- with this class provides the interface by which it can do so.------ @ShowTag tag f => t@ is conceptually equivalent to something like this--- imaginary syntax:  @(forall a. Inhabited (tag a) => Show (f a)) => t@,--- where 'Inhabited' is an imaginary predicate that characterizes --- non-empty types, and 'f' and 'a' do not occur free in 't'.------ The @Tag@ example type introduced in the 'DSum' section could be given the--- following instances, among others:--- --- > instance GShow Tag where--- >     gshowsPrec _p AString = showString "AString"--- >     gshowsPrec _p AnInt   = showString "AnInt"--- > instance ShowTag Tag [] where--- >     showTaggedPrec AString = showsPrec--- >     showTaggedPrec AnInt   = showsPrec--- -class GShow tag => ShowTag tag f where-    -- |Given a value of type @tag a@, return the 'showsPrec' function for -    -- the type @f a@.-    showTaggedPrec :: tag a -> Int -> f a -> ShowS--instance Show (f a) => ShowTag ((:=) a) f where-    showTaggedPrec Refl = showsPrec---- This instance is questionable.  It works, but is pretty useless.-instance Show (f a) => ShowTag (GOrdering a) f where-    showTaggedPrec GEQ = showsPrec-    showTaggedPrec _   = \p _ -> showParen (p > 10)-        ( showString "error "-        . shows "type information lost into the mists of oblivion"-        )--instance ShowTag tag f => Show (DSum tag f) where+instance forall tag f. (GShow tag, Has' Show tag f) => Show (DSum tag f) where     showsPrec p (tag :=> value) = showParen (p >= 10)         ( gshowsPrec 0 tag         . showString " :=> "-        . showTaggedPrec tag 1 value+        . has' @Show @f tag (showsPrec 1 value)         ) -class GRead tag => ReadTag tag f where-    readTaggedPrec :: tag a -> Int -> ReadS (f a)---- |In order to make a 'Read' instance for @DSum tag f@, @tag@ must be able--- to parse itself as well as any value of the tagged type.  'GRead' together--- with this class provides the interface by which it can do so.------ @ReadTag tag f => t@ is conceptually equivalent to something like this--- imaginary syntax:  @(forall a. Inhabited (tag a) => Read (f a)) => t@,--- where 'Inhabited' is an imaginary predicate that characterizes --- non-empty types, and 'f' and 'a' do not occur free in 't'.------ The @Tag@ example type introduced in the 'DSum' section could be given the--- following instances, among others:--- --- > instance GRead Tag where--- >     greadsPrec _p str = case tag of--- >        "AString"   -> [(\k -> k AString, rest)]--- >        "AnInt"     -> [(\k -> k AnInt,   rest)]--- >        _           -> []--- >        where (tag, rest) = break isSpace str--- > instance ReadTag Tag [] where--- >     readTaggedPrec AString = readsPrec--- >     readTaggedPrec AnInt   = readsPrec--- -instance Read (f a) => ReadTag ((:=) a) f where-    readTaggedPrec Refl = readsPrec---- This instance is questionable.  It works, but is partial (and is also pretty useless)--- instance Read a => ReadTag (GOrdering a) where---     readTaggedPrec GEQ = readsPrec---     readTaggedPrec tag = \p -> readParen (p>10) $ \s ->---         [ (error msg, rest')---         | let (con, rest) = splitAt 6 s---         , con == "error "---         , (msg, rest') <- reads rest :: [(String, String)]---         ]--instance ReadTag tag f => Read (DSum tag f) where-    readsPrec p = readParen (p > 1) $ \s -> +instance forall tag f. (GRead tag, Has' Read tag f) => Read (DSum tag f) where+    readsPrec p = readParen (p > 1) $ \s ->         concat             [ getGReadResult withTag $ \tag ->                 [ (tag :=> val, rest'')-                | (val, rest'') <- readTaggedPrec tag 1 rest'+                | (val, rest'') <- has' @Read @f tag (readsPrec 1 rest')                 ]             | (withTag, rest) <- greadsPrec p s             , let (con, rest') = splitAt 5 rest             , con == " :=> "             ] --- |In order to test @DSum tag f@ for equality, @tag@ must know how to test--- both itself and its tagged values for equality.  'EqTag' defines--- the interface by which they are expected to do so.--- --- Continuing the @Tag@ example from the 'DSum' section, we can define:--- --- > instance GEq Tag where--- >     geq AString AString = Just Refl--- >     geq AnInt   AnInt   = Just Refl--- >     geq _       _       = Nothing--- > instance EqTag Tag [] where--- >     eqTagged AString AString = (==)--- >     eqTagged AnInt   AnInt   = (==)--- --- Note that 'eqTagged' is not called until after the tags have been--- compared, so it only needs to consider the cases where 'gcompare' returns 'GEQ'.-class GEq tag => EqTag tag f where-    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),-    -- return the '==' function for the type @f a@.-    eqTagged :: tag a -> tag a -> f a -> f a -> Bool--instance Eq (f a) => EqTag ((:=) a) f where-    eqTagged Refl Refl = (==)--instance EqTag tag f => Eq (DSum tag f) where+instance forall tag f. (GEq tag, Has' Eq tag f) => Eq (DSum tag f) where     (t1 :=> x1) == (t2 :=> x2)  = fromMaybe False $ do         Refl <- geq t1 t2-        return (eqTagged t1 t2 x1 x2)---- |In order to compare @DSum tag f@ values, @tag@ must know how to compare--- both itself and its tagged values.  'OrdTag' defines the --- interface by which they are expected to do so.--- --- Continuing the @Tag@ example from the 'EqTag' section, we can define:--- --- > instance GCompare Tag where--- >     gcompare AString AString = GEQ--- >     gcompare AString AnInt   = GLT--- >     gcompare AnInt   AString = GGT--- >     gcompare AnInt   AnInt   = GEQ--- > instance OrdTag Tag [] where--- >     compareTagged AString AString = compare--- >     compareTagged AnInt   AnInt   = compare--- --- As with 'eqTagged', 'compareTagged' only needs to consider cases where--- 'gcompare' returns 'GEQ'.-class (EqTag tag f, GCompare tag) => OrdTag tag f where-    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),-    -- return the 'compare' function for the type @f a@.-    compareTagged :: tag a -> tag a -> f a -> f a -> Ordering--instance Ord (f a) => OrdTag ((:=) a) f where-    compareTagged Refl Refl = compare+        return $ has' @Eq @f t1 (x1 == x2) -instance OrdTag tag f => Ord (DSum tag f) where+instance forall tag f. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f) where     compare (t1 :=> x1) (t2 :=> x2)  = case gcompare t1 t2 of         GLT -> LT         GGT -> GT-        GEQ -> compareTagged t1 t2 x1 x2+        GEQ -> has' @Ord @f t1 (x1 `compare` x2)++{-# DEPRECATED ShowTag "Instead of 'ShowTag tag f', use '(GShow tag, Has' Show tag f)'" #-}+type ShowTag tag f = (GShow tag, Has' Show tag f)++showTaggedPrec :: forall tag f a. (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS+showTaggedPrec tag = has' @Show @f tag showsPrec++{-# DEPRECATED ReadTag "Instead of 'ReadTag tag f', use '(GRead tag, Has' Read tag f)'" #-}+type ReadTag tag f = (GRead tag, Has' Read tag f)++readTaggedPrec :: forall tag f a. (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a)+readTaggedPrec tag = has' @Read @f tag readsPrec++{-# DEPRECATED EqTag "Instead of 'EqTag tag f', use '(GEq tag, Has' Eq tag f)'" #-}+type EqTag tag f = (GEq tag, Has' Eq tag f)++eqTaggedPrec :: forall tag f a. (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool+eqTaggedPrec tag1 tag2 f1 f2 = case tag1 `geq` tag2 of+  Nothing -> False+  Just Refl -> has' @Eq @f tag1 $ f1 == f2++{-# DEPRECATED OrdTag "Instead of 'OrdTag tag f', use '(GCompare tag, Has' Ord tag f)'" #-}+type OrdTag tag f = (GCompare tag, Has' Ord tag f)++compareTaggedPrec :: forall tag f a. (GCompare tag, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering+compareTaggedPrec tag1 tag2 f1 f2 = case tag1 `gcompare` tag2 of+  GLT -> LT+  GEQ -> has' @Ord @f tag1 $ f1 `compare` f2+  GGT -> GT

@@ -1,5 +0,0 @@-{-# LANGUAGE ExistentialQuantification, TypeOperators #-}-module Data.Dependent.Sum where--data DSum tag f = forall a. !(tag a) :=> f a-infixr 1 :=>

@@ -1,26 +0,0 @@-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Trustworthy #-}-#endif--- |Separate module for Typeable declaration, to minimize the amount of--- visual inspection required to determine that this package is "safe"--- --- This separation is not necessary with base >= 4.7, so this module will--- not be compiled at all with GHC >= 7.8.-module Data.Dependent.Sum.Typeable where--import {-# SOURCE #-} Data.Dependent.Sum-import Data.Typeable---instance (Typeable1 t, Typeable1 f) => Typeable (DSum t f) where-    typeOf ds = mkTyConApp dSumCon [typeOfF, typeOfT]-        where-            typeOfF = typeOf1 $ (undefined :: DSum f t -> f a) ds-            typeOfT = typeOf1 $ (undefined :: DSum f t -> t a) ds--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-            dSumCon = mkTyCon3 "dependent-sum" "Data.Dependent.Sum" "DSum"-#else -            dSumCon = mkTyCon "Data.Dependent.Sum.DSum"-#endif

@@ -1,136 +1,110 @@ {-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DeriveDataTypeable #-}-{-# OPTIONS_GHC -fno-warn-deprecated-flags #-} {-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 {-# LANGUAGE PolyKinds #-}-#endif-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Safe #-}-#endif {-# LANGUAGE ScopedTypeVariables #-}-+{-# OPTIONS_GHC -fno-warn-deprecated-flags #-} module Data.GADT.Compare     ( module Data.GADT.Compare-#if MIN_VERSION_base(4,7,0)     , (:~:)(Refl)-#endif     ) where  import Data.Maybe import Data.GADT.Show+import Data.Type.Equality ((:~:) (..)) import Data.Typeable+import Data.Functor.Sum (Sum (..))+import Data.Functor.Product (Product (..))  #if MIN_VERSION_base(4,10,0) import qualified Type.Reflection as TR import Data.Type.Equality (testEquality) #endif -#if MIN_VERSION_base(4,7,0) -- |Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.+{-# DEPRECATED (:=) "use '(:~:)' from 'Data.Type,Equality'." #-} type (:=) = (:~:) -#else---- |A GADT witnessing equality of two types.  Its only inhabitant is 'Refl'.-data a := b where-    Refl :: a := a-    deriving Typeable--instance Eq (a := b) where-    Refl == Refl = True--instance Ord (a := b) where-    compare Refl Refl = EQ--instance Show (a := b) where-    showsPrec _ Refl = showString "Refl"--instance Read (a := a) where-    readsPrec _ s = case con of-        "Refl"  -> [(Refl, rest)]-        _       -> []-        where (con,rest) = splitAt 4 s--#endif--instance GShow ((:=) a) where-    gshowsPrec _ Refl = showString "Refl"--instance GRead ((:=) a) where-    greadsPrec p s = readsPrec p s >>= f-        where-            f :: forall x. (x := x, String) -> [(GReadResult ((:=) x), String)]-            f (Refl, rest) = return (GReadResult (\x -> x Refl) , rest)- -- |A class for type-contexts which contain enough information--- to (at least in some cases) decide the equality of types +-- to (at least in some cases) decide the equality of types -- occurring within them. class GEq f where     -- |Produce a witness of type-equality, if one exists.-    -- +    --     -- A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:-    -- +    --     -- > extract :: GEq tag => tag a -> DSum tag -> Maybe a     -- > extract t1 (t2 :=> x) = do     -- >     Refl <- geq t1 t2     -- >     return x-    -- +    --     -- Or in a list comprehension:-    -- +    --     -- > extractMany :: GEq tag => tag a -> [DSum tag] -> [a]     -- > extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]     --     -- (Making use of the 'DSum' type from "Data.Dependent.Sum" in both examples)-    geq :: f a -> f b -> Maybe (a := b)+    geq :: f a -> f b -> Maybe (a :~: b) --- |If 'f' has a 'GEq' instance, this function makes a suitable default +-- |If 'f' has a 'GEq' instance, this function makes a suitable default -- implementation of '(==)'. defaultEq :: GEq f => f a -> f b -> Bool defaultEq x y = isJust (geq x y) --- |If 'f' has a 'GEq' instance, this function makes a suitable default +-- |If 'f' has a 'GEq' instance, this function makes a suitable default -- implementation of '(/=)'. defaultNeq :: GEq f => f a -> f b -> Bool defaultNeq x y = isNothing (geq x y) -instance GEq ((:=) a) where-    geq (Refl :: a := b) (Refl :: a := c) = Just (Refl :: b := c)+instance GEq ((:~:) a) where+    geq (Refl :: a :~: b) (Refl :: a :~: c) = Just (Refl :: b :~: c) +instance (GEq a, GEq b) => GEq (Sum a b) where+    geq (InL x) (InL y) = geq x y+    geq (InR x) (InR y) = geq x y+    geq _ _ = Nothing++instance (GEq a, GEq b) => GEq (Product a b) where+    geq (Pair x y) (Pair x' y') = do+        Refl <- geq x x'+        Refl <- geq y y'+        return Refl+ #if MIN_VERSION_base(4,10,0) instance GEq TR.TypeRep where     geq = testEquality #endif  -- This instance seems nice, but it's simply not right:--- +-- -- > instance GEq StableName where -- >     geq sn1 sn2 -- >         | sn1 == unsafeCoerce sn2 -- >             = Just (unsafeCoerce Refl) -- >         | otherwise     = Nothing--- +-- -- Proof:--- +-- -- > x <- makeStableName id :: IO (StableName (Int -> Int)) -- > y <- makeStableName id :: IO (StableName ((Int -> Int) -> Int -> Int))--- > +-- > -- > let Just boom = geq x y--- > let coerce :: (a := b) -> a -> b; coerce Refl = id--- > +-- > let coerce :: (a :~: b) -> a -> b; coerce Refl = id+-- > -- > coerce boom (const 0) id 0 -- > let "Illegal Instruction" = "QED."--- +-- -- The core of the problem is that 'makeStableName' only knows the closure -- it is passed to, not any type information.  Together with the fact that--- the same closure has the same StableName each time 'makeStableName' is --- called on it, there is serious potential for abuse when a closure can +-- the same closure has the same StableName each time 'makeStableName' is+-- called on it, there is serious potential for abuse when a closure can -- be given many incompatible types.   -- |A type for the result of comparing GADT constructors; the type parameters--- of the GADT values being compared are included so that in the case where +-- of the GADT values being compared are included so that in the case where -- they are equal their parameter types can be unified. data GOrdering a b where     GLT :: GOrdering a b@@ -174,7 +148,7 @@ class GEq f => GCompare f where     gcompare :: f a -> f b -> GOrdering a b -instance GCompare ((:=) a) where+instance GCompare ((:~:) a) where     gcompare Refl Refl = GEQ  #if MIN_VERSION_base(4,10,0)@@ -193,3 +167,18 @@  defaultCompare :: GCompare f => f a -> f b -> Ordering defaultCompare x y = weakenOrdering (gcompare x y)++instance (GCompare a, GCompare b) => GCompare (Sum a b) where+    gcompare (InL x) (InL y) = gcompare x y+    gcompare (InL _) (InR _) = GLT+    gcompare (InR _) (InL _) = GGT+    gcompare (InR x) (InR y) = gcompare x y++instance (GCompare a, GCompare b) => GCompare (Product a b) where+    gcompare (Pair x y) (Pair x' y') = case gcompare x x' of+        GLT -> GLT+        GGT -> GGT+        GEQ -> case gcompare y y' of+            GLT -> GLT+            GEQ -> GEQ+            GGT -> GGT

@@ -1,17 +1,23 @@-{-# LANGUAGE RankNTypes #-} {-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Safe #-}-#endif-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+{-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-}-#endif+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-} module Data.GADT.Show where +import Data.Functor.Sum (Sum (..))+import Data.Functor.Product (Product (..))+import Data.Type.Equality ((:~:) (..))+ #if MIN_VERSION_base(4,10,0) import qualified Type.Reflection as TR #endif +-- $setup+-- >>> import Data.Some+ -- |'Show'-like class for 1-type-parameter GADTs.  @GShow t => ...@ is equivalent to something -- like @(forall a. Show (t a)) => ...@.  The easiest way to create instances would probably be -- to write (or derive) an @instance Show (T a)@, and then simply say:@@ -20,17 +26,36 @@ class GShow t where     gshowsPrec :: Int -> t a -> ShowS +gshows :: GShow t => t a -> ShowS+gshows = gshowsPrec (-1) +gshow :: (GShow t) => t a -> String+gshow x = gshows x ""++instance GShow ((:~:) a) where+    gshowsPrec _ Refl = showString "Refl"+ #if MIN_VERSION_base(4,10,0) instance GShow TR.TypeRep where     gshowsPrec = showsPrec #endif -gshows :: GShow t => t a -> ShowS-gshows = gshowsPrec (-1)+--+-- | >>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)+-- "InL Refl"+instance (GShow a, GShow b) => GShow (Sum a b) where+    gshowsPrec d = \s -> case s of+        InL x -> showParen (d > 10) (showString "InL " . gshowsPrec 11 x)+        InR x -> showParen (d > 10) (showString "InR " . gshowsPrec 11 x) -gshow :: (GShow t) => t a -> String-gshow x = gshows x ""+-- | >>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)+-- "Pair Refl Refl"+instance (GShow a, GShow b) => GShow (Product a b) where+    gshowsPrec d (Pair x y) = showParen (d > 10)+        $ showString "Pair "+        . gshowsPrec 11 x+        . showChar ' '+        . gshowsPrec 11 y  newtype GReadResult t = GReadResult   { getGReadResult :: forall b . (forall a . t a -> b) -> b }@@ -54,3 +79,34 @@     where         hd (x:_) = x         hd _ = error "gread: no parse"++-- |+--+-- >>> greadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool)))+-- Just (Some (InL Refl))+--+-- >>> greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int))+-- Nothing+--+greadMaybe :: GRead t => String -> (forall a. t a -> b) -> Maybe b+greadMaybe s g = case [f | (f, "") <- greads s] of+    (GReadResult res : _) -> Just (res g)+    _                     -> Nothing++instance GRead ((:~:) a) where+    greadsPrec p s = readsPrec p s >>= f+        where+            f :: forall x. (x :~: x, String) -> [(GReadResult ((:~:) x), String)]+            f (Refl, rest) = return (GReadResult (\x -> x Refl) , rest)++instance (GRead a, GRead b) => GRead (Sum a b) where+    greadsPrec d s = concat+        [ readParen (d > 10)+            (\s1 -> [ (GReadResult $ \k -> getGReadResult r (k . InL), t)+                    | ("InL", s2) <- lex s1+                    , (r, t) <- greadsPrec 11 s2 ]) s+        , readParen (d > 10)+            (\s1 -> [ (GReadResult $ \k -> getGReadResult r (k . InR), t)+                    | ("InR", s2) <- lex s1+                    , (r, t) <- greadsPrec 11 s2 ]) s+        ]

@@ -5,13 +5,51 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE ViewPatterns #-}-module Data.Some (Some(Some, This), withSome) where+{-# LANGUAGE Trustworthy #-}+module Data.Some (Some(Some, This), mkSome, withSome, mapSome) where  import Data.GADT.Show import Data.GADT.Compare import GHC.Exts (Any)-import Unsafe.Coerce+import Unsafe.Coerce (unsafeCoerce) +-- $setup+-- >>> :set -XKindSignatures -XGADTs++-- | Existential. This is type is useful to hide GADTs' parameters.+--+-- >>> data Tag :: * -> * where TagInt :: Tag Int; TagBool :: Tag Bool+-- >>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"+--+-- You can either use @PatternSynonyms@+--+-- >>> let x = Some TagInt+-- >>> x+-- Some TagInt+--+-- >>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String+-- "I"+--+-- or you can use functions+--+-- >>> let y = mkSome TagBool+-- >>> y+-- Some TagBool+--+-- >>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String+-- "B"+--+-- The implementation of 'mapSome' is /safe/.+--+-- >>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool+-- >>> mapSome f y+-- Some TagBool+--+-- but you can also use:+--+-- >>> withSome y (mkSome . f)+-- Some TagBool+-- newtype Some tag = UnsafeSome (tag Any)  #if __GLASGOW_HASKELL__ >= 801@@ -28,6 +66,11 @@ pattern This :: tag a -> Some tag pattern This x = Some x +-- | Constructor.+mkSome :: tag a -> Some tag+mkSome = Some++-- | Eliminator. withSome :: Some tag -> (forall a. tag a -> b) -> b withSome (Some thing) some = some thing @@ -50,3 +93,6 @@  instance GCompare tag => Ord (Some tag) where     compare (Some x) (Some y) = defaultCompare x y++mapSome :: (forall t. f t -> g t) -> Some f -> Some g+mapSome f (UnsafeSome x) = UnsafeSome (f x)