type-settheory 0.1.3 → 0.1.3.1

raw patch · 4 files changed

+20/−11 lines, 4 filesdep +transformersdep −mtl

Dependencies added: transformers

Dependencies removed: mtl

Files

• Helper.hs +10/−3
• Type/Function.hs +1/−0
• Type/Logic.hs +6/−5
• type-settheory.cabal +3/−3

@@ -1,5 +1,6 @@ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE CPP #-} {-# OPTIONS -fno-warn-overlapping-patterns #-} module Helper where     @@ -13,7 +14,15 @@                                        (x,y) -> (cxt++x,y) decomposeForallT t = ([],t) +#if __GLASGOW_HASKELL__ >= 700+classI_dec (ClassI x _ ) = x +#else+classI_dec (ClassI x ) = x +#endif+classI_dec info = error ("expected ClassI, got "++show info)+                          + lemma :: Name -> Name -> Q [Dec] lemma cls prf = do         prfInfo <- reify prf@@ -24,9 +33,7 @@                     _ -> error ("expected ValI, got "++show prfInfo)          info <- reify cls-        let methodId = case info of-                         ClassI (ClassD _ _ _ _ [SigD x _]) -> x-                         _ -> error ("expected ClassI, got "++show info)+        let methodId = (\(ClassD _ _ _ _ [SigD x _]) -> x) (classI_dec info)                                           (cxt,bodyT) = decomposeForallT typ 

@@ -174,6 +174,7 @@ domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2 domUniq f f' = SetEq (domUniq0 f f') (domUniq0 f' f)     where+      domUniq0 :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :⊆: dom2       domUniq0 f f' = Subset (\a -> case total f a of                                      ExSnd fa -> inDom f' fa)                                                   

@@ -36,11 +36,12 @@ -- module Type.Logic where     +import Control.Exception+import Control.Monad.Trans.Cont+import Data.Functor.Identity+import Data.Monoid hiding(All) import Data.Type.Equality-import Control.Monad.Cont import Data.Typeable-import Data.Monoid hiding(All)-import Control.Exception       -- class Prop p where@@ -238,10 +239,10 @@ type COr r a b = Cont r (Either a b)  lem :: COr r (a -> r) a-lem = Cont (\k -> k (Left (\a -> k (Right a))))+lem = ContT (\k -> k (Left (\a -> (runIdentity . k . Right) a)))  elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r-elimCor (Cont x) k1 k2 = x (either k1 k2) +elimCor (ContT x) k1 k2 = (runIdentity . x) (Identity . either k1 k2)                           

@@ -1,5 +1,5 @@ name:                type-settheory-version:             0.1.3+version:             0.1.3.1 synopsis:              Sets and functions-as-relations in the type system description:         @@ -15,7 +15,7 @@  .  The proposition-types (derived from the ':=:' equality type) aren't meaningful purely by convention; they relate to the rest of Haskell as follows: A proof of @A :=: B@ gives us a safe coercion operator @A -> B@ (while the logic is inevitably inconsistent /at compile-time/ since 'undefined' proves anything, I think that we still have the property that if the 'Refl' value is successfully pattern-matched, then the two parameters in its type are actually equal).   -category:            Math, Language+category:            Math,Language,Type System license:             BSD3 license-file:        LICENSE author:              Daniel Schüssler@@ -33,7 +33,7 @@                      , syb                      , type-equality                      , template-haskell-                     , mtl+                     , transformers                      , containers  exposed-modules:    Type.Logic                      Type.Set