dependent-sum 0.6.2.0 → 0.6.2.2

raw patch · 6 files changed

+59/−415 lines, 6 filesdep +somedep ~basenew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: some

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +8/−0
• dependent-sum.cabal +14/−8
• src/Data/Dependent/Sum.hs +37/−13
• src/Data/GADT/Compare.hs +0/−184
• src/Data/GADT/Show.hs +0/−112
• src/Data/Some.hs +0/−98

@@ -1,5 +1,13 @@ # Revision history for dependent-sum +## 0.6.2.2 - 2020-03-23++* Update GitHub repository in cabal metadata.++## 0.6.2.1 - 2020-03-21++* Update cabal meta-information (tested with GHC 8.8).+ ## 0.6.2.0 - 2019-08-04  * Revert change that increased strictness of Data.Some.Some in 0.6.1

@@ -1,14 +1,14 @@ name:                   dependent-sum-version:                0.6.2.0+version:                0.6.2.2 stability:              provisional -cabal-version:          >= 1.6+cabal-version:          1.22 build-type:             Simple  author:                 James Cook <mokus@deepbondi.net>-maintainer:             James Cook <mokus@deepbondi.net>+maintainer:             Obsidian Systems, LLC <maintainer@obsidian.systems> license:                PublicDomain-homepage:               https://github.com/mokus0/dependent-sum+homepage:               https://github.com/obsidiansystems/dependent-sum  category:               Data, Dependent Types synopsis:               Dependent sum type@@ -27,23 +27,29 @@ tested-with:            GHC == 8.0.2,                         GHC == 8.2.2,                         GHC == 8.4.4,-                        GHC == 8.6.4+                        GHC == 8.6.5,+                        GHC == 8.8.3  extra-source-files:     ChangeLog.md                       , examples/*.hs  source-repository head   type:     git-  location: git://github.com/mokus0/dependent-sum.git+  location: https://github.com/obsidiansystems/dependent-sum  Library+  default-language:     Haskell2010   hs-source-dirs:       src   exposed-modules:      Data.Dependent.Sum-                        Data.GADT.Compare-                        Data.GADT.Show+  reexported-modules:   Data.GADT.Compare,+                        Data.GADT.Show,                         Data.Some   other-extensions:     PatternSynonyms   build-depends:        base >= 4.9 && <5                       , constraints-extras >= 0.2 && < 0.4++  -- tight bounds, so re-exported API is versioned properly.+  build-depends:        some >= 1.0.0.3 && <1.0.1+   if impl(ghc >= 7.2)     ghc-options:        -trust base

@@ -25,37 +25,61 @@  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:+-- | A basic dependent sum type where 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+-- >    Rec     :: Tag (DSum Tag Identity) ----- Then, we have the following valid expressions of type @Applicative f => DSum Tag f@:+-- Then we can write expressions where the RHS of @(':=>')@ has+-- different types depending on the @Tag@ constructor used. Here are+-- some expressions of type @DSum Tag 'Identity'@: --+-- > AString :=> Identity "hello!"+-- > AnInt   :=> Identity 42+--+-- Often, the @f@ we choose has an 'Applicative' instance, and we can+-- use the helper function @('==>')@. The following expressions all+-- have the type @Applicative f => DSum Tag f@:+-- -- > AString ==> "hello!" -- > AnInt   ==> 42 ----- And we can write functions that consume @DSum Tag f@ values by matching,--- such as:+-- 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+-- > toString (Rec     :=> Identity sum) = toString sum ----- 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--- bind to the right, so if the @Tag@ GADT is extended with an additional--- constructor @Rec :: Tag (DSum Tag Identity)@, then @Rec ==> AnInt ==> 3 + 4@--- is parsed as would be expected (@Rec ==> (AnInt ==> (3 + 4))@) and has type--- @DSum Identity Tag@.  Its precedence is just above that of '$', so--- @foo bar $ AString ==> "eep"@ is equivalent to @foo bar (AString ==> "eep")@.+-- The @(':=>')@ constructor and @('==>')@ helper are chosen to+-- resemble the @(key => value)@ construction for dictionary entries+-- in many dynamic languages. The @:=>@ and @==>@ operators have very+-- low precedence and bind to the right, making repeated use of these+-- operators behave as you'd expect:+--+-- > -- Parses as: Rec ==> (AnInt ==> (3 + 4))+-- > -- Has type: Applicative f => DSum Tag f+-- > Rec ==> AnInt ==> 3 + 4+--+-- The precedence of these operators is just above that of '$', so+-- @foo bar $ AString ==> "eep"@ is equivalent to @foo bar (AString+-- ==> "eep")@.+--+-- To use the 'Eq', 'Ord', 'Read', and 'Show' instances for @'DSum'+-- tag f@, you will need an 'ArgDict' instance for your tag type. Use+-- 'Data.Constraint.Extras.TH.deriveArgDict' from the+-- @constraints-extras@ package to generate this+-- instance. data DSum tag f = forall a. !(tag a) :=> f a  infixr 1 :=>, ==> +-- | Convenience helper. Uses 'pure' to lift @a@ into @f a@. (==>) :: Applicative f => tag a -> a -> DSum tag f k ==> v = k :=> pure v 

@@ -1,184 +0,0 @@-{-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE Safe #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}-module Data.GADT.Compare-    ( module Data.GADT.Compare-    , (:~:)(Refl)-    ) 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---- |Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.-{-# DEPRECATED (:=) "use '(:~:)' from 'Data.Type,Equality'." #-}-type (:=) = (:~:)---- |A class for type-contexts which contain enough information--- 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)---- |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--- 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, 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--- >--- > 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--- 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--- they are equal their parameter types can be unified.-data GOrdering a b where-    GLT :: GOrdering a b-    GEQ :: GOrdering t t-    GGT :: GOrdering a b-    deriving Typeable---- |TODO: Think of a better name------ This operation forgets the phantom types of a 'GOrdering' value.-weakenOrdering :: GOrdering a b -> Ordering-weakenOrdering GLT = LT-weakenOrdering GEQ = EQ-weakenOrdering GGT = GT--instance Eq (GOrdering a b) where-    x == y =-        weakenOrdering x == weakenOrdering y--instance Ord (GOrdering a b) where-    compare x y = compare (weakenOrdering x) (weakenOrdering y)--instance Show (GOrdering a b) where-    showsPrec _ GGT = showString "GGT"-    showsPrec _ GEQ = showString "GEQ"-    showsPrec _ GLT = showString "GLT"--instance GShow (GOrdering a) where-    gshowsPrec = showsPrec--instance GRead (GOrdering a) where-    greadsPrec _ s = case con of-        "GGT"   -> [(GReadResult (\x -> x GGT), rest)]-        "GEQ"   -> [(GReadResult (\x -> x GEQ), rest)]-        "GLT"   -> [(GReadResult (\x -> x GLT), rest)]-        _       -> []-        where (con, rest) = splitAt 3 s---- |Type class for comparable GADT-like structures.  When 2 things are equal,--- must return a witness that their parameter types are equal as well ('GEQ').-class GEq f => GCompare f where-    gcompare :: f a -> f b -> GOrdering a b--instance GCompare ((:~:) a) where-    gcompare Refl Refl = GEQ--#if MIN_VERSION_base(4,10,0)-instance GCompare TR.TypeRep where-    gcompare t1 t2 =-      case testEquality t1 t2 of-        Just Refl -> GEQ-        Nothing ->-          case compare (TR.SomeTypeRep t1) (TR.SomeTypeRep t2) of-            LT -> GLT-            GT -> GGT-            EQ -> error "impossible: 'testEquality' and 'compare' \-                        \are inconsistent for TypeRep; report this \-                        \as a GHC bug"-#endif--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,112 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# 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:------ > instance GShow t where gshowsPrec = showsPrec-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------- | >>> 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 (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 }---- |@GReadS t@ is equivalent to @ReadS (forall b. (forall a. t a -> b) -> b)@, which is --- in turn equivalent to @ReadS (Exists t)@ (with @data Exists t where Exists :: t a -> Exists t@)-type GReadS t = String -> [(GReadResult t, String)]---- |'Read'-like class for 1-type-parameter GADTs.  Unlike 'GShow', this one cannot be --- mechanically derived from a 'Read' instance because 'greadsPrec' must choose the phantom--- type based on the 'String' being parsed.-class GRead t where-    greadsPrec :: Int -> GReadS t--greads :: GRead t => GReadS t-greads = greadsPrec (-1)--gread :: GRead t => String -> (forall a. t a -> b) -> b-gread s g = case hd [f | (f, "") <- greads s] of-              GReadResult res -> res g-    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-        ]

@@ -1,98 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE ViewPatterns #-}-{-# 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 (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-{-# COMPLETE Some #-}-#endif-pattern Some :: tag a -> Some tag-pattern Some x <- UnsafeSome ((unsafeCoerce :: tag Any -> tag a) -> x)-  where Some x = UnsafeSome ((unsafeCoerce :: tag a -> tag Any) x)--#if __GLASGOW_HASKELL__ >= 801-{-# COMPLETE This #-}-#endif-{-# DEPRECATED This "Use 'Some' instead" #-}-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--instance GShow tag => Show (Some tag) where-    showsPrec p (Some thing) = showParen (p > 10)-        ( showString "Some "-        . gshowsPrec 11 thing-        )--instance GRead f => Read (Some f) where-    readsPrec p = readParen (p>10) $ \s ->-        [ (getGReadResult withTag Some, rest')-        | let (con, rest) = splitAt 5 s-        , con == "Some "-        , (withTag, rest') <- greadsPrec 11 rest-        ]--instance GEq tag => Eq (Some tag) where-    Some x == Some y = defaultEq x y--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)