dependent-sum 0.2.1.0 → 0.3.1.0
raw patch · 7 files changed
+87/−37 lines, 7 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
- Data.Dependent.Sum: instance [safe] Eq a => EqTag ((:=) a)
- Data.Dependent.Sum: instance [safe] EqTag tag => Eq (DSum tag)
- Data.Dependent.Sum: instance [safe] Ord a => OrdTag ((:=) a)
- Data.Dependent.Sum: instance [safe] OrdTag tag => Ord (DSum tag)
- Data.Dependent.Sum: instance [safe] Read a => ReadTag ((:=) a)
- Data.Dependent.Sum: instance [safe] ReadTag tag => Read (DSum tag)
- Data.Dependent.Sum: instance [safe] Show a => ShowTag ((:=) a)
- Data.Dependent.Sum: instance [safe] Show a => ShowTag (GOrdering a)
- Data.Dependent.Sum: instance [safe] ShowTag tag => Show (DSum tag)
- Data.GADT.Compare: instance [safe] Eq (a := b)
- Data.GADT.Compare: instance [safe] Ord (a := b)
- Data.GADT.Compare: instance [safe] Read (a := a)
- Data.GADT.Compare: instance [safe] Show (a := b)
- Data.GADT.Compare: instance [safe] Typeable2 :=
- Data.GADT.Compare: instance [safe] Typeable2 GOrdering
+ Data.Dependent.Sum: (==>) :: Applicative f => tag a -> a -> DSum tag f
+ Data.Dependent.Sum: instance [safe] Eq (f a) => EqTag ((:=) a) f
+ Data.Dependent.Sum: instance [safe] EqTag tag f => Eq (DSum tag f)
+ Data.Dependent.Sum: instance [safe] Ord (f a) => OrdTag ((:=) a) f
+ Data.Dependent.Sum: instance [safe] OrdTag tag f => Ord (DSum tag f)
+ Data.Dependent.Sum: instance [safe] Read (f a) => ReadTag ((:=) a) f
+ Data.Dependent.Sum: instance [safe] ReadTag tag f => Read (DSum tag f)
+ Data.Dependent.Sum: instance [safe] Show (f a) => ShowTag ((:=) a) f
+ Data.Dependent.Sum: instance [safe] Show (f a) => ShowTag (GOrdering a) f
+ Data.Dependent.Sum: instance [safe] ShowTag tag f => Show (DSum tag f)
+ Data.Dependent.Sum: instance [safe] Typeable DSum
+ Data.GADT.Compare: defaultCompare :: GCompare f => f a -> f b -> Ordering
+ Data.GADT.Compare: instance [safe] Typeable GOrdering
+ Data.GADT.Compare: type (:=) = (:~:)
- Data.Dependent.Sum: (:=>) :: !(tag a) -> a -> DSum tag
+ Data.Dependent.Sum: (:=>) :: !(tag a) -> f a -> DSum tag f
- Data.Dependent.Sum: class GEq tag => EqTag tag
+ Data.Dependent.Sum: class GEq tag => EqTag tag f
- Data.Dependent.Sum: class (EqTag tag, GCompare tag) => OrdTag tag
+ Data.Dependent.Sum: class (EqTag tag f, GCompare tag) => OrdTag tag f
- Data.Dependent.Sum: class GRead tag => ReadTag tag
+ Data.Dependent.Sum: class GRead tag => ReadTag tag f
- Data.Dependent.Sum: class GShow tag => ShowTag tag
+ Data.Dependent.Sum: class GShow tag => ShowTag tag f
- Data.Dependent.Sum: compareTagged :: OrdTag tag => tag a -> tag a -> a -> a -> Ordering
+ Data.Dependent.Sum: compareTagged :: OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering
- Data.Dependent.Sum: data DSum tag
+ Data.Dependent.Sum: data DSum tag f
- Data.Dependent.Sum: eqTagged :: EqTag tag => tag a -> tag a -> a -> a -> Bool
+ Data.Dependent.Sum: eqTagged :: EqTag tag f => tag a -> tag a -> f a -> f a -> Bool
- Data.Dependent.Sum: readTaggedPrec :: ReadTag tag => tag a -> Int -> ReadS a
+ Data.Dependent.Sum: readTaggedPrec :: ReadTag tag f => tag a -> Int -> ReadS (f a)
- Data.Dependent.Sum: showTaggedPrec :: ShowTag tag => tag a -> Int -> a -> ShowS
+ Data.Dependent.Sum: showTaggedPrec :: ShowTag tag f => tag a -> Int -> f a -> ShowS
- Data.GADT.Compare: Refl :: a := a
+ Data.GADT.Compare: Refl :: (:~:) k a1 a1
- Data.GADT.Compare: data (:=) a b
+ Data.GADT.Compare: data (:~:) (a :: k) (b :: k) :: k -> k -> *
Files
- dependent-sum.cabal +3/−3
- src/Data/Dependent/Sum.hs +31/−19
- src/Data/Dependent/Sum.hs-boot +1/−1
- src/Data/Dependent/Sum/Typeable.hs +7/−12
- src/Data/GADT/Compare.hs +4/−2
- src/Data/GADT/Show.hs +3/−0
- src/Data/Some.hs +38/−0
dependent-sum.cabal view
@@ -1,5 +1,5 @@ name: dependent-sum-version: 0.2.1.0+version: 0.3.1.0 stability: provisional cabal-version: >= 1.6@@ -24,8 +24,6 @@ dependent sum types by using your own \"tag\" types. -tested-with: GHC == 7.6.3, GHC == 7.8.0.20140228- extra-source-files: examples/*.hs source-repository head@@ -40,6 +38,8 @@ if impl(ghc < 7.8) other-modules: Data.Dependent.Sum.Typeable+ Data.Some+ build-depends: base >= 3 && <5 if impl(ghc >= 7.2) ghc-options: -trust base
src/Data/Dependent/Sum.hs view
@@ -1,14 +1,23 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# 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 module Data.Dependent.Sum where +import Control.Applicative+ #if MIN_VERSION_base(4,7,0) import Data.Typeable (Typeable) #else@@ -47,12 +56,15 @@ -- 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+data DSum tag f = forall a. !(tag a) :=> f a #if MIN_VERSION_base(4,7,0) deriving Typeable #endif-infixr 1 :=>+infixr 1 :=>, ==> +(==>) :: 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.@@ -72,31 +84,31 @@ -- > showTaggedPrec AString = showsPrec -- > showTaggedPrec AnInt = showsPrec -- -class GShow tag => ShowTag tag where+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 -> a -> ShowS+ showTaggedPrec :: tag a -> Int -> f a -> ShowS -instance Show a => ShowTag ((:=) a) where+instance Show (f a) => ShowTag ((:=) a) f where showTaggedPrec Refl = showsPrec -- This instance is questionable. It works, but is pretty useless.-instance Show a => ShowTag (GOrdering a) where+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 => Show (DSum tag) where+instance ShowTag tag f => Show (DSum tag f) where showsPrec p (tag :=> value) = showParen (p >= 10) ( gshowsPrec 0 tag . showString " :=> " . showTaggedPrec tag 1 value ) -class GRead tag => ReadTag tag where- readTaggedPrec :: tag a -> Int -> ReadS a+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@@ -120,7 +132,7 @@ -- > readTaggedPrec AString = readsPrec -- > readTaggedPrec AnInt = readsPrec -- -instance Read a => ReadTag ((:=) a) where+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)@@ -133,7 +145,7 @@ -- , (msg, rest') <- reads rest :: [(String, String)] -- ] -instance ReadTag tag => Read (DSum tag) where+instance ReadTag tag f => Read (DSum tag f) where readsPrec p = readParen (p > 1) $ \s -> concat [ withTag $ \tag ->@@ -161,15 +173,15 @@ -- -- 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+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 -> a -> a -> Bool+ eqTagged :: tag a -> tag a -> f a -> f a -> Bool -instance Eq a => EqTag ((:=) a) where+instance Eq (f a) => EqTag ((:=) a) f where eqTagged Refl Refl = (==) -instance EqTag tag => Eq (DSum tag) where+instance EqTag tag f => Eq (DSum tag f) where (t1 :=> x1) == (t2 :=> x2) = fromMaybe False $ do Refl <- geq t1 t2 return (eqTagged t1 t2 x1 x2)@@ -191,15 +203,15 @@ -- -- As with 'eqTagged', 'compareTagged' only needs to consider cases where -- 'gcompare' returns 'GEQ'.-class (EqTag tag, GCompare tag) => OrdTag tag where+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 -> a -> a -> Ordering+ compareTagged :: tag a -> tag a -> f a -> f a -> Ordering -instance Ord a => OrdTag ((:=) a) where+instance Ord (f a) => OrdTag ((:=) a) f where compareTagged Refl Refl = compare -instance OrdTag tag => Ord (DSum tag) where+instance OrdTag tag f => Ord (DSum tag f) where compare (t1 :=> x1) (t2 :=> x2) = case gcompare t1 t2 of GLT -> LT GGT -> GT
src/Data/Dependent/Sum.hs-boot view
@@ -1,5 +1,5 @@ {-# LANGUAGE ExistentialQuantification, TypeOperators #-} module Data.Dependent.Sum where -data DSum tag = forall a. !(tag a) :=> a+data DSum tag f = forall a. !(tag a) :=> f a infixr 1 :=>
src/Data/Dependent/Sum/Typeable.hs view
@@ -4,7 +4,7 @@ #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@@ -12,20 +12,15 @@ 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]+instance (Typeable1 t, Typeable1 f) => Typeable (DSum t f) where+ typeOf ds = mkTyConApp dSumCon [typeOfF, typeOfT] where- dSumCon = mkTyCon3 "dependent-sum" "Data.Dependent.Sum" "DSum"- typeOfT = typeOf1 $ (undefined :: DSum f -> f a) ds+ 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 --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 view
@@ -159,8 +159,6 @@ _ -> [] 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@@ -168,4 +166,8 @@ instance GCompare ((:=) a) where gcompare Refl Refl = GEQ++defaultCompare :: GCompare f => f a -> f b -> Ordering+defaultCompare x y = weakenOrdering (gcompare x y)+
src/Data/GADT/Show.hs view
@@ -3,6 +3,9 @@ #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
+ src/Data/Some.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE CPP #-}+#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