eq 3.1 → 3.1.1

raw patch · 3 files changed

+17/−9 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +4/−0
• eq.cabal +1/−1
• src/Data/Eq/Type.hs +12/−8

@@ -1,3 +1,7 @@+3.1.1+-----+* Claim to be `Trustworthy`+ 3.1 --- * Disabled observing injectivity through `TypeFamilies` for GHC >= 7.6

@@ -1,6 +1,6 @@ name:          eq category:      Type System-version:       3.1+version:       3.1.1 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE

@@ -1,4 +1,8 @@ {-# LANGUAGE CPP, Rank2Types, TypeOperators #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Eq.Type@@ -9,20 +13,20 @@ -- Stability   :  provisional -- Portability :  rank2 types, type operators, (optional) type families ----- Leibnizian equality. Injectivity in the presence of type families +-- Leibnizian equality. Injectivity in the presence of type families -- is provided by a generalization of a trick by Oleg Kiselyv posted here: -- -- <http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html> ----------------------------------------------------------------------------  module Data.Eq.Type-  ( +  (   -- * Leibnizian equality     (:=)(..)   -- * Equality as an equivalence relation   , refl   , trans-  , symm +  , symm   , coerce   -- * Lifting equality   , lift@@ -37,13 +41,13 @@   ) where  import Prelude ()-import Control.Category +import Control.Category import Data.Semigroupoid import Data.Groupoid  infixl 4 := --- | Leibnizian equality states that two things are equal if you can +-- | Leibnizian equality states that two things are equal if you can -- substite one for the other in all contexts data a := b = Refl { subst :: forall c. c a -> c b } @@ -51,7 +55,7 @@ refl :: a := a refl = Refl id -newtype Coerce a = Coerce { uncoerce :: a } +newtype Coerce a = Coerce { uncoerce :: a } -- | If two things are equal you can convert one to the other coerce :: a := b -> a -> b coerce f = uncoerce . subst f . Coerce@@ -71,12 +75,12 @@ trans :: a := b -> b := c -> a := c trans = (>>>) -newtype Symm p a b = Symm { unsymm :: p b a } +newtype Symm p a b = Symm { unsymm :: p b a } -- | Equality is symmetric symm :: (a := b) -> (b := a) symm a = unsymm (subst a (Symm id)) -newtype Lift f a b = Lift { unlift :: f a := f b } +newtype Lift f a b = Lift { unlift :: f a := f b } -- | You can lift equality into any type constructor lift :: a := b -> f a := f b lift a = unlift (subst a (Lift id))