packages feed

extended-categories (empty) → 0.1.0

raw patch · 11 files changed

+345/−0 lines, 11 filesdep +basedep +constraintsdep +ghc-primsetup-changed

Dependencies added: base, constraints, ghc-prim, tagged

Files

+ Category.hs view
@@ -0,0 +1,32 @@+module Category where++import qualified Prelude as P+import GHC.Prim+import Data.Constraint++-- |The class of categories @m@ with objects of kind @k@ which satisfy the+-- constraint @Object m@. For any objects @a@ and @b@, the type @m a b@ is the+-- type of morphisms with domain @a@ and codomain @b@.+class Category (m :: k -> k -> *) where+    -- |The set of objects.+    type Object m (a :: k) :: Constraint+    -- |The Identity operator.+    id :: Object m a => m a a+    -- |The Composition operator.+    (.) :: m b c -> m a b -> m a c+    -- |Morphisms are arrows between objects.+    observeObjects :: m a b -> Dict (Object m a, Object m b)++-- |The category Hask of functions between types.+instance Category (->) where+    type Object (->) a = ()+    id = P.id+    observeObjects = P.const Dict+    (.) = (P..)++-- |The category of entailment from 'constraints'+instance Category (:-) where+    type Object (:-) a = ()+    id = refl+    observeObjects = P.const Dict+    (.) = trans
+ Category/Product.hs view
@@ -0,0 +1,29 @@+module Category.Product where++import Data.Constraint+import Data.Proxy+import Data.Tagged++import Category+import Functor++data (c1 :><: c2) a b where+    (:><:) :: (a ~ '(L a, R a), b ~ '(L b, R b))  => c1 (L a) (L b) -> c2 (R a) (R b) -> (c1 :><: c2) a b++type family L t where L '(a, b) = a+type family R t where R '(a, b) = b++instance (Category c1, Category c2) => Category (c1 :><: c2) where+    type Object (c1 :><: c2) a = (Object c1 (L a), Object c2 (R a), a ~ '(L a, R a))+    id = id :><: id+    observeObjects (f :><: g)+        | Dict <- observeObjects f, Dict <- observeObjects g = Dict+    (f1 :><: f2) . (g1 :><: g2) = (f1 . g1) :><: (f2 . g2)++data Diag c where Diag :: Category c => Diag c++instance Category c => Functor (Diag (c :: k -> k -> *)) ('KProxy :: KProxy (k -> (k, k))) where+    type Domain (Diag c) = c+    type Codomain (Diag c) = c :><: c+    type FMap (Diag c) (a :: k) = '(a, a)+    morphMap = Tagged (\f -> f :><: f)
+ Functor.hs view
@@ -0,0 +1,62 @@+module Functor where++import qualified Prelude as P+import Data.Constraint+import Data.Proxy+import Data.Tagged++import Category++-- |The class of functors @f@ from @Domain f@ to @Codomain f@. Rather than+-- indexing functors on the type of their object mapping, Functor is indexed on+-- the phantom type variable @f@. This allows the object mapping to be any type+-- family @FMap f@, and for multiple functors to exist between categories. As a+-- consequence, a proxy @k@ for the  kind of @FMap f@ must be given as a second+-- parameter to Functor.+class (Category (Domain f :: o1 -> o1 -> *), Category (Codomain f :: o2 -> o2 -> *)) => Functor (f :: *) (k :: KProxy (o1 -> o2)) | f -> k where+    -- |The mapping of objects of @Domain f@ to objects of @Codomain f@.+    type FMap f (a :: o1) :: o2+    -- |The domain of @f@.+    type Domain f :: o1 -> o1 -> *+    -- |The codomain of @f@.+    type Codomain f :: o2 -> o2 -> *+    -- |The mapping of morphisms of @Domain f@ to morphisms of @Codomain f@, tagged on the type @f@.+    morphMap :: Tagged f (Domain f (a :: o1) (b :: o1) -> Codomain f (FMap f a :: o2) (FMap f b :: o2))++-- |Proof that functors map objects to objects. Defines a functor from Cat to (:-).+objectMap :: forall f (a :: o1). Functor f ('KProxy :: KProxy (o1 -> o2)) => Tagged '(f, a) (Object (Domain f) a :- Object (Codomain f) (FMap f a :: o2))+objectMap = Tagged (Sub (case observeObjects (proxy morphMap (Proxy :: Proxy f) (id :: Domain f a a)) of Dict -> Dict))++fmap :: forall f (a :: o1) (b :: o1). Functor f ('KProxy :: KProxy (o1 -> o2)) => f -> Domain f a b -> Codomain f (FMap f a :: o2) (FMap f b :: o2)+fmap _ = proxy morphMap (Proxy :: Proxy f)++-- |The composition of functors. The type variable @k@ is a proxy for the kind of the objects of the codomain of @g@.+data Comp (k :: KProxy o2) (f :: *) (g :: *) where+    (:.:) :: (Functor f ('KProxy :: KProxy (o2 -> o3)), Functor g ('KProxy :: KProxy (o1 -> o2)), (Domain f :: o2 -> o2 -> *) ~ Codomain g) =>+        f -> g -> Comp ('KProxy :: KProxy o2) f g++instance (Functor f ('KProxy :: KProxy (o2 -> o3)), Functor g ('KProxy :: KProxy (o1 -> o2)), (Domain f :: o2 -> o2 -> *) ~ Codomain g)+        => Functor (Comp ('KProxy :: KProxy o2) f g) ('KProxy :: KProxy (o1 -> o3)) where+    type FMap (Comp ('KProxy :: KProxy o2) f g) a = FMap f (FMap g a :: o2)+    type Domain (Comp 'KProxy f g) = Domain g+    type Codomain (Comp 'KProxy f g) = Codomain f+    morphMap = Tagged (proxy morphMap (Proxy :: Proxy f) . proxy morphMap (Proxy :: Proxy g))++-- |The identity functor.+data IdentityF c where IdentityF :: Category c => IdentityF c++instance Category c => Functor (IdentityF (c :: k -> k -> *)) ('KProxy :: KProxy (k -> k)) where+    type Domain (IdentityF c) = c+    type Codomain (IdentityF c) = c+    type FMap (IdentityF c) (a :: k) = a+    morphMap = Tagged id++-- |Functors derived from Prelude's Functor.+data CanonicalF (f :: * -> *) where+    CanonicalF :: P.Functor f => CanonicalF f++instance P.Functor f => Functor (CanonicalF f) ('KProxy :: KProxy (* -> *)) where+    type FMap (CanonicalF f) a = f a+    type Domain (CanonicalF f) = (->)+    type Codomain (CanonicalF f) = (->)+    morphMap = Tagged P.fmap
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, Ian Milligan++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * 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.++    * Neither the name of Ian Milligan nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS 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 COPYRIGHT+OWNER 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.
+ Monoidal.hs view
@@ -0,0 +1,16 @@+module Monoidal where++import Data.Tagged+import Data.Proxy++import Category+import Category.Product+import Functor++class (Category c, Functor (Mu c) ('KProxy :: KProxy ((k, k) -> k)), Domain (Mu c) ~ (c :><: c), Codomain (Mu c) ~ c, Object c (I c)) =>+        Monoidal (c :: k -> k -> *) where+    type Mu c+    type I c :: k++(<>) :: forall c a1 a2 b1 b2. Monoidal c => c a1 b1 -> c a2 b2 -> c (FMap (Mu c) '(a1, a2)) (FMap (Mu c) '(b1, b2))+f <> g = proxy morphMap (Proxy :: Proxy (Mu c)) (f :><: g)
+ NaturalTransformation.hs view
@@ -0,0 +1,47 @@+module NaturalTransformation where++import Data.Constraint+import Data.Tagged+import Data.Proxy++import Category+import Category.Product+import Functor+import Monoidal++data NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (f :: *) (g :: *) where+    NatTr :: (Object (NatTr c1 c2) f, Object (NatTr c1 c2) g) =>+        (forall (a :: o1). Object c1 a => Tagged a (c2 (FMap f a :: o2) (FMap g a :: o2))) -> NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g++instance (Category c1, Category c2) => Category (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) where+    type Object (NatTr c1 c2) f = (Functor f ('KProxy :: KProxy (o1 -> o2)), Domain f ~ c1, Codomain f ~ c2)+    observeObjects (NatTr _) = Dict+    id :: forall f. Object (NatTr c1 c2) f => NatTr c1 c2 f f+    id = NatTr f where+        f :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap f a))+        f = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))+    (.) :: forall g h f. NatTr c1 c2 g h -> NatTr c1 c2 f g -> NatTr c1 c2 f h+    NatTr f . NatTr g = NatTr h where+        h :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap h a))+        h = Tagged (proxy f (Proxy :: Proxy a) . proxy g (Proxy :: Proxy a))++data CompFF c1 c2 c3  where CompFF :: (Category c1, Category c2, Category c3) => CompFF c1 c2 c3++instance (Category c1, Category c2, Category c3) =>+        Functor (CompFF (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *)) ('KProxy :: KProxy ((*, *) -> *)) where+    type Domain (CompFF c1 c2 c3) = NatTr c2 c3 :><: NatTr c1 c2+    type Codomain (CompFF c1 c2 c3) = NatTr c1 c3+    type FMap (CompFF c1 c2 c3) '(f, g) = Comp ('KProxy :: KProxy o2) f g+    morphMap = Tagged (\(t1 :><: t2) -> compNat t1 t2)++compNat :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *) f1 f2 g1 g2.+    NatTr c2 c3 f1 g1 -> NatTr c1 c2 f2 g2 -> NatTr c1 c3 (Comp ('KProxy :: KProxy o2) f1 f2) (Comp ('KProxy :: KProxy o2) g1 g2)+compNat (NatTr t1) (NatTr t2) = NatTr t3 where+    t3 :: forall (a :: o1). Object c1 a => Tagged a (c3 (FMap f1 (FMap f2 a :: o2) :: o3) (FMap g1 (FMap g2 a :: o2) :: o3))+    t3 = Tagged (m1 . m2) where+        m2 = proxy morphMap (Proxy :: Proxy f1) (proxy t2 (Proxy :: Proxy a))+        m1 = proxy t1 (Proxy :: Proxy (FMap g2 a)) \\ proxy objectMap (Proxy :: Proxy '(g2, a))++instance Category c => Monoidal (NatTr c c) where+    type Mu (NatTr c c) = CompFF c c c+    type I (NatTr c c) = IdentityF c
+ Product.hs view
@@ -0,0 +1,72 @@+module Product where++import qualified Prelude as P+import Data.Constraint hiding ((***), (&&&))+import Data.Proxy+import Data.Tagged++import Category+import Category.Product+import Functor+import Terminal+import TerminalMorphism+import Monoidal++class Category c => ProductCategory (c :: k -> k -> *) where+    type (><) (a :: k) (b :: k) :: k+    productObjectMap :: Tagged '(c, a, b) ((Object c a, Object c b) :- Object c (a >< b))+    univProduct :: forall (a :: k) (b :: k). Tagged '(c, a, b) ((Object c a, Object c b) :- TerminalMorphism (Diag c) (a >< b) '(a, b))++proj1 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged b (c (a >< b) a)+proj1 = Tagged p where+    p :><: _ = t+    t :: (c :><: c) '(a >< b, a >< b) '(a, b)+    t = proxy terminalMorphism (Proxy :: Proxy '(Diag c, a >< b)) \\ proxy univProduct (Proxy :: Proxy '(c, a, b))++proj2 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged a (c (a >< b) b)+proj2 = Tagged p where+    _ :><: p = t+    t :: (c :><: c) '(a >< b, a >< b) '(a, b)+    t = proxy terminalMorphism (Proxy :: Proxy '(Diag c, a >< b)) \\ proxy univProduct (Proxy :: Proxy '(c, a, b))++(&&&) :: forall c a b1 b2. ProductCategory c => c a b1 -> c a b2 -> c a (b1 >< b2)+f &&& g+    | Dict <- observeObjects f, Dict <- observeObjects g+        = proxy terminalFactorization (Proxy :: Proxy (Diag c)) (f :><: g) \\ proxy univProduct (Proxy :: Proxy '(c, b1, b2))++(***) :: forall c a1 a2 b1 b2. ProductCategory c => c a1 b1 -> c a2 b2 -> c (a1 >< a2) (b1 >< b2)+f *** g = proxy morphMap (Proxy :: Proxy (ProductF c)) (f :><: g)++data ProductF c where ProductF :: ProductCategory c => ProductF c++instance ProductCategory (c :: k -> k -> *) => Functor (ProductF c) ('KProxy :: KProxy ((k, k) -> k)) where+    type Domain (ProductF c) = c :><: c+    type Codomain (ProductF c) = c+    type FMap (ProductF c) (a :: (k, k)) = L a >< R a+    morphMap :: forall (a :: (k, k)) (b :: (k, k)). Tagged (ProductF c)+        (Domain (ProductF c) a b -> Codomain (ProductF c) (FMap (ProductF c) a :: k) (FMap (ProductF c) b :: k))+    morphMap = Tagged m where+        m (f :><: g)+            | Dict <- observeObjects f, Dict <- observeObjects g = (f . (proxy proj1 (Proxy :: Proxy (R a)))) &&& (g . (proxy proj2 (Proxy :: Proxy (L a))))++instance (ProductCategory c, Terminal c) => Monoidal c where+    type Mu c = ProductF c+    type I c = T c++instance TerminalMorphism (Diag (->)) (a, b) '(a, b) where+    terminalMorphism = Tagged (P.fst :><: P.snd)+    terminalFactorization  = Tagged (\(f :><: g) z -> (f z, g z))++instance ProductCategory (->) where+    type (><) a b = (a, b)+    productObjectMap = Tagged (Sub Dict)+    univProduct = Tagged (Sub Dict)++instance TerminalMorphism (Diag (:-)) ((a :: Constraint), b) '(a, b) where+    terminalMorphism = Tagged (Sub Dict :><: Sub Dict)+    terminalFactorization = Tagged (\(f :><: g) -> Sub (Dict \\ f \\ g))++instance ProductCategory (:-) where+    type (><) a b = ((a, b) :: Constraint)+    productObjectMap = Tagged (Sub Dict)+    univProduct = Tagged (Sub Dict)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Terminal.hs view
@@ -0,0 +1,11 @@+module Terminal where++import Category++class (Category c, Object c (T c)) => Terminal c where+    type T c+    term :: Object c a => c a (T c)++instance Terminal (->) where+    type T (->) = ()+    term _ = ()
+ TerminalMorphism.hs view
@@ -0,0 +1,12 @@+module TerminalMorphism where++import Data.Tagged+import Data.Proxy++import Category+import Functor++class (Functor f ('KProxy :: KProxy (o1 -> o2)), Object (Domain f) a, Object (Codomain f) x) =>+        TerminalMorphism f (a :: o1) (x :: o2) where+    terminalMorphism :: Tagged '(f, a) (Codomain f (FMap f a) x)+    terminalFactorization :: Object (Domain f) y => Tagged f (Codomain f (FMap f y) x -> Domain f y a)
+ extended-categories.cabal view
@@ -0,0 +1,32 @@+name:                extended-categories+version:             0.1.0+synopsis:       Extended Categories+description:    An implementation of category theory which makes use of GHC's enriched kind system.+homepage:            github.com/ian-mi/extended-categories+license:             BSD3+license-file:        LICENSE+author:              Ian Milligan+maintainer:          ianmllgn@gmail.com+-- copyright:           +category:            Math+build-type:          Simple+-- extra-source-files:  +cabal-version:       >=1.10+stability: experimental++source-repository head+        type: git+        location: git@github.com:ian-mi/extended-categories.git++source-repository this+        type: git+        location: git@github.com:ian-mi/extended-categories.git+        tag: 0.1.0++library+  exposed-modules:     Category, Category.Product, Functor, Product, Terminal, TerminalMorphism, NaturalTransformation, Monoidal+  -- other-modules:       +  default-extensions:    PolyKinds, DataKinds, TypeFamilies, ConstraintKinds, InstanceSigs, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, UndecidableInstances, TypeOperators, GADTs, NoImplicitPrelude, RankNTypes+  build-depends:       base >=4.7 && <4.8, constraints >=0.3 && <0.5, tagged >=0.7 && <0.8, ghc-prim >=0.3 && <0.4+  -- hs-source-dirs:      +  default-language:    Haskell2010