diff --git a/dependent-sum.cabal b/dependent-sum.cabal --- a/dependent-sum.cabal +++ b/dependent-sum.cabal @@ -1,5 +1,5 @@ name: dependent-sum -version: 0.2.0.1 +version: 0.2.0.2 stability: provisional cabal-version: >= 1.6 @@ -12,10 +12,19 @@ category: Data, Dependent Types synopsis: Dependent sum type -description: Dependent sums and supporting typeclasses for - comparing and formatting them. +description: A dependent sum is a generalization of a + particular way of thinking about the @Either@ + type. @Either a b@ can be thought of as a + 2-tuple @(tag, value)@, where the value of the + tag determines the type of the value. In + particular, either @tag = Left@ and @value :: a@ + or @tag = Right@ and @value :: b@. + . + This package allows you to define your own + dependent sum types by using your own \"tag\" + types. -tested-with: GHC == 7.0.4, GHC == 6.12.3, GHC == 6.10.4 +tested-with: GHC == 7.6.3, GHC == 7.8.0.20140228 extra-source-files: examples/*.hs @@ -28,7 +37,9 @@ exposed-modules: Data.Dependent.Sum Data.GADT.Compare Data.GADT.Show - other-modules: Data.Dependent.Sum.Typeable + + if impl(ghc < 7.8) + other-modules: Data.Dependent.Sum.Typeable build-depends: base >= 3 && <5 if impl(ghc >= 7.2) ghc-options: -trust base 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,12 +1,19 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Safe #-} #endif 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 Data.GADT.Show import Data.GADT.Compare @@ -41,13 +48,16 @@ -- 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. -- --- @GShow tag => t@ is conceptually equivalent to something like this +-- @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'. @@ -56,8 +66,8 @@ -- following instances: -- -- > instance GShow Tag where --- > gshowsPrec _showsValPrec _p AString = showString "AString" --- > gshowsPrec _showsValPrec _p AnInt = showString "AnInt" +-- > gshowsPrec _p AString = showString "AString" +-- > gshowsPrec _p AnInt = showString "AnInt" -- > instance ShowTag Tag where -- > showTaggedPrec AString = showsPrec -- > showTaggedPrec AnInt = showsPrec @@ -88,6 +98,28 @@ 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 @@ -121,9 +153,8 @@ -- -- > instance GEq Tag where -- > geq AString AString = Just Refl --- > geq AString AnInt = Nothing --- > geq AnInt AString = Nothing -- > geq AnInt AnInt = Just Refl +-- > geq _ _ = Nothing -- > instance EqTag Tag where -- > eqTagged AString AString = (==) -- > eqTagged AnInt AnInt = (==) diff --git a/src/Data/Dependent/Sum/Typeable.hs b/src/Data/Dependent/Sum/Typeable.hs --- a/src/Data/Dependent/Sum/Typeable.hs +++ b/src/Data/Dependent/Sum/Typeable.hs @@ -4,6 +4,9 @@ #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 diff --git a/src/Data/GADT/Compare.hs b/src/Data/GADT/Compare.hs --- a/src/Data/GADT/Compare.hs +++ b/src/Data/GADT/Compare.hs @@ -7,12 +7,24 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Safe #-} #endif -module Data.GADT.Compare where +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 @@ -27,14 +39,16 @@ instance Show (a := b) where showsPrec _ Refl = showString "Refl" -instance GShow ((:=) a) where - gshowsPrec _ 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 diff --git a/src/Data/GADT/Show.hs b/src/Data/GADT/Show.hs --- a/src/Data/GADT/Show.hs +++ b/src/Data/GADT/Show.hs @@ -5,7 +5,11 @@ #endif module Data.GADT.Show where --- |'Show'-like class for 1-type-parameter GADTs +-- |'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 @@ -16,8 +20,13 @@ 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