License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.Fix

Description

Synopsis

newtype Fix f a b = Fix (f (Fix f) a b)
data Wrap (f :: Type -> Type -> Type) = Wrap
data Unwrap (f :: Type -> Type -> Type) = Unwrap
type WrapTensor f t = (Wrap f :.: t) :.: (Unwrap f :***: Unwrap f)
type Omega = Fix ((:>>:) Unit)
type Z = I1 ()
type S n = I2 n
pattern Z :: Obj Omega Z
pattern S :: Omega a b -> Omega (S a) (S b)
z2s :: Obj Omega n -> Omega Z (S n)

Documentation

newtype Fix f a b Source #

Constructors

Fix (f (Fix f) a b)

Instances

Instances details

Category (f (Fix f)) => Category (Fix f :: Type -> Type -> Type) Source #	`Fix f` is the fixed point category for a category combinator `f`.
Instance details Defined in Data.Category.Fix Methods src :: forall (a :: k) (b :: k). Fix f a b -> Obj (Fix f) a Source # tgt :: forall (a :: k) (b :: k). Fix f a b -> Obj (Fix f) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Fix f b c -> Fix f a b -> Fix f a c Source #
CartesianClosed (f (Fix f)) => CartesianClosed (Fix f :: Type -> Type -> Type) Source #	`Fix f` inherits its exponentials from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Exponential (Fix f) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (Fix f) y -> Obj (Fix f) z -> Fix f (BinaryProduct (Fix f) (Exponential (Fix f) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (Fix f) y -> Obj (Fix f) z -> Fix f z (Exponential (Fix f) y (BinaryProduct (Fix f) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Fix f z1 z2 -> Fix f y2 y1 -> Fix f (Exponential (Fix f) y1 z1) (Exponential (Fix f) y2 z2) Source #
HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f :: Type -> Type -> Type) Source #	`Fix f` inherits its (co)limits from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type BinaryCoproduct (Fix f) x y :: Kind k Source # Methods inj1 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f x (BinaryCoproduct (Fix f) x y) Source # inj2 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f y (BinaryCoproduct (Fix f) x y) Source # (\|\|\|) :: forall (x :: k) (a :: k) (y :: k). Fix f x a -> Fix f y a -> Fix f (BinaryCoproduct (Fix f) x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Fix f a1 b1 -> Fix f a2 b2 -> Fix f (BinaryCoproduct (Fix f) a1 a2) (BinaryCoproduct (Fix f) b1 b2) Source #
HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f :: Type -> Type -> Type) Source #	`Fix f` inherits its (co)limits from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type BinaryProduct (Fix f) x y :: Kind k Source # Methods proj1 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). Fix f a x -> Fix f a y -> Fix f a (BinaryProduct (Fix f) x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Fix f a1 b1 -> Fix f a2 b2 -> Fix f (BinaryProduct (Fix f) a1 a2) (BinaryProduct (Fix f) b1 b2) Source #
HasInitialObject (f (Fix f)) => HasInitialObject (Fix f :: Type -> Type -> Type) Source #	`Fix f` inherits its (co)limits from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type InitialObject (Fix f) :: Kind k Source # Methods initialObject :: Obj (Fix f) (InitialObject (Fix f)) Source # initialize :: forall (a :: k). Obj (Fix f) a -> Fix f (InitialObject (Fix f)) a Source #
HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f :: Type -> Type -> Type) Source #	`Fix f` inherits its (co)limits from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type TerminalObject (Fix f) :: Kind k Source # Methods terminalObject :: Obj (Fix f) (TerminalObject (Fix f)) Source # terminate :: forall (a :: k). Obj (Fix f) a -> Fix f a (TerminalObject (Fix f)) Source #
Category (f (Fix f)) => Functor (Unwrap (Fix f)) Source #	The `Unwrap` functor unwraps `Fix f` to `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Dom (Unwrap (Fix f)) :: Type -> Type -> Type Source # type Cod (Unwrap (Fix f)) :: Type -> Type -> Type Source # type (Unwrap (Fix f)) :% a Source # Methods (%) :: Unwrap (Fix f) -> Dom (Unwrap (Fix f)) a b -> Cod (Unwrap (Fix f)) (Unwrap (Fix f) :% a) (Unwrap (Fix f) :% b) Source #
Category (f (Fix f)) => Functor (Wrap (Fix f)) Source #	The `Wrap` functor wraps `Fix` around `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Dom (Wrap (Fix f)) :: Type -> Type -> Type Source # type Cod (Wrap (Fix f)) :: Type -> Type -> Type Source # type (Wrap (Fix f)) :% a Source # Methods (%) :: Wrap (Fix f) -> Dom (Wrap (Fix f)) a b -> Cod (Wrap (Fix f)) (Wrap (Fix f) :% a) (Wrap (Fix f) :% b) Source #
(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source #	`Fix f` inherits tensor products from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Unit (WrapTensor (Fix f) t) :: Kind (Cod f) Source # Methods unitObject :: WrapTensor (Fix f) t -> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t)) Source # leftUnitor :: 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 Source # leftUnitorInv :: 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)) Source # rightUnitor :: 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 Source # rightUnitorInv :: 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))) Source # associator :: 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))) Source # associatorInv :: 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)) Source #
type InitialObject (Fix f :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Fix type InitialObject (Fix f :: Type -> Type -> Type) = InitialObject (f (Fix f))
type TerminalObject (Fix f :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Fix type TerminalObject (Fix f :: Type -> Type -> Type) = TerminalObject (f (Fix f))
type Exponential (Fix f :: Type -> Type -> Type) (x :: Kind (Fix f)) (y :: Kind (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Exponential (Fix f :: Type -> Type -> Type) (x :: Kind (Fix f)) (y :: Kind (Fix f)) = Exponential (f (Fix f)) x y
type BinaryCoproduct (Fix f :: Type -> Type -> Type) (x :: Kind (Fix f)) (y :: Kind (Fix f)) Source #
Instance details Defined in Data.Category.Fix type BinaryCoproduct (Fix f :: Type -> Type -> Type) (x :: Kind (Fix f)) (y :: Kind (Fix f)) = BinaryCoproduct (f (Fix f)) x y
type BinaryProduct (Fix f :: Type -> Type -> Type) (x :: Kind (Fix f)) (y :: Kind (Fix f)) Source #
Instance details Defined in Data.Category.Fix type BinaryProduct (Fix f :: Type -> Type -> Type) (x :: Kind (Fix f)) (y :: Kind (Fix f)) = BinaryProduct (f (Fix f)) x y
type Cod (Unwrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Cod (Unwrap (Fix f)) = f (Fix f)
type Cod (Wrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Cod (Wrap (Fix f)) = Fix f
type Dom (Unwrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Dom (Unwrap (Fix f)) = Fix f
type Dom (Wrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Dom (Wrap (Fix f)) = f (Fix f)
type (Unwrap (Fix f)) :% a Source #
Instance details Defined in Data.Category.Fix type (Unwrap (Fix f)) :% a = a
type (Wrap (Fix f)) :% a Source #
Instance details Defined in Data.Category.Fix type (Wrap (Fix f)) :% a = a
type Unit (WrapTensor (Fix f) t) Source #
Instance details Defined in Data.Category.Fix type Unit (WrapTensor (Fix f) t) = Unit t

data Wrap (f :: Type -> Type -> Type) Source #

Constructors

Wrap

Instances

Instances details

Category (f (Fix f)) => Functor (Wrap (Fix f)) Source #	The `Wrap` functor wraps `Fix` around `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Dom (Wrap (Fix f)) :: Type -> Type -> Type Source # type Cod (Wrap (Fix f)) :: Type -> Type -> Type Source # type (Wrap (Fix f)) :% a Source # Methods (%) :: Wrap (Fix f) -> Dom (Wrap (Fix f)) a b -> Cod (Wrap (Fix f)) (Wrap (Fix f) :% a) (Wrap (Fix f) :% b) Source #
(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source #	`Fix f` inherits tensor products from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Unit (WrapTensor (Fix f) t) :: Kind (Cod f) Source # Methods unitObject :: WrapTensor (Fix f) t -> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t)) Source # leftUnitor :: 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 Source # leftUnitorInv :: 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)) Source # rightUnitor :: 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 Source # rightUnitorInv :: 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))) Source # associator :: 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))) Source # associatorInv :: 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)) Source #
type Cod (Wrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Cod (Wrap (Fix f)) = Fix f
type Dom (Wrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Dom (Wrap (Fix f)) = f (Fix f)
type (Wrap (Fix f)) :% a Source #
Instance details Defined in Data.Category.Fix type (Wrap (Fix f)) :% a = a
type Unit (WrapTensor (Fix f) t) Source #
Instance details Defined in Data.Category.Fix type Unit (WrapTensor (Fix f) t) = Unit t

data Unwrap (f :: Type -> Type -> Type) Source #

Constructors

Unwrap

Instances

Instances details

Category (f (Fix f)) => Functor (Unwrap (Fix f)) Source #	The `Unwrap` functor unwraps `Fix f` to `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Dom (Unwrap (Fix f)) :: Type -> Type -> Type Source # type Cod (Unwrap (Fix f)) :: Type -> Type -> Type Source # type (Unwrap (Fix f)) :% a Source # Methods (%) :: Unwrap (Fix f) -> Dom (Unwrap (Fix f)) a b -> Cod (Unwrap (Fix f)) (Unwrap (Fix f) :% a) (Unwrap (Fix f) :% b) Source #
(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source #	`Fix f` inherits tensor products from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Unit (WrapTensor (Fix f) t) :: Kind (Cod f) Source # Methods unitObject :: WrapTensor (Fix f) t -> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t)) Source # leftUnitor :: 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 Source # leftUnitorInv :: 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)) Source # rightUnitor :: 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 Source # rightUnitorInv :: 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))) Source # associator :: 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))) Source # associatorInv :: 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)) Source #
type Cod (Unwrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Cod (Unwrap (Fix f)) = f (Fix f)
type Dom (Unwrap (Fix f)) Source #
Instance details Defined in Data.Category.Fix type Dom (Unwrap (Fix f)) = Fix f
type (Unwrap (Fix f)) :% a Source #
Instance details Defined in Data.Category.Fix type (Unwrap (Fix f)) :% a = a
type Unit (WrapTensor (Fix f) t) Source #
Instance details Defined in Data.Category.Fix type Unit (WrapTensor (Fix f) t) = Unit t

type WrapTensor f t = (Wrap f :.: t) :.: (Unwrap f :***: Unwrap f) Source #

type Omega = Fix ((:>>:) Unit) Source #

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 Z = I1 () Source #

type S n = I2 n Source #

pattern Z :: Obj Omega Z Source #

pattern S :: Omega a b -> Omega (S a) (S b) Source #

z2s :: Obj Omega n -> Omega Z (S n) Source #