Massively improve usability by removing requirement for `Obj` constraints.
Instead, expect `morph a b` to evidence that `a` and `b` are objects,
and use `morph a a` equivalently to how `Obj morph a` was used before.
This results in some redundant parameters in categories in which every
type of a kind is an object ('nice categories', `NiceCat`),
but those can often be avoided with synonyms, and it's far better
than the constraint hell and `Dict`-passing I had to deal with before.
master
parent
d90d3ad679
commit
05ddc84fff
GPG Key ID:
4B7F3DA9351E577C
|
|
@ -1,42 +1,55 @@
|
|||
module Category.Base where
|
||||
-- The default type signatures for `idL` and `idR` trigger
|
||||
-- redundant constraints because `NiceCat` requires `Category`
|
||||
-- but it's forced to require `Category` because that's where it's defined.
|
||||
-- This seems like it might be a bug.
|
||||
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
|
||||
module Category.Base
|
||||
( Category, Obj, idL, idR, (.)
|
||||
, NiceCat, id
|
||||
, Yoneda (Op), Op, getOp
|
||||
) where
|
||||
|
||||
import Data.Dict
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import GHC.Types (Multiplicity)
|
||||
|
||||
-- | A one-parameter typeclass which is always implemented.
|
||||
type Unconst1 :: i -> Constraint
|
||||
class Unconst1 a
|
||||
instance Unconst1 a
|
||||
-- | Objects are uniquely identified by their identity arrow.
|
||||
type Obj :: (i -> i -> j) -> i -> j
|
||||
type Obj morph a = morph a a
|
||||
|
||||
type Category :: forall i. (i -> i -> Type) -> Constraint
|
||||
-- Scoped type variables does not make `i` in scope with standalone kind signatures,
|
||||
-- so this redundant type annotation is necessary.
|
||||
class Category (morph :: i -> i -> Type) where
|
||||
type Obj morph :: i -> Constraint
|
||||
type Obj _morph = Unconst1
|
||||
obj :: morph a b -> Dict (Obj morph a, Obj morph b)
|
||||
default obj :: forall a b. Obj morph ~ Unconst1 => morph a b -> Dict (Obj morph a, Obj morph b)
|
||||
obj _ = Dict
|
||||
class Category morph where
|
||||
idL :: morph a b -> Obj morph a
|
||||
default idL :: NiceCat morph => morph a b -> Obj morph a
|
||||
idL _ = id
|
||||
|
||||
idR :: morph a b -> Obj morph b
|
||||
default idR :: NiceCat morph => morph a b -> Obj morph b
|
||||
idR _ = id
|
||||
|
||||
id :: Obj morph a => morph a a
|
||||
-- | Associative composition of morphisms.
|
||||
(.) :: morph b c -> morph a b -> morph a c
|
||||
|
||||
instance forall (m :: Multiplicity). Category (FUN m) where
|
||||
id = \x -> x
|
||||
type NiceCat :: forall i. (i -> i -> Type) -> Constraint
|
||||
class Category morph => NiceCat morph where
|
||||
id :: Obj morph a
|
||||
|
||||
instance forall m. Category (FUN m) where
|
||||
f . g = \x -> f (g x)
|
||||
|
||||
instance forall m. NiceCat (FUN m) where
|
||||
id = \x -> x
|
||||
|
||||
type Yoneda :: (i -> i -> Type) -> i -> i -> Type
|
||||
newtype Yoneda morph a b = Op { getOp :: morph b a }
|
||||
|
||||
instance Category morph => Category (Yoneda morph) where
|
||||
type Obj (Yoneda morph) = Obj morph
|
||||
obj (Op f) = case obj f of Dict -> Dict
|
||||
id = Op id
|
||||
Op f . Op g = Op (g . f)
|
||||
|
||||
type Op :: (i -> i -> Type) -> i -> i -> Type
|
||||
type family Op morph where
|
||||
Op (Yoneda morph) = morph
|
||||
Op morph = Yoneda morph
|
||||
|
||||
instance Category morph => Category (Yoneda morph) where
|
||||
idL (Op f) = Op (idR f)
|
||||
idR (Op f) = Op (idL f)
|
||||
Op f . Op g = Op (g . f)
|
||||
|
||||
instance NiceCat morph => NiceCat (Yoneda morph) where
|
||||
id = Op id
|
||||
|
|
|
|||
|
|
@ -1,5 +1,8 @@
|
|||
{-# LANGUAGE UndecidableSuperClasses #-}
|
||||
module Category.Constraint where
|
||||
module Category.Constraint
|
||||
( (:-) (Sub), (\\)
|
||||
, ProdC
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
|
|
@ -14,12 +17,13 @@ data (:-) c d = Sub (c => Dict d)
|
|||
r \\ Sub Dict = r
|
||||
|
||||
instance Category (:-) where
|
||||
id = Sub Dict
|
||||
f . g = Sub (Dict \\ f \\ g)
|
||||
|
||||
instance NiceCat (:-) where
|
||||
id = Sub Dict
|
||||
|
||||
instance Functor (Nat (->) (:-)) (Yoneda (:-)) (:-) where
|
||||
map_ _ _ = Dict
|
||||
map (Op (Sub f)) = Nat \(Sub g) -> Sub case f of Dict -> case g of Dict -> Dict
|
||||
map (Op (Sub f)) = Nat \_ (Sub g) -> Sub case f of Dict -> case g of Dict -> Dict
|
||||
|
||||
instance Functor (->) (:-) ((:-) a) where
|
||||
map = (.)
|
||||
|
|
@ -35,17 +39,16 @@ instance (c, d) => ProdC c d
|
|||
-- (up to isomorphism), although I haven't seriously thought about it at all.
|
||||
|
||||
instance Functor (Nat (:-) (:-)) (:-) ProdC where
|
||||
map_ _ _ = Dict
|
||||
map (Sub f) = Nat (Sub case f of Dict -> Dict)
|
||||
map (Sub f) = Nat_ (Sub case f of Dict -> Dict)
|
||||
|
||||
instance Functor (:-) (:-) (ProdC a) where
|
||||
map (Sub f) = Sub case f of Dict -> Dict
|
||||
|
||||
instance Monoidal (:-) ProdC where
|
||||
instance TensorProduct (:-) ProdC where
|
||||
type Unit (:-) ProdC = ()
|
||||
uil = Sub Dict
|
||||
uir = Sub Dict
|
||||
uel = Sub Dict
|
||||
uer = Sub Dict
|
||||
pal = Sub Dict
|
||||
par = Sub Dict
|
||||
prodIL _ = Sub Dict
|
||||
prodIR _ = Sub Dict
|
||||
prodEL _ = Sub Dict
|
||||
prodER _ = Sub Dict
|
||||
prodAL _ _ _ = Sub Dict
|
||||
prodAR _ _ _ = Sub Dict
|
||||
|
|
|
|||
|
|
@ -1,24 +1,18 @@
|
|||
module Category.Enriched where
|
||||
module Category.Enriched
|
||||
( Enriched, eid, ecomp
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Monoidal
|
||||
import Data.Dict
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import GHC.Types (Multiplicity (One))
|
||||
|
||||
class Monoidal over prod => Enriched (over :: j -> j -> Type) prod (morph :: i -> i -> j) where
|
||||
type EObj over prod morph :: i -> Constraint
|
||||
type EObj _over _prod _morph = Unconst1
|
||||
eobj :: proxy prod -> over (Unit over prod) (morph a b) -> Dict (EObj over prod morph a, EObj over prod morph b)
|
||||
default eobj :: forall proxy a b. EObj over prod morph ~ Unconst1 => proxy prod -> over (Unit over prod) (morph a b) -> Dict (EObj over prod morph a, EObj over prod morph b)
|
||||
eobj _ _ = Dict
|
||||
|
||||
eid :: EObj over prod morph a => proxy prod -> over (Unit over prod) (morph a a)
|
||||
type Enriched :: (j -> j -> Type) -> (j -> j -> j) -> (i -> i -> j) -> Constraint
|
||||
class TensorProduct over prod => Enriched over prod morph where
|
||||
eid :: proxy prod -> over (Unit over prod) (Obj morph a)
|
||||
ecomp :: over (prod (morph b c) (morph a b)) (morph a c)
|
||||
|
||||
instance Category morph => Enriched (->) (,) morph where
|
||||
type EObj (->) (,) morph = Obj morph
|
||||
eobj _ f = obj (f ())
|
||||
instance NiceCat morph => Enriched (->) (,) morph where
|
||||
eid _ = \() -> id
|
||||
ecomp = \(f, g) -> f . g
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,15 @@
|
|||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Category.Functor where
|
||||
module Category.Functor
|
||||
( Functor, map
|
||||
, Endo, Endofunctor, endomap
|
||||
, Contravariant, contramap
|
||||
, Bifunctor, bimap, first, second
|
||||
, Profunctor, dimap, lmap, rmap
|
||||
, Nat (Nat), runNat, pattern Nat_, natId
|
||||
, Const (Const), getConst
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Data.Dict
|
||||
import Data.Either (Either (Left, Right))
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
|
|
@ -10,9 +17,6 @@ import Data.Proxy
|
|||
|
||||
type Functor :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> j) -> Constraint
|
||||
class (Category dest, Category src) => Functor dest src f where
|
||||
map_ :: Obj src a => proxy dest -> proxy' src -> Dict (Obj dest (f a))
|
||||
default map_ :: forall proxy proxy' a. Obj dest ~ Unconst1 => proxy dest -> proxy' src -> Dict (Obj dest (f a))
|
||||
map_ _ _ = Dict
|
||||
map :: src a b -> dest (f a) (f b)
|
||||
|
||||
type Endo f a = f a a
|
||||
|
|
@ -31,55 +35,67 @@ instance {-# INCOHERENT #-} Functor dest (Yoneda src) f => Contravariant dest sr
|
|||
instance {-# INCOHERENT #-} Functor dest src f => Contravariant dest (Yoneda src) f where
|
||||
contramap (Op f) = map f
|
||||
|
||||
-- FIXME:
|
||||
-- I'm not convinced this definition is sufficient.
|
||||
-- Don't feel like explaining why. Hopefully it won't be too long before I fix it.
|
||||
-- I'd hate to forget~
|
||||
type Bifunctor :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> i -> j) -> Constraint
|
||||
class (Functor (Nat dest src) src f, forall x. Functor dest src (f x)) => Bifunctor dest src f
|
||||
instance (Functor (Nat dest src) src f, forall x. Functor dest src (f x)) => Bifunctor dest src f
|
||||
bimap :: forall dest src f a b c d. Bifunctor dest src f => src a c -> src b d -> dest (f a b) (f c d)
|
||||
bimap f g = case obj g of Dict -> runNat @_ @_ @dest @src (map f) . map g
|
||||
--first :: forall dest src f a b c d. Bifunctor dest src f => src a b -> dest (f a c) (f b c)
|
||||
--first f = runNat @_ @_ @dest @src (map f)
|
||||
bimap :: Bifunctor dest src f => src a c -> src b d -> dest (f a b) (f c d)
|
||||
bimap f g = runNat (map f) (idR g) . map g
|
||||
-- FIXME: A NiceCat dependency should not be necessary here,
|
||||
-- this most likely means that my definition of Bifunctor is inadequate.
|
||||
first :: forall dest src f a b c. (Bifunctor dest src f, NiceCat src) => src a b -> dest (f a c) (f b c)
|
||||
first f = runNat (map f) (id :: Obj src c)
|
||||
second :: Bifunctor dest src f => src b c -> dest (f a b) (f a c)
|
||||
second g = map g
|
||||
|
||||
type Profunctor :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> i -> j) -> Constraint
|
||||
class (Functor (Nat dest src) (Yoneda src) f, forall x. Functor dest src (f x)) => Profunctor dest src f
|
||||
instance (Functor (Nat dest src) (Yoneda src) f, forall x. Functor dest src (f x)) => Profunctor dest src f
|
||||
dimap :: forall dest src f a b c d. Profunctor dest src f => src a b -> src c d -> dest (f b c) (f a d)
|
||||
dimap f g = case obj g of Dict -> runNat @_ @_ @dest @src (map (Op f)) . map g
|
||||
dimap :: Profunctor dest src f => src a b -> src c d -> dest (f b c) (f a d)
|
||||
dimap f g = runNat (map (Op f)) (idR g) . map g
|
||||
lmap :: forall dest src f a b c. (Profunctor dest src f, NiceCat src) => src a b -> dest (f b c) (f a c)
|
||||
lmap f = runNat (map (Op f)) (id :: Obj src c)
|
||||
rmap :: Profunctor dest src f => src b c -> dest (f a b) (f a c)
|
||||
rmap f = map f
|
||||
|
||||
type Nat :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> j) -> (i -> j) -> Type
|
||||
data Nat dest src f g = (Functor dest src f, Functor dest src g) => Nat { runNat :: !(forall a. Obj src a => dest (f a) (g a)) }
|
||||
data Nat dest src f g = (Functor dest src f, Functor dest src g) => Nat { runNat :: !(forall a. Obj src a -> dest (f a) (g a)) }
|
||||
|
||||
instance Category dest => Category (Nat dest src) where
|
||||
type Obj (Nat dest src) = Functor dest src
|
||||
obj (Nat _) = Dict
|
||||
id :: forall f. Obj (Nat dest src) f => Nat dest src f f
|
||||
id = Nat id'
|
||||
where id' :: forall a. Obj src a => dest (f a) (f a)
|
||||
id' = case map_ (Proxy @dest) (Proxy @src) :: Dict (Obj dest (f a)) of Dict -> id
|
||||
Nat f . Nat g = Nat (f . g)
|
||||
type Nat_' :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> j) -> (i -> j) -> Type
|
||||
data Nat_' dest src f g = (Functor dest src f, Functor dest src g) => Nat_' !(forall a. dest (f a) (g a))
|
||||
|
||||
nat_' :: NiceCat src => Nat dest src f g -> Nat_' dest src f g
|
||||
nat_' (Nat f) = Nat_' (f id)
|
||||
|
||||
pattern Nat_ :: forall dest src f g. NiceCat src => (Functor dest src f, Functor dest src g) => (forall a. dest (f a) (g a)) -> Nat dest src f g
|
||||
{-# COMPLETE Nat_ #-}
|
||||
pattern Nat_ f <- (nat_' -> Nat_' f)
|
||||
where Nat_ f = Nat \_ -> f
|
||||
|
||||
instance Category (Nat dest src) where
|
||||
idL (Nat _) = Nat map
|
||||
idR (Nat _) = Nat map
|
||||
Nat f . Nat g = Nat \x -> (f x . g x)
|
||||
|
||||
natId :: Functor dest src f => Obj (Nat dest src) f
|
||||
natId = Nat map
|
||||
|
||||
instance (forall f. Functor dest src f) => NiceCat (Nat dest src) where
|
||||
id = natId
|
||||
|
||||
instance Functor (->) (FUN m) (FUN m a) where
|
||||
map f = \g -> f . g
|
||||
|
||||
instance Functor (Nat (->) (FUN m)) (Yoneda (FUN m)) (FUN m) where
|
||||
map_ _ _ = Dict
|
||||
map (Op f) = Nat \g -> g . f
|
||||
map (Op f) = Nat \_ g -> g . f
|
||||
|
||||
instance Functor (Nat (FUN m) (FUN m)) (FUN m) (,) where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \(x, y) -> (f x, y)
|
||||
map f = Nat \_ (x, y) -> (f x, y)
|
||||
|
||||
instance Functor (FUN m) (FUN m) ((,) a) where
|
||||
map f = \(x, y) -> (x, f y)
|
||||
|
||||
instance Functor (Nat (FUN m) (FUN m)) (FUN m) Either where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \case
|
||||
map f = Nat \_ -> \case
|
||||
Left y -> Left (f y)
|
||||
Right x -> Right x
|
||||
|
||||
|
|
@ -100,8 +116,7 @@ type Const :: Type -> i -> Type
|
|||
newtype Const a b = Const { getConst :: a }
|
||||
|
||||
instance Functor (Nat (->) (->)) (->) Const where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \(Const x) -> Const (f x)
|
||||
map f = Nat \_ (Const x) -> Const (f x)
|
||||
|
||||
instance {-# INCOHERENT #-} Category src => Functor (->) src (Const a) where
|
||||
map _ = \(Const x) -> Const x
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
module Category.Groupoid where
|
||||
module Category.Groupoid (Groupoid, inv) where
|
||||
|
||||
import Category.Base
|
||||
import Data.Kind (Constraint, Type)
|
||||
|
|
|
|||
|
|
@ -1,10 +1,13 @@
|
|||
module Category.Monoid where
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Category.Monoid
|
||||
( Monoid, empty
|
||||
, (>>=)
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Category.Monoidal
|
||||
import Category.Semigroup
|
||||
import Data.Dict
|
||||
import Data.Kind (Constraint, Type)
|
||||
import Data.Maybe (Maybe (Just))
|
||||
import Data.Proxy
|
||||
|
|
@ -14,9 +17,13 @@ class Semigroup morph prod m => Monoid morph prod m where
|
|||
empty :: proxy morph -> proxy' prod -> morph (Unit morph prod) m
|
||||
|
||||
instance Monoid (Nat (->) (->)) Compose Maybe where
|
||||
empty _ _ = Nat \(Identity x) -> Just x
|
||||
empty _ _ = Nat_ \(Identity x) -> Just x
|
||||
|
||||
-- | A monad is a monoid object in the monoidal category of endofunctors and natural transformations between them!
|
||||
class Monoid (Nat (->) (->)) Compose m => Monad m
|
||||
instance Monoid (Nat (->) (->)) Compose m => Monad m
|
||||
|
||||
(>>=) :: forall f a b. Monoid (Nat (->) (->)) Compose f => f a -> (a -> f b) -> f b
|
||||
m >>= f = runNat (append @_ @(Nat (->) (->))) m'
|
||||
where m' :: Compose f f b
|
||||
m' = case obj (empty @_ @_ @_ @f (Proxy @(Nat (->) (->))) (Proxy @Compose)) of Dict -> Compose (map f m)
|
||||
m >>= f = runNat (append @_ @(Nat (->) (->))) id (lemma (Compose (map f m)))
|
||||
where lemma :: forall c. (Functor (->) (->) f => c) -> c
|
||||
lemma x = case empty (Proxy @(Nat (->) (->))) (Proxy @Compose) :: Nat (->) (->) Identity f of Nat _ -> x
|
||||
|
|
|
|||
|
|
@ -1,58 +1,68 @@
|
|||
module Category.Monoidal where
|
||||
module Category.Monoidal
|
||||
( TensorProduct, Unit, unitObj, prodObj, prodIL, prodIR, prodEL, prodER, prodAL, prodAR
|
||||
, Compose (Compose), getCompose
|
||||
, Identity (Identity), getIdentity
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Data.Dict
|
||||
import Data.Either (Either (Left, Right))
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import Data.Void (Void)
|
||||
|
||||
-- FIXME: Rename this.
|
||||
-- | A category is monoidal if it has a product and a unit for that product.
|
||||
-- A category can have multiple tensor products and be monoidal in multiple ways,
|
||||
-- including the category of types itself,
|
||||
-- so instead of using a @Monoidal@ typeclass, we use a @TensorProduct@ typeclass.
|
||||
-- Only we actually don't, because I haven't had a chance to rename it yet.
|
||||
type Monoidal :: (i -> i -> Type) -> (i -> i -> i) -> Constraint
|
||||
class Endo Bifunctor morph prod => Monoidal (morph :: i -> i -> Type) prod where
|
||||
-- FIXME: Fix all of these garbage names. `uil`? `pal`? seriously?
|
||||
type TensorProduct :: (i -> i -> Type) -> (i -> i -> i) -> Constraint
|
||||
class Endo Bifunctor morph prod => TensorProduct (morph :: i -> i -> Type) prod where
|
||||
type Unit morph prod :: i
|
||||
prodObj :: (Obj morph a, Obj morph b) => proxy morph -> proxy' prod -> proxy'' a -> proxy''' b -> Dict (Obj morph (prod a b))
|
||||
default prodObj :: Obj morph ~ Unconst1 => proxy morph -> proxy' prod -> proxy'' a -> proxy''' b -> Dict (Obj morph (prod a b))
|
||||
prodObj _ _ _ _ = Dict
|
||||
unitObj :: proxy morph -> proxy' prod -> Dict (Obj morph (Unit morph prod))
|
||||
default unitObj :: Obj morph ~ Unconst1 => proxy morph -> proxy' prod -> Dict (Obj morph (Unit morph prod))
|
||||
unitObj _ _ = Dict
|
||||
uil :: Obj morph a => morph a (prod (Unit morph prod) a)
|
||||
uir :: Obj morph a => morph a (prod a (Unit morph prod))
|
||||
uel :: Obj morph a => morph (prod (Unit morph prod) a) a
|
||||
uer :: Obj morph a => morph (prod a (Unit morph prod)) a
|
||||
pal :: (Obj morph a, Obj morph b, Obj morph c) => morph (prod a (prod b c)) (prod (prod a b) c)
|
||||
par :: (Obj morph a, Obj morph b, Obj morph c) => morph (prod (prod a b) c) (prod a (prod b c))
|
||||
-- | The unit is an object.
|
||||
unitObj :: proxy prod -> Obj morph (Unit morph prod)
|
||||
default unitObj :: NiceCat morph => proxy prod -> Obj morph (Unit morph prod)
|
||||
unitObj _ = id
|
||||
|
||||
instance Monoidal (FUN m) (,) where
|
||||
-- | Given two objects, their product is also an object.
|
||||
prodObj :: Obj morph a -> Obj morph b -> Obj morph (prod a b)
|
||||
default prodObj :: NiceCat morph => Obj morph a -> Obj morph b -> Obj morph (prod a b)
|
||||
prodObj _ _ = id
|
||||
|
||||
-- | Introduce a product with the value injected into the left side.
|
||||
prodIL :: Obj morph a -> morph a (prod a (Unit morph prod))
|
||||
-- | Introduce a product with the value injected into the right side.
|
||||
prodIR :: Obj morph a -> morph a (prod (Unit morph prod) a)
|
||||
-- | Eliminate a product with the value projected from the left side.
|
||||
prodEL :: Obj morph a -> morph (prod a (Unit morph prod)) a
|
||||
-- | Eliminate a product with the value projected from the right side.
|
||||
prodER :: Obj morph a -> morph (prod (Unit morph prod) a) a
|
||||
-- | Reassociate a product, nesting it to the left.
|
||||
prodAL :: Obj morph a -> Obj morph b -> Obj morph c -> morph (prod a (prod b c)) (prod (prod a b) c)
|
||||
-- | Reassociate a product, nesting it to the right.
|
||||
prodAR :: Obj morph a -> Obj morph b -> Obj morph c -> morph (prod (prod a b) c) (prod a (prod b c))
|
||||
|
||||
instance TensorProduct (FUN m) (,) where
|
||||
type Unit (FUN m) (,) = ()
|
||||
uil = \x -> ((), x)
|
||||
uir = \x -> (x, ())
|
||||
uel = \((), x) -> x
|
||||
uer = \(x, ()) -> x
|
||||
pal = \(x, (y, z)) -> ((x, y), z)
|
||||
par = \((x, y), z) -> (x, (y, z))
|
||||
prodIL _ = \x -> (x, ())
|
||||
prodIR _ = \x -> ((), x)
|
||||
prodEL _ = \(x, ()) -> x
|
||||
prodER _ = \((), x) -> x
|
||||
prodAL _ _ _ = \(x, (y, z)) -> ((x, y), z)
|
||||
prodAR _ _ _ = \((x, y), z) -> (x, (y, z))
|
||||
|
||||
instance Monoidal (FUN m) Either where
|
||||
instance TensorProduct (FUN m) Either where
|
||||
type Unit (FUN m) Either = Void
|
||||
uil = Right
|
||||
uir = Left
|
||||
uel (Left x) = (\case{}) x
|
||||
uel (Right x) = x
|
||||
uer (Left x) = x
|
||||
uer (Right x) = (\case{}) x
|
||||
pal (Left x) = Left (Left x)
|
||||
pal (Right (Left x)) = Left (Right x)
|
||||
pal (Right (Right x)) = Right x
|
||||
par (Left (Left x)) = Left x
|
||||
par (Left (Right x)) = Right (Left x)
|
||||
par (Right x) = Right (Right x)
|
||||
prodIL _ = Left
|
||||
prodIR _ = Right
|
||||
prodEL _ (Left x) = x
|
||||
prodEL _ (Right x) = (\case{}) x
|
||||
prodER _ (Left x) = (\case{}) x
|
||||
prodER _ (Right x) = x
|
||||
prodAL _ _ _ (Left x) = Left (Left x)
|
||||
prodAL _ _ _ (Right (Left x)) = Left (Right x)
|
||||
prodAL _ _ _ (Right (Right x)) = Right x
|
||||
prodAR _ _ _ (Left (Left x)) = Left x
|
||||
prodAR _ _ _ (Left (Right x)) = Right (Left x)
|
||||
prodAR _ _ _ (Right x) = Right (Right x)
|
||||
|
||||
data Compose f g x = (Functor (->) (->) f, Functor (->) (->) g) => Compose { getCompose :: !(f (g x)) }
|
||||
newtype Identity x = Identity { getIdentity :: x }
|
||||
|
|
@ -60,24 +70,22 @@ newtype Identity x = Identity { getIdentity :: x }
|
|||
instance Functor (FUN m) (FUN m) Identity where
|
||||
map f = \(Identity x) -> Identity (f x)
|
||||
|
||||
instance Functor (->) (->) (Compose f g) where
|
||||
map f = \(Compose x) -> Compose (map @_ @_ @(->) @(->) (map f) x)
|
||||
|
||||
instance Functor (Nat (Nat (->) (->)) (Nat (->) (->))) (Nat (->) (->)) Compose where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat (Nat \(Compose x) -> Compose (f x))
|
||||
map (Nat f) = Nat \(Nat _) -> Nat \_ (Compose x) -> Compose (f id x)
|
||||
|
||||
instance Functor (Nat (->) (->)) (Nat (->) (->)) (Compose f) where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat \(Compose x) -> Compose (map f x)
|
||||
map (Nat f) = Nat \_ (Compose x) -> Compose (map (f id) x)
|
||||
|
||||
instance Monoidal (Nat (->) (->)) Compose where
|
||||
instance Functor (->) (->) (Compose (f :: Type -> Type) g) where
|
||||
map f = \(Compose x) -> Compose (map @_ @_ @_ @(->) (map f) x)
|
||||
|
||||
instance TensorProduct (Nat (->) (->)) Compose where
|
||||
type Unit (Nat (->) (->)) Compose = Identity
|
||||
prodObj _ _ _ _ = Dict
|
||||
unitObj _ _ = Dict
|
||||
uil = Nat \x -> Compose (Identity x)
|
||||
uir = Nat \x -> Compose (map Identity x)
|
||||
uel = Nat \(Compose (Identity x)) -> x
|
||||
uer = Nat \(Compose x) -> map getIdentity x
|
||||
pal = Nat \(Compose x) -> Compose (Compose (map getCompose x))
|
||||
par = Nat \(Compose (Compose x)) -> Compose (map Compose x)
|
||||
unitObj _ = natId
|
||||
prodObj _ _ = natId
|
||||
prodIL (Nat _) = Nat_ \x -> Compose (map Identity x)
|
||||
prodIR (Nat _) = Nat_ \x -> Compose (Identity x)
|
||||
prodEL (Nat _) = Nat_ \(Compose x) -> map getIdentity x
|
||||
prodER (Nat _) = Nat_ \(Compose (Identity x)) -> x
|
||||
prodAL (Nat _) (Nat _) (Nat _) = Nat_ \(Compose x) -> Compose (Compose (map getCompose x))
|
||||
prodAR (Nat _) (Nat _) (Nat _) = Nat_ \(Compose (Compose x)) -> Compose (map Compose x)
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
module Category.Semigroup where
|
||||
module Category.Semigroup (Semigroup, append) where
|
||||
|
||||
import Category.Functor
|
||||
import Category.Monoidal
|
||||
|
|
@ -6,11 +6,11 @@ import Data.Kind (Constraint, Type)
|
|||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
|
||||
type Semigroup :: (i -> i -> Type) -> (i -> i -> i) -> i -> Constraint
|
||||
class Monoidal morph prod => Semigroup morph prod s where
|
||||
class TensorProduct morph prod => Semigroup morph prod s where
|
||||
append :: morph (prod s s) s
|
||||
|
||||
instance Semigroup (Nat (->) (->)) Compose Maybe where
|
||||
append = Nat \(Compose x') -> case x' of
|
||||
append = Nat \_ (Compose x') -> case x' of
|
||||
Nothing -> Nothing
|
||||
Just Nothing -> Nothing
|
||||
Just (Just x) -> Just x
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
module Data.Dict where
|
||||
module Data.Dict (Dict (Dict)) where
|
||||
|
||||
import Data.Kind (Constraint, Type)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,11 @@
|
|||
module Data.Fin where
|
||||
module Data.Fin
|
||||
( Fin (FZ, FS)
|
||||
, FinF (FZF, FSF)
|
||||
, fin2nat
|
||||
) where
|
||||
|
||||
import Category.Functor
|
||||
import Category.Functor.Foldable
|
||||
import Data.Dict
|
||||
import Data.Identity
|
||||
import Data.Kind (Type)
|
||||
import Data.Nat
|
||||
|
|
@ -16,24 +19,23 @@ data FinF r :: N -> Type where
|
|||
type instance Base Fin = FinF
|
||||
|
||||
instance Functor (Nat (->) (:~:)) (Nat (->) (:~:)) FinF where
|
||||
map_ _ _ = 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 r)
|
||||
|
||||
instance Recursive (Nat (->) (:~:)) Fin where
|
||||
project = Nat \case
|
||||
project = Nat_ \case
|
||||
FZ -> FZF
|
||||
(FS r) -> FSF r
|
||||
|
||||
instance Corecursive (Nat (->) (:~:)) 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)
|
||||
|
|
|
|||
|
|
@ -1,9 +1,8 @@
|
|||
module Data.Identity where
|
||||
module Data.Identity ((:~:) (Refl)) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Category.Groupoid
|
||||
import Data.Dict
|
||||
import Data.Kind (Type)
|
||||
|
||||
type (:~:) :: i -> i -> Type
|
||||
|
|
@ -11,9 +10,11 @@ data (:~:) :: i -> i -> Type where
|
|||
Refl :: a :~: a
|
||||
|
||||
instance Category (:~:) where
|
||||
id = Refl
|
||||
Refl . Refl = Refl
|
||||
|
||||
instance NiceCat (:~:) where
|
||||
id = Refl
|
||||
|
||||
instance Groupoid (:~:) where
|
||||
inv Refl = Refl
|
||||
|
||||
|
|
@ -25,9 +26,7 @@ instance {-# INCOHERENT #-} Functor (->) (Yoneda (:~:)) f where
|
|||
map (Op Refl) = id
|
||||
|
||||
instance {-# INCOHERENT #-} Functor (Nat (->) (:~:)) (:~:) f where
|
||||
map_ _ _ = Dict
|
||||
map Refl = id
|
||||
|
||||
instance {-# INCOHERENT #-} Functor (Nat (->) (:~:)) (Yoneda (:~:)) f where
|
||||
map_ _ _ = Dict
|
||||
map (Op Refl) = id
|
||||
|
|
|
|||
|
|
@ -1,5 +1,10 @@
|
|||
-- | The natural numbers and associated types and functions.
|
||||
module Data.Nat where
|
||||
module Data.Nat
|
||||
( N (Z, S), inf
|
||||
, NTyF (ZTyF, STyF)
|
||||
, (:+)
|
||||
, injective, rightZero
|
||||
) where
|
||||
|
||||
import Category.Functor
|
||||
import Category.Functor.Foldable
|
||||
|
|
@ -42,8 +47,7 @@ data NTyF r n where
|
|||
STyF :: r n -> NTyF r ('S n)
|
||||
|
||||
instance Functor (Nat (->) (:~:)) (Nat (->) (:~:)) NTyF where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat \case
|
||||
map (Nat_ f) = Nat_ \case
|
||||
ZTyF -> ZTyF
|
||||
(STyF r) -> STyF (f r)
|
||||
|
||||
|
|
@ -60,12 +64,12 @@ instance Corecursive (->) N where
|
|||
type instance Base (Ty N) = NTyF
|
||||
|
||||
instance Recursive (Nat (->) (:~:)) (Ty N) where
|
||||
project = Nat \case
|
||||
project = Nat_ \case
|
||||
ZTy -> ZTyF
|
||||
(STy r) -> STyF r
|
||||
|
||||
instance Corecursive (Nat (->) (:~:)) (Ty N) where
|
||||
embed = Nat \case
|
||||
embed = Nat_ \case
|
||||
ZTyF -> ZTy
|
||||
(STyF r) -> STy r
|
||||
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@
|
|||
-- and doesn't let you control which arguments are implicit and which are explicit.
|
||||
--
|
||||
-- 'Proxy' provides a better alternative for passing explicit type arguments.
|
||||
module Data.Proxy where
|
||||
module Data.Proxy (Proxy (Proxy)) where
|
||||
|
||||
import Data.Kind (Type)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,9 +1,12 @@
|
|||
module Data.Vec where
|
||||
module Data.Vec
|
||||
( Vec (VZ, VS)
|
||||
, VecF (VZF, VSF)
|
||||
, index
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Category.Functor.Foldable
|
||||
import Data.Dict
|
||||
import Data.Fin
|
||||
import Data.Identity
|
||||
import Data.Kind (Type)
|
||||
|
|
@ -21,20 +24,17 @@ data VecF a r :: N -> Type where
|
|||
type instance Base (Vec a) = VecF a
|
||||
|
||||
instance Functor (Nat (->) (:~:)) (->) Vec where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \case
|
||||
map f = Nat_ \case
|
||||
VZ -> VZ
|
||||
(VS x r) -> VS (f x) (runNat (map @_ @_ @(Nat (->) (:~:)) f) r)
|
||||
(VS x r) -> VS (f x) (runNat (map @_ @_ @(Nat (->) (:~:)) f) id r)
|
||||
|
||||
instance Functor (Nat (->) (:~:)) (Nat (->) (:~:)) (VecF a) where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat \case
|
||||
map (Nat_ f) = Nat_ \case
|
||||
VZF -> VZF
|
||||
(VSF x r) -> VSF x (f r)
|
||||
|
||||
instance Functor (Nat (Nat (->) (:~:)) (Nat (->) (:~:))) (->) VecF where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat $ Nat \case
|
||||
map f = Nat_ $ Nat_ \case
|
||||
VZF -> VZF
|
||||
(VSF x r) -> VSF (f x) r
|
||||
|
||||
|
|
@ -42,9 +42,9 @@ type Ixr :: (N -> Type) -> Type -> N -> Type
|
|||
newtype Ixr ty r a = Ixr { getIxr :: ty a -> r }
|
||||
|
||||
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 _ xs -> r xs
|
||||
|
||||
index :: Fin n -> Vec a n -> a
|
||||
index = getIxr . runNat indexer
|
||||
index = getIxr . runNat indexer id
|
||||
|
|
|
|||
|
|
@ -23,7 +23,11 @@
|
|||
--
|
||||
-- This technique was first described in [Conor McBride's Hasochism paper](https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf);
|
||||
-- the idea to make a `Pi` typeclass was my own, but I'm sure it's been done before.
|
||||
module Quantifier where
|
||||
module Quantifier
|
||||
( Forall (Forall), runForall
|
||||
, Pi, Ty, depi
|
||||
, PiC, TyC, depic
|
||||
) where
|
||||
|
||||
import Data.Kind (Constraint, Type)
|
||||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
|
|
|
|||
Loading…
Reference in New Issue