My previous definitions were insufficient. Hopefully these work.
parent
4566b6526f
commit
49ab5cf339
GPG Key ID:
4B7F3DA9351E577C
|
|
@ -4,7 +4,7 @@ cabal-version: 2.2
|
|||
--
|
||||
-- see: https://github.com/sol/hpack
|
||||
--
|
||||
-- hash: 73c8dbdf7c11bd3edb3a43f645558791b10821437430c5b2b4ba1c648be52910
|
||||
-- hash: 3a1a51f201a4bf26bb1002122fc79d0d4bb421ec1c4f5f4ba69125a18f1444b4
|
||||
|
||||
name: monoids-in-the-categoy-of-endofunctors
|
||||
version: 0.1.0.0
|
||||
|
|
@ -30,18 +30,14 @@ library
|
|||
Category.Applicative
|
||||
Category.Constraint
|
||||
Category.Functor
|
||||
Category.Functor.Const
|
||||
Category.Functor.Identity
|
||||
Category.Monad
|
||||
Category.Monoid
|
||||
Category.Monoidal
|
||||
Category.Nat
|
||||
Category.NaturalTransformation
|
||||
Category.Semigroup
|
||||
other-modules:
|
||||
Paths_monoids_in_the_categoy_of_endofunctors
|
||||
hs-source-dirs:
|
||||
src
|
||||
default-extensions: BlockArguments ConstraintKinds DataKinds FlexibleContexts FlexibleInstances TypeFamilies GADTs KindSignatures MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeOperators UndecidableInstances UndecidableSuperClasses
|
||||
default-extensions: BlockArguments ConstraintKinds FlexibleContexts FlexibleInstances GADTs InstanceSigs MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
|
||||
build-depends:
|
||||
base >=4.13 && <5
|
||||
default-language: Haskell2010
|
||||
|
|
|
|||
|
|
@ -14,12 +14,10 @@ description: Please see the README on GitHub at <https://github.com/jame
|
|||
default-extensions:
|
||||
- BlockArguments
|
||||
- ConstraintKinds
|
||||
- DataKinds
|
||||
- FlexibleContexts
|
||||
- FlexibleInstances
|
||||
- TypeFamilies
|
||||
- GADTs
|
||||
- KindSignatures
|
||||
- InstanceSigs
|
||||
- MultiParamTypeClasses
|
||||
- NoImplicitPrelude
|
||||
- PolyKinds
|
||||
|
|
@ -27,12 +25,11 @@ default-extensions:
|
|||
- RankNTypes
|
||||
- ScopedTypeVariables
|
||||
- TypeApplications
|
||||
- TypeFamilies
|
||||
- TypeOperators
|
||||
- UndecidableInstances
|
||||
- UndecidableSuperClasses
|
||||
|
||||
dependencies:
|
||||
- base >= 4.13 && < 5
|
||||
|
||||
library:
|
||||
source-dirs: src
|
||||
source-dirs: src
|
||||
|
|
|
|||
|
|
@ -1,53 +1,72 @@
|
|||
{-# LANGUAGE UndecidableSuperClasses #-}
|
||||
module Category where
|
||||
|
||||
import Data.Kind (Constraint)
|
||||
|
||||
type family Hom :: i -> i -> k
|
||||
type instance Hom = (~>)
|
||||
data Dict c where
|
||||
Dict :: c => Dict c
|
||||
|
||||
type family (~>) :: i -> i -> *
|
||||
data Proxy a where
|
||||
Proxy :: Proxy a
|
||||
|
||||
type Dom (a :: i -> j) = (~>) :: i -> i -> *
|
||||
newtype Identity a = Identity { getIdentity :: a }
|
||||
|
||||
data Proxy :: k -> * where
|
||||
Proxy :: Proxy k
|
||||
class Category (hom :: k -> k -> *) (obj :: k -> Constraint) where
|
||||
identity :: obj a => proxy obj -> a `hom` a
|
||||
compose :: (obj a, obj b, obj c) => proxy obj -> b `hom` c -> a `hom` b -> a `hom` c
|
||||
|
||||
class Category (r :: k -> Constraint) where
|
||||
identity :: forall proxy a. r a => proxy r -> Dom r a a
|
||||
compose :: forall proxy a b c. (r a, r b, r c) => proxy r -> Dom r b c -> Dom r a b -> Dom r a c
|
||||
|
||||
-- | A restricted alias of `identity` which does not cause type ambiguity.
|
||||
id :: forall r a. (r ~ AnyC, Category r) => Dom r a a
|
||||
id = identity (Proxy @r)
|
||||
|
||||
-- | A restricted alias of `compose` which does not cause type ambiguity.
|
||||
(.) :: forall r a b c. (r ~ AnyC, Category r) => Dom r b c -> Dom r a b -> Dom r a c
|
||||
(.) = compose (Proxy @r)
|
||||
|
||||
type instance (~>) = (->)
|
||||
|
||||
-- | The category of data types.
|
||||
instance Dom r ~ (->) => Category r where
|
||||
instance Category (->) obj where
|
||||
identity _ x = x
|
||||
compose _ f g x = f (g x)
|
||||
|
||||
-- Everything below is miscellaneous crap that doesn't have a better home.
|
||||
class MonoidalObjects (obj :: k -> Constraint) where
|
||||
type Unit obj :: k
|
||||
type Product obj :: k -> k -> k
|
||||
|
||||
class NoC
|
||||
instance NoC
|
||||
instance MonoidalObjects (obj :: * -> Constraint) where
|
||||
type Unit obj = ()
|
||||
type Product obj = (,)
|
||||
|
||||
class AnyC a
|
||||
instance AnyC a
|
||||
class MonoidalObjects obj => ContainsMonoidalObjects obj where
|
||||
unitObj :: Dict (obj (Unit obj))
|
||||
productObjFactor :: (obj a, obj b) => Dict (obj (Product obj a b))
|
||||
productObjDistribute :: obj (Product obj a b) => Dict (obj a, obj b)
|
||||
|
||||
class (f (g a)) => ComposeC f g a
|
||||
instance (f (g a)) => ComposeC f g a
|
||||
class EveryC a
|
||||
instance EveryC a
|
||||
|
||||
newtype Compose (f :: j -> *) (g :: i -> j) (a :: i) = Compose { getCompose :: f (g a) }
|
||||
instance ContainsMonoidalObjects (EveryC :: * -> Constraint) where
|
||||
unitObj = Dict
|
||||
productObjFactor = Dict
|
||||
productObjDistribute = Dict
|
||||
|
||||
class (forall a. c a) => LimC c
|
||||
instance (forall a. c a) => LimC c
|
||||
class (Category hom obj, ContainsMonoidalObjects obj) => MonoidalCategory (hom :: k -> k -> *) (obj :: k -> Constraint) where
|
||||
idLI :: obj a => proxy obj -> a `hom` Product obj a (Unit obj)
|
||||
idLE :: obj a => proxy obj -> Product obj a (Unit obj) `hom` a
|
||||
idRI :: obj a => proxy obj -> a `hom` Product obj (Unit obj) a
|
||||
idRE :: obj a => proxy obj -> Product obj (Unit obj) a `hom` a
|
||||
|
||||
class (LimC (ComposeC f g)) => Post f g
|
||||
instance (LimC (ComposeC f g)) => Post f g
|
||||
assocL :: (obj a, obj b, obj c) => proxy obj -> Product obj a (Product obj b c) `hom` Product obj (Product obj a b) c
|
||||
assocR :: (obj a, obj b, obj c) => proxy obj -> Product obj (Product obj a b) c `hom` Product obj a (Product obj b c)
|
||||
|
||||
newtype Lim f = Lim { getLim :: forall a. f a }
|
||||
instance ContainsMonoidalObjects obj => MonoidalCategory (->) obj where
|
||||
idLI _ x = (x, ())
|
||||
idLE _ (x, ()) = x
|
||||
idRI _ x = ((), x)
|
||||
idRE _ ((), x) = x
|
||||
|
||||
assocL _ (x, (y, z)) = ((x, y), z)
|
||||
assocR _ ((x, y), z) = (x, (y, z))
|
||||
|
||||
class (MonoidalCategory overHom overObj) => EnrichedCategory overHom (overObj :: k -> Constraint) (hom :: j -> j -> k) (obj :: j -> Constraint) where
|
||||
homObj :: (obj a, obj b) => proxy overHom -> proxy' obj -> Dict (overObj (a `hom` b))
|
||||
enrichedIdentity :: obj a => proxy overObj -> proxy' obj -> Unit overObj `overHom` (a `hom` a)
|
||||
enrichedCompose :: (obj a, obj b, obj c) => proxy overObj -> proxy' obj -> Product overObj (b `hom` c) (a `hom` b) `overHom` (a `hom` c)
|
||||
|
||||
instance Category hom obj => EnrichedCategory (->) EveryC hom obj where
|
||||
homObj _ _ = Dict
|
||||
enrichedIdentity _ px () = identity px
|
||||
enrichedCompose _ px (f, g) = compose px f g
|
||||
|
||||
class (c a, d a) => ProductCI c d a
|
||||
instance (c a, d a) => ProductCI c d a
|
||||
|
|
|
|||
|
|
@ -2,17 +2,13 @@ module Category.Applicative where
|
|||
|
||||
import Category
|
||||
import Category.Functor
|
||||
import Category.Functor.Identity
|
||||
import Category.Semigroup ()
|
||||
import qualified Prelude
|
||||
|
||||
class Functor r s f => Applicative r s f where
|
||||
pure :: (r a, s (f a)) => proxy r s -> a ~> f a
|
||||
ap :: (r a, r b, r (a ~> b), s (f (a ~> b)), s (f a), s (f b)) => proxy r s -> f (a ~> b) -> f a ~> f b
|
||||
class (MonoidalCategory domHom domObj, MonoidalCategory codHom codObj, Functor domHom domObj codHom codObj f) => Applicative domHom domObj codHom codObj f where
|
||||
unit :: proxy domHom -> proxy' domObj -> proxy'' codHom -> proxy''' codObj -> f (Unit domObj)
|
||||
zip :: proxy domHom -> proxy' domObj -> proxy'' codObj -> proxy''' codObj -> Product codObj (f a) (f b) `codHom` f (Product domObj a b)
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Prelude.Applicative f => Applicative r s f where
|
||||
pure _ = Prelude.pure
|
||||
ap _ = (Prelude.<*>)
|
||||
|
||||
instance Applicative r s Identity where
|
||||
pure _ = Identity
|
||||
ap _ (Identity f) x = f <$> x
|
||||
instance {-# INCOHERENT #-} Prelude.Applicative f => Applicative (->) EveryC (->) EveryC f where
|
||||
unit _ _ _ _ = Prelude.pure ()
|
||||
zip _ _ _ _ (x, y) = Prelude.fmap (,) x Prelude.<*> y
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
-- | The category of constraints.
|
||||
module Category.Constraint where
|
||||
|
||||
import Category
|
||||
|
|
@ -6,14 +5,9 @@ import Prelude (($))
|
|||
|
||||
newtype a :- b = Sub (a => Dict b)
|
||||
|
||||
type instance (~>) = (:-)
|
||||
|
||||
data Dict p where
|
||||
Dict :: p => Dict p
|
||||
|
||||
(\\) :: a => (b => r) -> (a :- b) -> r
|
||||
r \\ Sub Dict = r
|
||||
|
||||
instance Dom r ~ (:-) => Category r where
|
||||
instance Category (:-) obj where
|
||||
identity _ = Sub Dict
|
||||
compose _ f g = Sub $ Dict \\ f \\ g
|
||||
|
|
|
|||
|
|
@ -1,49 +1,21 @@
|
|||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Category.Functor where
|
||||
|
||||
import Category
|
||||
import Category.Nat
|
||||
import Data.Kind (Constraint)
|
||||
import qualified Prelude (Functor, fmap)
|
||||
import qualified Prelude
|
||||
|
||||
-- | A functor `f` from category `src` to `dest`.
|
||||
-- | This is *much more general* than Haskell's Functor, which is
|
||||
-- | 1. An endofunctor, i.e. a functor from a category to itself (`Functor cat cat f`)
|
||||
-- | 2. An endofunctor in the category of *types*, where cat can *only* be `AnyC :: * -> Constraint`.
|
||||
class (Category src, Category dest) => Functor (src :: srcKind -> Constraint) (dest :: destKind -> Constraint) (f :: srcKind -> destKind) where
|
||||
map :: forall proxy1 proxy2 a b. (src a, src b, dest (f a), dest (f b)) => proxy1 src -> proxy2 dest -> (a ~> b) -> f a ~> f b
|
||||
class (Category domHom domObj, Category codHom codObj) => Functor domHom domObj codHom codObj f where
|
||||
mapObj :: domObj a => proxy domHom -> proxy' domObj -> proxy'' codHom -> Dict (codObj (f a))
|
||||
map :: (domObj a, domObj b) => proxy domObj -> proxy' codObj -> a `domHom` b -> f a `codHom` f b
|
||||
|
||||
-- | A functor from a category to itself.
|
||||
class Functor cat cat f => Endofunctor cat f
|
||||
instance Functor cat cat f => Endofunctor cat f
|
||||
instance (Category (->) obj, forall a. obj (Identity a)) => Functor (->) obj (->) obj Identity where
|
||||
mapObj _ _ _ = Dict
|
||||
map _ _ f (Identity x) = Identity (f x)
|
||||
|
||||
-- | A restricted alias of `map` which does not cause type ambiguity.
|
||||
(<$>) :: forall r s f a b. (r ~ AnyC, s ~ AnyC, Functor r s f) => (a ~> b) -> f a ~> f b
|
||||
(<$>) = map (Proxy @r) (Proxy @s)
|
||||
class (Functor hom obj hom obj f) => Endofunctor hom obj f where
|
||||
endomapObj :: obj a => proxy hom -> proxy' obj -> Dict (obj (f a))
|
||||
endomap :: (obj a, obj b) => proxy obj -> a `hom` b -> f a `hom` f b
|
||||
|
||||
-- | A contravariant functor.
|
||||
class (Category src, Category dest) => Contravariant (src :: srcKind -> Constraint) (dest :: destKind -> Constraint) (f :: srcKind -> destKind) where
|
||||
contramap :: forall proxy1 proxy2 a b. (src a, src b, dest (f a), dest (f b)) => proxy1 src -> proxy2 dest -> (b ~> a) -> (f a ~> f b)
|
||||
|
||||
-- | An invariant functor.
|
||||
class (Category src, Category dest) => Invariant (src :: srcKind -> Constraint) (dest :: destKind -> Constraint) (f :: srcKind -> destKind) where
|
||||
invmap :: forall proxy1 proxy2 a b. (src a, src b, dest (f a), dest (f b)) => proxy1 src -> proxy2 dest -> (a ~> b) -> (b ~> a) -> (f a ~> f b)
|
||||
|
||||
{-
|
||||
instance {-# INCOHERENT #-} Functor src dest f => Invariant src dest f where
|
||||
invmap f _ = map f
|
||||
|
||||
instance {-# INCOHERENT #-} Contravariant src dest f => Invariant src dest f where
|
||||
invmap _ f = contramap f
|
||||
-}
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Prelude.Functor f => Functor r s f where
|
||||
map _ _ = Prelude.fmap
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest ((->) a) where
|
||||
map _ _ f g x = f (g x)
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest ((,) a) where
|
||||
map _ _ f (x, y) = (x, f y)
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest (,) where
|
||||
map _ _ f = Nat \(x, y) -> (f x, y)
|
||||
instance (Functor hom obj hom obj f) => Endofunctor hom obj f where
|
||||
endomapObj pxh pxo = mapObj pxh pxo pxh
|
||||
endomap px = map px px
|
||||
|
|
|
|||
|
|
@ -1,37 +0,0 @@
|
|||
module Category.Functor.Const where
|
||||
|
||||
import Category
|
||||
import Category.Functor
|
||||
import Category.Nat
|
||||
import Prelude (($))
|
||||
|
||||
newtype Const f a = Const { getConst :: f }
|
||||
|
||||
reconst :: Const f a -> Const f b
|
||||
reconst = Const . getConst
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest Const where
|
||||
map _ _ f = Nat $ Const . f . getConst
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest (Const f) where
|
||||
map _ _ _ = Const . getConst
|
||||
|
||||
instance (Category src, Category dest) => Contravariant src dest (Const f) where
|
||||
contramap _ _ _ = Const . getConst
|
||||
|
||||
newtype Const2 f a b = Const2 { getConst2 :: f }
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest Const2 where
|
||||
map _ _ f = nat2 $ Const2 . f . getConst2
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest (Const2 f) where
|
||||
map _ _ f = Nat $ Const2 . getConst2
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest (Const2 f a) where
|
||||
map _ _ f = Const2 . getConst2
|
||||
|
||||
instance (Category src, Category dest) => Contravariant src dest (Const2 f) where
|
||||
contramap _ _ _ = Nat $ Const2 . getConst2
|
||||
|
||||
instance (Category src, Category dest) => Contravariant src dest (Const2 f a) where
|
||||
contramap _ _ _ = Const2 . getConst2
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
module Category.Functor.Identity where
|
||||
|
||||
import Category
|
||||
import Category.Functor
|
||||
|
||||
newtype Identity a = Identity { getIdentity :: a }
|
||||
|
||||
instance (Category src, Category dest) => Functor src dest Identity where
|
||||
map _ _ f (Identity x) = Identity (f x)
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
module Category.Monad where
|
||||
|
||||
import Category
|
||||
import Category.Applicative
|
||||
import Category.Functor
|
||||
import Category.Functor.Identity
|
||||
import Category.Monoid
|
||||
import Category.Monoidal
|
||||
import Category.Nat
|
||||
import Category.Semigroup
|
||||
import Prelude (undefined)
|
||||
|
||||
class (Category (Functor r r), Monoid (Functor r r) m) => Monad r m
|
||||
instance (Category (Functor r r), Monoid (Functor r r) m) => Monad r m
|
||||
|
||||
return :: forall proxy r m. Monad r m => proxy r -> Dom (Functor r r) Unit m
|
||||
return _ = empty (Proxy @(Functor r r))
|
||||
|
||||
join :: forall proxy r m. Monad r m => proxy r -> Dom (Functor r r) (Product m m) m
|
||||
join _ = append (Proxy @(Functor r r))
|
||||
|
||||
class (Category (Endofunctor cat), Comonoid (Endofunctor cat) w) => Comonad cat w
|
||||
instance (Category (Endofunctor cat), Comonoid (Endofunctor cat) w) => Comonad cat w
|
||||
|
|
@ -1,27 +1,18 @@
|
|||
{-# LANGUAGE UndecidableSuperClasses #-}
|
||||
module Category.Monoid where
|
||||
|
||||
import Category
|
||||
import Category.Functor
|
||||
import Category.Functor.Identity
|
||||
import Category.Monoidal
|
||||
import Category.Nat
|
||||
import Category.NaturalTransformation
|
||||
import Category.Semigroup
|
||||
import Data.Kind (Constraint)
|
||||
import qualified Control.Monad
|
||||
import qualified Prelude
|
||||
|
||||
class Semigroup r m => Monoid r m where
|
||||
empty :: proxy r -> Unit ~> m
|
||||
class Semigroup hom obj m => Monoid hom obj m where
|
||||
empty :: proxy obj -> Unit obj `hom` m
|
||||
|
||||
instance {-# OVERLAPPABLE #-} (Category r, Prelude.Monoid m) => Monoid r m where
|
||||
empty _ _ = Prelude.mempty
|
||||
instance (Semigroup (->) obj m, Prelude.Monoid m) => Monoid (->) obj m where
|
||||
empty _ () = Prelude.mempty
|
||||
|
||||
instance {-# OVERLAPPABLE #-} (Category (Functor r r), Prelude.Monad m) => Monoid (Functor r r) m where
|
||||
instance (hom ~ Nat (->) EveryC (->) EveryC, MonoidalCategory hom (Endofunctor (->) EveryC), Prelude.Monad m) => Monoid hom (Endofunctor (->) EveryC) m where
|
||||
empty _ = Nat \(Identity x) -> Prelude.return x
|
||||
|
||||
class MonoidalCategory cat => Comonoid cat m where
|
||||
duplicate :: proxy cat -> Dom cat m (Product m m)
|
||||
extract :: proxy cat -> Dom cat m Unit
|
||||
|
||||
instance MonoidalCategory cat => Comonoid cat (m :: *) where
|
||||
duplicate _ x = (x, x)
|
||||
extract _ _ = ()
|
||||
|
|
|
|||
|
|
@ -1,72 +0,0 @@
|
|||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
module Category.Monoidal where
|
||||
|
||||
import Category
|
||||
import Category.Constraint
|
||||
import Category.Functor
|
||||
import Category.Functor.Identity
|
||||
import Category.Nat
|
||||
import Data.Kind (Constraint)
|
||||
import Prelude (($), undefined)
|
||||
import Unsafe.Coerce
|
||||
|
||||
class Category cat => MonoidalCategory (cat :: i -> Constraint) where
|
||||
type Product :: i -> i -> i
|
||||
type Unit :: i
|
||||
|
||||
assocL :: (cat a, cat b, cat c) => Dom cat (Product a (Product b c)) (Product (Product a b) c)
|
||||
assocR :: (cat a, cat b, cat c) => Dom cat (Product (Product a b) c) (Product a (Product b c))
|
||||
|
||||
idLI :: cat a => Dom cat a (Product a Unit)
|
||||
idLE :: cat a => Dom cat (Product a Unit) a
|
||||
idRI :: cat a => Dom cat a (Product Unit a)
|
||||
idRE :: cat a => Dom cat (Product Unit a) a
|
||||
|
||||
instance (Dom cat ~ (->)) => MonoidalCategory cat where
|
||||
type Product = (,)
|
||||
type Unit = ()
|
||||
|
||||
assocL (x, (y, z)) = ((x, y), z)
|
||||
assocR ((x, y), z) = (x, (y, z))
|
||||
|
||||
idLI x = (x, ())
|
||||
idLE (x, ()) = x
|
||||
idRI x = ((), x)
|
||||
idRE ((), x) = x
|
||||
|
||||
-- r :: (i -> k) -> Constraint
|
||||
instance (Category cat, Dom cat ~ Nat) => MonoidalCategory (cat :: (* -> *) -> Constraint) where
|
||||
-- FIXME: This instance can be broken by GADTs!
|
||||
-- You need a functor, contrafunctor, or invariant functor instance for this to be valid,
|
||||
-- but we can't express the category of functors yet so that'll need to be done later.
|
||||
type Product = Compose
|
||||
type Unit = Identity
|
||||
|
||||
assocL = Nat unsafeCoerce
|
||||
assocR = Nat unsafeCoerce
|
||||
|
||||
idLI = Nat unsafeCoerce
|
||||
idLE = Nat unsafeCoerce
|
||||
idRI = Nat unsafeCoerce
|
||||
idRE = Nat unsafeCoerce
|
||||
|
||||
class (a, b) => ProductC a b
|
||||
instance (a, b) => ProductC a b
|
||||
|
||||
class (a i, b i) => ProductCI a b i
|
||||
instance (a i, b i) => ProductCI a b i
|
||||
|
||||
class UnitC
|
||||
instance UnitC
|
||||
|
||||
instance (Dom cat ~ (:-)) => MonoidalCategory cat where
|
||||
type Product = ProductC
|
||||
type Unit = NoC
|
||||
|
||||
assocL = Sub Dict
|
||||
assocR = Sub Dict
|
||||
|
||||
idLI = Sub Dict
|
||||
idLE = Sub Dict
|
||||
idRI = Sub Dict
|
||||
idRE = Sub Dict
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
-- | The category of natural transformations.
|
||||
module Category.Nat where
|
||||
|
||||
import Category
|
||||
import Data.Kind (Constraint)
|
||||
|
||||
type instance (~>) = Nat
|
||||
|
||||
newtype Nat f g = Nat { runNat :: forall a. f a ~> g a }
|
||||
|
||||
nat2 :: forall f g. (forall a b. f a b -> g a b) -> f ~> g
|
||||
nat2 f = Nat (Nat f)
|
||||
|
||||
runNat2 = runNat . runNat
|
||||
runNat3 = runNat . runNat2
|
||||
runNat4 = runNat . runNat3
|
||||
|
||||
class (forall a. c (nat a)) => NatConstraint (c :: j -> Constraint) (nat :: i -> j)
|
||||
instance (forall a. c (nat a)) => NatConstraint (c :: j -> Constraint) (nat :: i -> j)
|
||||
|
||||
instance Category r => Category (NatConstraint r) where
|
||||
identity _ = Nat (identity (Proxy @r))
|
||||
compose _ (Nat f) (Nat g) = Nat (compose (Proxy @r) f g)
|
||||
|
|
@ -0,0 +1,59 @@
|
|||
module Category.NaturalTransformation where
|
||||
|
||||
import Category
|
||||
import Category.Functor
|
||||
import Data.Kind (Constraint)
|
||||
import Prelude (($), undefined)
|
||||
|
||||
data Nat domHom domObj codHom codObj f g where
|
||||
Nat :: (Functor domHom domObj codHom codObj f, Functor domHom domObj codHom codObj g) => (forall a. domObj a => f a `codHom` g a) -> Nat domHom domObj codHom codObj f g
|
||||
|
||||
instance (Category domHom domObj, Category codHom codObj) => Category (Nat domHom domObj codHom codObj) (ProductCI (Functor domHom domObj codHom codObj) obj) where
|
||||
-- This type signature is just boilerplate to get `f` into scope, which is necessary to get the `codObj (f a)` instance.
|
||||
identity :: forall f proxy. ProductCI (Functor domHom domObj codHom codObj) obj f => proxy (ProductCI (Functor domHom domObj codHom codObj) obj) -> Nat domHom domObj codHom codObj f f
|
||||
identity _ = Nat f
|
||||
where f :: forall a. domObj a => f a `codHom` f a
|
||||
f = case mapObj (Proxy @domHom) (Proxy @domObj) (Proxy @codHom) :: Dict (codObj (f a)) of Dict -> identity (Proxy @codObj)
|
||||
|
||||
compose :: forall a b c proxy. (ProductCI (Functor domHom domObj codHom codObj) obj a, ProductCI (Functor domHom domObj codHom codObj) obj b, ProductCI (Functor domHom domObj codHom codObj) obj c) => proxy (ProductCI (Functor domHom domObj codHom codObj) obj) -> Nat domHom domObj codHom codObj b c -> Nat domHom domObj codHom codObj a b -> Nat domHom domObj codHom codObj a c
|
||||
compose _ (Nat f) (Nat g) = Nat fg
|
||||
where fg :: forall x. domObj x => a x `codHom` c x
|
||||
fg = case mapObj' (Proxy @a) of
|
||||
Dict -> case mapObj' (Proxy @b) of
|
||||
Dict -> case mapObj' (Proxy @c) of
|
||||
Dict -> compose (Proxy @codObj) f g
|
||||
where mapObj' :: forall f proxy. Functor domHom domObj codHom codObj f => proxy f -> Dict (codObj (f x))
|
||||
mapObj' _ = mapObj (Proxy @domHom) (Proxy @domObj) (Proxy @codHom) :: Dict (codObj (f x))
|
||||
|
||||
data ComposeEndofunctor hom obj f g x where
|
||||
ComposeEndofunctor :: { getComposeEndofunctor :: (Endofunctor hom obj f, Endofunctor hom obj g, obj x) => f (g x) } -> ComposeEndofunctor hom obj f g x
|
||||
|
||||
instance {-# INCOHERENT #-} (Category (->) obj, Endofunctor (->) obj f, Endofunctor (->) obj g, forall a. obj (ComposeEndofunctor (->) obj f g a)) => Functor (->) obj (->) obj (ComposeEndofunctor (->) obj f g) where
|
||||
mapObj _ _ _ = Dict
|
||||
|
||||
map :: forall a b proxy proxy'. (obj a, obj b) => proxy obj -> proxy' obj -> (a -> b) -> ComposeEndofunctor (->) obj f g a -> ComposeEndofunctor (->) obj f g b
|
||||
map _ _ f (ComposeEndofunctor x) = ComposeEndofunctor $ case mapObj' (Proxy @a) of
|
||||
Dict -> case mapObj' (Proxy @b) of
|
||||
Dict -> endomap (Proxy @obj) (endomap (Proxy @obj) f) x
|
||||
where mapObj' :: forall x proxy. (Endofunctor (->) obj f, obj x) => proxy x -> Dict (obj (g x))
|
||||
mapObj' _ = mapObj (Proxy @(->)) (Proxy @obj) (Proxy @(->))
|
||||
|
||||
instance Category hom obj => MonoidalObjects (Endofunctor hom (obj :: * -> Constraint)) where
|
||||
type Unit (Endofunctor hom obj) = Identity
|
||||
type Product (Endofunctor hom obj) = ComposeEndofunctor hom obj
|
||||
|
||||
instance ContainsMonoidalObjects (Endofunctor (->) (EveryC :: * -> Constraint)) where
|
||||
unitObj = Dict
|
||||
productObjFactor = Dict
|
||||
-- FIXME: Implement this
|
||||
productObjDistribute = undefined
|
||||
|
||||
instance (obj ~ EveryC, hom ~ Nat (->) obj (->) obj, Category hom (Endofunctor (->) obj)) => MonoidalCategory hom (Endofunctor (->) obj) where
|
||||
idLI _ = Nat \x -> ComposeEndofunctor (endomap (Proxy @obj) Identity x)
|
||||
idLE _ = Nat \(ComposeEndofunctor x) -> endomap (Proxy @obj) getIdentity x
|
||||
idRI _ = Nat \x -> ComposeEndofunctor (Identity x)
|
||||
idRE _ = Nat \(ComposeEndofunctor (Identity x)) -> x
|
||||
|
||||
assocL _ = Nat \(ComposeEndofunctor x) -> ComposeEndofunctor (ComposeEndofunctor (endomap (Proxy @obj) getComposeEndofunctor x))
|
||||
-- FIXME: Finish implementing this
|
||||
assocR _ = Nat \(ComposeEndofunctor (ComposeEndofunctor x)) -> ComposeEndofunctor (endomap (Proxy @obj) ComposeEndofunctor undefined)
|
||||
|
|
@ -1,19 +1,22 @@
|
|||
{-# LANGUAGE UndecidableSuperClasses #-}
|
||||
module Category.Semigroup where
|
||||
|
||||
import Category
|
||||
import Category.Functor
|
||||
import Category.Monoidal
|
||||
import Category.Nat
|
||||
import Category.NaturalTransformation
|
||||
import qualified Control.Monad
|
||||
import Data.Kind (Constraint)
|
||||
import Prelude (curry, uncurry)
|
||||
import Prelude (uncurry)
|
||||
import qualified Prelude
|
||||
|
||||
class MonoidalCategory r => Semigroup r m where
|
||||
append :: proxy r -> Dom r (Product m m) m
|
||||
class (MonoidalCategory hom obj, obj m) => Semigroup hom obj m where
|
||||
append :: proxy obj -> Product obj m m `hom` m
|
||||
|
||||
instance {-# OVERLAPPABLE #-} (MonoidalCategory r, Prelude.Semigroup m) => Semigroup r m where
|
||||
instance {-# INCOHERENT #-} Prelude.Functor f => Functor (->) EveryC (->) EveryC f where
|
||||
mapObj _ _ _ = Dict
|
||||
map _ _ = Prelude.fmap
|
||||
|
||||
instance {-# OVERLAPPABLE #-} (MonoidalCategory (->) obj, obj m, Prelude.Semigroup m) => Semigroup (->) obj m where
|
||||
append _ = uncurry (Prelude.<>)
|
||||
|
||||
instance {-# OVERLAPPABLE #-} (Category (Functor r r), Prelude.Monad m) => Semigroup (Functor r r) m where
|
||||
append _ = Nat \(Compose x) -> Control.Monad.join x
|
||||
instance {-# OVERLAPPABLE #-} (hom ~ Nat (->) EveryC (->) EveryC, MonoidalCategory hom (Endofunctor (->) EveryC), Prelude.Monad m) => Semigroup hom (Endofunctor (->) EveryC) m where
|
||||
append _ = Nat \(ComposeEndofunctor x) -> Control.Monad.join x
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
resolver: lts-16.9
|
||||
resolver: lts-16.11
|
||||
|
||||
packages:
|
||||
- .
|
||||
- .
|
||||
|
|
|
|||
Loading…
Reference in New Issue