{-# 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.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)@.
deriving instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f)

-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
deriving instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)

-- | @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 :: 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) = f (Fix f) (BinaryProduct (f (Fix f)) x y) x
-> Fix f (BinaryProduct (f (Fix f)) x y) x
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) x x
-> f (Fix f) y y -> f (Fix f) (BinaryProduct (f (Fix f)) x y) x
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 :: 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) = f (Fix f) (BinaryProduct (f (Fix f)) x y) y
-> Fix f (BinaryProduct (f (Fix f)) x y) y
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) x x
-> f (Fix f) y y -> f (Fix f) (BinaryProduct (f (Fix f)) x y) y
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 &&& :: Fix f a x -> Fix f a y -> Fix f a (BinaryProduct (Fix f) x y)
&&& Fix f (Fix f) a y
b = f (Fix f) a (BinaryProduct (f (Fix f)) x y)
-> Fix f a (BinaryProduct (f (Fix f)) x y)
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) a x
a f (Fix f) a x
-> f (Fix f) a y -> f (Fix f) a (BinaryProduct (f (Fix f)) x y)
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 :: 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) = f (Fix f) x (BinaryCoproduct (f (Fix f)) x y)
-> Fix f x (BinaryCoproduct (f (Fix f)) x y)
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) x x
-> f (Fix f) y y -> f (Fix f) x (BinaryCoproduct (f (Fix f)) x y)
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 :: 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) = f (Fix f) y (BinaryCoproduct (f (Fix f)) x y)
-> Fix f y (BinaryCoproduct (f (Fix f)) x y)
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) x x
-> f (Fix f) y y -> f (Fix f) y (BinaryCoproduct (f (Fix f)) x y)
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 ||| :: Fix f x a -> Fix f y a -> Fix f (BinaryCoproduct (Fix f) x y) a
||| Fix f (Fix f) y a
b = f (Fix f) (BinaryCoproduct (f (Fix f)) x y) a
-> Fix f (BinaryCoproduct (f (Fix f)) x y) a
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) x a
a f (Fix f) x a
-> f (Fix f) y a -> f (Fix f) (BinaryCoproduct (f (Fix f)) x y) 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 :: 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) = f (Fix f)
  (BinaryProduct (f (Fix f)) (Exponential (f (Fix f)) y z) y)
  z
-> Fix
     f (BinaryProduct (f (Fix f)) (Exponential (f (Fix f)) y z) y) z
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) y y
-> f (Fix f) z z
-> f (Fix f)
     (BinaryProduct (f (Fix f)) (Exponential (f (Fix f)) y z) y)
     z
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 :: 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) = f (Fix f)
  z
  (Exponential (f (Fix f)) y (BinaryProduct (f (Fix f)) z y))
-> Fix
     f z (Exponential (f (Fix f)) y (BinaryProduct (f (Fix f)) z y))
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) y y
-> f (Fix f) z z
-> f (Fix f)
     z
     (Exponential (f (Fix f)) y (BinaryProduct (f (Fix f)) z y))
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 ^^^ :: 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 = f (Fix f)
  (Exponential (f (Fix f)) y1 z1)
  (Exponential (f (Fix f)) y2 z2)
-> Fix
     f (Exponential (f (Fix f)) y1 z1) (Exponential (f (Fix f)) y2 z2)
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (f (Fix f) z1 z2
a f (Fix f) z1 z2
-> f (Fix f) y2 y1
-> f (Fix f)
     (Exponential (f (Fix f)) y1 z1)
     (Exponential (f (Fix f)) y2 z2)
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 :: * -> * -> *) = 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 % :: 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 = f (Fix f) a b -> Fix f a b
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix f (Fix f) a b
Dom (Wrap (Fix f)) a b
f

data Unwrap (f :: * -> * -> *) = 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 % :: Unwrap (Fix f)
-> Dom (Unwrap (Fix f)) a b
-> Cod (Unwrap (Fix f)) (Unwrap (Fix f) :% a) (Unwrap (Fix f) :% b)
% Fix f = f (Fix f) a b
Cod (Unwrap (Fix f)) (Unwrap (Fix f) :% a) (Unwrap (Fix f) :% 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)
_) = f (Fix f) (Unit t) (Unit t) -> Fix f (Unit t) (Unit t)
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (t -> Obj (Cod t) (Unit t)
forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject t
t)

  leftUnitor :: 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 a) = f (Fix f) (t :% (Unit t, a)) a -> Fix f (t :% (Unit t, a)) a
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (t -> Obj (f (Fix f)) a -> f (Fix f) (t :% (Unit t, a)) a
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (Unit f, a)) a
leftUnitor t
t Obj (f (Fix f)) a
a)
  leftUnitorInv :: 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 a) = f (Fix f) a (t :% (Unit t, a)) -> Fix f a (t :% (Unit t, a))
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (t -> Obj (f (Fix f)) a -> f (Fix f) a (t :% (Unit t, a))
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv t
t Obj (f (Fix f)) a
a)
  rightUnitor :: 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 a) = f (Fix f) (t :% (a, Unit t)) a -> Fix f (t :% (a, Unit t)) a
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (t -> Obj (f (Fix f)) a -> f (Fix f) (t :% (a, Unit t)) a
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitor t
t Obj (f (Fix f)) a
a)
  rightUnitorInv :: 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 a) = f (Fix f) a (t :% (a, Unit t)) -> Fix f a (t :% (a, Unit t))
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (t -> Obj (f (Fix f)) a -> f (Fix f) a (t :% (a, Unit t))
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (a, Unit f))
rightUnitorInv t
t Obj (f (Fix f)) a
a)
  associator :: 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 a) (Fix b) (Fix c) = f (Fix f) (t :% (t :% (a, b), c)) (t :% (a, t :% (b, c)))
-> Fix f (t :% (t :% (a, b), c)) (t :% (a, t :% (b, c)))
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (t
-> Obj (f (Fix f)) a
-> Obj (f (Fix f)) b
-> Obj (f (Fix f)) c
-> f (Fix f) (t :% (t :% (a, b), c)) (t :% (a, t :% (b, c)))
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 Obj (f (Fix f)) a
a Obj (f (Fix f)) b
b Obj (f (Fix f)) c
c)
  associatorInv :: 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 a) (Fix b) (Fix c) = f (Fix f) (t :% (a, t :% (b, c))) (t :% (t :% (a, b), c))
-> Fix f (t :% (a, t :% (b, c))) (t :% (t :% (a, b), c))
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (t
-> Obj (f (Fix f)) a
-> Obj (f (Fix f)) b
-> Obj (f (Fix f)) c
-> f (Fix f) (t :% (a, t :% (b, c))) (t :% (t :% (a, b), c))
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 Obj (f (Fix f)) a
a Obj (f (Fix f)) b
b Obj (f (Fix f)) 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 -> (Void# -> r) -> (Void# -> r) -> r
Z = Fix (DC (I1A U.Unit))
pattern S :: Omega a b -> Omega (S a) (S b)
pattern $bS :: Omega a b -> Omega (S a) (S b)
$mS :: forall r a b.
Omega (S a) (S b) -> (Omega a b -> r) -> (Void# -> r) -> r
S n = Fix (DC (I2A n))
z2s :: Obj Omega n -> Omega Z (S n)
z2s :: Obj Omega n -> Omega Z (S n)
z2s Obj Omega n
n = (:>>:) Unit Omega Z (S n) -> Omega Z (S n)
forall (f :: (* -> * -> *) -> * -> * -> *) a b.
f (Fix f) a b -> Fix f a b
Fix (Cograph (Const (Op Unit :**: Omega) (->) ()) Z (S n)
-> (:>>:) Unit Omega Z (S n)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj Unit ()
-> Obj Omega n
-> Const (Op Unit :**: Omega) (->) ()
-> (Const (Op Unit :**: Omega) (->) () :% ((), n))
-> Cograph (Const (Op Unit :**: Omega) (->) ()) Z (S n)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj Unit ()
U.Unit Obj Omega n
n (Obj (->) () -> Const (Op Unit :**: Omega) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ()))