eq 3.0 → 3.1

raw patch · 10 files changed

+213/−127 lines, 10 filesdep ~basedep ~groupoidsdep ~semigroupoidsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, groupoids, semigroupoids

API changes (from Hackage documentation)

Files

• .ghci +1/−0
• .gitignore +13/−0
• .travis.yml +7/−0
• .vim.custom +31/−0
• CHANGELOG.markdown +9/−0
• Data/Eq/Type.hs +0/−120
• LICENSE +1/−1
• README.markdown +18/−0
• eq.cabal +13/−6
• src/Data/Eq/Type.hs +120/−0

@@ -0,0 +1,1 @@+:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h

@@ -0,0 +1,13 @@+dist+docs+wiki+TAGS+tags+wip+.DS_Store+.*.swp+.*.swo+*.o+*.hi+*~+*#

@@ -1,1 +1,8 @@ language: haskell+notifications:+  irc:+    channels:+      - "irc.freenode.org#haskell-lens"+    skip_join: true+    template:+      - "\x0313eq\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"

@@ -0,0 +1,31 @@+" Add the following to your .vimrc to automatically load this on startup++" if filereadable(".vim.custom")+"     so .vim.custom+" endif++function StripTrailingWhitespace()+  let myline=line(".")+  let mycolumn = col(".")+  silent %s/  *$//+  call cursor(myline, mycolumn)+endfunction++" enable syntax highlighting+syntax on++" search for the tags file anywhere between here and /+set tags=TAGS;/++" highlight tabs and trailing spaces+set listchars=tab:‗‗,trail:‗+set list++" f2 runs hasktags+map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR>++" strip trailing whitespace before saving+" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace()++" rebuild hasktags after saving+au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src"

@@ -0,0 +1,9 @@+3.1+---+* Disabled observing injectivity through `TypeFamilies` for GHC >= 7.6++3.0.1+-----+* Updated build system+* Removed my personal intra-package dependency upper bounds+* Added `README` and `CHANGELOG`

@@ -1,120 +0,0 @@-{-# LANGUAGE CPP, Rank2Types, TypeOperators #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Eq.Type--- Copyright   :  (C) 2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- 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-  ( -  -- * Leibnizian equality-    (:=)(..)-  -- * Equality as an equivalence relation-  , refl-  , trans-  , symm -  , coerce-  -- * Lifting equality-  , lift-  , lift2, lift2'-  , lift3, lift3'-#ifdef LANGUAGE_TypeFamilies-  -- * Lowering equality-  , lower-  , lower2-  , lower3-#endif-  ) where--import Prelude ()-import Control.Category -import Data.Semigroupoid-import Data.Groupoid--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--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---- | Equality forms a category-instance Category (:=) where-  id = Refl id-  (.) = subst--instance Semigroupoid (:=) where-  o = subst--instance Groupoid (:=) where-  inv = symm---- | Equality is transitive-trans :: a := b -> b := c -> a := c-trans = (>>>)--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 } --- | You can lift equality into any type constructor-lift :: a := b -> f a := f b-lift a = unlift (subst a (Lift id))--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 -> c := d -> f a c := f b d-lift2' ab cd = lift2 ab . lift cd--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 -> c := d -> e := f -> g a c e := g b d f-lift3' ab cd ef = lift3 ab . lift2 cd . lift ef--#ifdef LANGUAGE_TypeFamilies-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)))--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+Copyright 2010-2013 Edward Kmett  All rights reserved. 

@@ -0,0 +1,18 @@+eq+==++[![Build Status](https://secure.travis-ci.org/ekmett/eq.png?branch=master)](http://travis-ci.org/ekmett/eq)++This package provides a data type that witnesses equality between two types using Leibnizian equality.++It includes a [refinement to the notion of Leibnizian equality by Oleg Kiselyov](http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html) +that permits it to refine equality using the injectively of type constructors via type families.++Contact Information+-------------------++Contributions and bug reports are welcome!++Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.++-Edward Kmett

@@ -1,6 +1,6 @@ name:          eq category:      Type System-version:       3.0+version:       3.1 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -9,12 +9,18 @@ stability:     provisional homepage:      http://github.com/ekmett/eq/ bug-reports:   http://github.com/ekmett/eq/issues-copyright:     Copyright (C) 2011 Edward A. Kmett+copyright:     Copyright (C) 2011-2013 Edward A. Kmett synopsis:      Leibnizian equality description:   Leibnizian equality build-type:    Simple -extra-source-files: .travis.yml+extra-source-files:+  .ghci+  .gitignore+  .vim.custom+  .travis.yml+  CHANGELOG.markdown+  README.markdown  source-repository head   type: git@@ -28,14 +34,15 @@    build-depends:     base          == 4.*,-    semigroupoids == 3.0.*,-    groupoids     == 3.0.*+    semigroupoids >= 3,+    groupoids     >= 3    exposed-modules:     Data.Eq.Type -  if impl(ghc >= 7.0)+  if impl(ghc >= 7.0) && impl(ghc < 7.6)     extensions: TypeFamilies     cpp-options: -DLANGUAGE_TypeFamilies    ghc-options: -Wall+  hs-source-dirs: src

@@ -0,0 +1,120 @@+{-# LANGUAGE CPP, Rank2Types, TypeOperators #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Eq.Type+-- Copyright   :  (C) 2011 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  provisional+-- 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+  ( +  -- * Leibnizian equality+    (:=)(..)+  -- * Equality as an equivalence relation+  , refl+  , trans+  , symm +  , coerce+  -- * Lifting equality+  , lift+  , lift2, lift2'+  , lift3, lift3'+#ifdef LANGUAGE_TypeFamilies+  -- * Lowering equality+  , lower+  , lower2+  , lower3+#endif+  ) where++import Prelude ()+import Control.Category +import Data.Semigroupoid+import Data.Groupoid++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++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++-- | Equality forms a category+instance Category (:=) where+  id = Refl id+  (.) = subst++instance Semigroupoid (:=) where+  o = subst++instance Groupoid (:=) where+  inv = symm++-- | Equality is transitive+trans :: a := b -> b := c -> a := c+trans = (>>>)++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 } +-- | You can lift equality into any type constructor+lift :: a := b -> f a := f b+lift a = unlift (subst a (Lift id))++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 -> c := d -> f a c := f b d+lift2' ab cd = lift2 ab . lift cd++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 -> c := d -> e := f -> g a c e := g b d f+lift3' ab cd ef = lift3 ab . lift2 cd . lift ef++#ifdef LANGUAGE_TypeFamilies+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)))++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