Safe Haskell	None
Language	GHC2024

Circuit.Layer

Contents

Free-layer class
Free category
Derived vocabulary

Description

The free-layer / free-forgetful adjunction tower.

Each layer f is a free construction over a base arrow:

run Free — free category
run SMC — free symmetric monoidal category
run Trace — free traced monoidal category (in Circuit.Trace)
run Net — free symmetric monoidal category with bimonoid

Law says what the target category must satisfy to receive a bind fold; Run says what the base category must satisfy for a same-category run; and Bind captures any extra source constraints needed when the free syntax has structural rows.

The hom-set isomorphism is stated once, generically:

  bind h . unit = h              (β)
  bind unit      = id            (η)
  run            = bind id       (coherence, where both sides are defined)

Composition of layers is just nesting — no new operator, no bespoke coherence lemmas.

Synopsis

type Cat2 = Type -> Type -> Type
type (:~>) (arr :: k -> k1 -> Type) (arr' :: k -> k1 -> Type) = forall (x :: k) (y :: k1). arr x y -> arr' x y
class Layer (f :: Cat2 -> Cat2) where
- type Law (f :: Cat2 -> Cat2) (arr' :: Cat2)
- type Run (f :: Cat2 -> Cat2) (arr :: Cat2)
- type Bind (f :: Cat2 -> Cat2) (arr :: Cat2)
- unit :: forall (arr :: Type -> Type -> Type). Category arr => arr :~> f arr
- run :: (Run f arr, Law f arr, Bind f arr) => f arr a b -> arr a b
- bind :: forall arr' (arr :: Cat2) a b. (Law f arr', Bind f arr) => (arr :~> arr') -> f arr a b -> arr' a b
data Free (arr :: k -> k -> Type) (a :: k) (b :: k) where
- Lift :: forall {k} (arr :: k -> k -> Type) (a :: k) (b :: k). arr a b -> Free arr a b
- Compose :: forall {k} (arr :: k -> k -> Type) (b1 :: k) (b :: k) (a :: k). Free arr b1 b -> Free arr a b1 -> Free arr a b
freeze :: forall {k} arr (a :: k) (b :: k). Category arr => Free arr a b -> arr a b
lower :: forall (f :: Cat2 -> Cat2) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type). (Layer f, Category arr) => (f arr :~> arr') -> arr :~> arr'

Free-layer class

type Cat2 = Type -> Type -> Type Source #

The kind of Haskell categories: type-to-type hom-sets.

type (:~>) (arr :: k -> k1 -> Type) (arr' :: k -> k1 -> Type) = forall (x :: k) (y :: k1). arr x y -> arr' x y Source #

An arrow-to-arrow mapping (a natural transformation between profunctors).

class Layer (f :: Cat2 -> Cat2) where Source #

A free construction over a base arrow.

unit includes the generators.
run folds the free syntax back into the same base category.
bind folds the free syntax into any Law-abiding target.

Minimal complete definition

unit, bind

Associated Types

type Law (f :: Cat2 -> Cat2) (arr' :: Cat2) Source #

What the target category must satisfy to receive a bind fold. run only needs the base category's own structure.

type Run (f :: Cat2 -> Cat2) (arr :: Cat2) Source #

What the base category must satisfy to receive a run fold back into itself. Defaults to no extra constraints.

type Run (f :: Cat2 -> Cat2) (arr :: Cat2) = ()

type Bind (f :: Cat2 -> Cat2) (arr :: Cat2) Source #

Extra constraints the source category must satisfy for a bind fold. Defaults to no extra constraints.

type Bind (f :: Cat2 -> Cat2) (arr :: Cat2) = ()

Methods

unit :: forall (arr :: Type -> Type -> Type). Category arr => arr :~> f arr Source #

Include a base arrow as a single generator.

run :: (Run f arr, Law f arr, Bind f arr) => f arr a b -> arr a b Source #

Fold the free syntax into the same base category.

Defaults to bind id, so the single eliminator vocabulary is coherent wherever it type-checks. Instances may still override this with a direct implementation if the weaker constraints of Run do not already imply Law and Bind.

bind :: forall arr' (arr :: Cat2) a b. (Law f arr', Bind f arr) => (arr :~> arr') -> f arr a b -> arr' a b Source #

The universal fold out of the free construction into any Law-abiding target category.

Instances

Instances details

Layer (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) Source #

Layer instance for the free category.

Without object constraints, folding is just recursive application of the target category's composition.

Instance details

Defined in Circuit.Layer

Associated Types

type Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr'
Instance details Defined in Circuit.Layer type Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr' = Category arr'
type Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr
Instance details Defined in Circuit.Layer type Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr = Category arr
type Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr
Instance details Defined in Circuit.Layer type Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr = ()

Methods

unit :: forall (arr :: Type -> Type -> Type). Category arr => arr :~> Free arr Source #

run :: (Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr, Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr, Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr) => Free arr a b -> arr a b Source #

bind :: forall arr' (arr :: Cat2) a b. (Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr', Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr) => (arr :~> arr') -> Free arr a b -> arr' a b Source #

Free symmetric monoidal category with a bimonoid.

Structural rows are interpreted in the target category: parallel composition uses tensor, braiding uses braid, and the bimonoid generators are the images under h of the source dictionaries carried by the SigCopy, SigDiscard, SigPlus, and SigZero constructors.

Conditional: bind h interprets bimonoid generators as images under h of the source arrow's dictionaries. This is the free-PROP fold only when h is a bimonoid homomorphism (automatic for the generator embedding, but must be verified for custom h).

Instance details

Defined in Circuit.Net

Methods

unit :: forall (arr :: Type -> Type -> Type). Category arr => arr :~> Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr Source #

run :: (Run (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr, Law (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr, Bind (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr) => Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr a b -> arr a b Source #

bind :: forall arr' (arr :: Cat2) a b. (Law (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr', Bind (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr) => (arr :~> arr') -> Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr a b -> arr' a b Source #

Free category

data Free (arr :: k -> k -> Type) (a :: k) (b :: k) where Source #

The free category over a base arrow.

The two constructors are Lift, which embeds a base arrow, and Compose, which sequences two free morphisms. The universal fold out of Free is run.

>>> run (Lift (+1) :: Free (->) Int Int) 5
6
>>> run (Compose (Lift (+1)) (Lift (*2)) :: Free (->) Int Int) 5
11

Constructors

Lift :: forall {k} (arr :: k -> k -> Type) (a :: k) (b :: k). arr a b -> Free arr a b	Embed a base arrow.
Compose :: forall {k} (arr :: k -> k -> Type) (b1 :: k) (b :: k) (a :: k). Free arr b1 b -> Free arr a b1 -> Free arr a b	Sequential composition.

Instances

Instances details

Channel t arr => Channel (t :: k -> k -> k) (Free arr :: k -> k -> Type) Source #

Lift the Channel structure through Free.

Instance details

Defined in Circuit.Layer

Methods

assoc :: forall (a :: k) (b :: k) (c :: k). Free arr (t (t a b) c) (t a (t b c)) Source #

assoc' :: forall (a :: k) (b :: k) (c :: k). Free arr (t a (t b c)) (t (t a b) c) Source #

slide :: forall (a :: k) (b :: k) (c :: k). Free arr (t a (t b c)) (t b (t a c)) Source #

Strength t arr => Strength (t :: k -> k -> k) (Free arr :: k -> k -> Type) Source #

Lift the Strength class through Free.

A morphism is frozen before tensoring with the feedback channel.

Instance details

Defined in Circuit.Layer

Methods

strength :: forall (b :: k) (c :: k) (a :: k). Free arr b c -> Free arr (t a b) (t a c) Source #

Traced t arr => Traced (t :: k -> k -> k) (Free arr :: k -> k -> Type) Source #

Lift the Traced class through Free.

A loop body in Free arr is frozen before calling the base trace.

Instance details

Defined in Circuit.Layer

Methods

trace :: forall (a :: k) (b :: k) (c :: k). Free arr (t a b) (t a c) -> Free arr b c Source #

Category arr => Category (Free arr :: k -> k -> Type) Source #

Instance details

Defined in Circuit.Layer

Methods

id :: forall (a :: k). Free arr a a Source #

(.) :: forall (b :: k) (c :: k) (a :: k). Free arr b c -> Free arr a b -> Free arr a c Source #

Layer (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) Source #

Layer instance for the free category.

Without object constraints, folding is just recursive application of the target category's composition.

Instance details

Defined in Circuit.Layer

Associated Types

type Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr'
Instance details Defined in Circuit.Layer type Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr' = Category arr'
type Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr
Instance details Defined in Circuit.Layer type Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr = Category arr
type Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr
Instance details Defined in Circuit.Layer type Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr = ()

Methods

unit :: forall (arr :: Type -> Type -> Type). Category arr => arr :~> Free arr Source #

run :: (Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr, Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr, Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr) => Free arr a b -> arr a b Source #

bind :: forall arr' (arr :: Cat2) a b. (Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr', Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr) => (arr :~> arr') -> Free arr a b -> arr' a b Source #

type Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr Source #

Instance details

Defined in Circuit.Layer

type Bind (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr = ()

type Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr' Source #

Instance details

Defined in Circuit.Layer

type Law (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr' = Category arr'

type Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr Source #

Instance details

Defined in Circuit.Layer

type Run (Free :: (Type -> Type -> Type) -> Type -> Type -> Type) arr = Category arr

freeze :: forall {k} arr (a :: k) (b :: k). Category arr => Free arr a b -> arr a b Source #

Freeze a Free category into its base arrow.

This is a synonym for run Free.

>>> freeze (Lift (+1) :: Free (->) Int Int) 5
6

Derived vocabulary

lower :: forall (f :: Cat2 -> Cat2) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type). (Layer f, Category arr) => (f arr :~> arr') -> arr :~> arr' Source #

The left direction of the hom-set isomorphism: restrict a map out of the free layer to the generators.