packages feed

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 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