{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Finite-dimensional linear relations over GF(2).
--
-- This is a reference semantics for boolean signal-flow graphs: objects are
-- natural numbers (encoded as 'FinObj'), morphisms are GF(2)-linear relations
-- presented as the row space of a matrix with @(n+m)@ columns.
--
-- Values are 'Bool', addition is @xor@, multiplication is '&&'.  The category
-- carries the cartesian monoidal structure @(,)@, is traced, and supports the
-- copy/discard/plus/zero generators that 'Circuit.Net' uses for wiring.
--
-- This module is intentionally small and self-contained: it is the minimal
-- reference category needed to decide equality on wiring diagrams over a two-
-- element field.
module Circuit.FinRel
  ( -- * Objects
    FinObj (..),
    KnownDim (..),

    -- * Morphisms
    FinRel (..),

    -- * Smart constructors
    finId,
    compFinRel,
    parFinRel,
    unitlFinRel,
    unitl'FinRel,
    unitrFinRel,
    unitr'FinRel,
    swapFinRel,
    assocFinRel,
    assoc'FinRel,
    slideFinRel,
    strengthFinRel,
    traceFinRel,
    finCopy,
    finDiscard,
    finPlus,
    finZero,
    finScalar,
    wiring,
  )
where

import Circuit.Bimonoid (Copy (..), Discard (..), Merge (..), Zero (..))
import Circuit.Category (Category (..), (.>))
import Data.Kind (Type)
import Data.List (findIndex, foldl', transpose)
import Data.Maybe (listToMaybe, mapMaybe)
import Data.Proxy (Proxy (..))
import GHC.TypeNats (KnownNat, Nat, natVal)
import Prelude hiding (id, (.))

-- * GF(2) arithmetic

-- | Addition in GF(2) is exclusive-or.
gf2add :: Bool -> Bool -> Bool
gf2add :: Bool -> Bool -> Bool
gf2add = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)

-- | Multiplication in GF(2) is conjunction.
gf2mul :: Bool -> Bool -> Bool
gf2mul :: Bool -> Bool -> Bool
gf2mul = Bool -> Bool -> Bool
(&&)

-- | Additive unit of GF(2).
gf2zero :: Bool
gf2zero :: Bool
gf2zero = Bool
False

-- | Multiplicative unit of GF(2).
gf2one :: Bool
gf2one :: Bool
gf2one = Bool
True

-- | Additive inverse in GF(2) is the identity.
gf2neg :: Bool -> Bool
gf2neg :: Bool -> Bool
gf2neg = Bool -> Bool
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

-- | Multiplicative inverse in GF(2) is the identity.
gf2inv :: Bool -> Bool
gf2inv :: Bool -> Bool
gf2inv = Bool -> Bool
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

-- * Objects

-- | Object token for a finite-dimensional space of dimension @n@.
data FinObj (n :: Nat) = FinObj
  deriving (FinObj n -> FinObj n -> Bool
(FinObj n -> FinObj n -> Bool)
-> (FinObj n -> FinObj n -> Bool) -> Eq (FinObj n)
forall (n :: Nat). FinObj n -> FinObj n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). FinObj n -> FinObj n -> Bool
== :: FinObj n -> FinObj n -> Bool
$c/= :: forall (n :: Nat). FinObj n -> FinObj n -> Bool
/= :: FinObj n -> FinObj n -> Bool
Eq, Eq (FinObj n)
Eq (FinObj n) =>
(FinObj n -> FinObj n -> Ordering)
-> (FinObj n -> FinObj n -> Bool)
-> (FinObj n -> FinObj n -> Bool)
-> (FinObj n -> FinObj n -> Bool)
-> (FinObj n -> FinObj n -> Bool)
-> (FinObj n -> FinObj n -> FinObj n)
-> (FinObj n -> FinObj n -> FinObj n)
-> Ord (FinObj n)
FinObj n -> FinObj n -> Bool
FinObj n -> FinObj n -> Ordering
FinObj n -> FinObj n -> FinObj n
forall (n :: Nat). Eq (FinObj n)
forall (n :: Nat). FinObj n -> FinObj n -> Bool
forall (n :: Nat). FinObj n -> FinObj n -> Ordering
forall (n :: Nat). FinObj n -> FinObj n -> FinObj n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Nat). FinObj n -> FinObj n -> Ordering
compare :: FinObj n -> FinObj n -> Ordering
$c< :: forall (n :: Nat). FinObj n -> FinObj n -> Bool
< :: FinObj n -> FinObj n -> Bool
$c<= :: forall (n :: Nat). FinObj n -> FinObj n -> Bool
<= :: FinObj n -> FinObj n -> Bool
$c> :: forall (n :: Nat). FinObj n -> FinObj n -> Bool
> :: FinObj n -> FinObj n -> Bool
$c>= :: forall (n :: Nat). FinObj n -> FinObj n -> Bool
>= :: FinObj n -> FinObj n -> Bool
$cmax :: forall (n :: Nat). FinObj n -> FinObj n -> FinObj n
max :: FinObj n -> FinObj n -> FinObj n
$cmin :: forall (n :: Nat). FinObj n -> FinObj n -> FinObj n
min :: FinObj n -> FinObj n -> FinObj n
Ord, Int -> FinObj n -> ShowS
[FinObj n] -> ShowS
FinObj n -> String
(Int -> FinObj n -> ShowS)
-> (FinObj n -> String) -> ([FinObj n] -> ShowS) -> Show (FinObj n)
forall (n :: Nat). Int -> FinObj n -> ShowS
forall (n :: Nat). [FinObj n] -> ShowS
forall (n :: Nat). FinObj n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat). Int -> FinObj n -> ShowS
showsPrec :: Int -> FinObj n -> ShowS
$cshow :: forall (n :: Nat). FinObj n -> String
show :: FinObj n -> String
$cshowList :: forall (n :: Nat). [FinObj n] -> ShowS
showList :: [FinObj n] -> ShowS
Show)

-- | Dimension evidence for objects closed under the @(,)@ tensor.
--
-- @()@ has dimension 0, 'FinObj n' has dimension @n@, and pairs add.
class KnownDim a where
  dimVal :: Proxy a -> Int

instance KnownDim () where
  dimVal :: Proxy () -> Int
dimVal Proxy ()
_ = Int
0

instance (KnownNat n) => KnownDim (FinObj n) where
  dimVal :: Proxy (FinObj n) -> Int
dimVal Proxy (FinObj n)
_ = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))

instance (KnownDim a, KnownDim b) => KnownDim (a, b) where
  dimVal :: Proxy (a, b) -> Int
dimVal Proxy (a, b)
_ = Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy b -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)

-- * Morphisms

-- | A GF(2)-linear relation @n -> m@.
--
-- Internally a matrix whose rows span the relation:
--
-- @
--   { (take n v, drop n v) | v in row space }
-- @
--
-- The stored dimensions are trusted; the matrix is kept in reduced row
-- echelon form for canonical equality.
data FinRel (n :: Type) (m :: Type) = FinRel
  { forall n m. FinRel n m -> Int
finInDim :: !Int,
    forall n m. FinRel n m -> Int
finOutDim :: !Int,
    forall n m. FinRel n m -> [[Bool]]
finMat :: ![[Bool]]
  }
  deriving (Int -> FinRel n m -> ShowS
[FinRel n m] -> ShowS
FinRel n m -> String
(Int -> FinRel n m -> ShowS)
-> (FinRel n m -> String)
-> ([FinRel n m] -> ShowS)
-> Show (FinRel n m)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n m. Int -> FinRel n m -> ShowS
forall n m. [FinRel n m] -> ShowS
forall n m. FinRel n m -> String
$cshowsPrec :: forall n m. Int -> FinRel n m -> ShowS
showsPrec :: Int -> FinRel n m -> ShowS
$cshow :: forall n m. FinRel n m -> String
show :: FinRel n m -> String
$cshowList :: forall n m. [FinRel n m] -> ShowS
showList :: [FinRel n m] -> ShowS
Show)

instance Eq (FinRel n m) where
  FinRel Int
_ Int
_ [[Bool]]
m1 == :: FinRel n m -> FinRel n m -> Bool
== FinRel Int
_ Int
_ [[Bool]]
m2 = [[Bool]] -> [[Bool]]
rref [[Bool]]
m1 [[Bool]] -> [[Bool]] -> Bool
forall a. Eq a => a -> a -> Bool
== [[Bool]] -> [[Bool]]
rref [[Bool]]
m2

-- * Matrix primitives over GF(2)

zeros :: Int -> [Bool]
zeros :: Int -> [Bool]
zeros Int
n = Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate Int
n Bool
gf2zero

vscale :: Bool -> [Bool] -> [Bool]
vscale :: Bool -> [Bool] -> [Bool]
vscale Bool
c = (Bool -> Bool) -> [Bool] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Bool -> Bool
gf2mul Bool
c)

vdot :: [Bool] -> [Bool] -> Bool
vdot :: [Bool] -> [Bool] -> Bool
vdot [Bool]
xs [Bool]
ys = (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Bool -> Bool -> Bool
gf2add Bool
gf2zero ((Bool -> Bool -> Bool) -> [Bool] -> [Bool] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Bool -> Bool -> Bool
gf2mul [Bool]
xs [Bool]
ys)

-- | Matrix (rows) times vector.
mxv :: [[Bool]] -> [Bool] -> [Bool]
mxv :: [[Bool]] -> [Bool] -> [Bool]
mxv [[Bool]]
m [Bool]
v = ([Bool] -> Bool) -> [[Bool]] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ([Bool] -> [Bool] -> Bool
vdot [Bool]
v) [[Bool]]
m

setAt :: Int -> a -> [a] -> [a]
setAt :: forall a. Int -> a -> [a] -> [a]
setAt Int
i a
x [a]
xs = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
i [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
x] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [a]
xs

swapRows :: Int -> Int -> [a] -> [a]
swapRows :: forall a. Int -> Int -> [a] -> [a]
swapRows Int
i Int
j [a]
xs
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = [a]
xs
  | Bool
otherwise = Int -> a -> [a] -> [a]
forall a. Int -> a -> [a] -> [a]
setAt Int
i ([a]
xs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
j) (Int -> a -> [a] -> [a]
forall a. Int -> a -> [a] -> [a]
setAt Int
j ([a]
xs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) [a]
xs)

-- | Reduced row echelon form over GF(2).  Zero rows are removed.
rref :: [[Bool]] -> [[Bool]]
rref :: [[Bool]] -> [[Bool]]
rref [[Bool]]
rows = ([Bool] -> Bool) -> [[Bool]] -> [[Bool]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
gf2zero)) ([[Bool]] -> Int -> Int -> [[Bool]]
go [[Bool]]
rows Int
0 Int
0)
  where
    go :: [[Bool]] -> Int -> Int -> [[Bool]]
go [[Bool]]
m Int
r Int
c
      | Int
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [[Bool]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Bool]]
m Bool -> Bool -> Bool
|| Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [[Bool]] -> Int
forall {t :: * -> *} {a}. Foldable t => [t a] -> Int
width [[Bool]]
m = [[Bool]]
m
      | Bool
otherwise =
          case [[Bool]] -> Int -> Int -> Maybe Int
findPivot [[Bool]]
m Int
r Int
c of
            Maybe Int
Nothing -> [[Bool]] -> Int -> Int -> [[Bool]]
go [[Bool]]
m Int
r (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            Just Int
pr ->
              let m' :: [[Bool]]
m' = Int -> Int -> [[Bool]] -> [[Bool]]
forall a. Int -> Int -> [a] -> [a]
swapRows Int
r Int
pr [[Bool]]
m
                  pivotRow :: [Bool]
pivotRow = [[Bool]]
m' [[Bool]] -> Int -> [Bool]
forall a. HasCallStack => [a] -> Int -> a
!! Int
r
                  pivotVal :: Bool
pivotVal = [Bool]
pivotRow [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
c
                  m'' :: [[Bool]]
m'' = Int -> [Bool] -> [[Bool]] -> [[Bool]]
forall a. Int -> a -> [a] -> [a]
setAt Int
r (Bool -> [Bool] -> [Bool]
vscale (Bool -> Bool
gf2inv Bool
pivotVal) [Bool]
pivotRow) [[Bool]]
m'
                  m''' :: [[Bool]]
m''' = Int -> Int -> [[Bool]] -> [[Bool]]
eliminate Int
c Int
r [[Bool]]
m''
               in [[Bool]] -> Int -> Int -> [[Bool]]
go [[Bool]]
m''' (Int
r Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

    width :: [t a] -> Int
width [t a]
m = Int -> (t a -> Int) -> Maybe (t a) -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([t a] -> Maybe (t a)
forall a. [a] -> Maybe a
listToMaybe [t a]
m)

    findPivot :: [[Bool]] -> Int -> Int -> Maybe Int
findPivot [[Bool]]
m Int
r Int
c =
      (Int -> Int) -> Maybe Int -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r) (([Bool] -> Bool) -> [[Bool]] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
gf2zero) (Bool -> Bool) -> ([Bool] -> Bool) -> [Bool] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. ([Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
c)) (Int -> [[Bool]] -> [[Bool]]
forall a. Int -> [a] -> [a]
drop Int
r [[Bool]]
m))

    eliminate :: Int -> Int -> [[Bool]] -> [[Bool]]
eliminate Int
c Int
r [[Bool]]
m =
      [ if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
r
          then [Bool]
row
          else
            let factor :: Bool
factor = [Bool]
row [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
c
             in (Bool -> Bool -> Bool) -> [Bool] -> [Bool] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Bool
x Bool
y -> Bool -> Bool -> Bool
gf2add Bool
x (Bool -> Bool -> Bool
gf2mul Bool
factor Bool
y)) [Bool]
row ([[Bool]]
m [[Bool]] -> Int -> [Bool]
forall a. HasCallStack => [a] -> Int -> a
!! Int
r)
      | (Int
i, [Bool]
row) <- [Int] -> [[Bool]] -> [(Int, [Bool])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [[Bool]]
m
      ]

-- | Basis for the nullspace of a matrix with the given column width.
--
-- The matrix may have zero rows; in that case the nullspace is the whole
-- space of the given dimension.
nullspace :: Int -> [[Bool]] -> [[Bool]]
nullspace :: Int -> [[Bool]] -> [[Bool]]
nullspace Int
width [[Bool]]
rows =
  let rrefm :: [[Bool]]
rrefm = [[Bool]] -> [[Bool]]
rref [[Bool]]
rows
      pivots :: [Int]
pivots = ([Bool] -> Maybe Int) -> [[Bool]] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Int] -> Maybe Int
forall a. [a] -> Maybe a
listToMaybe ([Int] -> Maybe Int)
-> ([(Int, Bool)] -> [Int]) -> [(Int, Bool)] -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. ((Int, Bool) -> Int) -> [(Int, Bool)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Bool) -> Int
forall a b. (a, b) -> a
fst ([(Int, Bool)] -> Maybe Int)
-> ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. ((Int, Bool) -> Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
gf2zero) (Bool -> Bool) -> ((Int, Bool) -> Bool) -> (Int, Bool) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd) ([(Int, Bool)] -> Maybe Int)
-> ([Bool] -> [(Int, Bool)]) -> [Bool] -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..]) [[Bool]]
rrefm
      freeCols :: [Int]
freeCols = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
pivots) [Int
0 .. Int
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
      basis :: [[Bool]]
basis =
        [ let vec :: [Bool]
vec = [if Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
f then Bool
gf2one else Bool
gf2zero | Int
c <- [Int
0 .. Int
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
              pivotVals :: [Bool]
pivotVals = [Bool -> Bool
gf2neg ([Bool]
row [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
f) | [Bool]
row <- [[Bool]]
rrefm]
              vec' :: [Bool]
vec' = ([Bool] -> (Int, Bool) -> [Bool])
-> [Bool] -> [(Int, Bool)] -> [Bool]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\[Bool]
v (Int
pc, Bool
val) -> Int -> Bool -> [Bool] -> [Bool]
forall a. Int -> a -> [a] -> [a]
setAt Int
pc Bool
val [Bool]
v) [Bool]
vec ([Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
pivots [Bool]
pivotVals)
           in [Bool]
vec'
        | Int
f <- [Int]
freeCols
        ]
   in [[Bool]]
basis

-- * Wiring and generators

-- | Build a wiring isomorphism from explicit dimensions and a permutation.
mkWiring ::
  Int ->
  Int ->
  (Int -> Int) ->
  FinRel a b
mkWiring :: forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring Int
dIn Int
dOut Int -> Int
perm =
  let rows :: [[Bool]]
rows =
        [ [ if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
dIn Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int
perm Int
i
              then Bool
gf2one
              else Bool
gf2zero
          | Int
j <- [Int
0 .. Int
dIn Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
dOut Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
          ]
        | Int
i <- [Int
0 .. Int
dIn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        ]
   in Int -> Int -> [[Bool]] -> FinRel a b
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
dIn Int
dOut ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

-- | Build a wiring isomorphism from a permutation.
wiring ::
  forall a b.
  (KnownDim a, KnownDim b) =>
  (Int -> Int) ->
  FinRel a b
wiring :: forall a b. (KnownDim a, KnownDim b) => (Int -> Int) -> FinRel a b
wiring = Int -> Int -> (Int -> Int) -> FinRel a b
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy b -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b))

finId ::
  forall a.
  (KnownDim a) =>
  FinRel a a
finId :: forall a. KnownDim a => FinRel a a
finId =
  let n :: Int
n = Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
      rows :: [[Bool]]
rows =
        [ [if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i then Bool
gf2one else Bool
gf2zero | Int
j <- [Int
0 .. Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
        | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        ]
   in Int -> Int -> [[Bool]] -> FinRel a a
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
n Int
n ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

finCopy ::
  forall n.
  (KnownNat n) =>
  FinRel (FinObj n) (FinObj n, FinObj n)
finCopy :: forall (n :: Nat).
KnownNat n =>
FinRel (FinObj n) (FinObj n, FinObj n)
finCopy =
  let n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
      rows :: [[Bool]]
rows =
        [ [ if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
              then Bool
gf2one
              else Bool
gf2zero
          | Int
j <- [Int
0 .. Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
          ]
        | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        ]
   in Int -> Int -> [[Bool]] -> FinRel (FinObj n) (FinObj n, FinObj n)
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
n (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

finDiscard ::
  forall n.
  (KnownNat n) =>
  FinRel (FinObj n) ()
finDiscard :: forall (n :: Nat). KnownNat n => FinRel (FinObj n) ()
finDiscard =
  let n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
      rows :: [[Bool]]
rows = [[if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then Bool
gf2one else Bool
gf2zero | Int
j <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]] | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   in Int -> Int -> [[Bool]] -> FinRel (FinObj n) ()
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
n Int
0 ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

finPlus ::
  forall n.
  (KnownNat n) =>
  FinRel (FinObj n, FinObj n) (FinObj n)
finPlus :: forall (n :: Nat).
KnownNat n =>
FinRel (FinObj n, FinObj n) (FinObj n)
finPlus =
  let n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
      rows :: [[Bool]]
rows =
        (Int -> [[Bool]]) -> [Int] -> [[Bool]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
          ( \Int
i ->
              [ [if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i then Bool
gf2one else Bool
gf2zero | Int
j <- [Int
0 .. Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]],
                [if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i then Bool
gf2one else Bool
gf2zero | Int
j <- [Int
0 .. Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
              ]
          )
          [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
   in Int -> Int -> [[Bool]] -> FinRel (FinObj n, FinObj n) (FinObj n)
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) Int
n ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

finZero ::
  forall n.
  (KnownNat n) =>
  FinRel () (FinObj n)
finZero :: forall (n :: Nat). KnownNat n => FinRel () (FinObj n)
finZero =
  let n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
   in Int -> Int -> [[Bool]] -> FinRel () (FinObj n)
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
0 Int
n []

finScalar ::
  forall n.
  (KnownNat n) =>
  Bool ->
  FinRel (FinObj n) (FinObj n)
finScalar :: forall (n :: Nat).
KnownNat n =>
Bool -> FinRel (FinObj n) (FinObj n)
finScalar Bool
c =
  let n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
      rows :: [[Bool]]
rows =
        [ [ if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i
              then Bool
gf2one
              else
                if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
                  then Bool
c
                  else Bool
gf2zero
          | Int
j <- [Int
0 .. Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
          ]
        | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        ]
   in Int -> Int -> [[Bool]] -> FinRel (FinObj n) (FinObj n)
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
n Int
n ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

-- * Category structure (named constrained combinators)

--
-- The unconstrained class tower does not carry object evidence, so 'FinRel'
-- provides its structure as named combinators with explicit 'KnownDim'
-- constraints rather than as 'Category'/'Tensor'/'Traced' instances.

compFinRel ::
  forall a b c.
  FinRel b c ->
  FinRel a b ->
  FinRel a c
compFinRel :: forall a b c. FinRel b c -> FinRel a b -> FinRel a c
compFinRel (FinRel Int
pOut Int
m [[Bool]]
rowsB) (FinRel Int
n Int
pIn [[Bool]]
rowsA) =
  if Int
pIn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
pOut
    then String -> FinRel a c
forall a. HasCallStack => String -> a
error String
"compFinRel: middle dimension mismatch"
    else
      let rA :: Int
rA = [[Bool]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Bool]]
rowsA
          rB :: Int
rB = [[Bool]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Bool]]
rowsB
          ([[Bool]]
aIn, [[Bool]]
aOut) = [([Bool], [Bool])] -> ([[Bool]], [[Bool]])
forall a b. [(a, b)] -> ([a], [b])
unzip (([Bool] -> ([Bool], [Bool])) -> [[Bool]] -> [([Bool], [Bool])]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n) [[Bool]]
rowsA)
          ([[Bool]]
bIn, [[Bool]]
bOut) = [([Bool], [Bool])] -> ([[Bool]], [[Bool]])
forall a b. [(a, b)] -> ([a], [b])
unzip (([Bool] -> ([Bool], [Bool])) -> [[Bool]] -> [([Bool], [Bool])]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
pIn) [[Bool]]
rowsB)
          kRows :: [[Bool]]
kRows =
            [ [[Bool]
aOutRow [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | [Bool]
aOutRow <- [[Bool]]
aOut] [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [[Bool]
bInRow [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | [Bool]
bInRow <- [[Bool]]
bIn]
            | Int
i <- [Int
0 .. Int
pIn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
            ]
          basis :: [[Bool]]
basis = Int -> [[Bool]] -> [[Bool]]
nullspace (Int
rA Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
rB) [[Bool]]
kRows
          rows :: [[Bool]]
rows =
            [ let ([Bool]
x, [Bool]
y) = Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
rA [Bool]
v
                  a :: [Bool]
a = [[Bool]] -> [Bool] -> [Bool]
mxv ([[Bool]] -> [[Bool]]
forall a. [[a]] -> [[a]]
transpose [[Bool]]
aIn) [Bool]
x
                  c :: [Bool]
c = [[Bool]] -> [Bool] -> [Bool]
mxv ([[Bool]] -> [[Bool]]
forall a. [[a]] -> [[a]]
transpose [[Bool]]
bOut) [Bool]
y
               in [Bool]
a [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
c
            | [Bool]
v <- [[Bool]]
basis
            ]
       in Int -> Int -> [[Bool]] -> FinRel a c
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
n Int
m ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

-- * Monoidal / traced structure

unitlFinRel ::
  forall a.
  (KnownDim a) =>
  FinRel ((), a) a
unitlFinRel :: forall a. KnownDim a => FinRel ((), a) a
unitlFinRel = Int -> Int -> (Int -> Int) -> FinRel ((), a) a
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) Int -> Int
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

unitl'FinRel ::
  forall a.
  (KnownDim a) =>
  FinRel a ((), a)
unitl'FinRel :: forall a. KnownDim a => FinRel a ((), a)
unitl'FinRel = Int -> Int -> (Int -> Int) -> FinRel a ((), a)
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) Int -> Int
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

unitrFinRel ::
  forall a.
  (KnownDim a) =>
  FinRel (a, ()) a
unitrFinRel :: forall a. KnownDim a => FinRel (a, ()) a
unitrFinRel = Int -> Int -> (Int -> Int) -> FinRel (a, ()) a
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) Int -> Int
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

unitr'FinRel ::
  forall a.
  (KnownDim a) =>
  FinRel a (a, ())
unitr'FinRel :: forall a. KnownDim a => FinRel a (a, ())
unitr'FinRel = Int -> Int -> (Int -> Int) -> FinRel a (a, ())
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) Int -> Int
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

parFinRel ::
  forall a b c d.
  FinRel a b ->
  FinRel c d ->
  FinRel (a, c) (b, d)
parFinRel :: forall a b c d. FinRel a b -> FinRel c d -> FinRel (a, c) (b, d)
parFinRel (FinRel Int
n Int
p [[Bool]]
rowsA) (FinRel Int
m Int
q [[Bool]]
rowsB) =
  let rowA :: ([Bool], [Bool]) -> [Bool]
rowA ([Bool]
aIn, [Bool]
aOut) = [Bool]
aIn [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Int -> [Bool]
zeros Int
m [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
aOut [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Int -> [Bool]
zeros Int
q
      rowB :: ([Bool], [Bool]) -> [Bool]
rowB ([Bool]
bIn, [Bool]
bOut) = Int -> [Bool]
zeros Int
n [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
bIn [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Int -> [Bool]
zeros Int
p [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
bOut
      rows :: [[Bool]]
rows =
        ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (([Bool], [Bool]) -> [Bool]
rowA (([Bool], [Bool]) -> [Bool])
-> ([Bool] -> ([Bool], [Bool])) -> [Bool] -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n) [[Bool]]
rowsA
          [[Bool]] -> [[Bool]] -> [[Bool]]
forall a. [a] -> [a] -> [a]
++ ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (([Bool], [Bool]) -> [Bool]
rowB (([Bool], [Bool]) -> [Bool])
-> ([Bool] -> ([Bool], [Bool])) -> [Bool] -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m) [[Bool]]
rowsB
   in Int -> Int -> [[Bool]] -> FinRel (a, c) (b, d)
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
q) ([[Bool]] -> [[Bool]]
rref [[Bool]]
rows)

swapFinRel ::
  forall a b.
  (KnownDim a, KnownDim b) =>
  FinRel (a, b) (b, a)
swapFinRel :: forall a b. (KnownDim a, KnownDim b) => FinRel (a, b) (b, a)
swapFinRel =
  let n :: Int
n = Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
      m :: Int
m = Proxy b -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
   in Int -> Int -> (Int -> Int) -> FinRel (a, b) (b, a)
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) ((Int -> Int) -> FinRel (a, b) (b, a))
-> (Int -> Int) -> FinRel (a, b) (b, a)
forall a b. (a -> b) -> a -> b
$ \Int
i ->
        if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n then Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i else Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n

assocFinRel ::
  forall a b c.
  (KnownDim a, KnownDim b, KnownDim c) =>
  FinRel ((a, b), c) (a, (b, c))
assocFinRel :: forall a b c.
(KnownDim a, KnownDim b, KnownDim c) =>
FinRel ((a, b), c) (a, (b, c))
assocFinRel =
  let n :: Int
n = Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
      m :: Int
m = Proxy b -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
      l :: Int
l = Proxy c -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c)
   in Int -> Int -> (Int -> Int) -> FinRel ((a, b), c) (a, (b, c))
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) Int -> Int
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

assoc'FinRel ::
  forall a b c.
  (KnownDim a, KnownDim b, KnownDim c) =>
  FinRel (a, (b, c)) ((a, b), c)
assoc'FinRel :: forall a b c.
(KnownDim a, KnownDim b, KnownDim c) =>
FinRel (a, (b, c)) ((a, b), c)
assoc'FinRel =
  let n :: Int
n = Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
      m :: Int
m = Proxy b -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
      l :: Int
l = Proxy c -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c)
   in Int -> Int -> (Int -> Int) -> FinRel (a, (b, c)) ((a, b), c)
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) Int -> Int
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

slideFinRel ::
  forall a b c.
  (KnownDim a, KnownDim b, KnownDim c) =>
  FinRel (a, (b, c)) (b, (a, c))
slideFinRel :: forall a b c.
(KnownDim a, KnownDim b, KnownDim c) =>
FinRel (a, (b, c)) (b, (a, c))
slideFinRel =
  let n :: Int
n = Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
      m :: Int
m = Proxy b -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
      l :: Int
l = Proxy c -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c)
   in Int -> Int -> (Int -> Int) -> FinRel (a, (b, c)) (b, (a, c))
forall a b. Int -> Int -> (Int -> Int) -> FinRel a b
mkWiring (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) ((Int -> Int) -> FinRel (a, (b, c)) (b, (a, c)))
-> (Int -> Int) -> FinRel (a, (b, c)) (b, (a, c))
forall a b. (a -> b) -> a -> b
$ \Int
i ->
        if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n
          then Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
          else
            if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m
              then Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n
              else Int
i

strengthFinRel ::
  forall a b c.
  (KnownDim a) =>
  FinRel b c ->
  FinRel (a, b) (a, c)
strengthFinRel :: forall a b c. KnownDim a => FinRel b c -> FinRel (a, b) (a, c)
strengthFinRel = FinRel a a -> FinRel b c -> FinRel (a, b) (a, c)
forall a b c d. FinRel a b -> FinRel c d -> FinRel (a, c) (b, d)
parFinRel FinRel a a
forall a. KnownDim a => FinRel a a
finId

traceFinRel ::
  forall a b c.
  (KnownDim a, KnownDim b, KnownDim c) =>
  FinRel (a, b) (a, c) ->
  FinRel b c
traceFinRel :: forall a b c.
(KnownDim a, KnownDim b, KnownDim c) =>
FinRel (a, b) (a, c) -> FinRel b c
traceFinRel (FinRel Int
inDim Int
_ [[Bool]]
rows) =
  let aDim :: Int
aDim = Proxy a -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
      bDim :: Int
bDim = Proxy b -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
      cDim :: Int
cDim = Proxy c -> Int
forall {k} (a :: k). KnownDim a => Proxy a -> Int
dimVal (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c)
      splitRow :: [Bool] -> ([Bool], [Bool], [Bool], [Bool])
splitRow [Bool]
row =
        let ([Bool]
ab, [Bool]
ac) = Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
inDim [Bool]
row
            ([Bool]
aIn, [Bool]
bIn) = Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
aDim [Bool]
ab
            ([Bool]
aOut, [Bool]
cOut) = Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
aDim [Bool]
ac
         in ([Bool]
aIn, [Bool]
bIn, [Bool]
aOut, [Bool]
cOut)
      parts :: [([Bool], [Bool], [Bool], [Bool])]
parts = ([Bool] -> ([Bool], [Bool], [Bool], [Bool]))
-> [[Bool]] -> [([Bool], [Bool], [Bool], [Bool])]
forall a b. (a -> b) -> [a] -> [b]
map [Bool] -> ([Bool], [Bool], [Bool], [Bool])
splitRow [[Bool]]
rows
      bInRows :: [[Bool]]
bInRows = [[Bool]
bIn | ([Bool]
_, [Bool]
bIn, [Bool]
_, [Bool]
_) <- [([Bool], [Bool], [Bool], [Bool])]
parts]
      cOutRows :: [[Bool]]
cOutRows = [[Bool]
cOut | ([Bool]
_, [Bool]
_, [Bool]
_, [Bool]
cOut) <- [([Bool], [Bool], [Bool], [Bool])]
parts]
      kRows :: [[Bool]]
kRows =
        [ [Bool -> Bool -> Bool
gf2add ([Bool]
aIn [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) ([Bool]
aOut [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) | ([Bool]
aIn, [Bool]
_, [Bool]
aOut, [Bool]
_) <- [([Bool], [Bool], [Bool], [Bool])]
parts]
        | Int
i <- [Int
0 .. Int
aDim Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        ]
      basis :: [[Bool]]
basis = Int -> [[Bool]] -> [[Bool]]
nullspace ([[Bool]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Bool]]
rows) [[Bool]]
kRows
      bcRows :: [[Bool]]
bcRows =
        [ let b :: [Bool]
b = [[Bool]] -> [Bool] -> [Bool]
mxv ([[Bool]] -> [[Bool]]
forall a. [[a]] -> [[a]]
transpose [[Bool]]
bInRows) [Bool]
v
              c :: [Bool]
c = [[Bool]] -> [Bool] -> [Bool]
mxv ([[Bool]] -> [[Bool]]
forall a. [[a]] -> [[a]]
transpose [[Bool]]
cOutRows) [Bool]
v
           in [Bool]
b [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
c
        | [Bool]
v <- [[Bool]]
basis
        ]
   in Int -> Int -> [[Bool]] -> FinRel b c
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
bDim Int
cDim ([[Bool]] -> [[Bool]]
rref [[Bool]]
bcRows)

-- * Bimonoid generators

instance (KnownNat n) => Copy FinRel (FinObj n) where
  copy :: FinRel (FinObj n) (FinObj n, FinObj n)
copy = FinRel (FinObj n) (FinObj n, FinObj n)
forall (n :: Nat).
KnownNat n =>
FinRel (FinObj n) (FinObj n, FinObj n)
finCopy

instance (KnownNat n) => Discard FinRel (FinObj n) where
  discard :: FinRel (FinObj n) ()
discard = FinRel (FinObj n) ()
forall (n :: Nat). KnownNat n => FinRel (FinObj n) ()
finDiscard

instance (KnownNat n) => Merge FinRel (FinObj n) where
  plus :: FinRel (FinObj n, FinObj n) (FinObj n)
plus = FinRel (FinObj n, FinObj n) (FinObj n)
forall (n :: Nat).
KnownNat n =>
FinRel (FinObj n, FinObj n) (FinObj n)
finPlus

instance (KnownNat n) => Zero FinRel (FinObj n) where
  zero :: FinRel () (FinObj n)
zero = FinRel () (FinObj n)
forall (n :: Nat). KnownNat n => FinRel () (FinObj n)
finZero

finCopyUnit :: FinRel () ((), ())
finCopyUnit :: FinRel () ((), ())
finCopyUnit = Int -> Int -> [[Bool]] -> FinRel () ((), ())
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
0 Int
0 []

finDiscardUnit :: FinRel () ()
finDiscardUnit :: FinRel () ()
finDiscardUnit = Int -> Int -> [[Bool]] -> FinRel () ()
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
0 Int
0 []

finPlusUnit :: FinRel ((), ()) ()
finPlusUnit :: FinRel ((), ()) ()
finPlusUnit = Int -> Int -> [[Bool]] -> FinRel ((), ()) ()
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
0 Int
0 []

finZeroUnit :: FinRel () ()
finZeroUnit :: FinRel () ()
finZeroUnit = Int -> Int -> [[Bool]] -> FinRel () ()
forall n m. Int -> Int -> [[Bool]] -> FinRel n m
FinRel Int
0 Int
0 []

instance Copy FinRel () where
  copy :: FinRel () ((), ())
copy = FinRel () ((), ())
finCopyUnit

instance Discard FinRel () where
  discard :: FinRel () ()
discard = FinRel () ()
finDiscardUnit

instance Merge FinRel () where
  plus :: FinRel ((), ()) ()
plus = FinRel ((), ()) ()
finPlusUnit

instance Zero FinRel () where
  zero :: FinRel () ()
zero = FinRel () ()
finZeroUnit