type-equality (empty) → 0.1.0

raw patch · 4 files changed

+162/−0 lines, 4 filesdep +basesetup-changed

Dependencies added: base

Files

LICENSE +28/−0
Setup.lhs +5/−0
src/Data/Type/Equality.hs +103/−0
type-equality.cabal +26/−0

+ LICENSE view

@@ -0,0 +1,28 @@+Copyright (c) Erik Hesselink 2009++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.++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.+

+ Setup.lhs view

@@ -0,0 +1,5 @@+#! /usr/bin/env runhaskell++>import Distribution.Simple+>main = defaultMain+

+ src/Data/Type/Equality.hs view

@@ -0,0 +1,103 @@+{-# LANGUAGE TypeOperators+           , GADTs+           , CPP+           #-}+-------------------------------------------------------------------------------+-- |+-- 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+  +  , 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 :=:++#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++-- | 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

@@ -0,0 +1,26 @@+Name:             type-equality+Version:          0.1.0+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.2.1+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+Build-Depends:    base >= 3 && < 5+Tested-With:      GHC == 6.8.2, GHC == 6.10.3++HS-Source-Dirs:   src+GHC-Options:      -Wall+Exposed-Modules:  Data.Type.Equality