packages feed

type-equality 0.1.2 → 1

raw patch · 8 files changed

+369/−198 lines, 8 filesdep ~basesetup-changednew-uploader

Dependency ranges changed: base

Files

− 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,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.
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,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
+ src-old/Data/Type/Equality.hs view
@@ -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
− 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,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 <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).+  .+  @+  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