dependent-sum 0.2.1.0 → 0.7.2.0
raw patch · 8 files changed
Files
- ChangeLog.md +56/−0
- dependent-sum.cabal +23/−13
- examples/FooGADT.hs +37/−36
- src/Data/Dependent/Sum.hs +112/−169
- src/Data/Dependent/Sum.hs-boot +0/−5
- src/Data/Dependent/Sum/Typeable.hs +0/−31
- src/Data/GADT/Compare.hs +0/−171
- src/Data/GADT/Show.hs +0/−40
+ ChangeLog.md view
@@ -0,0 +1,56 @@+# Revision history for dependent-sum++## 0.7.2.0 - 2022-12-22++* Update to some-1.0.4.*++## 0.7.1.1 - 2022-12-12++* Support constraints-extras 0.4++## 0.7.1.0 - 2020-03-25++* Shift version bounds for `some` to 1.0.1.* versions.++## 0.7.0.0 - 2020-03-24++* Fix ChangeLog to include the breaking change in 0.6.2.1/0.6.2.2 and properly do *major* version bump to reflect the breaking change.++## 0.6.2.2 - 2020-03-23++* Update GitHub repository in cabal metadata.++## 0.6.2.1 - 2020-03-21++* (Breaking change) Removed modules `Data.GADT.Compare`, `Data.GADT.Show`, `Data.Some` and now re-export them from the `some` package. This forced some deprecations to be fully realized.+* 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++## 0.6.1.0 - 2019-08-04++* Add legacy `eqTagged` and `compareTagged` functions. Fix deprecated `OrdTag` synonym (it was missing the `Has' Eq` constraint). To upgrade from dependent-sum <0.6, you will likely need to add enable the `FlexibleContexts` language extension, and possible others.++## 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`+ to avoid the GADT performance overhead. This shouldn't affect users.+* Deprecate the constructor name `This` in favor of `Some`.+* Drop support for GHC older than 8.0.
dependent-sum.cabal view
@@ -1,14 +1,14 @@ name: dependent-sum-version: 0.2.1.0+version: 0.7.2.0 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@@ -24,22 +24,32 @@ dependent sum types by using your own \"tag\" types. -tested-with: GHC == 7.6.3, GHC == 7.8.0.20140228+tested-with: GHC == 8.6.5,+ GHC == 8.8.4,+ GHC == 8.10.7,+ GHC == 9.0.1,+ GHC == 9.4.3 -extra-source-files: examples/*.hs+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- - if impl(ghc < 7.8)- other-modules: Data.Dependent.Sum.Typeable- build-depends: base >= 3 && <5+ reexported-modules: Data.GADT.Compare,+ Data.GADT.Show,+ Data.Some+ other-extensions: PatternSynonyms+ build-depends: base >= 4.9 && <5+ , constraints-extras >= 0.2 && < 0.5++ -- tight bounds, so re-exported API is versioned properly.+ build-depends: some >= 1.0.4 && < 1.0.5+ if impl(ghc >= 7.2) ghc-options: -trust base
examples/FooGADT.hs view
@@ -1,9 +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@@ -11,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 @@ -21,13 +43,6 @@ geq Qux Qux = Just Refl geq _ _ = Nothing -instance EqTag Foo 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@@ -43,14 +58,6 @@ gcompare Qux Qux = GEQ -instance OrdTag Foo 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"@@ -60,34 +67,28 @@ instance GShow Foo where gshowsPrec = showsPrec -instance ShowTag Foo where- showTaggedPrec Foo = showsPrec- showTaggedPrec Bar = showsPrec- showTaggedPrec Baz = showsPrec- showTaggedPrec Qux = showsPrec-- instance GRead Foo where greadsPrec _ str = case tag of- "Foo" -> [(\k -> k Foo, rest)]- "Bar" -> [(\k -> k Bar, rest)]- "Baz" -> [(\k -> k Baz, rest)]- "Qux" -> [(\k -> k Qux, rest)]+ "Foo" -> [(GReadResult (\k -> k Foo), rest)]+ "Bar" -> [(GReadResult (\k -> k Bar), rest)]+ "Baz" -> [(GReadResult (\k -> k Baz), rest)]+ "Qux" -> [(GReadResult (\k -> k Qux), rest)] _ -> [] where (tag, rest) = splitAt 3 str -instance ReadTag Foo where- readTaggedPrec Foo = readsPrec- readTaggedPrec Bar = readsPrec- readTaggedPrec Baz = readsPrec- readTaggedPrec Qux = readsPrec+foo :: Double -> DSum Foo Identity+foo x = Foo ==> x +bar :: Int -> DSum Foo Identity+bar x = Bar ==> x -foo x = Foo :=> x-bar x = Bar :=> x-baz x = Baz :=> x-qux x = Qux :=> x+baz :: String -> DSum Foo Identity+baz x = Baz ==> x +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
src/Data/Dependent/Sum.hs view
@@ -1,206 +1,149 @@-{-# LANGUAGE ExistentialQuantification, GADTs #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE ImpredicativeTypes #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE Safe #-}-#endif+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-} module Data.Dependent.Sum where -#if MIN_VERSION_base(4,7,0)-import Data.Typeable (Typeable)-#else-import Data.Dependent.Sum.Typeable ({- instance Typeable ... -})-#endif+import Control.Applicative +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 --- the type of the second; for example, think of a GADT such as:--- +import Text.Read++-- | 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--- --- Then, we have the following valid expressions of type @DSum Tag@:+-- > Rec :: Tag (DSum Tag Identity) ----- > AString :=> "hello!"--- > AnInt :=> 42--- --- And we can write functions that consume @DSum Tag@ values by matching, --- such as:--- --- > toString :: DSum Tag -> String--- > toString (AString :=> str) = str--- > toString (AnInt :=> 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 :=> operator has very low precedence and binds to --- the right, so if the @Tag@ GADT is extended with an additional constructor--- @Rec :: Tag (DSum Tag)@, then @Rec :=> AnInt :=> 3 + 4@ is parsed as--- would be expected (@Rec :=> (AnInt :=> (3 + 4))@) and has type @DSum Tag@.--- Its precedence is just above that of '$', so @foo bar $ AString :=> "eep"@--- is equivalent to @foo bar (AString :=> "eep")@.-data DSum tag = forall a. !(tag a) :=> a-#if MIN_VERSION_base(4,7,0)- deriving Typeable-#endif-infixr 1 :=>---- |In order to make a 'Show' instance for @DSum tag@, @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.+-- 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'@: ----- @ShowTag tag => t@ is conceptually equivalent to something like this--- imaginary syntax: @(forall a. Inhabited (tag a) => Show a) => t@,--- where 'Inhabited' is an imaginary predicate that characterizes --- non-empty types, and 'a' does not occur free in 't'.+-- > AString :=> Identity "hello!"+-- > AnInt :=> Identity 42 ----- The @Tag@ example type introduced in the 'DSum' section could be given the--- following instances:--- --- > 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 where- -- |Given a value of type @tag a@, return the 'showsPrec' function for - -- the type parameter @a@.- showTaggedPrec :: tag a -> Int -> a -> ShowS+-- 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+--+-- 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+--+-- 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 -instance Show a => ShowTag ((:=) a) where- showTaggedPrec Refl = showsPrec+infixr 1 :=>, ==> --- This instance is questionable. It works, but is pretty useless.-instance Show a => ShowTag (GOrdering a) where- showTaggedPrec GEQ = showsPrec- showTaggedPrec _ = \p _ -> showParen (p > 10)- ( showString "error "- . shows "type information lost into the mists of oblivion"- )+-- | Convenience helper. Uses 'pure' to lift @a@ into @f a@.+(==>) :: Applicative f => tag a -> a -> DSum tag f+k ==> v = k :=> pure v -instance ShowTag tag => Show (DSum tag) 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 where- readTaggedPrec :: tag a -> Int -> ReadS a---- |In order to make a 'Read' instance for @DSum tag@, @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 => t@ is conceptually equivalent to something like this--- imaginary syntax: @(forall a. Inhabited (tag a) => Read a) => t@,--- where 'Inhabited' is an imaginary predicate that characterizes --- non-empty types, and 'a' does not occur free in 't'.------ The @Tag@ example type introduced in the 'DSum' section could be given the--- following instances:--- --- > 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 a => ReadTag ((:=) a) 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 => Read (DSum tag) 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- [ withTag $ \tag ->+ [ 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@ 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 where- -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),- -- return the '==' function for the type @a@.- eqTagged :: tag a -> tag a -> a -> a -> Bool--instance Eq a => EqTag ((:=) a) where- eqTagged Refl Refl = (==)--instance EqTag tag => Eq (DSum tag) 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@ 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, GCompare tag) => OrdTag tag where- -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),- -- return the 'compare' function for the type @a@.- compareTagged :: tag a -> tag a -> a -> a -> Ordering--instance Ord a => OrdTag ((:=) a) where- compareTagged Refl Refl = compare+ return $ has' @Eq @f t1 (x1 == x2) -instance OrdTag tag => Ord (DSum tag) 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' @Eq @f t1 $ 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++eqTagged :: forall tag f a. EqTag tag f => tag a -> tag a -> f a -> f a -> Bool+eqTagged k _ x0 x1 = has' @Eq @f k (x0 == x1)++{-# DEPRECATED OrdTag "Instead of 'OrdTag tag f', use '(GCompare tag, Has' Eq tag f, Has' Ord tag f)'" #-}+type OrdTag tag f = (GCompare tag, Has' Eq tag f, Has' Ord tag f)++compareTaggedPrec :: forall tag f a. (GCompare tag, Has' Eq tag f, 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' @Eq @f tag1 $ has' @Ord @f tag1 $ f1 `compare` f2+ GGT -> GT++compareTagged :: forall tag f a. OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering+compareTagged k _ x0 x1 = has' @Eq @f k $ has' @Ord @f k (compare x0 x1)
− src/Data/Dependent/Sum.hs-boot
@@ -1,5 +0,0 @@-{-# LANGUAGE ExistentialQuantification, TypeOperators #-}-module Data.Dependent.Sum where--data DSum tag = forall a. !(tag a) :=> a-infixr 1 :=>
− src/Data/Dependent/Sum/Typeable.hs
@@ -1,31 +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--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702--instance Typeable1 t => Typeable (DSum t) where- typeOf ds = mkTyConApp dSumCon [typeOfT]- where- dSumCon = mkTyCon3 "dependent-sum" "Data.Dependent.Sum" "DSum"- typeOfT = typeOf1 $ (undefined :: DSum f -> f a) ds--#else --instance Typeable1 t => Typeable (DSum t) where- typeOf ds = mkTyConApp dSumCon [typeOfT]- where- dSumCon = mkTyCon "Data.Dependent.Sum.DSum"- typeOfT = typeOf1 $ (undefined :: DSum f -> f a) ds--#endif
− src/Data/GADT/Compare.hs
@@ -1,171 +0,0 @@-{-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}-{-# LANGUAGE ImpredicativeTypes #-}-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708-{-# LANGUAGE PolyKinds #-}-#endif-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Safe #-}-#endif--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.Typeable--#if MIN_VERSION_base(4,7,0)--- |Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.-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 :: (x := x, String) -> [(forall b. (forall a. x := a -> b) -> b, String)]- f (Refl, rest) = return (\x -> x Refl, rest)---- |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 Refl = Just Refl---- 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" -> [(\x -> x GGT, rest)]- "GEQ" -> [(\x -> x GEQ, rest)]- "GLT" -> [(\x -> x GLT, rest)]- _ -> []- where (con, rest) = splitAt 3 s---- |Type class for orderable GADT-like structures. When 2 things are equal,--- must return a witness that their parameter types are equal as well (GEQ).--- |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-
− src/Data/GADT/Show.hs
@@ -1,40 +0,0 @@-{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Safe #-}-#endif-module Data.GADT.Show where---- |'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 ""---- |@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 -> [(forall b. (forall a. t a -> b) -> b, 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 = hd [f | (f, "") <- greads s]- where- hd (x:_) = x- hd _ = error "gread: no parse"