packages feed

type-eq (empty) → 0.1

raw patch · 9 files changed

+489/−0 lines, 9 filesdep +basedep +groupoidsdep +semigroupoidssetup-changed

Dependencies added: base, groupoids, semigroupoids

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright 2012 Gábor Lehel++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 AUTHORS ``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.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Type/Eq.hs view
@@ -0,0 +1,173 @@+{-# LANGUAGE GADTs, TypeFamilies, Rank2Types, TypeOperators, FlexibleInstances, FlexibleContexts, CPP #-}++#include "macros.h"++LANGUAGE_POLYKINDS+LANGUAGE_TRUSTWORTHY++{-# OPTIONS_GHC -fno-warn-unused-imports #-}++-- | Types and combinators for storing and manipulating type equality evidence.+-- +--   This module is kind-polymorphic if @PolyKinds@ are available (GHC 7.6+).+--+--   Notable combinators missing from this module include @applyEq@, @constructorEq@, and @sameOuterEq@.+-- +--   See also @"Type.Eq.Higher"@ and @"Type.Eq.Poly"@.++module Type.Eq where++import Control.Category         (Category(..))+import Control.Applicative      (Applicative) -- for haddock+#ifdef HAVE_DEPENDENCIES+--import Control.Category.Product (Tensor(..))+import Data.Groupoid            (Groupoid(..))+import Data.Semigroupoid        (Semigroupoid(..))+#endif+import Data.Typeable     hiding (cast)+import Type.Eq.Unsafe+import Prelude           hiding ((.))+import Unsafe.Coerce++-- * Full equality++-- | Evidence that type @a@ is the same as type @b@.+-- +--   The @'Functor'@, @'Applicative'@, and @'Monad'@ instances of @Maybe@+--   are extremely useful for working with values of type @Maybe (a :~: b)@.+data a :~: b where+    Eq :: (a ~ b) => a :~: b++-- deriving Typeable and PolyKinds don't play well+instance Typeable2 (:~:) where+    typeOf2 = const $ mkTyConApp tyCon []+        where tyCon = MK_TY_CON("Type.Eq",":~:")++-- | Unpack equality evidence and use it.+-- +--   This function compiles with GHC 6.10, but doesn't work. Beware!+withEq :: (a ~ b => r) -> (a :~: b) -> r+withEq x Eq = x+-- This doesn't seem to work in 6.10, so for compatibility, we're not going to use it++instance Category (:~:) where+    id  = idEq+    (.) = composeEq++#ifdef HAVE_DEPENDENCIES+instance Semigroupoid (:~:) where+    o = composeEq++instance Groupoid (:~:) where+    inv = flipEq+#endif++-- would require a dependency on data-lens+-- instance Tensor (:~:) where+--  a *** b = idEq2 ||$|| a |$| b++-- | Reflexivity+idEq :: a :~: a+idEq = Eq++-- | Transitivity+composeEq :: (b :~: c) -> (a :~: b) -> (a :~: c)+composeEq Eq Eq = Eq++-- | Symmetry+flipEq :: (a :~: b) -> (b :~: a)+flipEq Eq = Eq++-- | Type constructors are injective+argumentEq :: (f a :~: g b) -> (a :~: b)+argumentEq Eq = BUG_5591(Eq)++-- | Use equality evidence to cast between types+cast, (|>) :: a -> (a :~: b) -> b+cast a Eq = a+(|>) = cast++-- * Partial equality++-- | Evidence that @f@ is the outermost type constructor of @a@+data OuterEq f a where+    OuterEq :: f i ~ a => OuterEq f a++-- | Evidence that @i@ is the argument type of the outermost type constructor of @a@+data InnerEq i a where+    InnerEq :: f i ~ a => InnerEq i a++-- | Unpack partial equality evidence and use it.+--+--   This function compiles with GHC 6.10, but doesn't work. Beware!+withOuterEq :: (forall i. f i ~ a => r) -> OuterEq f a -> r+withOuterEq x OuterEq = x++-- | Unpack partial equality evidence and use it.+--+--   This function compiles with GHC 6.10, but doesn't work. Beware!+withInnerEq :: (forall f. f i ~ a => r) -> InnerEq i a -> r+withInnerEq x InnerEq = x++outerEq :: f i :~: a -> OuterEq f a+outerEq Eq = OuterEq++innerEq :: f i :~: a -> InnerEq i a+innerEq Eq = InnerEq++assembleEq :: OuterEq f a -> InnerEq i a -> f i :~: a+assembleEq OuterEq InnerEq = BUG_5591(Eq)++sameInnerEq :: InnerEq i a -> InnerEq j a -> i :~: j+sameInnerEq InnerEq InnerEq = BUG_5591(Eq)++-- * Testing for equality++DYNAMIC_EQ(,,:~:,a,b,)++-- | Can be implemented by types storing evidence of type equalities, i.e. GADTs.+-- +--   A return value of @Nothing@ can mean any of definite inequality, impossible arguments, or insufficient information.+--+--   Minimal complete definition: @maybeEq@ or @(~~)@, plus either:+-- +--       - @piecewiseMaybeEq@, or+-- +--       - both @maybeOuterEq@ and @maybeInnerEq@. or+-- +--       - @(\<~>)@, or+-- +--       - both @(~>)@ and @(<~)@.+class TypeEq t where+    maybeEq,          (~~)  :: t a     -> t b -> Maybe (a :~: b)+    maybeOuterEq,     (~>)  :: t (f i) -> t a -> Maybe (OuterEq f a)+    maybeInnerEq,     (<~)  :: t (f i) -> t a -> Maybe (InnerEq i a)+    piecewiseMaybeEq, (<~>) :: t (f i) -> t a -> (Maybe (OuterEq f a), Maybe (InnerEq i a))+    -- ^ > uncurry (liftA2 assembleEq) (a <~> b) = a ~~ b+    maybeEq = (~~)+    (~~)    = maybeEq+    maybeOuterEq     a b = fst (a <~> b)+    maybeInnerEq     a b = snd (a <~> b)+    piecewiseMaybeEq a b = (a ~> b, a <~ b)+    (~>)  = maybeOuterEq+    (<~)  = maybeInnerEq+    (<~>) = piecewiseMaybeEq++instance TypeEq ((:~:) a) where+    maybeEq      Eq Eq = Just Eq+    maybeOuterEq Eq Eq = Just OuterEq+    maybeInnerEq Eq Eq = Just InnerEq++instance TypeEq (InnerEq i) where+    maybeEq      _ _ = Nothing+    maybeOuterEq _ _ = Nothing+    maybeInnerEq InnerEq InnerEq = Just BUG_5591(InnerEq)++instance TypeEq (OuterEq f) where+    maybeEq      _ _ = Nothing+    maybeOuterEq OuterEq OuterEq = Just BUG_5591(OuterEq)+    maybeInnerEq _ _ = Nothing++-- TODO+-- fixities+-- other compilers
+ Type/Eq.hs-boot view
@@ -0,0 +1,11 @@+{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, CPP #-}++#include "macros.h"++LANGUAGE_POLYKINDS+LANGUAGE_TRUSTWORTHY++module Type.Eq where++data a :~: b where+    Eq :: (a ~ b) => a :~: b
+ Type/Eq/Higher.hs view
@@ -0,0 +1,127 @@+{-# LANGUAGE GADTs, TypeFamilies, Rank2Types, KindSignatures, TypeOperators, FlexibleContexts, CPP #-}++#include "macros.h"++LANGUAGE_TRUSTWORTHY++{-# OPTIONS_GHC -fno-warn-unused-imports #-}++-- |  Types and combinators for storing and manipulating evidence of equality between types of higher kind.+-- +--    Available up to @* -> * -> *@. Yell if you need more.++module Type.Eq.Higher (module Type.Eq, module Type.Eq.Higher) where++import Data.Typeable hiding (cast)+import Type.Eq+import Type.Eq.Higher.Unsafe+import Unsafe.Coerce++-- * Additional combinators, kind @*@++-- | Type constructors are generative+constructorEq :: f a :~: g b -> f ::~:: g+constructorEq Eq = BUG_5591(Eq1)++sameOuterEq :: OuterEq f a -> OuterEq g a -> f ::~:: g+sameOuterEq OuterEq OuterEq = BUG_5591(Eq1)+++-- * Full equality, kind @* -> *@++data (f :: * -> *) ::~:: (g :: * -> *) where+    Eq1 :: (f ~ g) => f ::~:: g++-- INSTANCE_TYPEABLE(1,::~::,f,g,"Type.Eq.Higher","::~::",())++withEq1 :: (f ~ g => r) -> (f ::~:: g) -> r+withEq1 x Eq1 = x++-- | Reflexivity+idEq1 :: f ::~:: f+idEq1 = Eq1++-- | Transitivity+composeEq1, (|.|) :: (g ::~:: h) -> (f ::~:: g) -> (f ::~:: h)+composeEq1 Eq1 Eq1 = Eq1+(|.|) = composeEq1++-- | Symmetry+flipEq1 :: (f ::~:: g) -> (g ::~:: f)+flipEq1 Eq1 = Eq1++-- | Congruence?+applyEq1, (|$|) :: f ::~:: g -> a :~: b -> f a :~: g b+applyEq1 Eq1 Eq = Eq+(|$|) = applyEq1++-- | Type constructors are generative+constructorEq1 :: m a ::~:: n b -> m :::~::: n+constructorEq1 Eq1 = BUG_5591(Eq2)++-- | Type constructors are injective+argumentEq1 :: m a ::~:: n b -> a :~: b+argumentEq1 Eq1 = BUG_5591(Eq)++DYNAMIC_EQ(1,1,::~::,f,g,())+++-- * Partial equality, kind @* -> *@++data OuterEq1 (m :: * -> * -> *) (f :: * -> *) where+    OuterEq1 :: m a ~ f => OuterEq1 m f++data InnerEq1 (a :: *) (f :: * -> *) where+    InnerEq1 :: m a ~ f => InnerEq1 a f++withOuterEq1 :: (forall a. m a ~ f => r) -> OuterEq1 m f -> r+withOuterEq1 a OuterEq1 = a++withInnerEq1 :: (forall m. m a ~ f => r) -> InnerEq1 a f -> r+withInnerEq1 a InnerEq1 = a++outerEq1 :: m a ::~:: f -> OuterEq1 m f+outerEq1 Eq1 = OuterEq1++innerEq1 :: m a ::~:: f -> InnerEq1 a f+innerEq1 Eq1 = InnerEq1++assembleEq1 :: OuterEq1 m f -> InnerEq1 a f -> m a ::~:: f+assembleEq1 OuterEq1 InnerEq1 = BUG_5591(Eq1)++sameOuterEq1 :: OuterEq1 m f -> OuterEq1 n f -> m :::~::: n+sameOuterEq1 OuterEq1 OuterEq1 = BUG_5591(Eq2)++sameInnerEq1 :: InnerEq1 a f -> InnerEq1 b f -> a :~: b+sameInnerEq1 InnerEq1 InnerEq1 = BUG_5591(Eq)+++-- * Full equality, kind @* -> * -> *@++data (m :: * -> * -> *) :::~::: (n :: * -> * -> *) where+    Eq2 :: (m ~ n) => m :::~::: n++-- INSTANCE_TYPEABLE(2,:::~:::,m,n,"Type.Eq.Higher",":::~:::",() ())++withEq2 :: (m ~ n => r) -> (m :::~::: n) -> r+withEq2 x Eq2 = x++-- | Reflexivity+idEq2 :: m :::~::: m+idEq2 = Eq2++-- | Transitivity+composeEq2, (||.||) :: (n :::~::: o) -> (m :::~::: n) -> (m :::~::: o)+composeEq2 Eq2 Eq2 = Eq2+(||.||) = composeEq2++-- | Symmetry+flipEq2 :: (m :::~::: n) -> (n :::~::: m)+flipEq2 Eq2 = Eq2++-- | Congruence?+applyEq2, (||$||) :: m :::~:::n -> a :~: b -> m a ::~:: n b+applyEq2 Eq2 Eq = Eq1+(||$||) = applyEq2++DYNAMIC_EQ(2,2,:::~:::,n,m,() ())
+ Type/Eq/Higher.hs-boot view
@@ -0,0 +1,13 @@+{-# LANGUAGE GADTs, TypeFamilies, KindSignatures, TypeOperators, CPP #-}++#include "macros.h"++LANGUAGE_TRUSTWORTHY++module Type.Eq.Higher where++data (f :: * -> *) ::~:: (g :: * -> *) where+    Eq1 :: (f ~ g) => f ::~:: g++data (m :: * -> * -> *) :::~::: (n :: * -> * -> *) where+    Eq2 :: (m ~ n) => m :::~::: n
+ Type/Eq/Higher/Unsafe.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE TypeOperators, CPP #-}++#include "macros.h"++LANGUAGE_UNSAFE++module Type.Eq.Higher.Unsafe (module Type.Eq.Unsafe, module Type.Eq.Higher.Unsafe) where++import Type.Eq.Unsafe+import {-# SOURCE #-} Type.Eq.Higher+import Unsafe.Coerce++-- | Very unsafe! The same rules apply as for 'unsafeCoerce'.+unsafeCoercion1 :: f ::~:: g+unsafeCoercion1 = unsafeCoerce Eq1++-- | Very unsafe! The same rules apply as for 'unsafeCoerce'.+unsafeCoercion2 :: m :::~::: n+unsafeCoercion2 = unsafeCoerce Eq2
+ Type/Eq/Unsafe.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE TypeOperators, CPP #-}++#include "macros.h"++LANGUAGE_POLYKINDS+LANGUAGE_UNSAFE++-- | This module is kind-polymorphic if @PolyKinds@ are available (GHC 7.6+).++module Type.Eq.Unsafe where++import {-# SOURCE #-} Type.Eq+import Unsafe.Coerce++-- | Very unsafe! The same rules apply as for 'unsafeCoerce'.+unsafeCoercion :: a :~: b+unsafeCoercion = unsafeCoerce Eq
+ type-eq.cabal view
@@ -0,0 +1,97 @@+name:          type-eq+category:      Type System+version:       0.1+author:        Gábor Lehel+maintainer:    Gábor Lehel <illissius@gmail.com>+homepage:      http://github.com/glehel/type-eq+copyright:     Copyright (C) 2012 Gábor Lehel+license:       BSD3+license-file:  LICENSE+stability:     experimental+cabal-version: >= 1.10+build-type:    Simple+synopsis:      Type equality evidence you can carry around+description:+    This package provides types and combinators to store and manipulate evidence of equality between types.+    .+    To take advantage of kind-polymorphism when it is available but not require it, this it is split into the following primary modules:+    .+        - @/Type.Eq/@: Types and combinators which can be kind-polymorphic if @PolyKinds@ are available, but are specific to kind @*@ otherwise.+    .+        - @/Type.Eq.Higher/@: Kind-monomorphic types and combinators of higher kind, up to @* -> * -> *@.+    .+        - @/Type.Eq.Poly/@: Combinators that require kind-polymorphism. This module is only available if @PolyKinds@ are available.+    .+    Support for kind-polymorphism first appeared with GHC 7.4, but because it is too buggy to be practical, it will only be enabled with GHC 7.6.+    .+    Major required extensions: @GADTs@, @TypeFamilies@ (for @~@), @Rank2Types@, @TypeOperators@+    .+    Optional extensions: @PolyKinds@ (GHC 7.6+)+    .+    Minimum GHC: 6.10+    .+    Related packages:+    .+        - <http://hackage.haskell.org/package/type-equality>+    .+        - <http://hackage.haskell.org/package/eq>+    .+        - <http://hackage.haskell.org/package/ty>+    .+        - <http://hackage.haskell.org/package/dependent-sum>+    .+        - <http://hackage.haskell.org/package/categories> (@Data.Category.Discrete@)++source-repository head+    type:      git+    location:  git://github.com/glehel/type-eq.git++library+    default-language:+        Haskell98++    other-extensions:+        CPP+        GADTs+        Rank2Types+        TypeFamilies+        TypeOperators+        KindSignatures+        FlexibleContexts++    build-depends:+        base >= 3.0 && < 4.6++    exposed-modules:+        Type.Eq+        Type.Eq.Unsafe+        Type.Eq.Higher+        Type.Eq.Higher.Unsafe++-- DeriveDataTypeable and PolyKinds sadly don't mix+--    if impl(ghc)+--        cpp-options: -DHAVE_TYPEABLE+--        other-extensions: DeriveDataTypeable++-- Ran into dependency problems with 6.10 and 6.12 and didn't feel like dealing with it+    if impl(ghc >= 7.0)+        cpp-options: -DHAVE_DEPENDENCIES+        build-depends:+-- Semigroupoid+            semigroupoids >= 1.0 && < 1.4,+-- Groupoid+            groupoids     >= 0.1 && < 0.3+-- Tensor+--            data-lens     >= 2.9 && < 2.11++    if impl(ghc >= 7.2)+        other-extensions: Trustworthy++--    if impl(ghc >= 7.6)+--        exposed-modules:  Type.Eq.Poly+--        other-extensions: PolyKinds, Unsafe++    include-dirs: .++    ghc-options:+        -Wall