eq 4.1 → 4.2

raw patch · 6 files changed

+295/−26 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• .gitignore +1/−0
• .travis.yml +3/−4
• CHANGELOG.markdown +7/−0
• eq.cabal +5/−2
• src/Data/Eq/Type.hs +28/−20
• src/Data/Eq/Type/Hetero.hs +251/−0

@@ -1,4 +1,5 @@ dist+dist-newstyle docs wiki TAGS

@@ -60,9 +60,9 @@     - 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-8.4.2"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.2,ghc-8.4.2], sources: [hvr-ghc]}}     - compiler: "ghc-head"       env: GHCHEAD=true       addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-head], sources: [hvr-ghc]}}@@ -70,7 +70,6 @@   allow_failures:     - compiler: "ghc-7.0.4"     - compiler: "ghc-7.2.2"-    - compiler: "ghc-8.4.1"     - compiler: "ghc-head"  before_install:

@@ -1,3 +1,10 @@+4.2 [2018.04.24]+----------------+* Make `lower`, `lower2`, and `lower3` in `Data.Eq.Type` poly-kinded.+* Introduce the `Data.Eq.Type.Hetero` module, which exposes `(:==)`, a+  heterogeneously kinded version of `(:=)`. This module is only available+  on GHC 8.2 and later.+ 4.1 --- * Add `TestEquality` and `TestCoercion` instances for `(:=)`.

@@ -1,6 +1,6 @@ name:          eq category:      Type System-version:       4.1+version:       4.2 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -21,7 +21,7 @@              , GHC == 7.10.3              , GHC == 8.0.2              , GHC == 8.2.2-             , GHC == 8.4.1+             , GHC == 8.4.2  extra-source-files:   .ghci@@ -51,6 +51,9 @@   if impl(ghc >= 7.0)     extensions: TypeFamilies     cpp-options: -DLANGUAGE_TypeFamilies++  if impl(ghc >= 8.2)+    exposed-modules: Data.Eq.Type.Hetero    ghc-options: -Wall   hs-source-dirs: src

@@ -1,5 +1,6 @@ {-# LANGUAGE CPP, Rank2Types, TypeOperators #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706+#define LANGUAGE_PolyKinds {-# LANGUAGE PolyKinds #-} #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707@@ -127,29 +128,36 @@ lift3' ab cd ef = lift3 ab `subst` lift2 cd `subst` 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 :: forall (a :: *) (b :: *) (f :: * -> *). f a := f b -> a := b-lower eq = unlower (subst eq (Lower refl :: Lower (f a) (f a)))+# ifdef LANGUAGE_PolyKinds+type family Inj  (f :: j -> k)           (a :: k) :: j+type family Inj2 (f :: i -> j -> k)      (a :: k) :: i+type family Inj3 (f :: h -> i -> j -> k) (a :: k) :: h+# else+type family Inj  (f :: * -> *)           (a :: *) :: *+type family Inj2 (f :: * -> * -> *)      (a :: *) :: *+type family Inj3 (f :: * -> * -> * -> *) (a :: *) :: *+# endif -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 :: 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 instance Inj  f (f a)     = a+type instance Inj2 f (f a b)   = a+type instance Inj3 f (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 }--- | 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)))+newtype Lower  f a b = Lower  { unlower  :: Inj  f a := Inj  f b }+newtype Lower2 f a b = Lower2 { unlower2 :: Inj2 f a := Inj2 f b }+newtype Lower3 f a b = Lower3 { unlower3 :: Inj3 f a := Inj3 f b } +-- | Type constructors are injective, so you can lower equality through any+-- type constructor ...+lower :: forall a b f. f a := f b -> a := b+lower eq = unlower (subst eq (Lower refl :: Lower f (f a) (f a)))++-- | ... in any position ...+lower2 :: forall a b c f. f a c := f b c -> a := b+lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 f (f a c) (f a c)))++-- | ... these definitions are poly-kinded on GHC 7.6 and up.+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 (f a c d) (f a c d))) #endif  #ifdef HAS_DATA_TYPE_EQUALITY

@@ -0,0 +1,251 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Eq.Type.Hetero+-- Copyright   :  (C) 2011-2014 Edward Kmett, 2018 Ryan Scott+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  provisional+-- Portability :  GHC+--+-- Leibnizian equality à la "Data.Eq.Type", generalized to be heterogenous+-- using higher-rank kinds.+--+-- This module is only exposed on GHC 8.2 and later.+----------------------------------------------------------------------------+module Data.Eq.Type.Hetero+  (+  -- * Heterogeneous Leibnizian equality+    (:==)(..)+  -- * Equality as an equivalence relation+  , refl+  , trans+  , symm+  , coerce+  -- * Lifting equality+  , lift+  , lift2, lift2'+  , lift3, lift3'+  -- * Lowering equality+  , lower+  , lower2+  , lower3+  -- * 'ET.:=' equivalence+  -- | 'ET.:=' is equivalent in power+  , toHomogeneous+  , fromHomogeneous+  -- * 'Eq.:~:' equivalence+  -- | 'Eq.:~:' is equivalent in power+  , fromLeibniz+  , toLeibniz+  -- * 'Eq.:~~:' equivalence+  -- | 'Eq.:~~:' is equivalent in power+  , heteroFromLeibniz+  , heteroToLeibniz+  -- * 'Co.Coercion' conversion+  -- | Leibnizian equality can be converted to representational equality+  , reprLeibniz+  ) where++import           Control.Category+import           Data.Groupoid+import           Data.Semigroupoid+import qualified Data.Type.Coercion as Co+import qualified Data.Type.Equality as Eq+import           Data.Kind+import qualified Data.Eq.Type as ET+import           GHC.Exts (Any)+import           Prelude hiding (id, (.))++infixl 4 :==++-- | Heterogeneous Leibnizian equality.+--+-- Leibnizian equality states that two things are equal if you can+-- substitute one for the other in all contexts.+newtype (a :: j) :== (b :: k)+  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }+type role (:==) nominal nominal++-- | Equality is reflexive.+refl :: a :== a+refl = HRefl id++newtype Coerce (a :: k) = Coerce { uncoerce :: MassageKind Type a }++type family MassageKind (j :: Type) (a :: k) :: j where+  MassageKind j (a :: j) = a+  MassageKind _ _        = Any++-- | If two things are equal, you can convert one to the other.+coerce :: a :== b -> a -> b+coerce f = uncoerce . hsubst f . Coerce++newtype Push :: (forall (j :: Type) (k :: Type). j -> k -> Type)+             -> forall (j :: Type). j -> forall (k :: Type). k -> Type where+  Push :: forall (p :: forall (j :: Type) (k :: Type). j -> k -> Type)+                 (j :: Type) (k :: Type) (a :: j) (b :: k).+          { unpush :: p a b } -> Push p a b++-- | Equality is compositional.+comp :: b :== c -> a :== b -> a :== c+comp f = unpush . hsubst f . Push++-- | Equality forms a category.+instance Category (:==) where+  id  = refl+  (.) = comp++instance Semigroupoid (:==) where+  o = comp++instance Groupoid (:==) where+  inv = symm++-- | Equality is transitive.+trans :: a :== b -> b :== c -> a :== c+trans = flip comp++newtype Symm :: (forall (i1 :: Type). i1 -> forall (i2 :: Type). i2 -> Type)+             -> forall (j :: Type). j+             -> forall (k :: Type). k+             -> Type where+  Symm :: forall (p :: forall (i1 :: Type). i1 -> forall (i2 :: Type). i2 -> Type)+                 (j :: Type) (k :: Type)+                 (a :: j) (b :: k).+          { unsymm :: p b a } -> Symm p a b++-- | Equality is symmetric.+symm :: a :== b -> b :== a+symm ab = unpush $ unsymm $ hsubst ab $ Symm $ Push refl++newtype Lift :: forall (j :: Type) (r :: Type).+                (j -> r) -> j+             -> forall (k :: Type). k+             -> Type where+  Lift :: forall (j :: Type) (k :: Type) (r :: Type)+                 (f :: j -> r) (a :: j) (b :: k).+          { unlift :: f a :== f (MassageKind j b) } -> Lift f a b++-- | You can lift equality into any type constructor...+lift :: a :== b -> f a :== f b+lift f = unlift $ hsubst f $ Lift refl++newtype Lift2 :: forall (j1 :: Type) (j2 :: Type) (r :: Type).+                 (j1 -> j2 -> r) -> j1 -> j2+              -> forall (k :: Type). k+              -> Type where+  Lift2 :: forall (j1 :: Type) (j2 :: Type) (k :: Type) (r :: Type)+                  (f :: j1 -> j2 -> r) (a :: j1) (b :: k) (c :: j2).+           { unlift2 :: f a c :== f (MassageKind j1 b) c } -> Lift2 f a c b++-- | ... in any position.+lift2 :: a :== b -> f a c :== f b c+lift2 f = unlift2 $ hsubst f $ Lift2 refl++lift2' :: a :== b -> c :== d -> f a c :== f b d+lift2' ab cd = unpush $ lift2 ab `hsubst` Push (lift cd)++newtype Lift3 :: forall (j1 :: Type) (j2 :: Type) (j3 :: Type) (r :: Type).+                 (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3+              -> forall (k :: Type). k+              -> Type where+  Lift3 :: forall (j1 :: Type) (j2 :: Type) (j3 :: Type) (k :: Type) (r :: Type)+                  (f :: j1 -> j2 -> j3 -> r) (a :: j1) (b :: k) (c :: j2) (d :: j3).+           { unlift3 :: f a c d :== f (MassageKind j1 b) c d } -> Lift3 f a c d b++lift3 :: a :== b -> f a c d :== f b c d+lift3 f = unlift3 $ hsubst f $ Lift3 refl++lift3' :: a :== b -> c :== d -> e :== f -> g a c e :== g b d f+lift3' ab cd ef = unpush $ unpush (lift3 ab `hsubst` Push (lift2 cd)) `hsubst` Push (lift ef)++newtype Lower :: Type+              -> forall (j :: Type). j+              -> forall (k :: Type). k -> Type where+  Lower :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).+           { unlower :: Inj i a :== Inj i (MassageKind j b) } -> Lower i a b++type family Inj (j :: Type) (a :: k) :: j where+  Inj j (f (a :: j)) = a+  Inj _ _            = Any++-- | Type constructors are injective, so you can lower equality through any type constructor.+lower :: forall (j :: Type) (k :: Type) (f :: j -> k) (a :: j) (b :: j).+         f a :== f b -> a :== b+lower f = unlower $ hsubst f (Lower refl :: Lower j (f a) (f a))++newtype Lower2 :: Type+               -> forall (j :: Type). j+               -> forall (k :: Type). k -> Type where+  Lower2 :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).+            { unlower2 :: Inj2 i a :== Inj2 i (MassageKind j b) } -> Lower2 i a b++type family Inj2 (j :: Type) (a :: k) :: j where+  Inj2 j (f (a :: j) b) = a+  Inj2 _ _              = Any++lower2 :: forall (i :: Type) (j :: Type) (k :: Type)+                 (f :: i -> j -> k) (a :: i) (b :: i) (c :: j).+          f a c :== f b c -> a :== b+lower2 f = unlower2 $ hsubst f (Lower2 refl :: Lower2 i (f a c) (f a c))++newtype Lower3 :: Type+               -> forall (j :: Type). j+               -> forall (k :: Type). k -> Type where+  Lower3 :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).+            { unlower3 :: Inj3 i a :== Inj3 i (MassageKind j b) } -> Lower3 i a b++type family Inj3 (j :: Type) (a :: k) :: j where+  Inj3 j (f (a :: j) b c) = a+  Inj3 _ _                = Any++lower3 :: forall (h :: Type) (i :: Type) (j :: Type) (k :: Type)+                 (f :: h -> i -> j -> k) (a :: h) (b :: h) (c :: i) (d :: j).+          f a c d :== f b c d -> a :== b+lower3 f = unlower3 $ hsubst f (Lower3 refl :: Lower3 h (f a c d) (f a c d))++newtype Flay :: forall (j :: Type).+                (j -> j -> Type) -> j+             -> forall (k :: Type). k -> Type where+  Flay :: forall (j :: Type) (k :: Type)+                 (p :: j -> j -> Type) (a :: j) (b :: k).+          { unflay :: p a (MassageKind j b) } -> Flay p a b++-- | Convert an appropriately kinded heterogeneous Leibnizian equality into+-- a homogeneous Leibnizian equality '(ET.:=)'.+toHomogeneous :: a :== b -> a ET.:= b+toHomogeneous f = unflay $ hsubst f $ Flay ET.refl++-- | Convert a homogeneous Leibnizian equality '(ET.:=)' to an appropriately kinded+-- heterogeneous Leibizian equality.+fromHomogeneous :: a ET.:= b -> a :== b+fromHomogeneous f = ET.subst f refl++fromLeibniz :: forall a b. a :== b -> a Eq.:~: b+fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl++toLeibniz :: a Eq.:~: b -> a :== b+toLeibniz Eq.Refl = refl++heteroFromLeibniz :: a :== b -> a Eq.:~~: b+heteroFromLeibniz f = unpush $ hsubst f $ Push $ Eq.HRefl++heteroToLeibniz :: a Eq.:~~: b -> a :== b+heteroToLeibniz Eq.HRefl = refl++instance Eq.TestEquality ((:==) a) where+  testEquality fa fb = Just (fromLeibniz (trans (symm fa) fb))++reprLeibniz :: a :== b -> Co.Coercion a b+reprLeibniz f = unflay $ hsubst f $ Flay Co.Coercion++instance Co.TestCoercion ((:==) a) where+  testCoercion fa fb = Just (reprLeibniz (trans (symm fa) fb))