packages feed

type-eq 0.1.2 → 0.2

raw patch · 8 files changed

+129/−23 lines, 8 filesdep ~basedep ~groupoidsdep ~semigroupoids

Dependency ranges changed: base, groupoids, semigroupoids

Files

Type/Eq.hs view
@@ -34,7 +34,7 @@ -- | 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)@.+--   are very useful for working with values of type @Maybe (a :~: b)@. data a :~: b where     Eq :: (a ~ b) => a :~: b @@ -45,7 +45,7 @@  -- | Unpack equality evidence and use it. -- ---   This function compiles with GHC 6.10, but doesn't work. Beware!+--   This function compiles with GHC 6.10, but doesn't work. 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@@ -99,13 +99,13 @@  -- | Unpack partial equality evidence and use it. -----   This function compiles with GHC 6.10, but doesn't work. Beware!+--   This function compiles with GHC 6.10, but doesn't work. 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!+--   This function compiles with GHC 6.10, but doesn't work. withInnerEq :: (forall f. f i ~ a => r) -> InnerEq i a -> r withInnerEq x InnerEq = x @@ -138,7 +138,9 @@ --       - @(\<~>)@, or --  --       - both @(~>)@ and @(<~)@.-class TypeEq t where+-- +--   Due to <http://hackage.haskell.org/trac/ghc/ticket/5591> you may have to use 'unsafeOuterEq' and/or 'unsafeInnerEq' to define some of these.+class TypeCompare 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)@@ -153,21 +155,17 @@     (<~)  = maybeInnerEq     (<~>) = piecewiseMaybeEq -instance TypeEq ((:~:) a) where+instance TypeCompare ((:~:) a) where     maybeEq      Eq Eq = Just Eq     maybeOuterEq Eq Eq = Just OuterEq     maybeInnerEq Eq Eq = Just InnerEq -instance TypeEq (InnerEq i) where+instance TypeCompare (InnerEq i) where     maybeEq      _ _ = Nothing     maybeOuterEq _ _ = Nothing     maybeInnerEq InnerEq InnerEq = Just BUG_5591(InnerEq) -instance TypeEq (OuterEq f) where+instance TypeCompare (OuterEq f) where     maybeEq      _ _ = Nothing     maybeOuterEq OuterEq OuterEq = Just BUG_5591(OuterEq)     maybeInnerEq _ _ = Nothing---- TODO--- fixities--- other compilers
Type/Eq.hs-boot view
@@ -9,3 +9,9 @@  data a :~: b where     Eq :: (a ~ b) => a :~: b++data OuterEq f a where+    OuterEq :: f i ~ a => OuterEq f a++data InnerEq i a where+    InnerEq :: f i ~ a => InnerEq i a
Type/Eq/Higher.hs-boot view
@@ -11,3 +11,9 @@  data (m :: * -> * -> *) :::~::: (n :: * -> * -> *) where     Eq2 :: (m ~ n) => m :::~::: n++data OuterEq1 (m :: * -> * -> *) (f :: * -> *) where+    OuterEq1 :: m a ~ f => OuterEq1 m f++data InnerEq1 (a :: *) (f :: * -> *) where+    InnerEq1 :: m a ~ f => InnerEq1 a f
Type/Eq/Higher/Unsafe.hs view
@@ -17,3 +17,11 @@ -- | Very unsafe! The same rules apply as for 'unsafeCoerce'. unsafeCoercion2 :: m :::~::: n unsafeCoercion2 = unsafeCoerce Eq2++-- | Very unsafe!+unsafeOuterEq1 :: OuterEq1 m f+unsafeOuterEq1 = unsafeCoerce OuterEq1++-- | Very unsafe!+unsafeInnerEq1 :: InnerEq1 a f+unsafeInnerEq1 = unsafeCoerce InnerEq1
+ Type/Eq/Poly.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE GADTs, TypeOperators, PolyKinds, RankNTypes, CPP #-}++#include "macros.h"++LANGUAGE_TRUSTWORTHY++{-# OPTIONS_GHC -fno-warn-unused-imports -fno-warn-orphans #-}++-- | Kind-polymorphic combinators for manipulating type equality evidence.+-- +--   This module is available only if @PolyKinds@ are available (GHC 7.6+).++module Type.Eq.Poly (module Type.Eq, module Type.Eq.Poly) where++import Control.Applicative ((<$>))+import Control.Category ((.)) -- for haddock+import Data.Typeable hiding (cast)+import Type.Eq+import Type.Eq.Higher ((::~::)(..), (:::~:::)(..), OuterEq1(..), InnerEq1(..))+import Type.Eq.Unsafe+import Prelude hiding ((.))+import Unsafe.Coerce++{-+INSTANCE_TYPEABLE(1,:~:,f,g,"Type.Eq",":~:",())+INSTANCE_TYPEABLE(2,:~:,m,n,"Type.Eq",":~:",() ())+INSTANCE_TYPEABLE(3,:~:,x,y,"Type.Eq",":~:",() () ())+INSTANCE_TYPEABLE(4,:~:,x,y,"Type.Eq",":~:",() () () ())+INSTANCE_TYPEABLE(5,:~:,x,y,"Type.Eq",":~:",() () () () ())+INSTANCE_TYPEABLE(6,:~:,x,y,"Type.Eq",":~:",() () () () () ())+INSTANCE_TYPEABLE(7,:~:,x,y,"Type.Eq",":~:",() () () () () () ())+-}++-- | Synonym for @'composeEq'@. Kind-polymorphic, unlike @('.')@.+(|.|) :: b :~: c -> a :~: b -> a :~: c+(|.|) = composeEq++-- | Congruence?+applyEq, (|$|) :: f :~: g -> a :~: b -> f a :~: g b+applyEq = withEq (withEq Eq)+(|$|) = applyEq++-- | Type constructors are generative+constructorEq :: f a :~: g b -> f :~: g+constructorEq = withEq BUG_5591(Eq)++DYNAMIC_EQ(1,,:~:,f,g,())+DYNAMIC_EQ(2,,:~:,n,m,() ())+DYNAMIC_EQ(3,,:~:,x,y,() () ())+DYNAMIC_EQ(4,,:~:,x,y,() () () ())+DYNAMIC_EQ(5,,:~:,x,y,() () () () ())+DYNAMIC_EQ(6,,:~:,x,y,() () () () () ())+DYNAMIC_EQ(7,,:~:,x,y,() () () () () () ())++sameOuterEq :: OuterEq f a -> OuterEq g a -> f :~: g+sameOuterEq OuterEq OuterEq = BUG_5591(Eq)++-- * Compatibility with Type.Eq.Higher++fromEq1 :: f ::~:: g -> f :~: g+fromEq1 Eq1 = Eq++toEq1 :: f :~: g -> f ::~:: g+toEq1 Eq = Eq1++fromEq2 :: n :::~::: m -> n :~: m+fromEq2 Eq2 = Eq++toEq2 :: n :~: m -> n :::~::: m+toEq2 Eq = Eq2++fromOuterEq1 :: OuterEq1 m f -> OuterEq m f+fromOuterEq1 OuterEq1 = BUG_5591(OuterEq)++toOuterEq1 :: OuterEq m f -> OuterEq1 m f+toOuterEq1 OuterEq = OuterEq1++fromInnerEq1 :: InnerEq1 a f -> InnerEq a f+fromInnerEq1 InnerEq1 = BUG_5591(InnerEq)++toInnerEq1 :: InnerEq a f -> InnerEq1 a f+toInnerEq1 InnerEq = InnerEq1
Type/Eq/Unsafe.hs view
@@ -15,3 +15,11 @@ -- | Very unsafe! The same rules apply as for 'unsafeCoerce'. unsafeCoercion :: a :~: b unsafeCoercion = unsafeCoerce Eq++-- | Very unsafe!+unsafeOuterEq :: OuterEq f a+unsafeOuterEq = unsafeCoerce OuterEq++-- | Very unsafe!+unsafeInnerEq :: InnerEq i a+unsafeInnerEq = unsafeCoerce InnerEq
macros.h view
@@ -38,7 +38,7 @@ #endif  -- http://hackage.haskell.org/trac/ghc/ticket/5591-#if (__GLASGOW_HASKELL__ >= 702) && (__GLASGOW_HASKELL__ <= 704)+#if (__GLASGOW_HASKELL__ >= 702) && (__GLASGOW_HASKELL__ <= 706) #   define BUG_5591(X) (unsafeCoerce X) #else #   define BUG_5591(X) X
type-eq.cabal view
@@ -1,6 +1,6 @@ name:          type-eq category:      Type System-version:       0.1.2+version:       0.2 author:        Gábor Lehel maintainer:    Gábor Lehel <illissius@gmail.com> homepage:      http://github.com/glehel/type-eq@@ -14,15 +14,13 @@ 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, it is split into the following primary modules:+    To take advantage of kind polymorphism when it is available but not require it, 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.+        - @/Type.Eq.Poly/@: Combinators that require kind polymorphism. This module is only available if @PolyKinds@ are available.     .     Major required extensions: @GADTs@, @TypeFamilies@ (for @~@), @Rank2Types@, @TypeOperators@     .@@ -62,7 +60,7 @@         FlexibleContexts      build-depends:-        base >= 3.0 && < 4.6+        base >= 3.0 && < 4.7      exposed-modules:         Type.Eq@@ -80,17 +78,17 @@         cpp-options: -DHAVE_DEPENDENCIES         build-depends: -- Semigroupoid-            semigroupoids >= 1.0 && < 1.4,+            semigroupoids >= 1.0 && < 3.1, -- Groupoid-            groupoids     >= 0.1 && < 0.3+            groupoids     >= 0.1 && < 3.1 -- 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+    if impl(ghc >= 7.6)+        exposed-modules:  Type.Eq.Poly --        other-extensions: PolyKinds, Unsafe      include-dirs: .