diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -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. diff --git a/dependent-sum.cabal b/dependent-sum.cabal --- a/dependent-sum.cabal +++ b/dependent-sum.cabal @@ -1,14 +1,14 @@ name: dependent-sum -version: 0.3.2.2 +version: 0.7.2.0 stability: provisional -cabal-version: >= 1.6 +cabal-version: 1.22 build-type: Simple author: James Cook -maintainer: James Cook +maintainer: Obsidian Systems, LLC 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,30 +24,32 @@ dependent sum types by using your own \"tag\" types. -tested-with: GHC == 7.0.4, - GHC == 7.2.2, - GHC == 7.4.2, - GHC == 7.6.3, - GHC == 7.8.4, - GHC == 7.10.1, - GHC == 7.11 +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 + reexported-modules: 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.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 diff --git a/examples/FooGADT.hs b/examples/FooGADT.hs --- a/examples/FooGADT.hs +++ b/examples/FooGADT.hs @@ -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,28 +67,15 @@ 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" -> [(\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 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 diff --git a/src/Data/Dependent/Sum.hs b/src/Data/Dependent/Sum.hs --- a/src/Data/Dependent/Sum.hs +++ b/src/Data/Dependent/Sum.hs @@ -1,218 +1,149 @@ -{-# LANGUAGE ExistentialQuantification, GADTs #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# 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 --- 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")@. +-- 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 +-- +-- 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 -#if MIN_VERSION_base(4,7,0) - deriving Typeable -#endif + 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 --- |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. --- --- @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'. --- --- 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 f where - -- |Given a value of type @tag a@, return the 'showsPrec' function for - -- the type parameter @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@, @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 (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 - [ 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 f 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 -> 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@ 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 @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' @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) diff --git a/src/Data/Dependent/Sum.hs-boot b/src/Data/Dependent/Sum.hs-boot deleted file mode 100644 --- a/src/Data/Dependent/Sum.hs-boot +++ /dev/null @@ -1,5 +0,0 @@ -{-# LANGUAGE ExistentialQuantification, TypeOperators #-} -module Data.Dependent.Sum where - -data DSum tag f = forall a. !(tag a) :=> f a -infixr 1 :=> diff --git a/src/Data/Dependent/Sum/Typeable.hs b/src/Data/Dependent/Sum/Typeable.hs deleted file mode 100644 --- a/src/Data/Dependent/Sum/Typeable.hs +++ /dev/null @@ -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 diff --git a/src/Data/GADT/Compare.hs b/src/Data/GADT/Compare.hs deleted file mode 100644 --- a/src/Data/GADT/Compare.hs +++ /dev/null @@ -1,174 +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 -{-# LANGUAGE ScopedTypeVariables #-} - -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 :: forall x. (x := x, String) -> [(forall b. (forall a. x := a -> b) -> b, String)] - f (Refl, rest) = return ((\x -> x Refl) :: forall b. (forall a. x := a -> b) -> b, 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 :: a := b) (Refl :: a := c) = Just (Refl :: b := c) - --- 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 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 - -defaultCompare :: GCompare f => f a -> f b -> Ordering -defaultCompare x y = weakenOrdering (gcompare x y) - - diff --git a/src/Data/GADT/Show.hs b/src/Data/GADT/Show.hs deleted file mode 100644 --- a/src/Data/GADT/Show.hs +++ /dev/null @@ -1,43 +0,0 @@ -{-# LANGUAGE RankNTypes, ImpredicativeTypes #-} -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 -{-# LANGUAGE Safe #-} -#endif -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 -{-# LANGUAGE PolyKinds #-} -#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" diff --git a/src/Data/Some.hs b/src/Data/Some.hs deleted file mode 100644 --- a/src/Data/Some.hs +++ /dev/null @@ -1,41 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ImpredicativeTypes #-} -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 -{-# LANGUAGE Safe #-} -#endif -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 -{-# LANGUAGE PolyKinds #-} -#endif -module Data.Some where - -import Data.GADT.Show -import Data.GADT.Compare -import Data.Maybe - -data Some tag where - This :: !(tag t) -> Some tag - -withSome :: Some tag -> (forall a. tag a -> b) -> b -withSome (This thing) some = some thing - -instance GShow tag => Show (Some tag) where - showsPrec p (This thing) = showParen (p > 10) - ( showString "This " - . gshowsPrec 11 thing - ) - -instance GRead f => Read (Some f) where - readsPrec p = readParen (p>10) $ \s -> - [ (withTag This, rest') - | let (con, rest) = splitAt 5 s - , con == "This " - , (withTag, rest') <- greadsPrec 11 rest - ] - -instance GEq tag => Eq (Some tag) where - This x == This y = defaultEq x y - -instance GCompare tag => Ord (Some tag) where - compare (This x) (This y) = defaultCompare x y