WeightedLimit.hs

{-# LANGUAGE TypeOperators, RankNTypes, GADTs, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, NoImplicitPrelude, FlexibleContexts #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.WeightedLimit
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.WeightedLimit where

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor
import Data.Category.Product
import Data.Category.NaturalTransformation
import qualified Data.Category.Limit as L


type WeightedCone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d e (d :% a)

-- | @w@-weighted limits in the category @k@.
class (Functor w, Cod w ~ (->), Category k) => HasWLimits k w where
  type WeightedLimit k w d :: Type
  limitObj :: FunctorOf (Dom w) k d => w -> d -> Obj k (WLimit w d)
  limit :: FunctorOf (Dom w) k d => w -> d -> WeightedCone w d (WLimit w d)
  limitFactorizer :: FunctorOf (Dom w) k d => w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)

type WLimit w d = WeightedLimit (Cod d) w d

data LimitFunctor (k :: Type -> Type -> Type) w = LimitFunctor w
instance HasWLimits k w => Functor (LimitFunctor k w) where
  type Dom (LimitFunctor k w) = Nat (Dom w) k
  type Cod (LimitFunctor k w) = k
  type LimitFunctor k w :% d = WeightedLimit k w d

  LimitFunctor w % Nat d d' n = limitFactorizer w d' (limitObj w d) (\a wa -> n a . limit w d a wa)


-- | Regular limits as weigthed limits, weighted by the constant functor to '()'.
instance L.HasLimits j k => HasWLimits k (Const j (->) ()) where
  type WeightedLimit k (Const j (->) ()) d = L.Limit d
  limitObj Const{} d = L.coneVertex (L.limit (natId d))
  limit Const{} d a () = L.limit (natId d) ! a
  limitFactorizer Const{} d e f = L.limitFactorizer (Nat (Const e) d (`f` ()))


class Category v => HasEnds v where
  type End (v :: Type -> Type -> Type) t :: Type
  end :: FunctorOf (Op k :**: k) v t => t -> Obj v (End v t)
  endCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (End v t) (t :% (a, a))
  endFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)

-- | Ends as Hom-weighted limits
instance HasEnds k => HasWLimits k (Hom k) where
  type WeightedLimit k (Hom k) d = End k d
  limitObj Hom d = end d
  limit Hom d (Op a :**: _) ab = d % (Op a :**: ab) . endCounit d a
  limitFactorizer Hom d _ f = endFactorizer d (\a -> f (Op a :**: a) a)

data EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = EndFunctor
instance (HasEnds v, Category k) => Functor (EndFunctor k v) where
  type Dom (EndFunctor k v) = Nat (Op k :**: k) v
  type Cod (EndFunctor k v) = v
  type EndFunctor k v :% t = End v t

  EndFunctor % Nat f g n = endFactorizer g (\a -> n (Op a :**: a) . endCounit f a)

newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) }
instance HasEnds (->) where
  type End (->) t = HaskEnd t
  end _ e = e
  endCounit t a (HaskEnd f) = f t a
  endFactorizer _ e x = HaskEnd (\_ a -> e a x)


type WeightedCocone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d (d :% a) e

-- | @w@-weighted colimits in the category @k@.
class (Functor w, Cod w ~ (->), Category k) => HasWColimits k w where
  type WeightedColimit k w d :: Type
  colimitObj :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k (WColimit w d)
  colimit :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> WeightedCocone w d (WColimit w d)
  colimitFactorizer :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e

type WColimit w d = WeightedColimit (Cod d) w d

data ColimitFunctor (k :: Type -> Type -> Type) w = ColimitFunctor w
instance (Functor w, Category k, HasWColimits k (w :.: OpOp (Dom w))) => Functor (ColimitFunctor k w) where
  type Dom (ColimitFunctor k w) = Nat (Op (Dom w)) k
  type Cod (ColimitFunctor k w) = k
  type ColimitFunctor k w :% d = WeightedColimit k (w :.: OpOp (Dom w)) d

  ColimitFunctor w % Nat d d' n = colimitFactorizer (w :.: OpOp) d (colimitObj (w :.: OpOp) d') (\(Op a) wa -> colimit (w :.: OpOp) d' (Op a) wa . n a)


-- | Regular colimits as weigthed colimits, weighted by the constant functor to '()'.
instance L.HasColimits j k => HasWColimits k (Const (Op j) (->) ()) where
  type WeightedColimit k (Const (Op j) (->) ()) d = L.Colimit d
  colimitObj (Const _) d = L.coconeVertex (L.colimit (natId d))
  colimit (Const _) d (Op a) () = L.colimit (natId d) ! a
  colimitFactorizer (Const _) d e f = L.colimitFactorizer (Nat d (Const e) (\z -> f (Op z) ()))


class Category v => HasCoends v where
  type Coend (v :: Type -> Type -> Type) t :: Type
  coend :: FunctorOf (Op k :**: k) v t => t -> Obj v (Coend v t)
  coendCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (t :% (a, a)) (Coend v t)
  coendFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x

data OpHom (k :: Type -> Type -> Type) = OpHom
-- | The Hom-functor but with opposite domain.
instance Category k => Functor (OpHom k) where
  type Dom (OpHom k) = Op (Op k :**: k)
  type Cod (OpHom k) = (->)
  type OpHom k :% (a1, a2) = k a2 a1
  OpHom % Op (Op f1 :**: f2) = \g -> f1 . g . f2

-- | Coends as OpHom-weighted colimits
instance HasCoends k => HasWColimits k (OpHom k) where
  type WeightedColimit k (OpHom k) d = Coend k d
  colimitObj OpHom d = coend d
  colimit OpHom d (Op (Op a :**: _)) ab = coendCounit d a . d % (Op a :**: ab)
  colimitFactorizer OpHom d _ f = coendFactorizer d (\a -> f (Op (Op a :**: a)) a)

data CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = CoendFunctor
instance (HasCoends v, Category k) => Functor (CoendFunctor k v) where
  type Dom (CoendFunctor k v) = Nat (Op k :**: k) v
  type Cod (CoendFunctor k v) = v
  type CoendFunctor k v :% t = Coend v t

  CoendFunctor % Nat f g n = coendFactorizer f (\a -> coendCounit g a . n (Op a :**: a))

data HaskCoend t where
  HaskCoend :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) -> HaskCoend t
instance HasCoends (->) where
  type Coend (->) t = HaskCoend t
  coend _ e = e
  coendCounit t a taa = HaskCoend t a taa
  coendFactorizer _ f (HaskCoend _ a taa) = f a taa