type-equality 1 → 1.0.1
raw patch · 4 files changed
+35/−301 lines, 4 filesdep ~base
Dependency ranges changed: base
Files
- CHANGELOG.md +4/−0
- src-hetero/Data/Type/Equality/Hetero.hs +1/−64
- src-old/Data/Type/Equality.hs +0/−212
- type-equality.cabal +30/−25
CHANGELOG.md view
@@ -1,3 +1,7 @@+## 1.0.1++ * Support GHC-8.6.5..GHC-9.10.1+ ## 1 * Rewrite the library to contain a shim of recent `base` `Data.Type.Equality` module.
src-hetero/Data/Type/Equality/Hetero.hs view
@@ -1,70 +1,7 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ <800-#error "Trying to compiled Data.Type.Equality.Hetero module with GHC <7.6"-#endif-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} -- | This module shims kind heterogeneous propositional equality.------ Note: some instances: 'Read', 'Enum', 'Bounded' and 'Data' would be available--- only since GHC-8.0 as we need @~~@ constraint.--- Also GH-7.10.3 is nitpicky /data constructor ‘HRefl’ cannot be GADT-like in its *kind* arguments/,--- thus this module is available only with GHC >= 8.0 module Data.Type.Equality.Hetero ( (:~~:)(..),- ) where+) where -#if MIN_VERSION_base(4,10,0) import Data.Type.Equality ((:~~:)(..))-#else--import qualified Control.Category as C-import Data.Data (Data)-import Data.Type.Equality-import Data.Typeable (Typeable)--#if MIN_VERSION_base(4,7,0)-import Data.Type.Coercion (TestCoercion (..), Coercion (..))-#endif---- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is--- inhabited by a terminating value if and only if @a@ is the same type as @b@.-data (a :: k1) :~~: (b :: k2) where- HRefl :: a :~~: a--infixr 4 :~~:--deriving instance Eq (a :~~: b)-deriving instance Show (a :~~: b)-deriving instance Ord (a :~~: b)--deriving instance a ~~ b => Read (a :~~: b)--instance a ~~ b => Enum (a :~~: b) where- toEnum 0 = HRefl- toEnum _ = errorWithoutStackTrace "Data.Type.Equality.Hetero.toEnum: bad argument"-- fromEnum HRefl = 0--deriving instance a ~~ b => Bounded (a :~~: b)--deriving instance Typeable (:~~:)-deriving instance (Typeable i, Typeable j, Typeable a, Typeable b,- (a :: i) ~~ (b :: j)) => Data (a :~~: b)--instance C.Category (:~~:) where- id = HRefl- HRefl . HRefl = HRefl--instance TestEquality ((:~~:) a) where- testEquality HRefl HRefl = Just Refl--instance TestCoercion ((:~~:) a) where- testCoercion HRefl HRefl = Just Coercion-#endif
− src-old/Data/Type/Equality.hs
@@ -1,212 +0,0 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 708-#error "Trying to compiled Data.Type.Equality module with GHC-7.8+"-#endif-{-# LANGUAGE GADTs #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-#if __GLASGOW_HASKELL__ >= 706-{-# LANGUAGE PolyKinds #-}-#endif-#if __GLASGOW_HASKELL__ >= 702--- only Trustworthy, as we have manual Typeable instance-{-# LANGUAGE Trustworthy #-}-#endif-module Data.Type.Equality (- -- * Type equality- (:~:) (..),- -- * Combinators- sym,- trans,- castWith,- gcastWith,--#if __GLASGOW_HASKELL__ >= 706- apply,-#endif- inner,-#if __GLASGOW_HASKELL__ >= 706- outer,-#endif-- -- inner and outer not implemented,- -- as GHC-7.6 fails to infer them:- -- Could not deduce (f ~ g) from the context (f a ~ g b)-- -- There are no (==) as it needs ClosedTypeFamilies (since GHC-7.8)-- -- * TestEquality- --- -- | Provided only for GHC-7.6.- -- Also there isn't @==@ type family, as it requires close type families,- -- which are available only since GHC-7.8.- TestEquality (..),- ) where--import qualified Control.Category as C-import Data.Typeable (Typeable2 (..), Typeable)-import Data.Data (Data (..), Constr, mkConstr, Fixity(Prefix), DataType, mkDataType, mkTyConApp, TyCon)--#if MIN_VERSION_base(4,4,0)-import Data.Data (mkTyCon3)-#else-import Data.Data (mkTyCon)-#endif--#ifndef CURRENT_PACKAGE_KEY-import Data.Version (showVersion)-import Paths_type_equality_compat (version)-#endif---- | Propositional equality. If @a ':~:' b@ is inhabited by some--- terminating value, then the type @a@ is the same as the type--- @b@. To use this equality in practice, pattern-match on the--- @a ':~:' b@ to get out the 'Refl' constructor; in the body of--- the pattern-match, the compiler knows that @a ~ b@.------ /Note:/ this definition is polykinded only since GHC-7.6.----data a :~: b where- Refl :: a :~: a--deriving instance Eq (a :~: b)-deriving instance Ord (a :~: b)-deriving instance a ~ b => Read (a :~: b)-deriving instance Show (a :~: b)--instance C.Category (:~:) where- id = Refl- Refl . Refl = Refl--instance a ~ b => Enum (a :~: b) where- toEnum 0 = Refl- toEnum _ = error "Data.Type.Equality.toEnum: bad argument"-- fromEnum Refl = 0--instance a ~ b => Bounded (a :~: b) where- minBound = Refl- maxBound = Refl------------------------------------------------------------------------------------ Typeable & Data----------------------------------------------------------------------------------instance Typeable2 (:~:) where- typeOf2 _ = mkTyConApp eqTyCon []--typeEqualityCompatPackageKey :: String-#ifdef CURRENT_PACKAGE_KEY-typeEqualityCompatPackageKey = CURRENT_PACKAGE_KEY-#else-typeEqualityCompatPackageKey = "type-equality-compat-" ++ showVersion version-#endif--eqTyCon :: TyCon-#if MIN_VERSION_base(4,4,0)-eqTyCon = mkTyCon3 typeEqualityCompatPackageKey "Data.Type.Equality" ":~:"-#else-eqTyCon = mkTyCon "Data.Type.Equality.:~:"-#endif--instance (Typeable a, Typeable b, a ~ b) => Data (a :~: b) where- gfoldl _ z Refl = z Refl- gunfold _ z _ = z Refl- toConstr Refl = reflConstr- dataTypeOf _ = eqDataType--eqDataType :: DataType-eqDataType = mkDataType ":~:" [reflConstr]--reflConstr :: Constr-reflConstr = mkConstr eqDataType "Refl" [] Prefix------------------------------------------------------------------------------------ Combinators------------------------------------------------------------------------------------ | Symmetry of equality-sym :: (a :~: b) -> (b :~: a)-sym Refl = Refl---- | Transitivity of equality-trans :: (a :~: b) -> (b :~: c) -> (a :~: c)-trans Refl Refl = Refl---- | Type-safe cast, using propositional equality-castWith :: (a :~: b) -> a -> b-castWith Refl x = x---- | Generalized form of type-safe cast using propositional equality-gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r-gcastWith Refl x = x--#if __GLASGOW_HASKELL__ >= 706--- | Apply one equality to another, respectively-apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)-apply Refl Refl = Refl-#endif---- | Extract equality of the arguments from an equality of applied types-inner :: f a :~: g b -> a :~: b-inner = fromLeibniz . innerLeibniz . toLeibniz--#if __GLASGOW_HASKELL__ >= 706--- | Extract equality of type constructors from an equality of applied types-outer :: f a :~: g b -> f :~: g-outer = fromLeibniz . outerLeibniz . toLeibniz-#endif------------------------------------------------------------------------------------ TestEquality------------------------------------------------------------------------------------ | This class contains types where you can learn the equality of two types--- from information contained in /terms/. Typically, only singleton types should--- inhabit this class.-class TestEquality f where- -- | Conditionally prove the equality of @a@ and @b@.- testEquality :: f a -> f b -> Maybe (a :~: b)--instance TestEquality ((:~:) a) where- testEquality Refl Refl = Just Refl------------------------------------------------------------------------------------ Leibniz----------------------------------------------------------------------------------newtype a := b = ReflLeibniz { subst :: forall c. c a -> c b }--reflLeibniz :: a := a-reflLeibniz = ReflLeibniz id--#if __GLASGOW_HASKELL__ >= 706-type family Inj (f :: j -> k) (a :: k) :: j-#else-type family Inj (f :: * -> *) (a :: *) :: *-#endif-type instance Inj f (g a) = a--newtype Lower f a b = Lower { unlower :: Inj f a := Inj f b }--fromLeibniz :: a := b -> a :~: b-fromLeibniz a = subst a Refl--toLeibniz :: a :~: b -> a := b-toLeibniz Refl = reflLeibniz--innerLeibniz :: f a := g b -> a := b-innerLeibniz eq = unlower (subst eq (Lower reflLeibniz :: Lower f (f a) (f a)))--#if __GLASGOW_HASKELL__ >= 706-type family Gen (f :: j -> k) (a :: k) :: j -> k-type instance Gen f (g a) = g--newtype Generate f a b = Generate { ungenerate :: Gen f a := Gen f b }--outerLeibniz :: f a := g b -> f := g-outerLeibniz eq = ungenerate (subst eq (Generate reflLeibniz :: Generate f (f a) (f a)))-#endif
type-equality.cabal view
@@ -1,18 +1,22 @@-name: type-equality-version: 1-stability: provisional-cabal-version: >=1.10-build-type: Simple-author: Oleg Grenrus <oleg.grenrus@iki.fi>, Ryan Scott <ryan.gl.scott@gmail.com>, Erik Hesselink <hesselink@gmail.com>, Martijn van Steenbergen-maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>, Ryan Scott <ryan.gl.scott@gmail.com>, Erik Hesselink <hesselink@gmail.com>-license: BSD3-license-file: LICENSE-homepage: https://github.com/hesselink/type-equality-category: Data, Dependent Types-synopsis: Data.Type.Equality compat package+name: type-equality+version: 1.0.1+stability: provisional+cabal-version: >=1.10+build-type: Simple+author:+ Oleg Grenrus <oleg.grenrus@iki.fi>, Ryan Scott <ryan.gl.scott@gmail.com>, Erik Hesselink <hesselink@gmail.com>, Martijn van Steenbergen++maintainer:+ Oleg Grenrus <oleg.grenrus@iki.fi>, Ryan Scott <ryan.gl.scott@gmail.com>, Erik Hesselink <hesselink@gmail.com>++license: BSD3+license-file: LICENSE+homepage: https://github.com/hesselink/type-equality+category: Data, Dependent Types+synopsis: Data.Type.Equality compat package description: This library defines a propositional equality data type,- shims @Data.Type.Equality" as well as possible for older GHCs (< 7.8).+ shims @Data.Type.Equality@ as well as possible for older GHCs (< 7.8). . @ data a :~: b where@@ -24,8 +28,15 @@ extra-source-files: CHANGELOG.md tested-with:- GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4 || ==7.6.3 || ==7.4.2 || ==7.2.2 || ==7.0.4-+ GHC ==8.6.5+ || ==8.8.4+ || ==8.10.7+ || ==9.0.2+ || ==9.2.8+ || ==9.4.8+ || ==9.6.5+ || ==9.8.2+ || ==9.10.1 source-repository head type: git@@ -33,13 +44,7 @@ library default-language: Haskell2010- build-depends: base >=4.3 && <4.14-- if !impl(ghc >=7.8)- hs-source-dirs: src-old- exposed-modules: Data.Type.Equality-- if impl(ghc >=8.0)- hs-source-dirs: src-hetero- exposed-modules: Data.Type.Equality.Hetero- other-extensions: PolyKinds+ build-depends: base >=4.12 && <4.21+ hs-source-dirs: src-hetero+ exposed-modules: Data.Type.Equality.Hetero+ other-extensions: PolyKinds