packages feed

dependent-sum 0.2.0.1 → 0.2.0.2

raw patch · 5 files changed

+84/−16 lines, 5 filesdep ~base

Dependency ranges changed: base

Files

dependent-sum.cabal view
@@ -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
src/Data/Dependent/Sum.hs view
@@ -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   = (==)
src/Data/Dependent/Sum/Typeable.hs view
@@ -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
src/Data/GADT/Compare.hs view
@@ -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
src/Data/GADT/Show.hs view
@@ -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