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

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor
import Data.Category.Limit
import Data.Category.CartesianClosed
import Data.Category.Monoidal

import qualified Data.Category.Unit as U
import Data.Category.Coproduct


newtype Fix f a b = Fix (f (Fix f) a b)

-- | @`Fix` f@ is the fixed point category for a category combinator `f`.
deriving instance Category (f (Fix f)) => Category (Fix f)

-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) where
  type InitialObject (Fix f) = InitialObject (f (Fix f))
  initialObject :: Obj (Fix f) (InitialObject (Fix f))
initialObject = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject
  initialize :: forall a. Obj (Fix f) a -> Fix f (InitialObject (Fix f)) a
initialize (Fix f (Fix f) a a
a) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize f (Fix f) a a
a)

-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) where
  type TerminalObject (Fix f) = TerminalObject (f (Fix f))
  terminalObject :: Obj (Fix f) (TerminalObject (Fix f))
terminalObject = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
  terminate :: forall a. Obj (Fix f) a -> Fix f a (TerminalObject (Fix f))
terminate (Fix f (Fix f) a a
a) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate f (Fix f) a a
a)

-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where
  type BinaryProduct (Fix f) x y = BinaryProduct (f (Fix f)) x y
  proj1 :: forall x y.
Obj (Fix f) x
-> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) x
proj1 (Fix f (Fix f) x x
a) (Fix f (Fix f) y y
b) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 f (Fix f) x x
a f (Fix f) y y
b)
  proj2 :: forall x y.
Obj (Fix f) x
-> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) y
proj2 (Fix f (Fix f) x x
a) (Fix f (Fix f) y y
b) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 f (Fix f) x x
a f (Fix f) y y
b)
  Fix f (Fix f) a x
a &&& :: forall a x y.
Fix f a x -> Fix f a y -> Fix f a (BinaryProduct (Fix f) x y)
&&& Fix f (Fix f) a y
b = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) a x
a forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& f (Fix f) a y
b)

-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where
  type BinaryCoproduct (Fix f) x y = BinaryCoproduct (f (Fix f)) x y
  inj1 :: forall x y.
Obj (Fix f) x
-> Obj (Fix f) y -> Fix f x (BinaryCoproduct (Fix f) x y)
inj1 (Fix f (Fix f) x x
a) (Fix f (Fix f) y y
b) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 f (Fix f) x x
a f (Fix f) y y
b)
  inj2 :: forall x y.
Obj (Fix f) x
-> Obj (Fix f) y -> Fix f y (BinaryCoproduct (Fix f) x y)
inj2 (Fix f (Fix f) x x
a) (Fix f (Fix f) y y
b) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 f (Fix f) x x
a f (Fix f) y y
b)
  Fix f (Fix f) x a
a ||| :: forall x a y.
Fix f x a -> Fix f y a -> Fix f (BinaryCoproduct (Fix f) x y) a
||| Fix f (Fix f) y a
b = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) x a
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| f (Fix f) y a
b)

-- | @Fix f@ inherits its exponentials from @f (Fix f)@.
instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) where
  type Exponential (Fix f) x y = Exponential (f (Fix f)) x y
  apply :: forall y z.
Obj (Fix f) y
-> Obj (Fix f) z
-> Fix f (BinaryProduct (Fix f) (Exponential (Fix f) y z) y) z
apply (Fix f (Fix f) y y
a) (Fix f (Fix f) z z
b) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply f (Fix f) y y
a f (Fix f) z z
b)
  tuple :: forall y z.
Obj (Fix f) y
-> Obj (Fix f) z
-> Fix f z (Exponential (Fix f) y (BinaryProduct (Fix f) z y))
tuple (Fix f (Fix f) y y
a) (Fix f (Fix f) z z
b) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple f (Fix f) y y
a f (Fix f) z z
b)
  Fix f (Fix f) z1 z2
a ^^^ :: forall z1 z2 y2 y1.
Fix f z1 z2
-> Fix f y2 y1
-> Fix f (Exponential (Fix f) y1 z1) (Exponential (Fix f) y2 z2)
^^^ Fix f (Fix f) y2 y1
b = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) z1 z2
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ f (Fix f) y2 y1
b)

data Wrap (f :: Type -> Type -> Type) = Wrap
-- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.
instance Category (f (Fix f)) => Functor (Wrap (Fix f)) where
  type Dom (Wrap (Fix f)) = f (Fix f)
  type Cod (Wrap (Fix f)) = Fix f
  type Wrap (Fix f) :% a = a
  Wrap (Fix f)
Wrap % :: forall a b.
Wrap (Fix f)
-> Dom (Wrap (Fix f)) a b
-> Cod (Wrap (Fix f)) (Wrap (Fix f) :% a) (Wrap (Fix f) :% b)
% Dom (Wrap (Fix f)) a b
f = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix Dom (Wrap (Fix f)) a b
f

data Unwrap (f :: Type -> Type -> Type) = Unwrap
-- | The `Unwrap` functor unwraps @Fix f@ to @f (Fix f)@.
instance Category (f (Fix f)) => Functor (Unwrap (Fix f)) where
  type Dom (Unwrap (Fix f)) = Fix f
  type Cod (Unwrap (Fix f)) = f (Fix f)
  type Unwrap (Fix f) :% a = a
  Unwrap (Fix f)
Unwrap % :: forall a b.
Unwrap (Fix f)
-> Dom (Unwrap (Fix f)) a b
-> Cod (Unwrap (Fix f)) (Unwrap (Fix f) :% a) (Unwrap (Fix f) :% b)
% Fix f (Fix f) a b
f = f (Fix f) a b
f

type WrapTensor f t = Wrap f :.: t :.: (Unwrap f :***: Unwrap f)
-- | @Fix f@ inherits tensor products from @f (Fix f)@.
instance (TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) where
  type Unit (WrapTensor (Fix f) t) = Unit t
  unitObject :: WrapTensor (Fix f) t
-> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t))
unitObject (Wrap (Fix f)
_ :.: t
t :.: Unwrap (Fix f) :***: Unwrap (Fix f)
_) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject t
t)

  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod (WrapTensor (Fix f) t) ~ k) =>
WrapTensor (Fix f) t
-> Obj k a
-> k (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) a
leftUnitor (Wrap (Fix f)
_ :.: t
t :.: Unwrap (Fix f) :***: Unwrap (Fix f)
_) (Fix f (Fix f) a a
a) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (Unit f, a)) a
leftUnitor t
t f (Fix f) a a
a)
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (WrapTensor (Fix f) t) ~ k) =>
WrapTensor (Fix f) t
-> Obj k a
-> k a (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a))
leftUnitorInv (Wrap (Fix f)
_ :.: t
t :.: Unwrap (Fix f) :***: Unwrap (Fix f)
_) (Fix f (Fix f) a a
a) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv t
t f (Fix f) a a
a)
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod (WrapTensor (Fix f) t) ~ k) =>
WrapTensor (Fix f) t
-> Obj k a
-> k (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) a
rightUnitor (Wrap (Fix f)
_ :.: t
t :.: Unwrap (Fix f) :***: Unwrap (Fix f)
_) (Fix f (Fix f) a a
a) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitor t
t f (Fix f) a a
a)
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (WrapTensor (Fix f) t) ~ k) =>
WrapTensor (Fix f) t
-> Obj k a
-> k a (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t)))
rightUnitorInv (Wrap (Fix f)
_ :.: t
t :.: Unwrap (Fix f) :***: Unwrap (Fix f)
_) (Fix f (Fix f) a a
a) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (a, Unit f))
rightUnitorInv t
t f (Fix f) a a
a)
  associator :: forall (k :: * -> * -> *) a b c.
(Cod (WrapTensor (Fix f) t) ~ k) =>
WrapTensor (Fix f) t
-> Obj k a
-> Obj k b
-> Obj k c
-> k (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c))
     (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c)))
associator (Wrap (Fix f)
_ :.: t
t :.: Unwrap (Fix f) :***: Unwrap (Fix f)
_) (Fix f (Fix f) a a
a) (Fix f (Fix f) b b
b) (Fix f (Fix f) c c
c) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
associator t
t f (Fix f) a a
a f (Fix f) b b
b f (Fix f) c c
c)
  associatorInv :: forall (k :: * -> * -> *) a b c.
(Cod (WrapTensor (Fix f) t) ~ k) =>
WrapTensor (Fix f) t
-> Obj k a
-> Obj k b
-> Obj k c
-> k (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c)))
     (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c))
associatorInv (Wrap (Fix f)
_ :.: t
t :.: Unwrap (Fix f) :***: Unwrap (Fix f)
_) (Fix f (Fix f) a a
a) (Fix f (Fix f) b b
b) (Fix f (Fix f) c c
c) = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
associatorInv t
t f (Fix f) a a
a f (Fix f) b b
b f (Fix f) c c
c)

-- | Take the `Omega` category, add a new disctinct object, and an arrow from that object to every object in `Omega`,
--   and you get `Omega` again.
type Omega = Fix ((:>>:) U.Unit)

type Z = I1 ()
type S n = I2 n
pattern Z :: Obj Omega Z
pattern $bZ :: Obj Omega Z
$mZ :: forall {r}. Obj Omega Z -> ((# #) -> r) -> ((# #) -> r) -> r
Z = Fix (DC (I1A U.Unit))
pattern S :: Omega a b -> Omega (S a) (S b)
pattern $bS :: forall a b. Omega a b -> Omega (S a) (S b)
$mS :: forall {r} {a} {b}.
Omega (S a) (S b) -> (Omega a b -> r) -> ((# #) -> r) -> r
S n = Fix (DC (I2A n))
z2s :: Obj Omega n -> Omega Z (S n)
z2s :: forall n. Obj Omega n -> Omega Z (S n)
z2s Obj Omega n
n = forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) a (d :: * -> * -> *) b f.
Obj c a
-> Obj d b -> f -> (f :% (a, b)) -> Cograph c d f (I1 a) (I2 b)
I12 Unit () ()
U.Unit Obj Omega n
n (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ()))