james
/
monoids-in-the-category-of-endofunctors
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Go back to the old rep. for categories, which is cleaner.

master
James T. Martin 2020-10-22 23:49:46 -07:00
parent 0dd45dfd9a
commit e5d265e124
Signed by: james
GPG Key ID: 4B7F3DA9351E577C
12 changed files with 95 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
monoids-in-the-categoy-of-endofunctors.cabal → monoids-in-the-category-of-endofunctors.cabal
View File

@ -4,9 +4,9 @@ cabal-version: 2.2
--
-- see: https://github.com/sol/hpack
--
-- hash: 4d5299830f70602c840afe07491da0f469a43100f9e7c8ccb7452202fe810a77
-- hash: 9da0ab5910c39708370abf34bf6550033a06f63815096534e1c3fb9aa07ad25d
name: monoids-in-the-categoy-of-endofunctors
name: monoids-in-the-category-of-endofunctors
version: 0.1.0.0
description: Please see the README on GitHub at <https://github.com/jamestmartin/monoids-in-the-categoy-of-endofunctors#readme>
homepage: https://github.com/jamestmartin/monoids-in-the-categoy-of-endofunctors#readme
@ -32,14 +32,14 @@ library
Category.Functor
Category.Functor.Foldable
Category.Functor.Foldable.TH
Category.Functor.Foldable.THT
Data.Dict
Data.Fin
Data.Nat
Data.Proxy
Data.Vec
Quantifier
other-modules:
Paths_monoids_in_the_categoy_of_endofunctors
Paths_monoids_in_the_category_of_endofunctors
hs-source-dirs:
src
default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators

2
package.yaml
View File

@ -1,4 +1,4 @@
name: monoids-in-the-categoy-of-endofunctors
name: monoids-in-the-category-of-endofunctors
version: 0.1.0.0
github: "jamestmartin/monoids-in-the-categoy-of-endofunctors"
license: GPL-3.0-or-later

28
src/Category/Base.hs
View File

@ -1,22 +1,27 @@
module Category.Base where
import Data.Kind (Type)
import Data.Dict (Dict (Dict))
import Data.Kind (Constraint, Type)
type Obj q a = a `q` a
class Vacuous (a :: i)
instance Vacuous (a :: i)
class Semigroupoid (q :: i -> i -> Type) where
type Obj q :: i -> Constraint
type Obj _ = Vacuous
observe :: a `q` b -> Dict (Obj q a, Obj q b)
default observe :: Obj q ~ Vacuous => a `q` b -> Dict (Obj q a, Obj q b)
observe _ = Dict
(.) :: b `q` c -> a `q` b -> a `q` c
instance Semigroupoid (->) where
(.) f g x = f (g x)
class Semigroupoid q => Category q where
src :: a `q` b -> Obj q a
tgt :: a `q` b -> Obj q b
id :: Obj q a => a `q` a
instance Category (->) where
src _ x = x
tgt _ x = x
id x = x
class Category q => Groupoid q where
inv :: a `q` b -> b `q` a
@ -24,11 +29,12 @@ class Category q => Groupoid q where
newtype Yoneda (q :: i -> i -> Type) (a :: i) (b :: i) = Op { getOp :: b `q` a }
instance Semigroupoid q => Semigroupoid (Yoneda q) where
type Obj (Yoneda q) = Obj q
observe (Op f) = case observe f of Dict -> Dict
Op f . Op g = Op (g . f)
instance Category q => Category (Yoneda q) where
src (Op f) = Op (tgt f)
tgt (Op f) = Op (src f)
id = Op id
type family Op (q :: i -> i -> Type) :: i -> i -> Type where
Op (Yoneda q) = q
@ -44,8 +50,7 @@ instance Semigroupoid (:~:) where
Refl . Refl = Refl
instance Category (:~:) where
src _ = Refl
tgt _ = Refl
id = Refl
instance Groupoid (:~:) where
inv Refl = Refl
@ -56,8 +61,7 @@ instance Semigroupoid Unit where
Unit . Unit = Unit
instance Category Unit where
src _ = Unit
tgt _ = Unit
id = Unit
instance Groupoid Unit where
inv _ = Unit

3
src/Category/Constraint.hs
View File

@ -16,5 +16,4 @@ instance Semigroupoid (:-) where
f . g = Sub (Dict \\ f \\ g)
instance Category (:-) where
src _ = Sub Dict
tgt _ = Sub Dict
id = Sub Dict

56
src/Category/Functor.hs
View File

@ -2,6 +2,7 @@
module Category.Functor where
import Category.Base
import Category.Constraint ((:-) (Sub), Dict (Dict))
import Data.Kind (Type)
import Data.Maybe (Maybe (Nothing, Just))
import Quantifier
@ -9,6 +10,9 @@ import Quantifier
class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
type Dom f :: i -> i -> Type
type Cod f :: j -> j -> Type
map_ :: Obj (Dom f) a :- Obj (Cod f) (f a)
default map_ :: Obj (Cod f) ~ Vacuous => Obj (Dom f) a :- Obj (Cod f) (f a)
map_ = Sub Dict
map :: Dom f a b -> Cod f (f a) (f b)
class (Functor f, Dom f ~ q, Cod f ~ r) => FunctorOf q r f
@ -18,39 +22,68 @@ class (Functor f, Dom f ~ Cod f) => Endofunctor f
instance (Functor f, Dom f ~ Cod f) => Endofunctor f
data Nat (q :: i -> i -> Type) (r :: j -> j -> Type) (f :: i -> j) (g :: i -> j) :: Type where
Nat :: (FunctorOf q r f, FunctorOf q r g) => (forall a. Obj q a -> r (f a) (g a)) -> Nat q r f g
runNat :: Nat q r f g -> forall a. Obj q a -> r (f a) (g a)
runNat (Nat f) = f
Nat :: (FunctorOf q r f, FunctorOf q r g) => { runNat :: forall a. Obj q a => r (f a) (g a) } -> Nat q r f g
instance Semigroupoid r => Semigroupoid (Nat q r) where
(.) (Nat f) (Nat g) = Nat \p -> (f p . g p)
type Obj (Nat q r) = FunctorOf q r
observe (Nat _) = Dict
(.) (Nat f) (Nat g) = Nat (f . g)
instance Category r => Category (Nat q r) where
src (Nat f) = Nat (src . f)
tgt (Nat f) = Nat (tgt . f)
id :: forall f. Obj (Nat q r) f => Nat q r f f
id = Nat id'
where id' :: forall a. Obj q a => r (f a) (f a)
id' = case map_ :: Obj q a :- Obj r (f a) of Sub Dict -> id
instance Functor (->) where
type Dom (->) = Op (->)
type Cod (->) = Nat (->) (->)
map (Op f) = Nat \_ -> (. f)
map_ = Sub Dict
map (Op f) = Nat (. f)
instance Functor ((->) a) where
type Dom ((->) a) = (->)
type Cod ((->) a) = (->)
map f g = f . g
instance Functor (:-) where
type Dom (:-) = Op (:-)
type Cod (:-) = Nat (:-) (->)
map_ = Sub Dict
map (Op f) = Nat (. f)
instance Functor ((:-) a) where
type Dom ((:-) a) = (:-)
type Cod ((:-) a) = (->)
map = (.)
instance Functor (:~:) where
type Dom (:~:) = (:~:)
type Cod (:~:) = Nat (:~:) (->)
map_ = Sub Dict
map Refl = Nat id
instance Functor ((:~:) a) where
type Dom ((:~:) a) = (:~:)
type Cod ((:~:) a) = (->)
map = (.)
instance Functor (,) where
type Dom (,) = (->)
type Cod (,) = Nat (->) (->)
map f = Nat \_ (x, y) -> (f x, y)
map_ = Sub Dict
map f = Nat \(x, y) -> (f x, y)
instance Functor ((,) a) where
type Dom ((,) a) = (->)
type Cod ((,) a) = (->)
map f (x, y) = (x, f y)
--
instance Functor Dict where
type Dom Dict = (:-)
type Cod Dict = (->)
map f Dict = case f of Sub Dict -> Dict
type family NatDom (f :: (i -> j) -> (i -> j) -> Type) :: (i -> i -> Type) where
NatDom (Nat p _) = p
@ -74,7 +107,8 @@ instance Category cat => Functor (Const cat a) where
instance Category cat => Functor (Const cat) where
type Dom (Const cat) = (->)
type Cod (Const cat) = Nat cat (->)
map f = Nat \_ -> \case (Const x) -> Const (f x)
map_ = Sub Dict
map f = Nat \case (Const x) -> Const (f x)
instance Functor Maybe where
type Dom Maybe = (->)

53
src/Category/Functor/Foldable/THT.hs
View File

@ -1,53 +0,0 @@
{-# LANGUAGE TemplateHaskell #-}
module Category.Functor.Foldable.THT where
import Category.Functor.Foldable.TH
import Data.Kind (Type)
import Category
import Category.Functor.Foldable
data N = Z | S N
makeBaseFunctor ''N 0
data Fin :: N -> Type where
FZ :: forall n. Fin ('S n)
FS :: forall n. Fin n -> Fin ('S n)
makeBaseFunctor ''Fin 0
type instance Base Fin = FinF
instance Functor Fin where
type Dom Fin = (:~:)
type Cod Fin = (->)
map Refl x = x
instance Functor (FinF r) where
type Dom (FinF r) = (:~:)
type Cod (FinF r) = (->)
map Refl x = x
instance Functor FinF where
type Dom FinF = Nat (:~:) (->)
type Cod FinF = Nat (:~:) (->)
map :: forall f g. Nat (:~:) (->) f g -> Nat (:~:) (->) (FinF f) (FinF g)
map (Nat f) = Nat \_ -> \case
FZF -> FZF
(FSF r) -> FSF (f Refl r)
instance Recursive Fin where
project = Nat \_ -> \case
FZ -> FZF
(FS r) -> FSF r
instance Corecursive Fin where
embed = Nat \_ -> \case
FZF -> FZ
(FSF r) -> FS r
data Vec a :: N -> Type where
VZ :: Vec a 'Z
VS :: a -> Vec a n -> Vec a ('S n)
makeBaseFunctor ''Vec 0

11
src/Data/Fin.hs
View File

@ -26,23 +26,24 @@ instance Functor (FinF r) where
instance Functor FinF where
type Dom FinF = Nat (:~:) (->)
type Cod FinF = Nat (:~:) (->)
map_ = Sub Dict
map :: forall f g. Nat (:~:) (->) f g -> Nat (:~:) (->) (FinF f) (FinF g)
map (Nat f) = Nat \_ -> \case
map (Nat f) = Nat \case
FZF -> FZF
(FSF r) -> FSF (f Refl r)
(FSF r) -> FSF (f r)
instance Recursive Fin where
project = Nat \_ -> \case
project = Nat \case
FZ -> FZF
(FS r) -> FSF r
instance Corecursive Fin where
embed = Nat \_ -> \case
embed = Nat \case
FZF -> FZ
(FSF r) -> FS r
fin2nat :: Nat (:~:) (->) Fin (Const (:~:) N)
fin2nat = cata (Nat \_ -> alg)
fin2nat = cata (Nat alg)
where alg :: FinF (Const (:~:) N) n -> Const (:~:) N n
alg FZF = Const Z
alg (FSF (Const n)) = Const (S n)

10
src/Data/Nat.hs
View File

@ -10,7 +10,6 @@ import Quantifier
data N = Z | S N
instance Pi N where
type PiCat N = (->)
data Ty N :: N -> Type where
ZTy :: Ty N 'Z
STy :: Ty N n -> Ty N ('S n)
@ -40,9 +39,10 @@ instance Functor (NTyF r) where
instance Functor NTyF where
type Dom NTyF = Nat (:~:) (->)
type Cod NTyF = Nat (:~:) (->)
map (Nat f) = Nat \_ -> \case
map_ = Sub Dict
map (Nat f) = Nat \case
ZTyF -> ZTyF
(STyF r) -> STyF (f Refl r)
(STyF r) -> STyF (f r)
type instance Base N = Maybe
@ -57,11 +57,11 @@ instance Corecursive N where
type instance Base (Ty N) = NTyF
instance Recursive (Ty N) where
project = Nat \_ -> \case
project = Nat \case
ZTy -> ZTyF
(STy r) -> STyF r
instance Corecursive (Ty N) where
embed = Nat \_ -> \case
embed = Nat \case
ZTyF -> ZTy
(STyF r) -> STy r

4
src/Data/Proxy.hs Normal file
View File

@ -0,0 +1,4 @@
module Data.Proxy where
data Proxy (a :: i) where
Proxy :: Proxy a

21
src/Data/Vec.hs
View File

@ -5,7 +5,7 @@ import Category.Functor.Foldable
import Data.Fin
import Data.Kind (Type)
import Data.Nat
import Quantifier
import Prelude (($))
data Vec a :: N -> Type where
VZ :: Vec a 'Z
@ -23,9 +23,10 @@ instance Functor (Vec a) where
instance Functor Vec where
type Dom Vec = (->)
type Cod Vec = Nat (:~:) (->)
map f = Nat \_ -> \case
map_ = Sub Dict
map f = Nat \case
VZ -> VZ
(VS x r) -> VS (f x) (runNat (map f) Refl r)
(VS x r) -> VS (f x) (runNat (map f) r)
instance Functor (VecF a r) where
type Dom (VecF a r) = (:~:)
@ -35,14 +36,16 @@ instance Functor (VecF a r) where
instance Functor (VecF a) where
type Dom (VecF a) = Nat (:~:) (->)
type Cod (VecF a) = Nat (:~:) (->)
map (Nat f) = Nat \_ -> \case
map_ = Sub Dict
map (Nat f) = Nat \case
VZF -> VZF
(VSF x r) -> VSF x (f Refl r)
(VSF x r) -> VSF x (f r)
instance Functor VecF where
type Dom VecF = (->)
type Cod VecF = Nat (Nat (:~:) (->)) (Nat (:~:) (->))
map f = Nat \_ -> Nat \_ -> \case
map_ = Sub Dict
map f = Nat $ Nat \case
VZF -> VZF
(VSF x r) -> VSF (f x) r
@ -54,9 +57,9 @@ instance Functor (Ixr ty r) where
map Refl x = x
indexer :: Nat (:~:) (->) Fin (Ixr (Vec a) a)
indexer = cata (Nat \_ -> \case
indexer = cata $ Nat \case
FZF -> Ixr \case VS x _ -> x
(FSF (Ixr r)) -> Ixr \case VS x xs -> r xs)
(FSF (Ixr r)) -> Ixr \case VS _ xs -> r xs
index :: Fin n -> Vec a n -> a
index = getIxr . runNat indexer Refl
index = getIxr . runNat indexer

1
src/Quantifier.hs
View File

@ -5,7 +5,6 @@ import Data.Maybe (Maybe (Nothing, Just))
-- | An explicit dependent quantifier.
class Pi (ty :: Type) where
type PiCat ty :: i -> i -> Type
data Ty ty :: ty -> Type
depi :: forall a. Ty ty a -> ty

2
stack.yaml
View File

@ -1,5 +1,5 @@
# Required to use GHC 8.10, which is required for ImportQualifiedPost.
resolver: nightly-2020-10-20
resolver: nightly-2020-10-22
packages:
- .