{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.FinRel where

import Data.Fin (Fin (..))
import Data.Type.Nat (Mult, Nat (..), Nat0, Nat1, Plus, SNat (..), SNatI, snat, snatToNatural)
import Data.Vec.Lazy (Vec (..), chunks, concatMap, repeat, universe, zipWith, (++))
import GHC.Bits qualified as B
import GHC.Natural (Natural)
import Prelude (Bounded, Enum (..), Eq, Num (..), Ord, Show, divMod, fromIntegral, ($))
import Prelude qualified as P

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Instance.FinSet (FINSET (..), FinSet (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (Costrong (..), MonoidalAction (..), Strong (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Category.Monoidal.Hypergraph (Frobenius (..), Hypergraph, spiderDefault)
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, obj, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), HasBiproducts, Coprod (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Dual (CompactClosed (..), ExpSA, StarAutonomous (..), applySA, coactCC, currySA, expSA)
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Representable (Rep (..))

newtype Bitstring (n :: Nat) = BS Natural
  deriving (Bitstring n -> Bitstring n -> Bool
(Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool) -> Eq (Bitstring n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
$c== :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
== :: Bitstring n -> Bitstring n -> Bool
$c/= :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
/= :: Bitstring n -> Bitstring n -> Bool
Eq, Eq (Bitstring n)
Eq (Bitstring n) =>
(Bitstring n -> Bitstring n -> Ordering)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> Ord (Bitstring n)
Bitstring n -> Bitstring n -> Bool
Bitstring n -> Bitstring n -> Ordering
Bitstring n -> Bitstring n -> Bitstring 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
forall (n :: Nat). Eq (Bitstring n)
forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
forall (n :: Nat). Bitstring n -> Bitstring n -> Ordering
forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
$ccompare :: forall (n :: Nat). Bitstring n -> Bitstring n -> Ordering
compare :: Bitstring n -> Bitstring n -> Ordering
$c< :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
< :: Bitstring n -> Bitstring n -> Bool
$c<= :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
<= :: Bitstring n -> Bitstring n -> Bool
$c> :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
> :: Bitstring n -> Bitstring n -> Bool
$c>= :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bool
>= :: Bitstring n -> Bitstring n -> Bool
$cmax :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
max :: Bitstring n -> Bitstring n -> Bitstring n
$cmin :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
min :: Bitstring n -> Bitstring n -> Bitstring n
Ord)
  deriving newtype (Integer -> Bitstring n
Bitstring n -> Bitstring n
Bitstring n -> Bitstring n -> Bitstring n
(Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n)
-> (Integer -> Bitstring n)
-> Num (Bitstring n)
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
forall (n :: Nat). Integer -> Bitstring n
forall (n :: Nat). Bitstring n -> Bitstring n
forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
$c+ :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
+ :: Bitstring n -> Bitstring n -> Bitstring n
$c- :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
- :: Bitstring n -> Bitstring n -> Bitstring n
$c* :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
* :: Bitstring n -> Bitstring n -> Bitstring n
$cnegate :: forall (n :: Nat). Bitstring n -> Bitstring n
negate :: Bitstring n -> Bitstring n
$cabs :: forall (n :: Nat). Bitstring n -> Bitstring n
abs :: Bitstring n -> Bitstring n
$csignum :: forall (n :: Nat). Bitstring n -> Bitstring n
signum :: Bitstring n -> Bitstring n
$cfromInteger :: forall (n :: Nat). Integer -> Bitstring n
fromInteger :: Integer -> Bitstring n
Num, Eq (Bitstring n)
Bitstring n
Eq (Bitstring n) =>
(Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> Bitstring n
-> (Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bool)
-> (Bitstring n -> Maybe Int)
-> (Bitstring n -> Int)
-> (Bitstring n -> Bool)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int -> Bitstring n)
-> (Bitstring n -> Int)
-> Bits (Bitstring n)
Int -> Bitstring n
Bitstring n -> Bool
Bitstring n -> Int
Bitstring n -> Maybe Int
Bitstring n -> Bitstring n
Bitstring n -> Int -> Bool
Bitstring n -> Int -> Bitstring n
Bitstring n -> Bitstring n -> Bitstring n
forall a.
Eq a =>
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> a
-> (Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> Bool)
-> (a -> Maybe Int)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int)
-> Bits a
forall (n :: Nat). Eq (Bitstring n)
forall (n :: Nat). Bitstring n
forall (n :: Nat). Int -> Bitstring n
forall (n :: Nat). Bitstring n -> Bool
forall (n :: Nat). Bitstring n -> Int
forall (n :: Nat). Bitstring n -> Maybe Int
forall (n :: Nat). Bitstring n -> Bitstring n
forall (n :: Nat). Bitstring n -> Int -> Bool
forall (n :: Nat). Bitstring n -> Int -> Bitstring n
forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
$c.&. :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
.&. :: Bitstring n -> Bitstring n -> Bitstring n
$c.|. :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
.|. :: Bitstring n -> Bitstring n -> Bitstring n
$cxor :: forall (n :: Nat). Bitstring n -> Bitstring n -> Bitstring n
xor :: Bitstring n -> Bitstring n -> Bitstring n
$ccomplement :: forall (n :: Nat). Bitstring n -> Bitstring n
complement :: Bitstring n -> Bitstring n
$cshift :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
shift :: Bitstring n -> Int -> Bitstring n
$crotate :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
rotate :: Bitstring n -> Int -> Bitstring n
$czeroBits :: forall (n :: Nat). Bitstring n
zeroBits :: Bitstring n
$cbit :: forall (n :: Nat). Int -> Bitstring n
bit :: Int -> Bitstring n
$csetBit :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
setBit :: Bitstring n -> Int -> Bitstring n
$cclearBit :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
clearBit :: Bitstring n -> Int -> Bitstring n
$ccomplementBit :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
complementBit :: Bitstring n -> Int -> Bitstring n
$ctestBit :: forall (n :: Nat). Bitstring n -> Int -> Bool
testBit :: Bitstring n -> Int -> Bool
$cbitSizeMaybe :: forall (n :: Nat). Bitstring n -> Maybe Int
bitSizeMaybe :: Bitstring n -> Maybe Int
$cbitSize :: forall (n :: Nat). Bitstring n -> Int
bitSize :: Bitstring n -> Int
$cisSigned :: forall (n :: Nat). Bitstring n -> Bool
isSigned :: Bitstring n -> Bool
$cshiftL :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
shiftL :: Bitstring n -> Int -> Bitstring n
$cunsafeShiftL :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
unsafeShiftL :: Bitstring n -> Int -> Bitstring n
$cshiftR :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
shiftR :: Bitstring n -> Int -> Bitstring n
$cunsafeShiftR :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
unsafeShiftR :: Bitstring n -> Int -> Bitstring n
$crotateL :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
rotateL :: Bitstring n -> Int -> Bitstring n
$crotateR :: forall (n :: Nat). Bitstring n -> Int -> Bitstring n
rotateR :: Bitstring n -> Int -> Bitstring n
$cpopCount :: forall (n :: Nat). Bitstring n -> Int
popCount :: Bitstring n -> Int
B.Bits)

instance (SNatI n) => Bounded (Bitstring n) where
  minBound :: Bitstring n
minBound = Natural -> Bitstring n
forall (n :: Nat). Natural -> Bitstring n
BS Natural
0
  maxBound :: Bitstring n
maxBound = Natural -> Bitstring n
forall (n :: Nat). Natural -> Bitstring n
BS (forall (n :: Nat). SNatI n => Natural -> Natural
shiftN @n Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
instance Enum (Bitstring n) where
  fromEnum :: Bitstring n -> Int
fromEnum (BS Natural
x) = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
x
  toEnum :: Int -> Bitstring n
toEnum Int
x = Natural -> Bitstring n
forall (n :: Nat). Natural -> Bitstring n
BS (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x)
instance (SNatI n) => Show (Bitstring n) where
  show :: Bitstring n -> String
show Bitstring n
n = case forall (n :: Nat). SNatI n => SNat n
snat @n of
    SNat n
SZ -> String
""
    SNat n
SS -> case Bitstring ('S n1) -> (Bitstring n1, Bool)
forall (n :: Nat). Bitstring ('S n) -> (Bitstring n, Bool)
pop Bitstring n
Bitstring ('S n1)
n of (Bitstring n1
n', Bool
b) -> (if Bool
b then String
"1" else String
"0") String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Bitstring n1 -> String
forall a. Show a => a -> String
P.show Bitstring n1
n'

shiftN :: forall n. (SNatI n) => Natural -> Natural
shiftN :: forall (n :: Nat). SNatI n => Natural -> Natural
shiftN Natural
n = Natural
n Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`B.shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
snatToNatural (forall (n :: Nat). SNatI n => SNat n
snat @n))

-- | Split n + m bits into two parts: the lower n bits and the higher m bits.
split :: (SNatI n) => Bitstring (Plus n m) -> (Bitstring n, Bitstring m)
split :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring (Plus n m) -> (Bitstring n, Bitstring m)
split @n (BS Natural
x) = case (Natural
x Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` (forall (n :: Nat). SNatI n => Natural -> Natural
shiftN @n Natural
1)) of (Natural
m, Natural
n) -> (Natural -> Bitstring n
forall (n :: Nat). Natural -> Bitstring n
BS Natural
n, Natural -> Bitstring m
forall (n :: Nat). Natural -> Bitstring n
BS Natural
m)

splits :: forall n m. (SNatI n, SNatI m) => Bitstring (Mult n m) -> Vec n (Bitstring m)
splits :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Bitstring (Mult n m) -> Vec n (Bitstring m)
splits Bitstring (Mult n m)
bs = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> Vec n (Bitstring m)
Vec 'Z (Bitstring m)
forall a. Vec 'Z a
VNil
  SNat n
SS -> case forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring (Plus n m) -> (Bitstring n, Bitstring m)
split @m Bitstring (Mult n m)
Bitstring (Plus m (Mult n1 m))
bs of
    (Bitstring m
v, Bitstring (Mult n1 m)
vs) -> Bitstring m
v Bitstring m -> Vec n1 (Bitstring m) -> Vec ('S n1) (Bitstring m)
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Bitstring (Mult n1 m) -> Vec n1 (Bitstring m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Bitstring (Mult n m) -> Vec n (Bitstring m)
splits Bitstring (Mult n1 m)
vs

-- | Combine two bitstrings of lengths n and m into one bitstring with the n lower bits or m higher bits.
combine :: (SNatI n) => Bitstring n -> Bitstring m -> Bitstring (Plus n m)
combine :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring n -> Bitstring m -> Bitstring (Plus n m)
combine @n (BS Natural
x) (BS Natural
y) = Natural -> Bitstring (Plus n m)
forall (n :: Nat). Natural -> Bitstring n
BS ((forall (n :: Nat). SNatI n => Natural -> Natural
shiftN @n Natural
y) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
B..|. Natural
x)

combines :: (SNatI m) => Vec n (Bitstring m) -> Bitstring (Mult n m)
combines :: forall (m :: Nat) (n :: Nat).
SNatI m =>
Vec n (Bitstring m) -> Bitstring (Mult n m)
combines Vec n (Bitstring m)
VNil = Bitstring 'Z
Bitstring (Mult n m)
0
combines (Bitstring m
v ::: Vec n1 (Bitstring m)
vs) = Bitstring m
-> Bitstring (Mult n1 m) -> Bitstring (Plus m (Mult n1 m))
forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring n -> Bitstring m -> Bitstring (Plus n m)
combine Bitstring m
v (Vec n1 (Bitstring m) -> Bitstring (Mult n1 m)
forall (m :: Nat) (n :: Nat).
SNatI m =>
Vec n (Bitstring m) -> Bitstring (Mult n m)
combines Vec n1 (Bitstring m)
vs)

pop :: Bitstring (S n) -> (Bitstring n, P.Bool)
pop :: forall (n :: Nat). Bitstring ('S n) -> (Bitstring n, Bool)
pop (BS Natural
n) = (Natural -> Bitstring n
forall (n :: Nat). Natural -> Bitstring n
BS (Natural
n Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`B.shiftR` Int
1), Natural -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
B.testBit Natural
n Int
0)

push :: P.Bool -> Bitstring n -> Bitstring (S n)
push :: forall (n :: Nat). Bool -> Bitstring n -> Bitstring ('S n)
push Bool
b (BS Natural
n) = Natural -> Bitstring ('S n)
forall (n :: Nat). Natural -> Bitstring n
BS (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ if Bool
b then Natural
1 else Natural
0)

mult :: forall n m. (SNatI n, SNatI m) => Bitstring n -> Bitstring m -> Bitstring (Mult n m)
mult :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Bitstring n -> Bitstring m -> Bitstring (Mult n m)
mult Bitstring n
n Bitstring m
m = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> Bitstring 'Z
Bitstring (Mult n m)
0
  SNat n
SS -> case Bitstring ('S n1) -> (Bitstring n1, Bool)
forall (n :: Nat). Bitstring ('S n) -> (Bitstring n, Bool)
pop Bitstring n
Bitstring ('S n1)
n of (Bitstring n1
n', Bool
b) -> Bitstring m
-> Bitstring (Mult n1 m) -> Bitstring (Plus m (Mult n1 m))
forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring n -> Bitstring m -> Bitstring (Plus n m)
combine (if Bool
b then Bitstring m
m else Bitstring m
0) (Bitstring n1 -> Bitstring m -> Bitstring (Mult n1 m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Bitstring n -> Bitstring m -> Bitstring (Mult n m)
mult Bitstring n1
n' Bitstring m
m)

bit :: (SNatI n) => Fin n -> Bitstring n
bit :: forall (n :: Nat). SNatI n => Fin n -> Bitstring n
bit = Int -> Bitstring n
forall a. Bits a => Int -> a
B.bit (Int -> Bitstring n) -> (Fin n -> Int) -> Fin n -> Bitstring n
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fin n -> Int
forall a. Enum a => a -> Int
fromEnum

zero :: (SNatI n, SNatI m) => Vec n (Bitstring m)
zero :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m)
zero = Bitstring m -> Vec n (Bitstring m)
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat Bitstring m
0

pick :: forall n a. Vec n a -> Bitstring n -> [a]
pick :: forall (n :: Nat) a. Vec n a -> Bitstring n -> [a]
pick Vec n a
VNil Bitstring n
_ = []
pick (a
a ::: Vec n1 a
as) Bitstring n
n = case Bitstring ('S n1) -> (Bitstring n1, Bool)
forall (n :: Nat). Bitstring ('S n) -> (Bitstring n, Bool)
pop Bitstring n
Bitstring ('S n1)
n of (Bitstring n1
n', Bool
b) -> (if Bool
b then (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) else [a] -> [a]
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) (Vec n1 a -> Bitstring n1 -> [a]
forall (n :: Nat) a. Vec n a -> Bitstring n -> [a]
pick Vec n1 a
as Bitstring n1
n')

fromBools :: forall n. Vec n P.Bool -> Bitstring n
fromBools :: forall (n :: Nat). Vec n Bool -> Bitstring n
fromBools Vec n Bool
VNil = Bitstring n
0
fromBools (Bool
b ::: Vec n1 Bool
bs) = Bool -> Bitstring n1 -> Bitstring ('S n1)
forall (n :: Nat). Bool -> Bitstring n -> Bitstring ('S n)
push Bool
b (Vec n1 Bool -> Bitstring n1
forall (n :: Nat). Vec n Bool -> Bitstring n
fromBools Vec n1 Bool
bs)

toBools :: forall n. (SNatI n) => Bitstring n -> Vec n P.Bool
toBools :: forall (n :: Nat). SNatI n => Bitstring n -> Vec n Bool
toBools Bitstring n
n = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> Vec n Bool
Vec 'Z Bool
forall a. Vec 'Z a
VNil
  SNat n
SS -> case Bitstring ('S n1) -> (Bitstring n1, Bool)
forall (n :: Nat). Bitstring ('S n) -> (Bitstring n, Bool)
pop Bitstring n
Bitstring ('S n1)
n of (Bitstring n1
n', Bool
b) -> Bool
b Bool -> Vec n1 Bool -> Vec ('S n1) Bool
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Bitstring n1 -> Vec n1 Bool
forall (n :: Nat). SNatI n => Bitstring n -> Vec n Bool
toBools Bitstring n1
n'

arr :: forall n m. FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr :: forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (FinSet Vec n (Fin m)
v) = Vec m (Bitstring n) -> FinRel (FR m) (FR n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Fin n -> Bitstring n) -> Vec m (Fin n) -> Vec m (Bitstring n)
forall a b. (a -> b) -> Vec m a -> Vec m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Fin n -> Bitstring n
forall (n :: Nat). SNatI n => Fin n -> Bitstring n
bit Vec m (Fin n)
Vec n (Fin m)
v)

type data FINREL = FR Nat
type instance UN FR (FR n) = n

type FinRel :: CAT FINREL
data FinRel a b where
  FinRel :: (SNatI n, SNatI m) => {forall (n :: Nat) (m :: Nat).
FinRel (FR n) (FR m) -> Vec n (Bitstring m)
unFinRel :: Vec n (Bitstring m)} -> FinRel (FR n) (FR m)

deriving instance P.Show (FinRel a b)
deriving instance P.Eq (FinRel a b)

instance Profunctor FinRel where
  dimap :: forall (c :: FINREL) (a :: FINREL) (b :: FINREL) (d :: FINREL).
(c ~> a) -> (b ~> d) -> FinRel a b -> FinRel c d
dimap = (c ~> a) -> (b ~> d) -> FinRel a b -> FinRel c d
FinRel c a -> FinRel b d -> FinRel a b -> FinRel c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: FINREL) (b :: FINREL) r.
((Ob a, Ob b) => r) -> FinRel a b -> r
\\ FinRel{} = r
(Ob a, Ob b) => r
r
instance Promonad FinRel where
  id :: forall (a :: FINREL). Ob a => FinRel a a
id = Vec (UN FR a) (Bitstring (UN FR a))
-> FinRel (FR (UN FR a)) (FR (UN FR a))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Fin (UN FR a) -> Bitstring (UN FR a))
-> Vec (UN FR a) (Fin (UN FR a))
-> Vec (UN FR a) (Bitstring (UN FR a))
forall a b. (a -> b) -> Vec (UN FR a) a -> Vec (UN FR a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Fin (UN FR a) -> Bitstring (UN FR a)
forall (n :: Nat). SNatI n => Fin n -> Bitstring n
bit Vec (UN FR a) (Fin (UN FR a))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)
  FinRel Vec n (Bitstring m)
l . :: forall (b :: FINREL) (c :: FINREL) (a :: FINREL).
FinRel b c -> FinRel a b -> FinRel a c
. FinRel Vec n (Bitstring m)
r = Vec n (Bitstring m) -> FinRel (FR n) (FR m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Bitstring m -> Bitstring m)
-> Vec n (Bitstring m) -> Vec n (Bitstring m)
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap ((Bitstring m -> Bitstring m -> Bitstring m)
-> Bitstring m -> [Bitstring m] -> Bitstring m
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr Bitstring m -> Bitstring m -> Bitstring m
forall a. Bits a => a -> a -> a
(B..|.) Bitstring m
0 ([Bitstring m] -> Bitstring m)
-> (Bitstring n -> [Bitstring m]) -> Bitstring n -> Bitstring m
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Vec n (Bitstring m) -> Bitstring n -> [Bitstring m]
forall (n :: Nat) a. Vec n a -> Bitstring n -> [a]
pick Vec n (Bitstring m)
l) Vec n (Bitstring m)
r)
instance CategoryOf FINREL where
  type (~>) = FinRel
  type Ob a = (Is FR a, SNatI (UN FR a))

instance DaggerProfunctor FinRel where
  dagger :: forall (a :: FINREL) (b :: FINREL). FinRel a b -> FinRel b a
dagger (FinRel Vec n (Bitstring m)
v) = Vec m (Bitstring n) -> FinRel (FR m) (FR n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (Vec n Bool -> Bitstring n
forall (n :: Nat). Vec n Bool -> Bitstring n
fromBools (Vec n Bool -> Bitstring n)
-> Vec m (Vec n Bool) -> Vec m (Bitstring n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> (Bitstring m -> Vec m Bool)
-> Vec n (Bitstring m) -> Vec m (Vec n Bool)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
P.traverse Bitstring m -> Vec m Bool
forall (n :: Nat). SNatI n => Bitstring n -> Vec n Bool
toBools Vec n (Bitstring m)
v)

instance HasInitialObject FINREL where
  type InitialObject = FR Nat0
  initiate :: forall (a :: FINREL). Ob a => InitialObject ~> a
initiate = Vec 'Z (Bitstring (UN FR a)) -> FinRel (FR 'Z) (FR (UN FR a))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel Vec 'Z (Bitstring (UN FR a))
forall a. Vec 'Z a
VNil
instance HasBinaryCoproducts FINREL where
  type FR a || FR b = FR (Plus a b)
  withObCoprod :: forall (a :: FINREL) (b :: FINREL) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(FR a) @b Ob (a || b) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @a of
    SNat (UN FR a)
SZ -> r
Ob (a || b) => r
r
    SS @a' -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FR a') @b r
Ob (a || b) => r
Ob (FR n1 || b) => r
r
  lft :: forall (a :: FINREL) (b :: FINREL). (Ob a, Ob b) => a ~> (a || b)
lft @(FR a) @(FR b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FR a) @(FR b) ((Ob (FR (UN FR a) || FR (UN FR b)) => a ~> (a || b))
 -> a ~> (a || b))
-> (Ob (FR (UN FR a) || FR (UN FR b)) => a ~> (a || b))
-> a ~> (a || b)
forall a b. (a -> b) -> a -> b
$ Vec (UN FR a) (Bitstring (Plus (UN FR a) (UN FR b)))
-> FinRel (FR (UN FR a)) (FR (Plus (UN FR a) (UN FR b)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Fin (UN FR a) -> Bitstring (Plus (UN FR a) (UN FR b)))
-> Vec (UN FR a) (Fin (UN FR a))
-> Vec (UN FR a) (Bitstring (Plus (UN FR a) (UN FR b)))
forall a b. (a -> b) -> Vec (UN FR a) a -> Vec (UN FR a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap ((\Bitstring (UN FR a)
a -> forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring n -> Bitstring m -> Bitstring (Plus n m)
combine @a @b Bitstring (UN FR a)
a Bitstring (UN FR b)
0) (Bitstring (UN FR a) -> Bitstring (Plus (UN FR a) (UN FR b)))
-> (Fin (UN FR a) -> Bitstring (UN FR a))
-> Fin (UN FR a)
-> Bitstring (Plus (UN FR a) (UN FR b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fin (UN FR a) -> Bitstring (UN FR a)
forall (n :: Nat). SNatI n => Fin n -> Bitstring n
bit) Vec (UN FR a) (Fin (UN FR a))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)
  rgt :: forall (a :: FINREL) (b :: FINREL). (Ob a, Ob b) => b ~> (a || b)
rgt @(FR a) @(FR b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FR a) @(FR b) ((Ob (FR (UN FR a) || FR (UN FR b)) => b ~> (a || b))
 -> b ~> (a || b))
-> (Ob (FR (UN FR a) || FR (UN FR b)) => b ~> (a || b))
-> b ~> (a || b)
forall a b. (a -> b) -> a -> b
$ Vec (UN FR b) (Bitstring (Plus (UN FR a) (UN FR b)))
-> FinRel (FR (UN FR b)) (FR (Plus (UN FR a) (UN FR b)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Fin (UN FR b) -> Bitstring (Plus (UN FR a) (UN FR b)))
-> Vec (UN FR b) (Fin (UN FR b))
-> Vec (UN FR b) (Bitstring (Plus (UN FR a) (UN FR b)))
forall a b. (a -> b) -> Vec (UN FR b) a -> Vec (UN FR b) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap ((\Bitstring (UN FR b)
b -> forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring n -> Bitstring m -> Bitstring (Plus n m)
combine @a @b Bitstring (UN FR a)
0 Bitstring (UN FR b)
b) (Bitstring (UN FR b) -> Bitstring (Plus (UN FR a) (UN FR b)))
-> (Fin (UN FR b) -> Bitstring (UN FR b))
-> Fin (UN FR b)
-> Bitstring (Plus (UN FR a) (UN FR b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fin (UN FR b) -> Bitstring (UN FR b)
forall (n :: Nat). SNatI n => Fin n -> Bitstring n
bit) Vec (UN FR b) (Fin (UN FR b))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)
  FinRel @a Vec n (Bitstring m)
l ||| :: forall (x :: FINREL) (a :: FINREL) (y :: FINREL).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FinRel @b Vec n (Bitstring m)
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FR a) @(FR b) ((Ob (FR n || FR n) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (FR n || FR n) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$ Vec (Plus n n) (Bitstring m) -> FinRel (FR (Plus n n)) (FR m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (Vec n (Bitstring m)
l Vec n (Bitstring m)
-> Vec n (Bitstring m) -> Vec (Plus n n) (Bitstring m)
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec n (Bitstring m)
Vec n (Bitstring m)
r)

instance HasTerminalObject FINREL where
  type TerminalObject = FR Nat0
  terminate :: forall (a :: FINREL). Ob a => a ~> TerminalObject
terminate = Vec (UN FR a) (Bitstring 'Z) -> FinRel (FR (UN FR a)) (FR 'Z)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (Bitstring 'Z -> Vec (UN FR a) (Bitstring 'Z)
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat Bitstring 'Z
0)
instance HasBinaryProducts FINREL where
  type a && b = FR (Plus (UN FR a) (UN FR b))
  withObProd :: forall (a :: FINREL) (b :: FINREL) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @a @b r
Ob (a && b) => r
Ob (a || b) => r
r
  fst :: forall (a :: FINREL) (b :: FINREL). (Ob a, Ob b) => (a && b) ~> a
fst @(FR a) @(FR b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FR a) @(FR b) ((Ob (FR (UN FR a) && FR (UN FR b)) => (a && b) ~> a)
 -> (a && b) ~> a)
-> (Ob (FR (UN FR a) && FR (UN FR b)) => (a && b) ~> a)
-> (a && b) ~> a
forall a b. (a -> b) -> a -> b
$ Vec (Plus (UN FR a) (UN FR b)) (Bitstring (UN FR a))
-> FinRel (FR (Plus (UN FR a) (UN FR b))) (FR (UN FR a))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (FinRel (FR (UN FR a)) (FR (UN FR a))
-> Vec (UN FR a) (Bitstring (UN FR a))
forall (n :: Nat) (m :: Nat).
FinRel (FR n) (FR m) -> Vec n (Bitstring m)
unFinRel (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FINREL). (CategoryOf FINREL, Ob a) => Obj a
obj @(FR a)) Vec (UN FR a) (Bitstring (UN FR a))
-> Vec (UN FR b) (Bitstring (UN FR a))
-> Vec (Plus (UN FR a) (UN FR b)) (Bitstring (UN FR a))
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m)
zero @b @a)
  snd :: forall (a :: FINREL) (b :: FINREL). (Ob a, Ob b) => (a && b) ~> b
snd @(FR a) @(FR b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FR a) @(FR b) ((Ob (FR (UN FR a) && FR (UN FR b)) => (a && b) ~> b)
 -> (a && b) ~> b)
-> (Ob (FR (UN FR a) && FR (UN FR b)) => (a && b) ~> b)
-> (a && b) ~> b
forall a b. (a -> b) -> a -> b
$ Vec (Plus (UN FR a) (UN FR b)) (Bitstring (UN FR b))
-> FinRel (FR (Plus (UN FR a) (UN FR b))) (FR (UN FR b))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m)
zero @a @b Vec (UN FR a) (Bitstring (UN FR b))
-> Vec (UN FR b) (Bitstring (UN FR b))
-> Vec (Plus (UN FR a) (UN FR b)) (Bitstring (UN FR b))
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ FinRel (FR (UN FR b)) (FR (UN FR b))
-> Vec (UN FR b) (Bitstring (UN FR b))
forall (n :: Nat) (m :: Nat).
FinRel (FR n) (FR m) -> Vec n (Bitstring m)
unFinRel (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FINREL). (CategoryOf FINREL, Ob a) => Obj a
obj @(FR b)))
  FinRel @_ @a Vec n (Bitstring m)
l &&& :: forall (a :: FINREL) (x :: FINREL) (y :: FINREL).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& FinRel @_ @b Vec n (Bitstring m)
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FR a) @(FR b) ((Ob (FR m && FR m) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (FR m && FR m) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$ Vec n (Bitstring (Plus m m)) -> FinRel (FR n) (FR (Plus m m))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Bitstring m -> Bitstring m -> Bitstring (Plus m m))
-> Vec n (Bitstring m)
-> Vec n (Bitstring m)
-> Vec n (Bitstring (Plus m m))
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith Bitstring m -> Bitstring m -> Bitstring (Plus m m)
forall (n :: Nat) (m :: Nat).
SNatI n =>
Bitstring n -> Bitstring m -> Bitstring (Plus n m)
combine Vec n (Bitstring m)
l Vec n (Bitstring m)
Vec n (Bitstring m)
r)

instance HasBiproducts FINREL

instance MonoidalProfunctor FinRel where
  par0 :: FinRel Unit Unit
par0 = FinRel Unit Unit
FinRel (FR Nat1) (FR Nat1)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FINREL). Ob a => FinRel a a
id
  FinRel @nl @ml Vec n (Bitstring m)
l par :: forall (x1 :: FINREL) (x2 :: FINREL) (y1 :: FINREL) (y2 :: FINREL).
FinRel x1 x2 -> FinRel y1 y2 -> FinRel (x1 ** y1) (x2 ** y2)
`par` FinRel @nr @mr Vec n (Bitstring m)
r =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(FR nl) @(FR nr) ((Ob (FR n ** FR n) => FinRel (x1 ** y1) (x2 ** y2))
 -> FinRel (x1 ** y1) (x2 ** y2))
-> (Ob (FR n ** FR n) => FinRel (x1 ** y1) (x2 ** y2))
-> FinRel (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(FR ml) @(FR mr) ((Ob (FR m ** FR m) => FinRel (x1 ** y1) (x2 ** y2))
 -> FinRel (x1 ** y1) (x2 ** y2))
-> (Ob (FR m ** FR m) => FinRel (x1 ** y1) (x2 ** y2))
-> FinRel (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
        Vec (Mult n n) (Bitstring (Mult m m))
-> FinRel (FR (Mult n n)) (FR (Mult m m))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Bitstring m -> Vec n (Bitstring (Mult m m)))
-> Vec n (Bitstring m) -> Vec (Mult n n) (Bitstring (Mult m m))
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap (\Bitstring m
l' -> (Bitstring m -> Bitstring (Mult m m))
-> Vec n (Bitstring m) -> Vec n (Bitstring (Mult m m))
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Bitstring m -> Bitstring m -> Bitstring (Mult m m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Bitstring n -> Bitstring m -> Bitstring (Mult n m)
mult Bitstring m
l') Vec n (Bitstring m)
r) Vec n (Bitstring m)
l)

instance Monoidal FINREL where
  type FR a ** FR b = FR (Mult a b)
  type Unit = FR Nat1
  withOb2 :: forall (a :: FINREL) (b :: FINREL) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(FR a) @b Ob (a ** b) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @a of
    SNat (UN FR a)
SZ -> r
Ob (a ** b) => r
r
    SS @a' -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(FR a') @b ((Ob (FR n1 ** b) => r) -> r) -> (Ob (FR n1 ** b) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @b @(FR (Mult a' (UN FR b))) r
Ob (a ** b) => r
Ob (b || FR (Mult n1 (UN FR b))) => r
r
  leftUnitor :: forall (a :: FINREL). Ob a => (Unit ** a) ~> a
leftUnitor = FinSet (FS (Plus (UN FR a) 'Z)) (FS (UN FR a))
-> FinRel (FR (Plus (UN FR a) 'Z)) (FR (UN FR a))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (Unit ** FS (UN FR a)) ~> FS (UN FR a)
FinSet (FS (Plus (UN FR a) 'Z)) (FS (UN FR a))
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: FINSET). Ob a => (Unit ** a) ~> a
leftUnitor
  leftUnitorInv :: forall (a :: FINREL). Ob a => a ~> (Unit ** a)
leftUnitorInv = FinSet (FS (UN FR a)) (FS (Plus (UN FR a) 'Z))
-> FinRel (FR (UN FR a)) (FR (Plus (UN FR a) 'Z))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr FS (UN FR a) ~> (Unit ** FS (UN FR a))
FinSet (FS (UN FR a)) (FS (Plus (UN FR a) 'Z))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: FINSET). Ob a => a ~> (Unit ** a)
leftUnitorInv
  rightUnitor :: forall (a :: FINREL). Ob a => (a ** Unit) ~> a
rightUnitor = FinSet (FS (Mult (UN FR a) Nat1)) (FS (UN FR a))
-> FinRel (FR (Mult (UN FR a) Nat1)) (FR (UN FR a))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (FS (UN FR a) ** Unit) ~> FS (UN FR a)
FinSet (FS (Mult (UN FR a) Nat1)) (FS (UN FR a))
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
forall (a :: FINSET). Ob a => (a ** Unit) ~> a
rightUnitor
  rightUnitorInv :: forall (a :: FINREL). Ob a => a ~> (a ** Unit)
rightUnitorInv = FinSet (FS (UN FR a)) (FS (Mult (UN FR a) Nat1))
-> FinRel (FR (UN FR a)) (FR (Mult (UN FR a) Nat1))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr FS (UN FR a) ~> (FS (UN FR a) ** Unit)
FinSet (FS (UN FR a)) (FS (Mult (UN FR a) Nat1))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
forall (a :: FINSET). Ob a => a ~> (a ** Unit)
rightUnitorInv
  associator :: forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(FR a) @(FR b) @(FR c) = FinSet
  (FS (Mult (Mult (UN FR a) (UN FR b)) (UN FR c)))
  (FS (Mult (UN FR a) (Mult (UN FR b) (UN FR c))))
-> FinRel
     (FR (Mult (Mult (UN FR a) (UN FR b)) (UN FR c)))
     (FR (Mult (UN FR a) (Mult (UN FR b) (UN FR c))))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @(FS a) @(FS b) @(FS c))
  associatorInv :: forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(FR a) @(FR b) @(FR c) = FinSet
  (FS (Mult (UN FR a) (Mult (UN FR b) (UN FR c))))
  (FS (Mult (Mult (UN FR a) (UN FR b)) (UN FR c)))
-> FinRel
     (FR (Mult (UN FR a) (Mult (UN FR b) (UN FR c))))
     (FR (Mult (Mult (UN FR a) (UN FR b)) (UN FR c)))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @(FS a) @(FS b) @(FS c))

instance SymMonoidal FINREL where
  swap :: forall (a :: FINREL) (b :: FINREL).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(FR a) @(FR b) = FinSet
  (FS (Mult (UN FR a) (UN FR b))) (FS (Mult (UN FR b) (UN FR a)))
-> FinRel
     (FR (Mult (UN FR a) (UN FR b))) (FR (Mult (UN FR b) (UN FR a)))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(FS a) @(FS b))

instance Distributive FINREL where
  distL :: forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @(FR a) @(FR b) @(FR c) = FinSet
  (FS (Mult (UN FR a) (Plus (UN FR b) (UN FR c))))
  (FS (Plus (Mult (UN FR a) (UN FR b)) (Mult (UN FR a) (UN FR c))))
-> FinRel
     (FR (Mult (UN FR a) (Plus (UN FR b) (UN FR c))))
     (FR (Plus (Mult (UN FR a) (UN FR b)) (Mult (UN FR a) (UN FR c))))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @_ @(FS a) @(FS b) @(FS c))
  distR :: forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @(FR a) @(FR b) @(FR c) = FinSet
  (FS (Mult (Plus (UN FR a) (UN FR b)) (UN FR c)))
  (FS (Plus (Mult (UN FR a) (UN FR c)) (Mult (UN FR b) (UN FR c))))
-> FinRel
     (FR (Mult (Plus (UN FR a) (UN FR b)) (UN FR c)))
     (FR (Plus (Mult (UN FR a) (UN FR c)) (Mult (UN FR b) (UN FR c))))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @_ @(FS a) @(FS b) @(FS c))
  distL0 :: forall (a :: FINREL). Ob a => (a ** InitialObject) ~> InitialObject
distL0 @(FR a) = FinSet (FS (Mult (UN FR a) 'Z)) (FS 'Z)
-> FinRel (FR (Mult (UN FR a) 'Z)) (FR 'Z)
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
distL0 @_ @(FS a))
  distR0 :: forall (a :: FINREL). Ob a => (InitialObject ** a) ~> InitialObject
distR0 @(FR a) = FinSet (FS 'Z) (FS 'Z) -> FinRel (FR 'Z) (FR 'Z)
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr (forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
distR0 @_ @(FS a))

instance Closed FINREL where
  type x ~~> y = ExpSA x y
  withObExp :: forall (a :: FINREL) (b :: FINREL) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @x @y Ob (a ~~> b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @y r
Ob (a ** b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @x @y = forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(StarAutonomous FINREL, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA @x @y
  apply :: forall (a :: FINREL) (b :: FINREL).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @y @z = forall {k} (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
forall (b :: FINREL) (c :: FINREL).
(StarAutonomous FINREL, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
applySA @y @z
  ^^^ :: forall (a :: FINREL) (b :: FINREL) (x :: FINREL) (y :: FINREL).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) = (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA

instance StarAutonomous FINREL where
  type Dual n = n
  dual :: forall (a :: FINREL) (b :: FINREL). (a ~> b) -> Dual b ~> Dual a
dual = (a ~> b) -> Dual b ~> Dual a
FinRel a b -> FinRel b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: FINREL) (b :: FINREL). FinRel a b -> FinRel b a
dagger
  dualInv :: forall (a :: FINREL) (b :: FINREL).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv = (Dual a ~> Dual b) -> b ~> a
FinRel (FR (UN FR a)) (FR (UN FR b))
-> FinRel (FR (UN FR b)) (FR (UN FR a))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: FINREL) (b :: FINREL). FinRel a b -> FinRel b a
dagger
  linDist :: forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @(FR a) @(FR b) @(FR c) (FinRel Vec n (Bitstring m)
m) = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(FR b) @(FR c) ((Ob (FR (UN FR b) ** FR (UN FR c)) => a ~> Dual (b ** c))
 -> a ~> Dual (b ** c))
-> (Ob (FR (UN FR b) ** FR (UN FR c)) => a ~> Dual (b ** c))
-> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$ Vec (UN FR a) (Bitstring (Mult (UN FR b) (UN FR c)))
-> FinRel (FR (UN FR a)) (FR (Mult (UN FR b) (UN FR c)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel ((Vec (UN FR b) (Bitstring m)
 -> Bitstring (Mult (UN FR b) (UN FR c)))
-> Vec (UN FR a) (Vec (UN FR b) (Bitstring m))
-> Vec (UN FR a) (Bitstring (Mult (UN FR b) (UN FR c)))
forall a b. (a -> b) -> Vec (UN FR a) a -> Vec (UN FR a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Vec (UN FR b) (Bitstring m) -> Bitstring (Mult (UN FR b) m)
Vec (UN FR b) (Bitstring m) -> Bitstring (Mult (UN FR b) (UN FR c))
forall (m :: Nat) (n :: Nat).
SNatI m =>
Vec n (Bitstring m) -> Bitstring (Mult n m)
combines (forall (n :: Nat) (m :: Nat) a.
(SNatI n, SNatI m) =>
Vec (Mult n m) a -> Vec n (Vec m a)
chunks @a @b Vec n (Bitstring m)
Vec (Mult (UN FR a) (UN FR b)) (Bitstring m)
m))
  linDistInv :: forall (a :: FINREL) (b :: FINREL) (c :: FINREL).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @(FR a) @(FR b) @(FR c) (FinRel Vec n (Bitstring m)
m) = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(FR a) @(FR b) ((Ob (FR (UN FR a) ** FR (UN FR b)) => (a ** b) ~> Dual c)
 -> (a ** b) ~> Dual c)
-> (Ob (FR (UN FR a) ** FR (UN FR b)) => (a ** b) ~> Dual c)
-> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$ Vec (Mult (UN FR a) (UN FR b)) (Bitstring (UN FR c))
-> FinRel (FR (Mult (UN FR a) (UN FR b))) (FR (UN FR c))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap @_ @b @_ @a (forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Bitstring (Mult n m) -> Vec n (Bitstring m)
splits @b @c) Vec n (Bitstring m)
Vec (UN FR a) (Bitstring m)
m)

instance CompactClosed FINREL where
  distribDual :: forall (a :: FINREL) (b :: FINREL).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @m @n = FinRel (FR (UN FR a)) (FR (UN FR a))
-> FinRel (FR (UN FR a)) (FR (UN FR a))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: FINREL) (b :: FINREL). FinRel a b -> FinRel b a
dagger (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FINREL). (CategoryOf FINREL, Ob a) => Obj a
obj @m) FinRel (FR (UN FR a)) (FR (UN FR a))
-> FinRel (FR (UN FR b)) (FR (UN FR b))
-> FinRel
     (FR (UN FR a) ** FR (UN FR b)) (FR (UN FR a) ** FR (UN FR b))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: FINREL) (x2 :: FINREL) (y1 :: FINREL) (y2 :: FINREL).
FinRel x1 x2 -> FinRel y1 y2 -> FinRel (x1 ** y1) (x2 ** y2)
`par` FinRel (FR (UN FR b)) (FR (UN FR b))
-> FinRel (FR (UN FR b)) (FR (UN FR b))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: FINREL) (b :: FINREL). FinRel a b -> FinRel b a
dagger (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FINREL). (CategoryOf FINREL, Ob a) => Obj a
obj @n)
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
FinRel (FR Nat1) (FR Nat1)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FINREL). Ob a => FinRel a a
id

instance MonoidalAction FINREL FINREL where
  type Act p x = p ** x
  withObAct :: forall (a :: FINREL) (x :: FINREL) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @b @c Ob (Act a x) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c r
Ob (a ** x) => r
Ob (Act a x) => r
r
  unitor :: forall (x :: FINREL). Ob x => Act Unit x ~> x
unitor = (Unit ** FR (UN FR x)) ~> FR (UN FR x)
Act Unit x ~> x
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: FINREL). Ob a => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall (x :: FINREL). Ob x => x ~> Act Unit x
unitorInv = x ~> Act Unit x
FR (UN FR x) ~> (Unit ** FR (UN FR x))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: FINREL). Ob a => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall (a :: FINREL) (b :: FINREL) (x :: FINREL).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @b @c @d = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @b @c @d
  multiplicatorInv :: forall (a :: FINREL) (b :: FINREL) (x :: FINREL).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv @b @c @d = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @b @c @d

instance Strong FINREL FinRel where
  act :: forall (a :: FINREL) (b :: FINREL) (x :: FINREL) (y :: FINREL).
(a ~> b) -> FinRel x y -> FinRel (Act a x) (Act b y)
act = (a ~> b) -> FinRel x y -> FinRel (Act a x) (Act b y)
FinRel a b -> FinRel x y -> FinRel (a ** x) (b ** y)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: FINREL) (x2 :: FINREL) (y1 :: FINREL) (y2 :: FINREL).
FinRel x1 x2 -> FinRel y1 y2 -> FinRel (x1 ** y1) (x2 ** y2)
par

instance Costrong FINREL FinRel where
  coact :: forall (a :: FINREL) (x :: FINREL) (y :: FINREL).
(Ob a, Ob x, Ob y) =>
FinRel (Act a x) (Act a y) -> FinRel x y
coact @x = forall {m} {k} (u :: m) (x :: k) (y :: k).
(CompactClosed m, MonoidalAction m k, Ob x, Ob y, Ob u) =>
(Act u x ~> Act u y) -> x ~> y
forall (u :: FINREL) (x :: FINREL) (y :: FINREL).
(CompactClosed FINREL, MonoidalAction FINREL FINREL, Ob x, Ob y,
 Ob u) =>
(Act u x ~> Act u y) -> x ~> y
coactCC @x

-- >>> import Data.Type.Nat
-- >>> mappend @(FR Nat3)
-- FinRel {unFinRel = 100 ::: 000 ::: 000 ::: 000 ::: 010 ::: 000 ::: 000 ::: 000 ::: 001 ::: VNil}
instance (SNatI a) => Monoid (FR a) where
  mempty :: Unit ~> FR a
mempty = Vec Nat1 (Bitstring a) -> FinRel (FR Nat1) (FR a)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (Bitstring a
forall a. Bounded a => a
P.maxBound Bitstring a -> Vec 'Z (Bitstring a) -> Vec Nat1 (Bitstring a)
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Bitstring a)
forall a. Vec 'Z a
VNil)
  mappend :: (FR a ** FR a) ~> FR a
mappend =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(FR a) @(FR a) ((Ob (FR a ** FR a) => (FR a ** FR a) ~> FR a)
 -> (FR a ** FR a) ~> FR a)
-> (Ob (FR a ** FR a) => (FR a ** FR a) ~> FR a)
-> (FR a ** FR a) ~> FR a
forall a b. (a -> b) -> a -> b
$
      Vec (Mult a a) (Bitstring a) -> FinRel (FR (Mult a a)) (FR a)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Bitstring m) -> FinRel (FR n) (FR m)
FinRel (forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap @_ @a @_ @a (\Fin a
i -> (Fin a -> Bitstring a) -> Vec a (Fin a) -> Vec a (Bitstring a)
forall a b. (a -> b) -> Vec a a -> Vec a b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\Fin a
j -> if Fin a
i Fin a -> Fin a -> Bool
forall a. Eq a => a -> a -> Bool
P.== Fin a
j then Fin a -> Bitstring a
forall (n :: Nat). SNatI n => Fin n -> Bitstring n
bit Fin a
i else Bitstring a
0) Vec a (Fin a)
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe) Vec a (Fin a)
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)

-- >>> import Data.Type.Nat
-- >>> comult @(FR Nat3)
-- FinRel {unFinRel = 100000000 ::: 000010000 ::: 000000001 ::: VNil}
instance (SNatI a) => Comonoid (FR a) where
  counit :: FR a ~> Unit
counit = FinSet (FS a) (FS Nat1) -> FinRel (FR a) (FR Nat1)
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr FS a ~> Unit
FinSet (FS a) (FS Nat1)
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  comult :: FR a ~> (FR a ** FR a)
comult = FinSet (FS a) (FS (Mult a a)) -> FinRel (FR a) (FR (Mult a a))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr FS a ~> (FS a ** FS a)
FinSet (FS a) (FS (Mult a a))
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

instance (SNatI a) => Frobenius (FR a) where
  spider :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
NFold n (FR a) ~> NFold m (FR a)
spider @x @y = forall {k} (n :: Nat) (m :: Nat) (a :: k).
(Monoid a, Comonoid a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
forall (n :: Nat) (m :: Nat) (a :: FINREL).
(Monoid a, Comonoid a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
spiderDefault @x @y @(FR a)
instance Hypergraph FINREL
instance CopyDiscard FINREL

data family Fun :: FINSET +-> FINREL
instance FunctorForRep Fun where
  type Fun @ FS a = FR a
  fmap :: forall (a :: FINSET) (b :: FINSET).
(a ~> b) -> (Fun @ a) ~> (Fun @ b)
fmap a ~> b
f = FinSet (FS (UN FS a)) (FS (UN FS b))
-> FinRel (FR (UN FS a)) (FR (UN FS b))
forall (n :: Nat) (m :: Nat).
FinSet (FS m) (FS n) -> FinRel (FR m) (FR n)
arr a ~> b
FinSet (FS (UN FS a)) (FS (UN FS b))
f ((Ob a, Ob b) => FinRel (Fun @ a) (Fun @ b))
-> FinSet a b -> FinRel (Fun @ a) (Fun @ b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FINSET) (b :: FINSET) r.
((Ob a, Ob b) => r) -> FinSet a b -> r
\\ a ~> b
FinSet a b
f
instance MonoidalProfunctor (Rep Fun) where
  par0 :: Rep Fun Unit Unit
par0 = (FR Nat1 ~> (Fun @ FS Nat1)) -> Rep Fun (FR Nat1) (FS Nat1)
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep FR Nat1 ~> (Fun @ FS Nat1)
FinRel Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Rep @_ @_ @b x1 ~> (Fun @ x2)
l par :: forall (x1 :: FINREL) (x2 :: FINSET) (y1 :: FINREL) (y2 :: FINSET).
Rep Fun x1 x2 -> Rep Fun y1 y2 -> Rep Fun (x1 ** y1) (x2 ** y2)
`par` Rep @_ @_ @d y1 ~> (Fun @ y2)
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @d ((Ob (x2 ** y2) => Rep Fun (x1 ** y1) (x2 ** y2))
 -> Rep Fun (x1 ** y1) (x2 ** y2))
-> (Ob (x2 ** y2) => Rep Fun (x1 ** y1) (x2 ** y2))
-> Rep Fun (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ ((x1 ** y1) ~> (Fun @ FS (Mult (UN FS x2) (UN FS y2))))
-> Rep Fun (x1 ** y1) (FS (Mult (UN FS x2) (UN FS y2)))
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (x1 ~> (Fun @ x2)
FinRel x1 (FR (UN FS x2))
l FinRel x1 (FR (UN FS x2))
-> FinRel y1 (FR (UN FS y2))
-> FinRel (x1 ** y1) (FR (UN FS x2) ** FR (UN FS y2))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: FINREL) (x2 :: FINREL) (y1 :: FINREL) (y2 :: FINREL).
FinRel x1 x2 -> FinRel y1 y2 -> FinRel (x1 ** y1) (x2 ** y2)
`par` y1 ~> (Fun @ y2)
FinRel y1 (FR (UN FS y2))
r)
instance MonoidalProfunctor (Coprod (Rep Fun)) where
  par0 :: Coprod (Rep Fun) Unit Unit
par0 = Rep Fun (FR 'Z) (FS 'Z)
-> Coprod (Rep Fun) ('COPR (FR 'Z)) ('COPR (FS 'Z))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((FR 'Z ~> (Fun @ FS 'Z)) -> Rep Fun (FR 'Z) (FS 'Z)
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep FR 'Z ~> (Fun @ FS 'Z)
FinRel (FR 'Z) (FR 'Z)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FINREL). Ob a => FinRel a a
id)
  Coprod (Rep @_ @_ @b a1 ~> (Fun @ b1)
l) par :: forall (x1 :: COPROD FINREL) (x2 :: COPROD FINSET)
       (y1 :: COPROD FINREL) (y2 :: COPROD FINSET).
Coprod (Rep Fun) x1 x2
-> Coprod (Rep Fun) y1 y2 -> Coprod (Rep Fun) (x1 ** y1) (x2 ** y2)
`par` Coprod (Rep @_ @_ @d a1 ~> (Fun @ b1)
r) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @b @d ((Ob (b1 || b1) => Coprod (Rep Fun) (x1 ** y1) (x2 ** y2))
 -> Coprod (Rep Fun) (x1 ** y1) (x2 ** y2))
-> (Ob (b1 || b1) => Coprod (Rep Fun) (x1 ** y1) (x2 ** y2))
-> Coprod (Rep Fun) (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ Rep Fun (a1 || a1) (FS (Plus (UN FS b1) (UN FS b1)))
-> Coprod
     (Rep Fun)
     ('COPR (a1 || a1))
     ('COPR (FS (Plus (UN FS b1) (UN FS b1))))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (((a1 || a1) ~> (Fun @ FS (Plus (UN FS b1) (UN FS b1))))
-> Rep Fun (a1 || a1) (FS (Plus (UN FS b1) (UN FS b1)))
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (a1 ~> (Fun @ b1)
a1 ~> FR (UN FS b1)
l (a1 ~> FR (UN FS b1))
-> (a1 ~> FR (UN FS b1))
-> (a1 || a1) ~> (FR (UN FS b1) || FR (UN FS b1))
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall (a :: FINREL) (b :: FINREL) (x :: FINREL) (y :: FINREL).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ a1 ~> (Fun @ b1)
a1 ~> FR (UN FS b1)
r))