diff --git a/.gitignore b/.gitignore --- a/.gitignore +++ b/.gitignore @@ -11,3 +11,21 @@ *.hi *~ *# +.stack-work/ +cabal-dev +*.chi +*.chs.h +*.dyn_o +*.dyn_hi +.hpc +.hsenv +.cabal-sandbox/ +cabal.sandbox.config +*.prof +*.aux +*.hp +*.eventlog +cabal.project.local +cabal.project.local~ +.HTF/ +.ghc.environment.* diff --git a/.travis.yml b/.travis.yml --- a/.travis.yml +++ b/.travis.yml @@ -1,61 +1,146 @@ -# NB: don't set `language: haskell` here +# This Travis job script has been generated by a script via +# +# runghc make_travis_yml_2.hs '-o' '.travis.yml' '--irc-channel=irc.freenode.org#haskell-lens' '--no-no-tests-no-bench' '--no-installed' 'cabal.project' +# +# For more information, see https://github.com/hvr/multi-ghc-travis +# +language: c +sudo: false -# See also https://github.com/hvr/multi-ghc-travis for more information -env: - # we have to use CABALVER=1.16 for GHC<7.6 as well, as there's - # no package for earlier cabal versions in the PPA - - GHCVER=7.4.2 CABALVER=1.16 - - GHCVER=7.6.3 CABALVER=1.16 - - GHCVER=7.8.2 CABALVER=1.18 - # NOTE: we can't use Cabal 1.20 yet due to - # https://github.com/haskell/cabal/issues/1806 - - GHCVER=head CABALVER=1.20 +git: + submodules: false # whether to recursively clone submodules +notifications: + irc: + channels: + - "irc.freenode.org#haskell-lens" + skip_join: true + template: + - "\x0313eq\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}" + +cache: + directories: + - $HOME/.cabal/packages + - $HOME/.cabal/store + +before_cache: + - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log + # remove files that are regenerated by 'cabal update' + - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.* + - rm -fv $HOME/.cabal/packages/hackage.haskell.org/*.json + - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.cache + - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar + - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar.idx + + - rm -rfv $HOME/.cabal/packages/head.hackage + matrix: + include: + - compiler: "ghc-7.0.4" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.0.4], sources: [hvr-ghc]}} + - compiler: "ghc-7.2.2" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.2.2], sources: [hvr-ghc]}} + - compiler: "ghc-7.4.2" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.4.2], sources: [hvr-ghc]}} + - compiler: "ghc-7.6.3" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.6.3], sources: [hvr-ghc]}} + - compiler: "ghc-7.8.4" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.8.4], sources: [hvr-ghc]}} + - compiler: "ghc-7.10.3" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.10.3], sources: [hvr-ghc]}} + - compiler: "ghc-8.0.2" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-8.0.2], sources: [hvr-ghc]}} + - compiler: "ghc-8.2.2" + # env: TEST=--disable-tests BENCH=--disable-benchmarks + addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-8.2.2], sources: [hvr-ghc]}} + - compiler: "ghc-8.4.1" + env: GHCHEAD=true + addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-8.4.1], sources: [hvr-ghc]}} + - compiler: "ghc-head" + env: GHCHEAD=true + addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-head], sources: [hvr-ghc]}} + allow_failures: - - env: GHCVER=head CABALVER=1.20 + - compiler: "ghc-7.0.4" + - compiler: "ghc-7.2.2" + - compiler: "ghc-8.4.1" + - compiler: "ghc-head" -# Note: the distinction between `before_install` and `install` is not -# important. before_install: - - travis_retry sudo add-apt-repository -y ppa:hvr/ghc - - travis_retry sudo apt-get update - - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER - - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH - - cabal --version + - HC=${CC} + - HCPKG=${HC/ghc/ghc-pkg} + - unset CC + - ROOTDIR=$(pwd) + - mkdir -p $HOME/.local/bin + - "PATH=/opt/ghc/bin:/opt/ghc-ppa-tools/bin:$HOME/local/bin:$PATH" + - HCNUMVER=$(( $(${HC} --numeric-version|sed -E 's/([0-9]+)\.([0-9]+)\.([0-9]+).*/\1 * 10000 + \2 * 100 + \3/') )) + - echo $HCNUMVER install: - - travis_retry cabal update - - cabal install --only-dependencies + - cabal --version + - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]" + - BENCH=${BENCH---enable-benchmarks} + - TEST=${TEST---enable-tests} + - HADDOCK=${HADDOCK-true} + - INSTALLED=${INSTALLED-true} + - GHCHEAD=${GHCHEAD-false} + - travis_retry cabal update -v + - "sed -i.bak 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config" + - rm -fv cabal.project cabal.project.local + # Overlay Hackage Package Index for GHC HEAD: https://github.com/hvr/head.hackage + - | + if $GHCHEAD; then + sed -i.bak 's/-- allow-newer:.*/allow-newer: *:base, *:template-haskell, *:ghc, *:Cabal/' ${HOME}/.cabal/config -# Here starts the actual work to be performed for the package under -# test; any command which exits with a non-zero exit code causes the -# build to fail. + echo 'repository head.hackage' >> ${HOME}/.cabal/config + echo ' url: http://head.hackage.haskell.org/' >> ${HOME}/.cabal/config + echo ' secure: True' >> ${HOME}/.cabal/config + echo ' root-keys: 07c59cb65787dedfaef5bd5f987ceb5f7e5ebf88b904bbd4c5cbdeb2ff71b740' >> ${HOME}/.cabal/config + echo ' 2e8555dde16ebd8df076f1a8ef13b8f14c66bad8eafefd7d9e37d0ed711821fb' >> ${HOME}/.cabal/config + echo ' 8f79fd2389ab2967354407ec852cbe73f2e8635793ac446d09461ffb99527f6e' >> ${HOME}/.cabal/config + echo ' key-threshold: 3' >> ${HOME}/.cabal.config + + cabal new-update head.hackage -v + fi + - grep -Ev -- '^\s*--' ${HOME}/.cabal/config | grep -Ev '^\s*$' + - "printf 'packages: \".\"\\n' > cabal.project" + - cat cabal.project + - if [ -f "./configure.ac" ]; then + (cd "." && autoreconf -i); + fi + - rm -f cabal.project.freeze + - cabal new-build -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dep -j2 all + - rm -rf "."/.ghc.environment.* "."/dist + - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX) + +# Here starts the actual work to be performed for the package under test; +# any command which exits with a non-zero exit code causes the build to fail. script: - # -v2 provides useful information for debugging - - cabal configure -v2 + # test that source-distributions can be generated + - (cd "." && cabal sdist) + - mv "."/dist/eq-*.tar.gz ${DISTDIR}/ + - cd ${DISTDIR} || false + - find . -maxdepth 1 -name '*.tar.gz' -exec tar -xvf '{}' \; + - "printf 'packages: eq-*/*.cabal\\n' > cabal.project" + - cat cabal.project - # this builds all libraries and executables - # (including tests/benchmarks) - - cabal build - # tests that a source-distribution can be generated - - cabal sdist + # build & run tests, build benchmarks + - cabal new-build -w ${HC} ${TEST} ${BENCH} all - # check that the generated source-distribution can be built & installed - - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ; - cd dist/; - if [ -f "$SRC_TGZ" ]; then - cabal install --force-reinstalls "$SRC_TGZ"; - else - echo "expected '$SRC_TGZ' not found"; - exit 1; - fi + # cabal check + - (cd eq-* && cabal check) -notifications: - irc: - channels: - - "irc.freenode.org#haskell-lens" - skip_join: true - template: - - "\x0313eq\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}" + # haddock + - rm -rf ./dist-newstyle + - if $HADDOCK; then cabal new-haddock -w ${HC} ${TEST} ${BENCH} all; else echo "Skipping haddock generation";fi + +# REGENDATA ["-o",".travis.yml","--irc-channel=irc.freenode.org#haskell-lens","--no-no-tests-no-bench","--no-installed","cabal.project"] +# EOF diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown --- a/CHANGELOG.markdown +++ b/CHANGELOG.markdown @@ -1,3 +1,13 @@ +4.1 +--- +* Add `TestEquality` and `TestCoercion` instances for `(:=)`. +* Add `fromLeibniz` and `toLeibniz` functions for converting between `(:~:)` + (from `Data.Type.Equality`) and `(:=)`. +* Add a `reprLeibniz` function to convert `(:=)` to a `Coercion` + (i.e., representational equality). +* Make `(:=)` a newtype. +* We can remove the `Trustworthy` claim and infer as `Safe` on modern GHCs. + 4.0.2 ----- * Made := kind polymorphic. diff --git a/README.markdown b/README.markdown --- a/README.markdown +++ b/README.markdown @@ -1,7 +1,7 @@ eq == -[![Build Status](https://secure.travis-ci.org/ekmett/eq.png?branch=master)](http://travis-ci.org/ekmett/eq) +[![Hackage](https://img.shields.io/hackage/v/eq.svg)](https://hackage.haskell.org/package/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. diff --git a/eq.cabal b/eq.cabal --- a/eq.cabal +++ b/eq.cabal @@ -1,6 +1,6 @@ name: eq category: Type System -version: 4.0.4 +version: 4.1 license: BSD3 cabal-version: >= 1.6 license-file: LICENSE @@ -11,8 +11,17 @@ bug-reports: http://github.com/ekmett/eq/issues copyright: Copyright (C) 2011-2013 Edward A. Kmett synopsis: Leibnizian equality -description: Leibnizian equality +description: Leibnizian equality. build-type: Simple +tested-with: GHC == 7.0.4 + , GHC == 7.2.2 + , GHC == 7.4.2 + , GHC == 7.6.3 + , GHC == 7.8.4 + , GHC == 7.10.3 + , GHC == 8.0.2 + , GHC == 8.2.2 + , GHC == 8.4.1 extra-source-files: .ghci @@ -39,7 +48,7 @@ exposed-modules: Data.Eq.Type - if impl(ghc >= 7.0) && impl(ghc < 7.6) + if impl(ghc >= 7.0) extensions: TypeFamilies cpp-options: -DLANGUAGE_TypeFamilies diff --git a/src/Data/Eq/Type.hs b/src/Data/Eq/Type.hs --- a/src/Data/Eq/Type.hs +++ b/src/Data/Eq/Type.hs @@ -1,13 +1,15 @@ {-# LANGUAGE CPP, Rank2Types, TypeOperators #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 -{-# LANGUAGE Trustworthy #-} -#endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706 {-# LANGUAGE PolyKinds #-} #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 {-# LANGUAGE RoleAnnotations #-} #endif +#if defined(__GLASGOW_HASKELL__) && MIN_VERSION_base(4,7,0) +#define HAS_DATA_TYPE_EQUALITY 1 +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +#endif ----------------------------------------------------------------------------- -- | @@ -20,7 +22,7 @@ -- 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: +-- is provided by a generalization of a trick by Oleg Kiselyov posted here: -- -- ---------------------------------------------------------------------------- @@ -44,18 +46,33 @@ , lower2 , lower3 #endif +#ifdef HAS_DATA_TYPE_EQUALITY + -- * 'Eq.:~:' equivalence + -- | "Data.Type.Equality" GADT definition is equivalent in power + , fromLeibniz + , toLeibniz + + -- * 'Co.Coercion' conversion + -- | Leibnizian equality can be converted to representational equality + , reprLeibniz +#endif ) where -import Prelude (flip) +import Prelude (Maybe(..), flip) import Control.Category import Data.Semigroupoid import Data.Groupoid +#ifdef HAS_DATA_TYPE_EQUALITY +import qualified Data.Type.Coercion as Co +import qualified Data.Type.Equality as Eq +#endif + 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 } +-- substitute one for the other in all contexts +newtype a := b = Refl { subst :: forall c. c a -> c b } #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 type role (:=) nominal nominal #endif @@ -110,24 +127,44 @@ lift3' ab cd ef = lift3 ab `subst` lift2 cd `subst` lift ef #ifdef LANGUAGE_TypeFamilies -type family Inj f +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 :: forall (a :: *) (b :: *) (f :: * -> *). f a := f b -> a := b lower eq = unlower (subst eq (Lower refl :: Lower (f a) (f a))) -type family Inj2 f -type instance Inj2 (f a b) = 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 :: forall (a :: *) (b :: *) (c :: *) (f :: * -> * -> *). + f a c := f b c -> a := b lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 (f a c) (f a c))) -type family Inj3 f -type instance Inj3 (f a b c) = a +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 +-- | But unfortunately these definitions aren't polykinded. Everything is just a star. +lower3 :: forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> * -> *). + f a c d := f b c d -> a := b lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 (f a c d) (f a c d))) +#endif + +#ifdef HAS_DATA_TYPE_EQUALITY +fromLeibniz :: a := b -> a Eq.:~: b +fromLeibniz a = subst a Eq.Refl + +toLeibniz :: a Eq.:~: b -> a := b +toLeibniz Eq.Refl = refl + +instance Eq.TestEquality ((:=) a) where + testEquality fa fb = Just (fromLeibniz (trans (symm fa) fb)) + +reprLeibniz :: a := b -> Co.Coercion a b +reprLeibniz a = subst a Co.Coercion + +instance Co.TestCoercion ((:=) a) where + testCoercion fa fb = Just (reprLeibniz (trans (symm fa) fb)) #endif