diff --git a/CHANGELOG b/CHANGELOG deleted file mode 100644 --- a/CHANGELOG +++ /dev/null @@ -1,17 +0,0 @@ -0.1.2 - * Add subst2. Thanks to James Koppel. - -0.1.1 - * Turn on PolyKinds for GHC >= 7.6. Thanks to Ben Franksen. - -0.1.0.2 - * Move 'Build-depends' to 'Library' section. Thanks to Brent Yorgey. - -0.1.0.1 - * Added EqT instance for (:=:) - * Removed 'cast' as synonym for 'coerce'. - * Show and read instances for (:=:). - * Lots of small changes. - -0.1.0 - * Initial version. diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,20 @@ +## 1 + * Rewrite the library to contain a shim of recent `base` `Data.Type.Equality` module. + +## 0.1.2 + * Add subst2. Thanks to James Koppel. + +## 0.1.1 + * Turn on PolyKinds for GHC >= 7.6. Thanks to Ben Franksen. + +## 0.1.0.2 + * Move 'Build-depends' to 'Library' section. Thanks to Brent Yorgey. + +## 0.1.0.1 + * Added EqT instance for (:=:) + * Removed 'cast' as synonym for 'coerce'. + * Show and read instances for (:=:). + * Lots of small changes. + +## 0.1.0 + * Initial version. diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,28 +1,30 @@ -Copyright (c) Erik Hesselink 2009 +Copyright (c) 2009 Erik Hesselink, 2019 Oleg Grenrus, Ryan Scott All rights reserved. Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions -are met: -1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. -2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. -3. Neither the name of the author nor the names of his contributors - may be used to endorse or promote products derived from this software - without specific prior written permission. +modification, are permitted provided that the following conditions are met: -THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE -IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE -ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT -LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY -OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF -SUCH DAMAGE. + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of authors nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.lhs b/Setup.lhs deleted file mode 100644 --- a/Setup.lhs +++ /dev/null @@ -1,5 +0,0 @@ -#! /usr/bin/env runhaskell - ->import Distribution.Simple ->main = defaultMain - diff --git a/src-hetero/Data/Type/Equality/Hetero.hs b/src-hetero/Data/Type/Equality/Hetero.hs new file mode 100644 --- /dev/null +++ b/src-hetero/Data/Type/Equality/Hetero.hs @@ -0,0 +1,70 @@ +{-# 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 + +#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 diff --git a/src-old/Data/Type/Equality.hs b/src-old/Data/Type/Equality.hs new file mode 100644 --- /dev/null +++ b/src-old/Data/Type/Equality.hs @@ -0,0 +1,212 @@ +{-# 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 diff --git a/src/Data/Type/Equality.hs b/src/Data/Type/Equality.hs deleted file mode 100644 --- a/src/Data/Type/Equality.hs +++ /dev/null @@ -1,124 +0,0 @@ -{-# LANGUAGE TypeOperators - , GADTs - , FlexibleInstances - , CPP - #-} -#if __GLASGOW_HASKELL__ >= 706 -{-# LANGUAGE PolyKinds #-} -#endif -------------------------------------------------------------------------------- --- | --- Module : Data.Type.Equality --- Copyright : (c) 2009, Erik Hesselink --- License : BSD3 --- --- Maintainer : Erik Hesselink --- Stability : Experimental --- --- Type equality, coercion/cast and other operations. --- -------------------------------------------------------------------------------- -module Data.Type.Equality - ( (:=:)(Refl) - , sym - , trans - , subst - , subst2 - - , cong - , cong2 - , cong3 - - , coerce - - , EqT(eqT) - , EqT2(eqT2) - , EqT3(eqT3) - ) where - -import Prelude -#if __GLASGOW_HASKELL__ >= 609 - hiding (id, (.)) -import Control.Category -#endif - --- | Type equality. A value of @a :=: b@ is a proof that types @a@ and --- @b@ are equal. By pattern matching on @Refl@ this fact is --- introduced to the type checker. -data a :=: b where - Refl :: a :=: a - -infix 4 :=: - --- | Any value is just shown as "Refl", but this cannot be derived for --- a GADT, so it is defined here manually. -instance Show (a :=: b) where - showsPrec _ Refl = showString "Refl" - --- | We can only read values if the result is @a :=: a@, not @a :=: b@ --- since that is not true, in general. We just parse the string --- "Refl", optionally surrounded with parentheses, and return 'Refl'. -instance Read (a :=: a) where - readsPrec _ = readParen False (\s -> [(Refl, r) | ("Refl", r) <- lex s]) - -#if __GLASGOW_HASKELL__ >= 609 -instance Category (:=:) where - id = Refl - Refl . Refl = Refl -#endif - --- | Equality is symmetric. -sym :: a :=: b -> b :=: a -sym Refl = Refl - --- | Equality is transitive. This is the same as (>>>) from the 'Category' --- instance, but also works in GHC 6.8. -trans :: a :=: b -> b :=: c -> a :=: c -trans Refl Refl = Refl - --- | Equality is substitutive. This is defined directly, but can also --- be defined as 'coerce' '.' 'cong'. -subst :: a :=: b -> f a -> f b -subst Refl = id - --- | Substitution inside nested type constructors. This is equivalent --- to 'coerce' '.' 'cong' '.' 'cong'. -subst2 :: a :=: b -> f (g a) -> f (g b) -subst2 Refl = id - --- | Equality is congruential. -cong :: a :=: b -> f a :=: f b -cong Refl = Refl - --- | Congruence for type constructors with two parameters. -cong2 :: a :=: b -> c :=: d -> f a c :=: f b d -cong2 Refl Refl = Refl - --- | Congruence for type constructors with three parameters. -cong3 :: a :=: a'-> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c' -cong3 Refl Refl Refl = Refl - --- | Coerce a type to another using an equality proof. -coerce :: a :=: b -> a -> b -coerce Refl = id - --- | A type class for constructing equality proofs. This is as close --- as we can get to decidable equality on types. Note that @f@ must be --- a GADT to be able to define 'eqT'. -class EqT f where - eqT :: f a -> f b -> Maybe (a :=: b) - --- | A type class for constructing equality proofs for type --- constructor with two parameters. Can be useful when representing --- relations between types. -class EqT2 f where - eqT2 :: f a b -> f c d -> (Maybe (a :=: c), Maybe (b :=: d)) - --- | A type class for constructing equality proofs for type --- constructor with three parameters. If you find a use for this, let --- me know. -class EqT3 f where - eqT3 :: f a b c -> f a' b' c' -> (Maybe (a :=: a'), Maybe (b :=: b'), Maybe (c :=: c')) - -instance EqT ((:=:) a) where - eqT Refl Refl = Just Refl diff --git a/type-equality.cabal b/type-equality.cabal --- a/type-equality.cabal +++ b/type-equality.cabal @@ -1,32 +1,45 @@ -Name: type-equality -Version: 0.1.2 -Synopsis: Type equality, coercion/cast and other operations. -Description: In the presence of GADTs, sometimes a proof is - needed that two types are equal. This package - contains an equality type for this purpose, plus its - properties (reflexive, symmetric, transitive) and - some useful operations (substitution, congruence, - coercion/cast). It also contains a type class for - producing equality proofs, providing some form of - decidable equality on types. -Category: Data -Cabal-Version: >= 1.6 -Author: Erik Hesselink, Martijn van Steenbergen -License: BSD3 -License-File: LICENSE -Maintainer: hesselink@gmail.com -Homepage: http://github.com/hesselink/type-equality/ -Stability: experimental -Build-Type: Simple -Tested-With: GHC == 7.0.4, GHC == 7.4.1, GHC == 7.6.1 -Extra-Source-Files: CHANGELOG +name: type-equality +version: 1 +stability: provisional +cabal-version: >=1.10 +build-type: Simple +author: Oleg Grenrus , Ryan Scott , Erik Hesselink , Martijn van Steenbergen +maintainer: Oleg Grenrus , Ryan Scott , Erik Hesselink +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). + . + @ + data a :~: b where + \ Refl :: a :~: a + @ + . + The module @Data.Type.Equality.Hetero@ shims @:~~:@ equality, for + compilers with @PolyKinds@ -Library - Build-Depends: base >= 3 && < 5 - HS-Source-Dirs: src - GHC-Options: -Wall - Exposed-Modules: Data.Type.Equality +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 -Source-Repository head - Type: git - Location: git://github.com/hesselink/type-equality.git + +source-repository head + type: git + location: git://github.com/hesselink/type-equality + +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