{-# 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)@.
deriving instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)
  
-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
deriving instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)

-- | @Fix f@ inherits its exponentials from @f (Fix f)@.
deriving instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f)
  
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 % f = Fix 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 = 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 (_ :.: t :.: _) = Fix (unitObject t)
  
  leftUnitor (_ :.: t :.: _) (Fix a) = Fix (leftUnitor t a)
  leftUnitorInv (_ :.: t :.: _) (Fix a) = Fix (leftUnitorInv t a)
  rightUnitor (_ :.: t :.: _) (Fix a) = Fix (rightUnitor t a)
  rightUnitorInv (_ :.: t :.: _) (Fix a) = Fix (rightUnitorInv t a)
  associator (_ :.: t :.: _) (Fix a) (Fix b) (Fix c) = Fix (associator t a b c)
  associatorInv (_ :.: t :.: _) (Fix a) (Fix b) (Fix c) = Fix (associatorInv t a b 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 Z = Fix (DC (I1A U.Unit))
pattern S :: Omega a b -> Omega (S a) (S b)
pattern S n = Fix (DC (I2A n))
z2s :: Obj Omega n -> Omega Z (S n)
z2s n = Fix (DC (I12 U.Unit n (Const (\() -> ())) ()))