{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | The generic substrate for modular circuit syntax.
--
-- This module holds the à-la-carte machinery: signatures, the free
-- construction over a signature, algebras, and the universal folds. Each
-- concrete language layer ('Circuit.Trace.Trace', 'Circuit.SMC.SMC',
-- 'Circuit.Net.Net', ...) is obtained by choosing a signature sum and adding
-- smart constructors and structural instances on top of this substrate.
--
-- The design is a profunctor-shaped variation of the classic "datatypes à la
-- carte":
--
-- * A 'Sig' is a signature functor indexed by a base arrow @arr@ and a
--   recursive arrow @rec@.
-- * @'Syntax' sig arr@ is the free construction over @sig@ with generators
--   drawn from @arr@.
-- * An 'Algebra' interprets the operations of a signature into a target arrow.
-- * 'evalInto' is the universal fold out of the free construction; 'eval' is
--   the same fold back into the base arrow.
module Circuit.Syntax
  ( -- * Signatures
    Sig,
    (:+:) (..),

    -- * Syntax and algebra
    Syntax (..),
    Algebra (..),
    eval,
    evalInto,

    -- * Sequential composition
    SigCompose (..),

    -- * Free category
    AlgCat,
  )
where

import Circuit.Category (Category (..))
import Circuit.Channel (Channel (..), Strength (..), Traced (..))
import Data.Kind (Constraint, Type)
import Prelude hiding (id, (.))

-- Signature functors

-- | A signature describes a set of constructors for a profunctor.
--
-- * @arr@ — the base arrow (used for constructor constraints)
-- * @rec@ — the recursive arrow type being defined
-- * @a@, @b@ — input and output objects
type Sig = (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type

-- | Coproduct of signatures.
data (sig1 :+: sig2) arr rec a b where
  L :: sig1 arr rec a b -> (sig1 :+: sig2) arr rec a b
  R :: sig2 arr rec a b -> (sig1 :+: sig2) arr rec a b

infixr 6 :+:

-- Free construction over a signature

-- | The free construction over a signature.
data Syntax (sig :: Sig) (arr :: Type -> Type -> Type) a b where
  Lift :: arr a b -> Syntax sig arr a b
  Op :: sig arr (Syntax sig arr) a b -> Syntax sig arr a b

-- | Algebra for a signature. Interprets operations of a signature over
-- source arrow @arr@ into a target arrow @arr'@.
--
-- * @emb@ maps base arrows of the source into the target.
-- * @rec@ maps recursive sub-terms into the target.
class Algebra (sig :: Sig) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type) where
  type Ctx sig arr arr' :: Constraint
  type Ctx sig arr arr' = ()
  alg ::
    (Ctx sig arr arr') =>
    (forall x y. arr x y -> arr' x y) ->
    (forall x y. rec x y -> arr' x y) ->
    sig arr rec a b ->
    arr' a b

-- | Coproduct algebra dispatches to the appropriate component.
instance (Algebra sig1 arr arr', Algebra sig2 arr arr') => Algebra (sig1 :+: sig2) arr arr' where
  type Ctx (sig1 :+: sig2) arr arr' = (Ctx sig1 arr arr', Ctx sig2 arr arr')
  alg :: forall (rec :: * -> * -> *) a b.
Ctx (sig1 :+: sig2) arr arr' =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> (:+:) sig1 sig2 arr rec a b
-> arr' a b
alg forall x y. arr x y -> arr' x y
emb forall x y. rec x y -> arr' x y
rec (L sig1 arr rec a b
op) = (forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> sig1 arr rec a b
-> arr' a b
forall (rec :: * -> * -> *) a b.
Ctx sig1 arr arr' =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> sig1 arr rec a b
-> arr' a b
forall (sig :: Sig) (arr :: * -> * -> *) (arr' :: * -> * -> *)
       (rec :: * -> * -> *) a b.
(Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y) -> sig arr rec a b -> arr' a b
alg arr x y -> arr' x y
forall x y. arr x y -> arr' x y
emb rec x y -> arr' x y
forall x y. rec x y -> arr' x y
rec sig1 arr rec a b
op
  alg forall x y. arr x y -> arr' x y
emb forall x y. rec x y -> arr' x y
rec (R sig2 arr rec a b
op) = (forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> sig2 arr rec a b
-> arr' a b
forall (rec :: * -> * -> *) a b.
Ctx sig2 arr arr' =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> sig2 arr rec a b
-> arr' a b
forall (sig :: Sig) (arr :: * -> * -> *) (arr' :: * -> * -> *)
       (rec :: * -> * -> *) a b.
(Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y) -> sig arr rec a b -> arr' a b
alg arr x y -> arr' x y
forall x y. arr x y -> arr' x y
emb rec x y -> arr' x y
forall x y. rec x y -> arr' x y
rec sig2 arr rec a b
op

-- | Fold a free construction into a target arrow using its algebra.
--
-- The embedding @emb@ maps base arrows of the source into the target.
-- For folding to the same arrow, use 'eval'.
evalInto ::
  (Category arr', Algebra sig arr arr', Ctx sig arr arr') =>
  (forall x y. arr x y -> arr' x y) ->
  Syntax sig arr a b ->
  arr' a b
evalInto :: forall (arr' :: * -> * -> *) (sig :: Sig) (arr :: * -> * -> *) a b.
(Category arr', Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b
evalInto forall x y. arr x y -> arr' x y
emb (Lift arr a b
f) = arr a b -> arr' a b
forall x y. arr x y -> arr' x y
emb arr a b
f
evalInto forall x y. arr x y -> arr' x y
emb (Op sig arr (Syntax sig arr) a b
op) = (forall x y. arr x y -> arr' x y)
-> (forall x y. Syntax sig arr x y -> arr' x y)
-> sig arr (Syntax sig arr) a b
-> arr' a b
forall (rec :: * -> * -> *) a b.
Ctx sig arr arr' =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y) -> sig arr rec a b -> arr' a b
forall (sig :: Sig) (arr :: * -> * -> *) (arr' :: * -> * -> *)
       (rec :: * -> * -> *) a b.
(Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y) -> sig arr rec a b -> arr' a b
alg arr x y -> arr' x y
forall x y. arr x y -> arr' x y
emb ((forall x y. arr x y -> arr' x y) -> Syntax sig arr x y -> arr' x y
forall (arr' :: * -> * -> *) (sig :: Sig) (arr :: * -> * -> *) a b.
(Category arr', Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b
evalInto arr x y -> arr' x y
forall x y. arr x y -> arr' x y
emb) sig arr (Syntax sig arr) a b
op

-- | Fold a free construction into its own base arrow.
eval ::
  (Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
  Syntax sig arr a b ->
  arr a b
eval :: forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval = (forall x y. arr x y -> arr x y) -> Syntax sig arr a b -> arr a b
forall (arr' :: * -> * -> *) (sig :: Sig) (arr :: * -> * -> *) a b.
(Category arr', Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b
evalInto arr x y -> arr x y
forall a. a -> a
forall x y. arr x y -> arr x y
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

-- Sequential composition

-- | Sequential composition.
data SigCompose arr rec a b where
  SigCompose :: rec b c -> rec a b -> SigCompose arr rec a c

instance Algebra SigCompose arr arr' where
  type Ctx SigCompose arr arr' = Category arr'
  alg ::
    forall (rec :: Type -> Type -> Type) (a :: Type) (c :: Type).
    (Ctx SigCompose arr arr') =>
    (forall x y. arr x y -> arr' x y) ->
    (forall x y. rec x y -> arr' x y) ->
    SigCompose arr rec a c ->
    arr' a c
  alg :: forall (rec :: * -> * -> *) a b.
Ctx SigCompose arr arr' =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> SigCompose arr rec a b
-> arr' a b
alg forall x y. arr x y -> arr' x y
_ forall x y. rec x y -> arr' x y
rec (SigCompose @_ @_ @_ @_ @_ rec b c
g rec a b
f) = rec b c -> arr' b c
forall x y. rec x y -> arr' x y
rec rec b c
g arr' b c -> arr' a b -> arr' a c
forall b c a. arr' b c -> arr' a b -> arr' a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. rec a b -> arr' a b
forall x y. rec x y -> arr' x y
rec rec a b
f

-- Common syntax combinations

-- | Free category.
type AlgCat arr = Syntax SigCompose arr

-- Instances for the free category

instance (Category arr) => Category (AlgCat arr) where
  id :: forall a. AlgCat arr a a
id = arr a a -> Syntax SigCompose arr a a
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift arr a a
forall a. arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  AlgCat arr b c
f . :: forall b c a. AlgCat arr b c -> AlgCat arr a b -> AlgCat arr a c
. AlgCat arr a b
g = SigCompose arr (AlgCat arr) a c -> Syntax SigCompose arr a c
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op (AlgCat arr b c -> AlgCat arr a b -> SigCompose arr (AlgCat arr) a c
forall {k} {k} (rec :: k -> k -> *) (b :: k) (c :: k) (a :: k)
       (arr :: k).
rec b c -> rec a b -> SigCompose arr rec a c
SigCompose AlgCat arr b c
f AlgCat arr a b
g)

instance (Category arr, Channel t arr) => Channel t (AlgCat arr) where
  assoc :: forall a b c. AlgCat arr (t (t a b) c) (t a (t b c))
assoc = arr (t (t a b) c) (t a (t b c))
-> Syntax SigCompose arr (t (t a b) c) (t a (t b c))
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift arr (t (t a b) c) (t a (t b c))
forall a b c. arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc
  assoc' :: forall a b c. AlgCat arr (t a (t b c)) (t (t a b) c)
assoc' = arr (t a (t b c)) (t (t a b) c)
-> Syntax SigCompose arr (t a (t b c)) (t (t a b) c)
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift arr (t a (t b c)) (t (t a b) c)
forall a b c. arr (t a (t b c)) (t (t a b) c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'
  slide :: forall a b c. AlgCat arr (t a (t b c)) (t b (t a c))
slide = arr (t a (t b c)) (t b (t a c))
-> Syntax SigCompose arr (t a (t b c)) (t b (t a c))
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift arr (t a (t b c)) (t b (t a c))
forall a b c. arr (t a (t b c)) (t b (t a c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide

instance (Category arr, Strength t arr) => Strength t (AlgCat arr) where
  strength :: forall b c a. AlgCat arr b c -> AlgCat arr (t a b) (t a c)
strength AlgCat arr b c
f = arr (t a b) (t a c) -> Syntax SigCompose arr (t a b) (t a c)
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift (arr b c -> arr (t a b) (t a c)
forall b c a. arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength (AlgCat arr b c -> arr b c
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval AlgCat arr b c
f))

instance (Category arr, Traced t arr) => Traced t (AlgCat arr) where
  trace :: forall a b c. AlgCat arr (t a b) (t a c) -> AlgCat arr b c
trace AlgCat arr (t a b) (t a c)
body = arr b c -> Syntax SigCompose arr b c
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift (arr (t a b) (t a c) -> arr b c
forall a b c. arr (t a b) (t a c) -> arr b c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Traced t arr =>
arr (t a b) (t a c) -> arr b c
trace (AlgCat arr (t a b) (t a c) -> arr (t a b) (t a c)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval AlgCat arr (t a b) (t a c)
body))