eq 0.1.3 → 0.2.0

raw patch · 3 files changed

+44/−81 lines, 3 filesdep +semigroupoidsPVP ok

version bump matches the API change (PVP)

Dependencies added: semigroupoids

API changes (from Hackage documentation)

Files

• Data/Eq/Type.hs +36/−67
• LICENSE +1/−1
• eq.cabal +7/−13

@@ -1,26 +1,21 @@-{-# LANGUAGE Rank2Types, TypeOperators #-}+{-# LANGUAGE GADTs, TypeOperators #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Eq.Type--- Copyright   :  (C) 2011 Edward Kmett+-- Copyright   :  (C) 2011 Edward Kmett, Dan Doel -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  Edward Kmett <ekmett@gmail.com> -- Stability   :  provisional--- Portability :  rank2 types, type operators, type families (optional)------ Leibnizian equality. Injectivity in the presence of type families --- is provided by a generalization of a trick by Oleg Kiselyv posted here:+-- Portability :  GADTs, type operators ----- <http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html> ----------------------------------------------------------------------------  module Data.Eq.Type   ( -  -- * Leibnizian equality+  -- * Equality     (:=)(..)   -- * Equality as an equivalence relation-  , refl   , trans   , symm    , coerce@@ -28,86 +23,60 @@   , lift   , lift2, lift2'   , lift3, lift3'-#ifdef LANGUAGE_TypeFamilies   -- * Lowering equality   , lower   , lower2   , lower3-#endif   ) where  import Prelude () import Control.Category +import Data.Semigroupoid  infixl 4 := --- | 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 } ---- | Equality is reflexive-refl :: a := a-refl = Refl id+data a := b where+  Refl :: a := 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+subst :: (a := b) -> p a -> p b+subst Refl pa = pa --- | Equality forms a category-instance Category (:=) where-  id = Refl id-  (.) = subst+trans :: (a := b) -> (b := c) -> (a := c)+trans Refl Refl = Refl --- | Equality is transitive-trans :: a := b -> b := c -> a := c-trans = (>>>)+symm :: (a := b) -> b := a+symm 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))+coerce :: (a := b) -> a -> b+coerce Refl x = x -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))+lift :: a := b -> (f a := f b)+lift 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))+lift2 :: a := b -> (f a c := f b c)+lift2 Refl = Refl -lift2' :: a := b -> c := d -> f a c := f b d-lift2' ab cd = lift2 ab . lift cd+lift2' :: (a := b) -> (c := d) -> f a c := f b d+lift2' Refl 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))+lift3 :: (a := b) -> (f a c d := f b c d)+lift3 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+lift3' :: (a := b) -> (c := d) -> (e := f) -> (g a c e := g b d f)+lift3' Refl Refl Refl = Refl -#ifdef LANGUAGE_TypeFamilies+lower :: (f a := f b) -> (a := b)+lower Refl = Refl -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)))+lower2 :: (f a c := f b c) -> (a := b)+lower2 Refl = Refl -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)))+lower3 :: (f a c d := f b c d) -> (a := b)+lower3 Refl = Refl -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)))+instance Category (:=) where+  id = Refl+  (.) = subst -#endif+instance Semigroupoid (:=) where+  o = subst

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

@@ -1,6 +1,6 @@ name:          eq category:      Type System-version:       0.1.3+version:       0.2.0 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -8,27 +8,21 @@ maintainer:    Edward A. Kmett <ekmett@gmail.com> stability:     provisional homepage:      http://github.com/ekmett/eq/-copyright:     Copyright (C) 2010-2011 Edward A. Kmett-synopsis:      Leibnizian equality-description:   Leibnizian equality+copyright:     Copyright (C) 2011 Edward A. Kmett, Dan Doel+synopsis:      GADT-based type-level equality+description:   GADT-based type-level equality build-type:    Simple  source-repository head   type: git   location: git://github.com/ekmett/eq.git -flag TypeFamilies-  default: True- library   build-depends: -    base >= 4 && < 5--  extensions: CPP+    base >= 4 && < 5,+    semigroupoids >= 1.1.1 && < 1.2.0 -  if flag(TypeFamilies)-    cpp-options: -DLANGUAGE_TypeFamilies-    extensions: TypeFamilies+  extensions: GADTs, TypeOperators    exposed-modules:     Data.Eq.Type