type-equality 0.1.2 → 1.0.1
raw patch · 7 files changed
Files
- CHANGELOG +0/−17
- CHANGELOG.md +24/−0
- LICENSE +24/−22
- Setup.lhs +0/−5
- src-hetero/Data/Type/Equality/Hetero.hs +7/−0
- src/Data/Type/Equality.hs +0/−124
- type-equality.cabal +48/−30
− CHANGELOG
@@ -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.
+ CHANGELOG.md view
@@ -0,0 +1,24 @@+## 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.++## 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.
LICENSE view
@@ -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.
− Setup.lhs
@@ -1,5 +0,0 @@-#! /usr/bin/env runhaskell-->import Distribution.Simple->main = defaultMain-
+ src-hetero/Data/Type/Equality/Hetero.hs view
@@ -0,0 +1,7 @@+{-# LANGUAGE TypeOperators #-}+-- | This module shims kind heterogeneous propositional equality.+module Data.Type.Equality.Hetero (+ (:~~:)(..),+) where++import Data.Type.Equality ((:~~:)(..))
− src/Data/Type/Equality.hs
@@ -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 <hesselink@gmail.com>--- 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
type-equality.cabal view
@@ -1,32 +1,50 @@-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.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 -Library- Build-Depends: base >= 3 && < 5- HS-Source-Dirs: src- GHC-Options: -Wall- Exposed-Modules: Data.Type.Equality+maintainer:+ Oleg Grenrus <oleg.grenrus@iki.fi>, Ryan Scott <ryan.gl.scott@gmail.com>, Erik Hesselink <hesselink@gmail.com> -Source-Repository head- Type: git- Location: git://github.com/hesselink/type-equality.git+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@++extra-source-files: CHANGELOG.md+tested-with:+ 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+ location: git://github.com/hesselink/type-equality++library+ default-language: Haskell2010+ build-depends: base >=4.12 && <4.21+ hs-source-dirs: src-hetero+ exposed-modules: Data.Type.Equality.Hetero+ other-extensions: PolyKinds