eq 0.2.0 → 0.3.0

raw patch · 3 files changed

+76/−41 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Eq/Type.hs +70/−35
• LICENSE +1/−1
• eq.cabal +5/−5

@@ -1,21 +1,26 @@-{-# LANGUAGE GADTs, TypeOperators #-}+{-# LANGUAGE CPP, Rank2Types, TypeOperators #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Eq.Type--- Copyright   :  (C) 2011 Edward Kmett, Dan Doel+-- Copyright   :  (C) 2011 Edward Kmett -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  Edward Kmett <ekmett@gmail.com> -- Stability   :  provisional--- Portability :  GADTs, type operators+-- Portability :  rank2 types, type operators, (optional) 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   ( -  -- * Equality+  -- * Leibnizian equality     (:=)(..)   -- * Equality as an equivalence relation+  , refl   , trans   , symm    , coerce@@ -23,10 +28,12 @@   , lift   , lift2, lift2'   , lift3, lift3'+#ifdef LANGUAGE_TypeFamilies   -- * Lowering equality   , lower   , lower2   , lower3+#endif   ) where  import Prelude ()@@ -35,48 +42,76 @@  infixl 4 := -data a := b where-  Refl :: a := a+-- | 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 }  -subst :: (a := b) -> p a -> p b-subst Refl pa = pa+-- | Equality is reflexive+refl :: a := a+refl = Refl id -trans :: (a := b) -> (b := c) -> (a := c)-trans Refl Refl = Refl+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 -symm :: (a := b) -> b := a-symm Refl = Refl+-- | Equality forms a category+instance Category (:=) where+  id = Refl id+  (.) = subst -coerce :: (a := b) -> a -> b-coerce Refl x = x+instance Semigroupoid (:=) where+  o = subst -lift :: a := b -> (f a := f b)-lift Refl = Refl+-- | Equality is transitive+trans :: a := b -> b := c -> a := c+trans = (>>>) -lift2 :: a := b -> (f a c := f b c)-lift2 Refl = Refl+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)) -lift2' :: (a := b) -> (c := d) -> f a c := f b d-lift2' Refl Refl = Refl+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)) -lift3 :: (a := b) -> (f a c d := f b c d)-lift3 Refl = Refl+newtype Lift2 f c a b = Lift2 { unlift2 :: f a c := f b c }  +-- | ... in any position+lift2 :: a := b -> f a c := f b c+lift2 a = unlift2 (subst a (Lift2 id)) -lift3' :: (a := b) -> (c := d) -> (e := f) -> (g a c e := g b d f)-lift3' Refl Refl Refl = Refl+lift2' :: a := b -> c := d -> f a c := f b d+lift2' ab cd = lift2 ab . lift cd -lower :: (f a := f b) -> (a := b)-lower Refl = Refl+newtype Lift3 f c d a b = Lift3 { unlift3 :: f a c d := f b c d } +lift3 :: a := b -> f a c d := f b c d+lift3 a = unlift3 (subst a (Lift3 id)) -lower2 :: (f a c := f b c) -> (a := b)-lower2 Refl = Refl+lift3' :: a := b -> c := d -> e := f -> g a c e := g b d f+lift3' ab cd ef = lift3 ab . lift2 cd . lift ef -lower3 :: (f a c d := f b c d) -> (a := b)-lower3 Refl = Refl+#ifdef LANGUAGE_TypeFamilies -instance Category (:=) where-  id = Refl-  (.) = subst+type family Inj f :: *+type instance Inj (f a) = a+newtype Lower a b = Lower { unlower :: Inj a := Inj b }+-- | Type constructors are injective, so you can lower equality through any type constructor+lower :: f a := f b -> a := b+lower eq = unlower (subst eq (Lower id :: Lower (f a) (f a))) -instance Semigroupoid (:=) where-  o = subst+type family Inj2 f :: *+type instance Inj2 (f a b) = a+newtype Lower2 a b = Lower2 { unlower2 :: Inj2 a := Inj2 b }+-- | ... in any position+lower2 :: f a c := f b c -> a := b+lower2 eq = unlower2 (subst eq (Lower2 id :: Lower2 (f a c) (f a c)))++type family Inj3 f :: *+type instance Inj3 (f a b c) = a+newtype Lower3 a b = Lower3 { unlower3 :: Inj3 a := Inj3 b }+lower3 :: f a c d := f b c d -> a := b+lower3 eq = unlower3 (subst eq (Lower3 id :: Lower3 (f a c d) (f a c d)))++#endif

@@ -1,4 +1,4 @@-Copyright 2010-2011 Edward Kmett, Dan Doel+Copyright 2010-2011 Edward Kmett  All rights reserved. 

@@ -1,6 +1,6 @@ name:          eq category:      Type System-version:       0.2.0+version:       0.3.0 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -8,9 +8,9 @@ maintainer:    Edward A. Kmett <ekmett@gmail.com> stability:     provisional homepage:      http://github.com/ekmett/eq/-copyright:     Copyright (C) 2011 Edward A. Kmett, Dan Doel-synopsis:      GADT-based type-level equality-description:   GADT-based type-level equality+copyright:     Copyright (C) 2011 Edward A. Kmett+synopsis:      Leibnizian equality+description:   Leibnizian equality build-type:    Simple  source-repository head@@ -22,7 +22,7 @@     base >= 4 && < 5,     semigroupoids >= 1.1.1 && < 1.2.0 -  extensions: GADTs, TypeOperators+  extensions: TypeOperators    exposed-modules:     Data.Eq.Type