{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Algebra.Category.BlockMatrix where

import Algebra.Category
import Algebra.Category.Laws
import Algebra.Category.Objects (Trivial,forallSumType)
import Algebra.Types
import Algebra.Classes
import Prelude (Int,Bool(..),Show(..),($),Semigroup(..),error)
import Test.QuickCheck hiding (scale)
import Test.QuickCheck.Property
import Data.Constraint
import Control.Applicative


data M s a b where
  Zero :: M s a b
  Diag :: s -> M s a a
  (:▵)  :: M s a b -> M s a c ->  M s a (b ⊕ c)
  (:▿)  :: M s b a -> M s c a ->  M s (b ⊕ c) a
  EmptyL :: M s Zero a -- no elements
  EmptyR :: M s a Zero -- no elements
  -- EmptyR and EmptyL are there to make the law unitorR . unitorR_ pass
deriving instance Show s => Show (M s a b)

    
instance (Show s, Additive s, TestEqual s) => TestEqual (M s a b) where
  M s a b
EmptyR =.= :: M s a b -> M s a b -> Property
=.= M s a b
_ = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
  M s a b
EmptyL =.= M s a b
_ = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
  M s a b
_ =.= M s a b
EmptyR = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
  M s a b
_ =.= M s a b
EmptyL = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
  (M s a b
a :▵ M s a c
b) =.= M s a b
c = case M s a (b ⊕ c) -> (M s a b, M s a c)
forall s a b c. M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit M s a b
M s a (b ⊕ c)
c of
    (M s a b
a',M s a c
b') -> (M s a b
a M s a b -> M s a b -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s a b
a') Property -> Property -> Property
forall a. Multiplicative a => a -> a -> a
* (M s a c
b M s a c -> M s a c -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s a c
b')
  (M s b b
a :▿ M s c b
b) =.= M s a b
c = case M s (b ⊕ c) b -> (M s b b, M s c b)
forall s b c a. M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' M s a b
M s (b ⊕ c) b
c of
    (M s b b
a',M s c b
b') -> (M s b b
a M s b b -> M s b b -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s b b
a') Property -> Property -> Property
forall a. Multiplicative a => a -> a -> a
* (M s c b
b M s c b -> M s c b -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s c b
b')
  M s a b
c =.= (M s a b
a :▵ M s a c
b) = case M s a (b ⊕ c) -> (M s a b, M s a c)
forall s a b c. M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit M s a b
M s a (b ⊕ c)
c of
    (M s a b
a',M s a c
b') -> (M s a b
a M s a b -> M s a b -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s a b
a') Property -> Property -> Property
forall a. Multiplicative a => a -> a -> a
* (M s a c
b M s a c -> M s a c -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s a c
b')
  M s a b
c =.= (M s b b
a :▿ M s c b
b) = case M s (b ⊕ c) b -> (M s b b, M s c b)
forall s b c a. M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' M s a b
M s (b ⊕ c) b
c of
    (M s b b
a',M s c b
b') -> (M s b b
a M s b b -> M s b b -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s b b
a') Property -> Property -> Property
forall a. Multiplicative a => a -> a -> a
* (M s c b
b M s c b -> M s c b -> Property
forall a. TestEqual a => a -> a -> Property
=.= M s c b
b')
  M s a b
Zero =.= M s a b
c = M s a b -> Property
forall s a b. (Additive s, TestEqual s) => M s a b -> Property
testZero M s a b
c
  M s a b
c =.= M s a b
Zero = M s a b -> Property
forall s a b. (Additive s, TestEqual s) => M s a b -> Property
testZero M s a b
c
  (Diag s
x) =.= (Diag s
y) = s
x s -> s -> Property
forall a. TestEqual a => a -> a -> Property
=.= s
y

testZero :: (Additive s, TestEqual s) => M s a b -> Property
testZero :: forall s a b. (Additive s, TestEqual s) => M s a b -> Property
testZero = \case
     M s a b
EmptyL -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
     M s a b
EmptyR -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
     M s a b
Zero -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
     Diag s
s -> s
s s -> s -> Property
forall a. TestEqual a => a -> a -> Property
=.= s
forall a. Additive a => a
zero
     M s a b
a :▵ M s a c
b -> M s a b -> Property
forall s a b. (Additive s, TestEqual s) => M s a b -> Property
testZero M s a b
a Property -> Property -> Property
forall a. Multiplicative a => a -> a -> a
* M s a c -> Property
forall s a b. (Additive s, TestEqual s) => M s a b -> Property
testZero M s a c
b
     M s b b
a :▿ M s c b
b -> M s b b -> Property
forall s a b. (Additive s, TestEqual s) => M s a b -> Property
testZero M s b b
a Property -> Property -> Property
forall a. Multiplicative a => a -> a -> a
* M s c b -> Property
forall s a b. (Additive s, TestEqual s) => M s a b -> Property
testZero M s c b
b

instance Ring s => Scalable s (M s a b) where
  s
s *^ :: s -> M s a b -> M s a b
*^ M s a b
c = case M s a b
c of
    M s a b
EmptyR -> M s a b
M s a Zero
forall s a. M s a Zero
EmptyR
    M s a b
EmptyL -> M s a b
M s Zero b
forall s a. M s Zero a
EmptyL
    M s a b
Zero -> M s a b
forall s a b. M s a b
Zero
    Diag s
x -> s -> M s a a
forall s a. s -> M s a a
Diag (s
ss -> s -> s
forall a. Multiplicative a => a -> a -> a
*s
x)
    M s b b
a :▿ M s c b
b -> (s
s s -> M s b b -> M s b b
forall s a. Scalable s a => s -> a -> a
*^ M s b b
a) M s b b -> M s c b -> M s (b ⊕ c) b
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿ (s
s s -> M s c b -> M s c b
forall s a. Scalable s a => s -> a -> a
*^ M s c b
b)
    M s a b
a :▵ M s a c
b -> (s
s s -> M s a b -> M s a b
forall s a. Scalable s a => s -> a -> a
*^ M s a b
a) M s a b -> M s a c -> M s a (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵ (s
s s -> M s a c -> M s a c
forall s a. Scalable s a => s -> a -> a
*^ M s a c
b)
  
instance Ring s => Category (M s) where
  M s b c
EmptyL . :: forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b c -> M s a b -> M s a c
. M s a b
EmptyR = M s a c
forall s a b. M s a b
Zero -- adding zero elements together for each position in the matrix
  M s b c
EmptyR . M s a b
_ = M s a c
M s a Zero
forall s a. M s a Zero
EmptyR
  M s b c
_ . M s a b
EmptyL = M s a c
M s Zero c
forall s a. M s Zero a
EmptyL
  M s b c
Zero . M s a b
_ = M s a c
forall s a b. M s a b
Zero
  M s b c
_ . M s a b
Zero = M s a c
forall s a b. M s a b
Zero
  Diag s
s . M s a b
m = s
s s -> M s a c -> M s a c
forall s a. Scalable s a => s -> a -> a
*^ M s a b
M s a c
m
  M s b c
m . Diag s
s = s
s s -> M s a c -> M s a c
forall s a. Scalable s a => s -> a -> a
*^ M s a c
M s b c
m
  (M s b b
a1 :▵ M s b c
a2) . M s a b
b = (M s b b
a1 M s b b -> M s a b -> M s a b
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b c -> M s a b -> M s a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. M s a b
b) M s a b -> M s a c -> M s a (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵ (M s b c
a2 M s b c -> M s a b -> M s a c
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b c -> M s a b -> M s a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. M s a b
b)
  M s b c
a . (M s b b
b1 :▿ M s c b
b2) = (M s b c
a M s b c -> M s b b -> M s b c
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b c -> M s a b -> M s a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. M s b b
b1) M s b c -> M s c c -> M s (b ⊕ c) c
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿ (M s b c
a M s b c -> M s c b -> M s c c
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b c -> M s a b -> M s a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. M s c b
b2)
  (M s b c
a1 :▿ M s c c
a2) . (M s a b
b1 :▵ M s a c
b2) = M s b c
a1 M s b c -> M s a b -> M s a c
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b c -> M s a b -> M s a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. M s a b
M s a b
b1 M s a c -> M s a c -> M s a c
forall a. Additive a => a -> a -> a
+ M s c c
a2 M s c c -> M s a c -> M s a c
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b c -> M s a b -> M s a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. M s a c
M s a c
b2

  type Obj (M s) = Trivial
  id :: forall a. Obj (M s) a => M s a a
id = s -> M s a a
forall s a. s -> M s a a
Diag s
forall a. Multiplicative a => a
one

instance Ring s => Monoidal (⊕) Zero (M s) where
  ⊗ :: forall a b c d.
(Obj (M s) a, Obj (M s) b, Obj (M s) c, Obj (M s) d) =>
M s a b -> M s c d -> M s (a ⊕ c) (b ⊕ d)
(⊗) = M s a b -> M s c d -> M s (a ⊕ c) (b ⊕ d)
forall {k1} (k2 :: k1 -> k1 -> *) (x :: k1 -> k1 -> k1) (b1 :: k1)
       (b2 :: k1) (b3 :: k1) (c :: k1) (i :: k1).
(Obj k2 (x b1 b2), Obj k2 b3, Obj k2 c, Obj k2 b1, Obj k2 b2,
 Cartesian x i k2) =>
k2 b1 b3 -> k2 b2 c -> k2 (x b1 b2) (x b3 c)
cartesianCross -- a potential optimisation is that two diagonals will be a new diagonal. Represent diagonals as (sparse) vectors?
  assoc :: forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
assoc = M s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
forall {k1} (a :: k1) (b :: k1) (x :: k1 -> k1 -> k1) (i :: k1)
       (c :: k1) (k2 :: k1 -> k1 -> *) (con :: k1 -> Constraint).
(Obj k2 a, Obj k2 b, Obj k2 c, Cartesian x i k2, Con' x con,
 con ~ Obj k2) =>
k2 (x (x a b) c) (x a (x b c))
cartesianAssoc
  assoc_ :: forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s (a ⊕ (b ⊕ c)) ((a ⊕ b) ⊕ c)
assoc_ = M s (a ⊕ (b ⊕ c)) ((a ⊕ b) ⊕ c)
forall {k1} (a :: k1) (b :: k1) (x :: k1 -> k1 -> k1) (i :: k1)
       (c :: k1) (k2 :: k1 -> k1 -> *) (con :: k1 -> Constraint).
(Obj k2 a, Obj k2 b, Obj k2 c, Cartesian x i k2, Con' x con,
 con ~ Obj k2) =>
k2 (x a (x b c)) (x (x a b) c)
cartesianAssoc_
  unitorR :: forall a. (Obj (M s) a, Obj (M s) Zero) => M s a (a ⊕ Zero)
unitorR = M s a (a ⊕ Zero)
forall {k1} (a :: k1) (k2 :: k1 -> k1 -> *) (x :: k1 -> k1 -> k1)
       (i :: k1).
(Obj k2 a, Obj k2 i, Cartesian x i k2) =>
k2 a (x a i)
cartesianUnitor
  unitorR_ :: forall a. (Obj (M s) a, Obj (M s) Zero) => M s (a ⊕ Zero) a
unitorR_ = M s a a
forall a. Obj (M s) a => M s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id M s a a -> M s Zero a -> M s (a ⊕ Zero) a
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b a -> M s c a -> M s (b ⊕ c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ M s Zero a
forall a. Obj (M s) a => M s Zero a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat i a
new

instance Ring s => Symmetric (⊕) Zero (M s)
instance Ring s => Braided (⊕) Zero (M s) where
  swap :: forall a b. (Obj (M s) a, Obj (M s) b) => M s (a ⊕ b) (b ⊕ a)
swap = (M s a b
forall a. Additive a => a
zero M s a b -> M s a a -> M s a (b ⊕ a)
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s a b -> M s a c -> M s a (b ⊕ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ M s a a
forall a. Obj (M s) a => M s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id) M s a (b ⊕ a) -> M s b (b ⊕ a) -> M s (a ⊕ b) (b ⊕ a)
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b a -> M s c a -> M s (b ⊕ c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ (M s b b
forall a. Obj (M s) a => M s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id M s b b -> M s b a -> M s b (b ⊕ a)
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s a b -> M s a c -> M s a (b ⊕ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ M s b a
forall a. Additive a => a
zero)
instance Ring s => Cartesian (⊕) Zero (M s) where
  ▵ :: forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s a b -> M s a c -> M s a (b ⊕ c)
(▵) = M s a b -> M s a c -> M s a (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
(:▵)
  dis :: forall a. Obj (M s) a => M s a Zero
dis = M s a Zero
forall s a. M s a Zero
EmptyR
  exl :: forall a b. O2 (M s) a b => M s (a ⊕ b) a
exl = M s a a
forall a. Obj (M s) a => M s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id M s a a -> M s b a -> M s (a ⊕ b) a
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b a -> M s c a -> M s (b ⊕ c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ M s b a
forall s a b. M s a b
Zero
  exr :: forall a b. O2 (M s) a b => M s (a ⊕ b) b
exr = M s a b
forall s a b. M s a b
Zero M s a b -> M s b b -> M s (a ⊕ b) b
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b a -> M s c a -> M s (b ⊕ c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ M s b b
forall a. Obj (M s) a => M s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id

instance Ring s => CoCartesian (⊕) Zero (M s) where
  ▿ :: forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s b a -> M s c a -> M s (b ⊕ c) a
(▿) = M s b a -> M s c a -> M s (b ⊕ c) a
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
(:▿)
  new :: forall a. Obj (M s) a => M s Zero a
new = M s Zero a
forall s a. M s Zero a
EmptyL
  inl :: forall a b. O2 (M s) a b => M s a (a ⊕ b)
inl = M s a a
forall a. Obj (M s) a => M s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id M s a a -> M s a b -> M s a (a ⊕ b)
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s a b -> M s a c -> M s a (b ⊕ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ M s a b
forall s a b. M s a b
Zero
  inr :: forall a b. O2 (M s) a b => M s b (a ⊕ b)
inr = M s b a
forall s a b. M s a b
Zero M s b a -> M s b b -> M s b (a ⊕ b)
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s a b -> M s a c -> M s a (b ⊕ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ M s b b
forall a. Obj (M s) a => M s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id

instance Additive s => Additive (M s a b) where
  zero :: M s a b
zero = M s a b
forall s a b. M s a b
Zero
  M s a b
Zero + :: M s a b -> M s a b -> M s a b
+ M s a b
a = M s a b
a
  M s a b
a + M s a b
Zero = M s a b
a
  M s a b
EmptyL + M s a b
_ = M s a b
M s Zero b
forall s a. M s Zero a
EmptyL
  M s a b
_ + M s a b
EmptyL = M s a b
M s Zero b
forall s a. M s Zero a
EmptyL
  M s a b
EmptyR + M s a b
_ = M s a b
M s a Zero
forall s a. M s a Zero
EmptyR
  M s a b
_ + M s a b
EmptyR = M s a b
M s a Zero
forall s a. M s a Zero
EmptyR
  (M s a b
a :▵ M s a c
b) + M s a b
m  = (M s a b
a M s a b -> M s a b -> M s a b
forall a. Additive a => a -> a -> a
+ M s a b
d) M s a b -> M s a c -> M s a (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵ (M s a c
b M s a c -> M s a c -> M s a c
forall a. Additive a => a -> a -> a
+ M s a c
c) where (M s a b
d,M s a c
c) = M s a (b ⊕ c) -> (M s a b, M s a c)
forall s a b c. M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit  M s a b
M s a (b ⊕ c)
m
  M s a b
m  + (M s a b
a :▵ M s a c
b) = (M s a b
a M s a b -> M s a b -> M s a b
forall a. Additive a => a -> a -> a
+ M s a b
d) M s a b -> M s a c -> M s a (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵ (M s a c
b M s a c -> M s a c -> M s a c
forall a. Additive a => a -> a -> a
+ M s a c
c) where (M s a b
d,M s a c
c) = M s a (b ⊕ c) -> (M s a b, M s a c)
forall s a b c. M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit  M s a b
M s a (b ⊕ c)
m
  (M s b b
a :▿ M s c b
b) + M s a b
m  = (M s b b
a M s b b -> M s b b -> M s b b
forall a. Additive a => a -> a -> a
+ M s b b
d) M s b b -> M s c b -> M s (b ⊕ c) b
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿ (M s c b
b M s c b -> M s c b -> M s c b
forall a. Additive a => a -> a -> a
+ M s c b
c) where (M s b b
d,M s c b
c) = M s (b ⊕ c) b -> (M s b b, M s c b)
forall s b c a. M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' M s a b
M s (b ⊕ c) b
m
  M s a b
m  + (M s b b
a :▿ M s c b
b) = (M s b b
a M s b b -> M s b b -> M s b b
forall a. Additive a => a -> a -> a
+ M s b b
d) M s b b -> M s c b -> M s (b ⊕ c) b
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿ (M s c b
b M s c b -> M s c b -> M s c b
forall a. Additive a => a -> a -> a
+ M s c b
c) where (M s b b
d,M s c b
c) = M s (b ⊕ c) b -> (M s b b, M s c b)
forall s b c a. M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' M s a b
M s (b ⊕ c) b
m
  Diag s
s + Diag s
t = s -> M s a a
forall s a. s -> M s a a
Diag (s
s s -> s -> s
forall a. Additive a => a -> a -> a
+ s
t)

instance Group s => Group (M s a b) where
  negate :: M s a b -> M s a b
negate = \case
    M s a b
EmptyL -> M s a b
M s Zero b
forall s a. M s Zero a
EmptyL
    M s a b
EmptyR -> M s a b
M s a Zero
forall s a. M s a Zero
EmptyR
    M s a b
Zero -> M s a b
forall s a b. M s a b
Zero
    Diag s
d -> s -> M s a a
forall s a. s -> M s a a
Diag (s -> s
forall a. Group a => a -> a
negate s
d)
    M s a b
f :▵ M s a c
g -> M s a b -> M s a b
forall a. Group a => a -> a
negate M s a b
f M s a b -> M s a c -> M s a (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵ M s a c -> M s a c
forall a. Group a => a -> a
negate M s a c
g
    M s b b
f :▿ M s c b
g -> M s b b -> M s b b
forall a. Group a => a -> a
negate M s b b
f M s b b -> M s c b -> M s (b ⊕ c) b
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿ M s c b -> M s c b
forall a. Group a => a -> a
negate M s c b
g

findSplit :: M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit :: forall s a b c. M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit M s a (b ⊕ c)
EmptyL = (M s a b
M s Zero b
forall s a. M s Zero a
EmptyL, M s a c
M s Zero c
forall s a. M s Zero a
EmptyL)
findSplit M s a (b ⊕ c)
Zero = (M s a b
forall s a b. M s a b
Zero,M s a c
forall s a b. M s a b
Zero)
findSplit (Diag s
s) = (s -> M s b b
forall s a. s -> M s a a
Diag s
sM s b b -> M s c b -> M s (b ⊕ c) b
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿M s c b
forall s a b. M s a b
Zero,M s b c
forall s a b. M s a b
Zero M s b c -> M s c c -> M s (b ⊕ c) c
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿ s -> M s c c
forall s a. s -> M s a a
Diag s
s)
findSplit (M s a b
a :▵ M s a c
b) = (M s a b
M s a b
a,M s a c
M s a c
b)
findSplit ((M s b (b ⊕ c) -> (M s b b, M s b c)
forall s a b c. M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit -> (M s b b
a1,M s b c
a2)) :▿ (M s c (b ⊕ c) -> (M s c b, M s c c)
forall s a b c. M s a (b ⊕ c) -> (M s a b, M s a c)
findSplit -> (M s c b
b1,M s c c
b2))) = (M s b b
a1M s b b -> M s c b -> M s (b ⊕ c) b
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿M s c b
b1,M s b c
a2M s b c -> M s c c -> M s (b ⊕ c) c
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿M s c c
b2)

findSplit' :: M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' :: forall s b c a. M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' M s (b ⊕ c) a
EmptyR = (M s b a
M s b Zero
forall s a. M s a Zero
EmptyR, M s c a
M s c Zero
forall s a. M s a Zero
EmptyR)
findSplit' M s (b ⊕ c) a
Zero = (M s b a
forall s a b. M s a b
Zero,M s c a
forall s a b. M s a b
Zero)
findSplit' (Diag s
s) = (s -> M s b b
forall s a. s -> M s a a
Diag s
sM s b b -> M s b c -> M s b (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵M s b c
forall s a b. M s a b
Zero,M s c b
forall s a b. M s a b
Zero M s c b -> M s c c -> M s c (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵ s -> M s c c
forall s a. s -> M s a a
Diag s
s)
findSplit' (M s b a
a :▿ M s c a
b) = (M s b a
M s b a
a,M s c a
M s c a
b)
findSplit' ((M s (b ⊕ c) b -> (M s b b, M s c b)
forall s b c a. M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' -> (M s b b
a1,M s c b
a2)) :▵ (M s (b ⊕ c) c -> (M s b c, M s c c)
forall s b c a. M s (b ⊕ c) a -> (M s b a, M s c a)
findSplit' -> (M s b c
b1,M s c c
b2))) = (M s b b
a1M s b b -> M s b c -> M s b (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵M s b c
b1,M s c b
a2M s c b -> M s c c -> M s c (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵M s c c
b2)


transpose :: M s a b -> M s b a
transpose :: forall s a b. M s a b -> M s b a
transpose = \case
  M s a b
EmptyL -> M s b a
M s b Zero
forall s a. M s a Zero
EmptyR
  M s a b
EmptyR -> M s b a
M s Zero a
forall s a. M s Zero a
EmptyL
  M s a b
Zero -> M s b a
forall s a b. M s a b
Zero
  (Diag s
s) -> s -> M s b b
forall s a. s -> M s a a
Diag s
s
  (M s b b
a :▿ M s c b
b) -> M s b b -> M s b b
forall s a b. M s a b -> M s b a
transpose M s b b
a M s b b -> M s b c -> M s b (b ⊕ c)
forall s a b c. M s a b -> M s a c -> M s a (b ⊕ c)
:▵ M s c b -> M s b c
forall s a b. M s a b -> M s b a
transpose M s c b
b
  (M s a b
a :▵ M s a c
b) -> M s a b -> M s b a
forall s a b. M s a b -> M s b a
transpose M s a b
a M s b a -> M s c a -> M s (b ⊕ c) a
forall s b a c. M s b a -> M s c a -> M s (b ⊕ c) a
:▿ M s a c -> M s c a
forall s a b. M s a b -> M s b a
transpose M s a c
b

genMorphism :: Arbitrary s => Ring s => Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
genMorphism :: forall s a b.
(Arbitrary s, Ring s) =>
Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
genMorphism Repr (⊗) One (⊕) Zero a
RZero Repr (⊗) One (⊕) Zero b
_ = M s a b -> Gen (M s a b)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure M s a b
M s Zero b
forall s a. M s Zero a
EmptyL
genMorphism Repr (⊗) One (⊕) Zero a
_ Repr (⊗) One (⊕) Zero b
RZero = M s a b -> Gen (M s a b)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure M s a b
M s a Zero
forall s a. M s a Zero
EmptyR
genMorphism (RPlus Repr (⊗) One (⊕) Zero a1
x Repr (⊗) One (⊕) Zero b
y) Repr (⊗) One (⊕) Zero b
b = M s b a -> M s a b
forall s a b. M s a b -> M s b a
transpose (M s b a -> M s a b) -> Gen (M s b a) -> Gen (M s a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (M s b a1 -> M s b b -> M s b a
M s b a1 -> M s b b -> M s b (a1 ⊕ b)
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s a b -> M s a c -> M s a (b ⊕ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
(▵) (M s b a1 -> M s b b -> M s b a)
-> Gen (M s b a1) -> Gen (M s b b -> M s b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Repr (⊗) One (⊕) Zero b
-> Repr (⊗) One (⊕) Zero a1 -> Gen (M s b a1)
forall s a b.
(Arbitrary s, Ring s) =>
Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
genMorphism Repr (⊗) One (⊕) Zero b
b Repr (⊗) One (⊕) Zero a1
x) Gen (M s b b -> M s b a) -> Gen (M s b b) -> Gen (M s b a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Repr (⊗) One (⊕) Zero b -> Repr (⊗) One (⊕) Zero b -> Gen (M s b b)
forall s a b.
(Arbitrary s, Ring s) =>
Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
genMorphism Repr (⊗) One (⊕) Zero b
b Repr (⊗) One (⊕) Zero b
y))
genMorphism Repr (⊗) One (⊕) Zero a
ROne (RPlus Repr (⊗) One (⊕) Zero a1
x Repr (⊗) One (⊕) Zero b
y) = M s a a1 -> M s a b -> M s a b
M s a a1 -> M s a b -> M s a (a1 ⊕ b)
forall a b c.
(Obj (M s) a, Obj (M s) b, Obj (M s) c) =>
M s a b -> M s a c -> M s a (b ⊕ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
(▵) (M s a a1 -> M s a b -> M s a b)
-> Gen (M s a a1) -> Gen (M s a b -> M s a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Repr (⊗) One (⊕) Zero a
-> Repr (⊗) One (⊕) Zero a1 -> Gen (M s a a1)
forall s a b.
(Arbitrary s, Ring s) =>
Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
genMorphism Repr (⊗) One (⊕) Zero a
Repr (⊗) One (⊕) Zero One
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o i
ROne Repr (⊗) One (⊕) Zero a1
x Gen (M s a b -> M s a b) -> Gen (M s a b) -> Gen (M s a b)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
forall s a b.
(Arbitrary s, Ring s) =>
Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
genMorphism Repr (⊗) One (⊕) Zero a
Repr (⊗) One (⊕) Zero One
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o i
ROne Repr (⊗) One (⊕) Zero b
y
genMorphism Repr (⊗) One (⊕) Zero a
ROne Repr (⊗) One (⊕) Zero b
ROne = s -> M s a a
s -> M s a b
forall s a. s -> M s a a
Diag (s -> M s a b) -> Gen s -> Gen (M s a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen s
forall a. Arbitrary a => Gen a
arbitrary
genMorphism Repr (⊗) One (⊕) Zero a
x Repr (⊗) One (⊕) Zero b
_ = String -> Gen (M s a b)
forall a. HasCallStack => String -> a
error (String
"genMorphism: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Repr (⊗) One (⊕) Zero a -> String
forall a. Show a => a -> String
show Repr (⊗) One (⊕) Zero a
x)


prop_block_matrix :: Property
prop_block_matrix :: Property
prop_block_matrix =
  forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, BiCartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
forall (cat :: * -> * -> *).
(Trivial ~ Obj cat, Con' (⊕) Trivial, BiCartesian (⊕) Zero cat,
 Trivial Zero) =>
TestableCat (⊕) Zero Trivial cat -> Property
laws_bicartesian @(M Int)
  (GenObj Trivial (Repr (⊗) One (⊕) Zero) (M Int)
-> (forall a b.
    Repr (⊗) One (⊕) Zero a
    -> Repr (⊗) One (⊕) Zero b -> (M Int a b -> Property) -> Property)
-> (forall a b.
    Repr (⊗) One (⊕) Zero a
    -> Repr (⊗) One (⊕) Zero b -> Dict (TT (M Int) a b))
-> (forall a b.
    Repr (⊗) One (⊕) Zero a
    -> Repr (⊗) One (⊕) Zero b -> Repr (⊗) One (⊕) Zero (a ⊕ b))
-> Repr (⊗) One (⊕) Zero Zero
-> TestableCat (⊕) Zero Trivial (M Int)
forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (o :: k -> *) (obj :: k -> Constraint).
GenObj obj o f
-> (forall (a :: k) (b :: k).
    o a -> o b -> (f a b -> Property) -> Property)
-> (forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b))
-> (forall (a :: k) (b :: k). o a -> o b -> o (x a b))
-> o i
-> TestableCat x i obj f
testableCat
     (\forall a. Trivial a => Repr (⊗) One (⊕) Zero a -> Property
k -> forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
(forall (a :: k). Repr x i t o a -> Property) -> Property
forall (x :: * -> * -> *) i (t :: * -> * -> *) o.
(forall a. Repr x i t o a -> Property) -> Property
forallSumType @(⊗) @One @(⊕) @Zero (\Repr (⊗) One (⊕) Zero a
t -> Repr (⊗) One (⊕) Zero a -> Property
forall a. Trivial a => Repr (⊗) One (⊕) Zero a -> Property
k Repr (⊗) One (⊕) Zero a
t))
     (\Repr (⊗) One (⊕) Zero a
tx Repr (⊗) One (⊕) Zero b
ty M Int a b -> Property
k -> Gen Prop -> Property
forall prop. Testable prop => prop -> Property
property (Gen Prop -> Property) -> Gen Prop -> Property
forall a b. (a -> b) -> a -> b
$ do
         M Int a b
x <- Repr (⊗) One (⊕) Zero a
-> Repr (⊗) One (⊕) Zero b -> Gen (M Int a b)
forall s a b.
(Arbitrary s, Ring s) =>
Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)
genMorphism Repr (⊗) One (⊕) Zero a
tx Repr (⊗) One (⊕) Zero b
ty
         Property -> Gen Prop
unProperty (M Int a b -> Property
k M Int a b
x))
     (\Repr (⊗) One (⊕) Zero a
_ Repr (⊗) One (⊕) Zero b
_ -> Dict (TT (M Int) a b)
forall (a :: Constraint). a => Dict a
Dict)
     Repr (⊗) One (⊕) Zero a
-> Repr (⊗) One (⊕) Zero b -> Repr (⊗) One (⊕) Zero (a ⊕ b)
forall a b.
Repr (⊗) One (⊕) Zero a
-> Repr (⊗) One (⊕) Zero b -> Repr (⊗) One (⊕) Zero (a ⊕ b)
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k)
       (a1 :: k) (b :: k).
Repr x i t o a1 -> Repr x i t o b -> Repr x i t o (t a1 b)
RPlus
     Repr (⊗) One (⊕) Zero Zero
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o o
RZero)