Universal properties with plain Control.Category

Univ.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}

import Control.Category
import Control.Comonad (Comonad(..))
import Control.Comonad.Cofree
import Control.Monad.Free
import Prelude hiding (id, (.), Functor)
import qualified Prelude as P
import Data.Fix
import Data.Kind
import Data.Functor.Const
import Data.Functor.Kan.Lan
import Data.Functor.Kan.Ran
import Data.Functor.Rep
import Data.Void


type family Obj (c :: k -> k -> Type) (a :: k) :: Constraint
type instance Obj (->) a = ()

class (Category (Dom f), Category (Cod f)) => Functor f where
  type Dom f :: k1 -> k1 -> Type
  type Cod f :: k2 -> k2 -> Type
  map :: Dom f a b -> Cod f (f a) (f b)


class Functor r => InitUniv r a where
  type L r a :: k
  initUnivArr :: d ~ Cod r => d a (r (L r a))
  initUnivProp :: (c ~ Dom r, d ~ Cod r, Obj c b) => d a (r b) -> c (L r a) b

class Functor l => TermUniv l b where
  type R l b :: k
  termUnivArr :: c ~ Cod l => c (l (R l b)) b
  termUnivProp :: (d ~ Dom l, c ~ Cod l, Obj d a) => c (l a) b -> d a (R l b)



data Unit a b where
  Unit :: Unit a b
type instance Obj Unit a = ()
instance Category Unit where
  id = Unit
  Unit . Unit = Unit

data Empty (c :: k -> k -> Type) (a :: k) = Empty
instance Category c => Functor (Empty c) where
  type Dom (Empty c) = c
  type Cod (Empty c) = Unit
  map _ = Unit

instance InitUniv (Empty (->)) a where
  type L (Empty (->)) a = Void
  initUnivArr = Unit
  initUnivProp Unit = absurd

instance TermUniv (Empty (->)) a where
  type R (Empty (->)) a = ()
  termUnivArr = Unit
  termUnivProp Unit _ = ()



type family Fst ab
type instance Fst (a, b) = a
type family Snd ab
type instance Snd (a, b) = b
data (c :**: d) a b where
  (:**:) :: c (Fst a) (Fst b) -> d (Snd a) (Snd b) -> (c :**: d) a b
type instance Obj (c :**: d) a = (Obj c (Fst a), Obj d (Snd a))
instance (Category c, Category d) => Category (c :**: d) where
  id = id :**: id
  (l1 :**: l2) . (r1 :**: r2) = (l1 . r1) :**: (l2 . r2)

type instance Fst (Diag a) = a
type instance Snd (Diag a) = a
newtype Diag a = Diag { getDiag :: a }
instance Functor Diag where
  type Dom Diag = (->)
  type Cod Diag = (->) :**: (->)
  map f = f :**: f

instance InitUniv Diag a where
  type L Diag a = Either (Fst a) (Snd a)
  initUnivArr = Left :**: Right
  initUnivProp (l :**: r) = either l r

instance TermUniv Diag a where
  type R Diag a = (Fst a, Snd a)
  termUnivArr = fst :**: snd
  termUnivProp (l :**: r) b = (l b, r b)


-- | Category of natural transformation with objects being an instance of class `c`.
newtype SubNat c f g = Nat { getNat :: forall a. f a -> g a }
type Nat = SubNat P.Functor
type instance Obj (SubNat c) f = c f
instance Category (SubNat c) where
  id = Nat id
  Nat m . Nat n = Nat (m . n)


instance Functor Const where
  type Dom Const = (->)
  type Cod Const = Nat
  map f = Nat $ Const . f . getConst

newtype Forall f = Forall (forall a. f a)
instance TermUniv Const f where
  type R Const f = Forall f
  termUnivArr = Nat $ \(Const (Forall fa)) -> fa
  termUnivProp (Nat n) a = Forall $ n (Const a)

data Exists f = forall a. Exists (f a)
instance InitUniv Const f where
  type L Const f = Exists f
  initUnivArr = Nat $ \fa -> Const (Exists fa)
  initUnivProp (Nat n) (Exists fa) = getConst (n fa)



type Precompose :: (k1 -> Type) -> (Type -> Type) -> k1 -> Type
newtype Precompose f g a = Precompose { getPrecompose :: g (f a) }
instance Functor (Precompose f) where
  type Dom (Precompose f) = Nat
  type Cod (Precompose f) = Nat
  map (Nat n) = Nat $ Precompose . n . getPrecompose

instance InitUniv (Precompose g) h where
  type L (Precompose g) h = Lan g h
  initUnivArr = Nat $ Precompose . glan
  initUnivProp (Nat n) = Nat $ toLan (getPrecompose . n)

instance TermUniv (Precompose g) h where
  type R (Precompose g) h = Ran g h
  termUnivArr = Nat $ gran . getPrecompose
  termUnivProp (Nat n) = Nat $ toRan (n . Precompose)



newtype SubHask c a b = Mor { getMor :: a -> b }
type instance Obj (SubHask c) a = c a
instance Category (SubHask c) where
  id = Mor id
  Mor f . Mor g = Mor (f . g)


newtype Forget (c :: Type -> Constraint) (a :: Type) = Forget { getForget :: a }
instance Functor (Forget c) where
  type Dom (Forget c) = SubHask c
  type Cod (Forget c) = (->)
  map (Mor f) = Forget . f . getForget

instance InitUniv (Forget Monoid) a where
  type L (Forget Monoid) a = [a]
  initUnivArr = Forget . pure
  initUnivProp f = Mor $ foldMap (getForget . f)



newtype FForget (c :: (Type -> Type) -> Constraint) (m :: Type -> Type) a = FForget { getFForget :: m a }
instance Functor (FForget c) where
  type Dom (FForget c) = SubNat c
  type Cod (FForget c) = Nat
  map (Nat n) = Nat $ FForget . n . getFForget

instance P.Functor f => InitUniv (FForget Monad) f where
  type L (FForget Monad) f = Free f
  initUnivArr = Nat $ FForget . liftF
  initUnivProp (Nat n) = Nat $ foldFree (getFForget . n)

-- The version from `free` requires `f` to be a `Comonad`, defeating the point!
lower :: P.Functor f => Cofree f b -> f b
lower (_ :< as) = fmap extract as

-- Missing from `free`.
unfoldCofree :: Comonad w => (forall x. w x -> f x) -> w a -> Cofree f a
unfoldCofree n w = extract w :< n (extend (unfoldCofree n) w)

instance P.Functor f => TermUniv (FForget Comonad) f where
  type R (FForget Comonad) f = Cofree f
  termUnivArr = Nat $ lower . getFForget
  termUnivProp (Nat n) = Nat $ unfoldCofree (n . FForget)


instance P.Functor f => Functor (Co f) where
  type Dom (Co f) = (->)
  type Cod (Co f) = (->)
  map = P.fmap

instance Representable f => InitUniv (Co f) () where
  type L (Co f) () = Rep f
  initUnivArr () = tabulate id
  initUnivProp f = index (f ())


class FAlg f a where
  alg :: f a -> a
instance FAlg f (Fix f) where
  alg = Fix

instance P.Functor f => InitUniv (Empty (SubHask (FAlg f))) a where
  type L (Empty (SubHask (FAlg f))) a = Fix f
  initUnivArr = Unit
  initUnivProp Unit = Mor $ foldFix alg

class FCoalg f a where
  coalg :: a -> f a
instance FCoalg f (Fix f) where
  coalg = unFix

instance P.Functor f => TermUniv (Empty (SubHask (FCoalg f))) a where
  type R (Empty (SubHask (FCoalg f))) a = Fix f
  termUnivArr = Unit
  termUnivProp Unit = Mor $ unfoldFix coalg