packages feed

type-settheory 0.1.1 → 0.1.2

raw patch · 8 files changed

+133/−91 lines, 8 files

Files

Data/Category.hs view
@@ -35,60 +35,109 @@ import Type.Logic import Data.Type.Equality import Control.Monad+import Control.Category+import Prelude hiding(id,(.))       -- | Category with type-level set of objects and type-level /hom/ function, but value-level composition and value-level definition of identity functions. data Cat ob hom =     Cat {       homIsFun :: ((ob :×: ob) :~>: Univ) hom-    , getId :: forall a aa. ((a,a), aa) :∈: hom -> aa+    , getid :: forall a. a :∈: ob -> ExId hom a     -- | Composition-    , cc :: forall a b c bc ab ac. +    , getc :: forall a b c. +           a :∈: ob ->+           b :∈: ob ->+           c :∈: ob ->+           ExC hom a b c+    }+                +-- | Existential wrapping of the identity function on a+data ExId hom a where+    ExId :: ((a,a),aa) :∈: hom -> aa -> ExId hom a+           +-- | Existential wrapping of the composition for types a,b,c+data ExC hom a b c where+    ExC ::            ((b,c), bc) :∈: hom ->            ((a,b), ab) :∈: hom ->            ((a,c), ac) :∈: hom ->+               +           (bc -> ab -> ac) -> -               bc -> ab -> ac-    }+           ExC hom a b c+                  hask :: Cat Univ HaskFun hask = Cat (extendCod haskFunIsFun auto)-       (\HaskFun -> id)-       (\HaskFun HaskFun HaskFun -> (.))+       (\_ -> ExId HaskFun id)+       (\_ _ _ -> ExC HaskFun HaskFun HaskFun (.))         kleisli :: Monad m => Cat Univ (KleisliHom m) kleisli = Cat (extendCod kleisliHomIsFun auto)-          (\KleisliHom -> return)-          (\KleisliHom KleisliHom KleisliHom -> (<=<))+          (\_ -> ExId KleisliHom return)+          (\_ _ _ -> ExC KleisliHom KleisliHom KleisliHom (<=<))+           -idEx :: Cat ob hom -> ob a -> (forall aa. ((a,a),aa) :∈: hom -> aa -> r) -> r-idEx cat a k = case total (homIsFun cat) (a :×: a) of-                 ExSnd faa -> k faa (getId cat faa)+fromControlCategory :: (Category hom) => Cat Univ (BiGraph hom)+fromControlCategory = Cat biGraphIsFun+                      (\_ -> ExId BiGraph id)+                      (\_ _ _ -> ExC BiGraph BiGraph BiGraph (.))++          +-- | Lemma for constructing categories; abstracts the usage of the hom function's 'total'+makeCat :: ((ob :×: ob) :~>: Univ) hom ->  +          (forall a aa. ((a,a),aa) :∈: hom -> aa) ->+              +          (forall a b c bc ab ac.+           ((b,c), bc) :∈: hom ->+           ((a,b), ab) :∈: hom ->+           ((a,c), ac) :∈: hom ->+               +           (bc -> ab -> ac)) ->+++          Cat ob hom++makeCat hom k1 k2 =+    Cat hom +     (\a -> case total hom (a :×: a) of+             ExSnd aa -> ExId aa (k1 aa))+     (\a b c -> case ( total hom (b :×: c)+                    , total hom (a :×: b)+                    , total hom (a :×: c) ) of+                      +                      ( ExSnd bc+                       ,ExSnd ab+                       ,ExSnd ac ) ->  ++                           ExC bc ab ac (k2 bc ab ac) )++               +                                                                -- idAuto :: forall ob hom a aa. Fact (((a, a), aa) :∈: hom) => Cat ob hom -> aa--- -- idAuto cat _ = idn cat auto--- idAuto cat _ = case total (homIsFun cat)  -idAuto :: forall a aa hom ob. (Fact (((a, a), aa) :∈: hom)) => Cat ob hom -> aa-idAuto cat = getId cat (auto :: ((a,a),aa) :∈: hom)-             --- ccAuto :: forall a b c bc ab ac hom ob.---      (Fact (((b, c), bc) :∈: hom),---       Fact (((a, b), ab) :∈: hom),---       Fact (((a, c), ac) :∈: hom)) =>+idauto :: (Fact (a :∈: ob)) => Cat ob hom -> ExId hom a+idauto cat = getid cat auto+ --      Cat ob hom -> bc -> ab -> ac-ccAuto cat = cc cat auto auto auto -test :: a -> a-test = idAuto hask +cauto :: (Fact (a :∈: ob), Fact (b :∈: ob), Fact (c :∈: ob)) =>+     Cat ob hom -> ExC hom a b c+cauto cat = getc cat auto auto auto -test2 :: (b -> c) -> (a -> b) -> a -> c-test2 = ccAuto hask+-- test :: a -> a+-- test = idAuto hask+++-- test2 :: (b -> c) -> (a -> b) -> a -> c+-- test2 = ccAuto hask          -test3 :: forall m a. Monad m => a -> m a-test3 = idAuto kleisli+-- test3 :: forall m a. Monad m => a -> m a+-- test3 = idAuto kleisli        -- foo :: forall a. a -> a -- foo = idEx hask (Univ :: Univ a) go@@ -97,4 +146,39 @@ --          go HaskFun x = x         --- data Functor omap+data GFunctor ob1 hom1 ob2 hom2 f = +    GFunctor {+      omapIsFun :: (ob1 :~>: ob2) f+    , getfmap :: forall a b.+              a :∈: ob1 ->+              b :∈: ob1 ->+              +              ExFmap hom1 hom2 f a b+                  +    }++data ExFmap hom1 hom2 f a b where+    ExFmap ::+              (a,fa) :∈: f ->+              (b,fb) :∈: f ->+              ((a,b),ab) :∈: hom1 ->+              ((fa,fb),fafb) :∈: hom2 ->++              (ab -> fafb) ->++                  ExFmap hom1 hom2 f a b++fromFunctor :: (Functor f) => GFunctor Univ HaskFun Univ HaskFun (Graph f)+fromFunctor = GFunctor graphIsFun (\_ _ -> ExFmap Graph Graph HaskFun HaskFun fmap)+++                                  +-- gmapCPS f afa bfb abab fafbfafb k+--         = case ( total (homIsFun cat) (b :×: c)+--                , total (homIsFun cat) (a :×: b)+--                , total (homIsFun cat) (a :×: c) ) of+                      +--                       ( ExSnd bc+--                        ,ExSnd ab+--                        ,ExSnd ac ) ->  k bc ab ac (cc cat bc ab ac) +
+ Defs.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE CPP #-}+{-# OPTIONS -DMODULE #-} -- works because Pragmas are parsed only /before/ CPP has kicked in++#ifdef MODULE+module Defs where+#endif++#define PROP *+#define SET (* -> PROP)+#define SET1 (SET -> PROP)+#define SET2 (SET1 -> PROP)+#define SET3 (SET2 -> PROP)++
Type/Dummies.hs view
@@ -27,7 +27,7 @@  module Type.Dummies where     -#include "defs.h.hs"+#include "../Defs.hs"           -- | \"Kind-cast\" @ SET @ to @*@ data Lower (a :: SET)
Type/Function.hs view
@@ -47,7 +47,7 @@       -#include "defs.h.hs"+#include "../Defs.hs"       -- * Preliminary
Type/Nat.hs view
@@ -46,7 +46,7 @@ import Control.Monad() import Control.Exception -#include "defs.h.hs"+#include "../Defs.hs"           -- | Sets equipped with a constant and a function to itself data NStructure set z succ where
Type/Set.hs view
@@ -74,7 +74,8 @@   -#include "defs.h.hs"++#include "../Defs.hs"
− Type/defs.h.hs 
@@ -1,56 +0,0 @@--------------------------------------------------------------------------------------------------------------------------------------------------------------------- |---Module       : ---Author       : ---License      : ---Copyright    : ------Maintainer   : ---Stability    : ---Portability  : ---------------------------------------------------------------------------------------Description  : ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |---Module       : ---Author       : ---License      : ---Copyright    : ------Maintainer   : ---Stability    : ---Portability  : ---------------------------------------------------------------------------------------Description  : ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |---Module       : ---Author       : ---License      : ---Copyright    : ------Maintainer   : ---Stability    : ---Portability  : ---------------------------------------------------------------------------------------Description  : --------------------------------------------------------------------------------------------------------------------------------------------------------------------#define PROP *-#define SET (* -> PROP)-#define SET1 (SET -> PROP)-#define SET2 (SET1 -> PROP)-#define SET3 (SET2 -> PROP)
type-settheory.cabal view
@@ -1,5 +1,5 @@ name:                type-settheory-version:             0.1.1+version:             0.1.2 synopsis:              Type-level sets and functions expressed as types description:         @@ -20,7 +20,6 @@ maintainer:          daniels@community.haskell.org build-type:          Simple cabal-version:       >= 1.6-extra-source-files:  Type/defs.h.hs stability:           Alpha  source-repository head@@ -43,5 +42,5 @@                      Data.Category                      Data.Typeable.Extras                      Control.SMonad- other-modules:       Helper+ other-modules:       Helper, Defs  ghc-options: