gasp 1.3.0.0 → 1.4.0.0

raw patch · 18 files changed

+2509/−240 lines, 18 filesdep +adjunctionsdep +constraintsdep +distributivePVP ok

version bump matches the API change (PVP)

Dependencies added: adjunctions, constraints, distributive

API changes (from Hackage documentation)

Files

• Algebra/Category.hs +224/−6
• Algebra/Category/BlockMatrix.hs +178/−0
• Algebra/Category/Endo.hs +23/−0
• Algebra/Category/Laws.hs +287/−0
• Algebra/Category/NatTrans.hs +40/−0
• Algebra/Category/Objects.hs +162/−0
• Algebra/Category/Op.hs +70/−0
• Algebra/Category/Relation.hs +108/−0
• Algebra/CategoryRecords.hs +53/−0
• Algebra/Classes.hs +531/−155
• Algebra/Linear.hs +201/−75
• Algebra/Morphism/Affine.hs +66/−0
• Algebra/Morphism/Exponential.hs +52/−0
• Algebra/Morphism/LinComb.hs +86/−0
• Algebra/Morphism/Pointwise.hs +55/−0
• Algebra/Morphism/Ratio.hs +126/−0
• Algebra/Types.hs +219/−0
• gasp.cabal +28/−4

@@ -1,11 +1,42 @@+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ConstrainedClassMethods #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE PolyKinds #-} module Algebra.Category where +import Algebra.Classes (Additive(..))+import Algebra.Types+import Algebra.Category.Objects import qualified Prelude-import Data.Kind (Constraint, Type)+import Data.Kind+import qualified Algebra.CategoryRecords as R +type O2 k a b = (Obj k a, Obj k b)+type O3 k a b c =+  (Obj k a, Obj k b, Obj k c)+type O4 k a b c d =+  (Obj k a, Obj k b, Obj k c, Obj k d)++infixr 9 .++   -- | A class for categories. Instances should satisfy the laws -- -- @@@ -13,14 +44,201 @@ -- 'id' '.' f  =  f  -- (left identity) -- f '.' (g '.' h)  =  (f '.' g) '.' h  -- (associativity) -- @+ class Category (cat :: k -> k -> Type) where-  type Con (a :: k) :: Constraint-  type Con a = ()-  (.) :: (Con a, Con b, Con c) => b `cat` c -> a `cat` b -> a `cat` c-  id :: Con a => a `cat` a+  type Obj (cat) :: k -> Constraint+  (.)      :: (Obj cat a, Obj cat b, Obj cat c) => b `cat` c -> a `cat` b -> a `cat` c+  id :: Obj cat a => a `cat` a ++-- , (∘) = (∘), id = id+++class Category cat => Dagger cat where+  dagger :: O2 cat a b => a `cat` b -> b `cat` a++(∘) :: forall {k} (cat :: k -> k -> Type) a b c con. (Category cat, con ~ Obj cat, con a, con b, con c) => cat b c -> cat a b -> cat a c+(∘) = (.) ++type Monoidal :: forall {k}. (k -> k -> k) -> k -> (k -> k -> Type) -> Constraint++class Category cat => Monoidal x i (cat :: k -> k -> Type) | x -> i, i -> x where+  (⊗)      :: (Obj cat a, Obj cat b, Obj cat c, Obj cat d) => (a `cat` b) -> (c `cat` d) -> (a `x` c) `cat` (b `x` d)+  assoc    :: (Obj cat a, Obj cat b, Obj cat c) => ((a `x` b) `x` c) `cat` (a `x` (b `x` c))+  assoc_   :: (Obj cat a, Obj cat b, Obj cat c) => (a `x` (b `x` c)) `cat` ((a `x` b) `x` c)+  unitorR   :: (Obj cat a, Obj cat i) => a `cat` (a `x` i)+  unitorR_  :: (Obj cat a, Obj cat i) => (a `x` i) `cat` a+  unitorL   :: (Obj cat a, Obj cat i) => a `cat` (i `x` a)+  unitorL_  :: (Obj cat a, Obj cat i) => (i `x` a) `cat` a++  default unitorL :: forall a con. (con ~ Obj cat, con i, con (x a i), con (x i a), Symmetric x i cat, Obj cat a) => a `cat` (i `x` a)+  unitorL = swap ∘ unitorR+  default unitorL_ :: forall a con. (con ~ Obj cat, Symmetric x i cat, con i, con (x a i), con (x i a), Obj cat a) => (i `x` a) `cat` a +  unitorL_ = unitorR_ ∘ swap++monoidalRec :: forall x cat i. Monoidal x i cat => R.MonoidalRec x i (Obj cat) cat+monoidalRec = R.MonoidalRec { (⊗) = (⊗), assoc = assoc, assoc_ = assoc_,   unitorR = unitorR, unitorL = unitorL, unitorL_ = unitorL_, unitorR_ = unitorR_}++++class Monoidal x i cat => Braided x i cat where+  swap     :: (Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a)+  swap_     :: (Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a)+  default swap_ :: (Symmetric x i cat, Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a)+  swap_ = swap++braidedRec :: forall x cat i. Braided x i cat => R.BraidedRec x i (Obj cat) cat+braidedRec = R.BraidedRec { swap = swap, swap_ = swap_}+++class Braided x i cat => Symmetric x i cat++++class Symmetric x i cat => Cartesian x i cat where+  {-# MINIMAL exl,exr,dup | exl,exr,(▵) | dis,dup | dis,(▵) #-}+  exl   ::   forall a b. O2 cat a b                     =>    (a `x` b) `cat` a+  exr   ::   forall a b. O2 cat a b                     =>    (a `x` b) `cat` b+  dis   ::   forall a.  Obj cat a                       =>    a `cat` i+  dup   ::   forall a. Obj cat a                        =>    a `cat` (a `x` a)+  (▵)   ::   forall a b c. (Obj cat a,Obj cat b, Obj cat c) =>    (a `cat` b) -> (a `cat` c) -> a `cat` (b `x` c)+  default dis :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => a `cat` i+  dis = exr . unitorR+  default dup :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => a `cat` (a `x` a)+  dup = id ▵ id+  default exl :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) =>  (a `x` b) `cat` a+  exl = unitorR_ . (id ⊗ dis)+  default exr :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) =>  (a `x` b) `cat` b+  exr = unitorL_ ∘ (dis ⊗ id)+  default (▵)   ::   forall a b c con. (con ~ Obj cat, con i, Con' x con, Obj cat a,Obj cat b, Obj cat c) =>    (a `cat` b) -> (a `cat` c) -> a `cat` (b `x` c)+  f ▵ g = (f ⊗ g) ∘ dup ++cartesianRec :: forall x cat i. Cartesian x i cat => R.CartesianRec x i (Obj cat) cat+cartesianRec = R.CartesianRec {exl = exl , exr = exr , dis = dis , dup = dup , (▵) = (▵)}++cartesianCross :: (Obj k (b1 `x` b2), Obj k b3, Obj k c, Obj k b1, Obj k b2, Cartesian x i k) => k b1 b3 -> k b2 c -> k (b1 `x` b2) (b3 `x` c)+cartesianCross a b = (a . exl) ▵ (b . exr)++cartesianUnitor :: forall a k x i. (Obj k a, Obj k i, Cartesian x i k) => a `k` (a `x` i)+cartesianUnitor = id ▵ dis+cartesianUnitor_ :: forall a k x i. (Obj k a, Obj k i, Cartesian x i k) => (a `x` i) `k` a+cartesianUnitor_ = exl+cartesianSwap :: forall a b k x i con. (Obj k a, Obj k b, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` b) `k` (b `x` a)+cartesianSwap = exr ▵ exl+cartesianAssoc :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => ((a `x` b) `x` c) `k` (a `x` (b `x` c))+cartesianAssoc = (exl . exl) ▵ ((exr . exl) ▵ exr)+cartesianAssoc_ :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` (b `x` c)) `k` ((a `x` b) `x` c)+cartesianAssoc_ = (exl ▵ (exl . exr)) ▵ (exr . exr)+++coCartesianExl ::  (O2 cat a b, CoCartesian x i cat, Additive (cat b a)) => (a `x` b) `cat` a+coCartesianExl = id ▿ zero+coCartesianExr ::  (O2 cat a b, CoCartesian x i cat, Additive (cat a b)) => (a `x` b) `cat` b+coCartesianExr = zero ▿ id++class Symmetric x i cat => CoCartesian x i cat where+  {-# MINIMAL inl,inr,jam | inl,inr,(▿) | new,jam | new,(▿) #-}+  inl   ::  O2 cat a b                                 =>  a `cat` (a `x` b)+  inr   ::  O2 cat a b                                 =>  b `cat` (a `x` b)+  new   ::  forall a. (Obj cat a)                      =>  i `cat` a+  jam   ::  Obj cat a                                  =>  (a `x` a) `cat` a+  (▿)    ::  forall a b c. (Obj cat a,Obj cat b, Obj cat c) =>  (b `cat` a) -> (c `cat` a) -> (b `x` c) `cat` a+  default new :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => i `cat` a +  new = unitorR_ . inr+  default jam :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => (a `x` a) `cat` a +  jam = id ▿ id+  default inl :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => a `cat` (a `x` b) +  inl = (id ⊗ new) . unitorR +  default inr :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => b `cat`  (a `x` b)+  inr = (new ⊗ id) ∘ unitorL+  default (▿)   ::   forall a b c con. (con ~ Obj cat, con i, Con' x con, Obj cat a,Obj cat b, Obj cat c) =>    (b `cat` a) -> (c `cat` a) -> (b `x` c) `cat` a+  f ▿ g = jam ∘ (f ⊗ g) ++type BiCartesian x i cat = (Cartesian x i cat, CoCartesian x i cat)++class Monoidal x i cat => Autonomous x i l r cat | x -> l, x -> r where+  turn   :: Obj cat a => i `cat` (l a `x` a)+  turn'  :: Obj cat a => (a `x` r a) `cat` i+  +class (Symmetric x i cat, Autonomous x i d d cat) => Compact x i d cat where+++---------------------------+-- Instances+----------------------------+ instance Category (->) where+  type Obj (->) = Trivial   (.) = (Prelude..)   id = Prelude.id -infixr 9 .+instance Monoidal (⊗) One (->) where+  (f ⊗ g) (x `Pair` y) = (f x `Pair` g y)+  assoc ((x `Pair` y) `Pair` z) = (x `Pair` (y `Pair` z)) +  assoc_ (x `Pair` (y `Pair` z)) = ((x `Pair` y) `Pair` z)  +  unitorR x = (x `Pair` Unit)+  unitorR_ (x `Pair` Unit) = x+instance Braided (⊗) One (->) where+  swap (x `Pair` y) = (y `Pair` x)+instance Symmetric (⊗) One (->)++instance Monoidal (,) () (->) where+  (f ⊗ g) (x , y) = (f x , g y)+  assoc ((x , y) , z) = (x , (y , z)) +  assoc_ (x , (y , z)) = ((x , y) , z)  +  unitorR x = (x , ())+  unitorR_ (x , ()) = x+instance Braided (,) () (->) where+  swap (x, y) = (y, x)+instance Symmetric (,) () (->)+++instance Monoidal (⊕) Zero (->) where+  f ⊗ g = \case+    Inj1 x -> Inj1 (f x)+    Inj2 x -> Inj2 (g x)+  assoc = \case+    Inj1 (Inj1 x) -> Inj1 x+    Inj1 (Inj2 x) -> Inj2 (Inj1 x)+    Inj2 x -> Inj2 (Inj2 x)+  assoc_ = \case+    (Inj1 x) -> (Inj1 (Inj1 x)) +    (Inj2 (Inj1 x)) -> (Inj1 (Inj2 x)) +    (Inj2 (Inj2 x)) -> (Inj2 x) +  unitorR = Inj1+  unitorL = Inj2+  unitorR_ = \case+    Inj1 x -> x+    Inj2 x -> case x of++instance Symmetric (⊕) Zero (->) where+instance Braided (⊕) Zero (->) where+  swap = \case+    Inj1 x -> Inj2 x+    Inj2 x -> Inj1 x++instance Cartesian (⊗) One (->) where+  dup x = Pair x x+  exr (Pair _ x) = x+  exl (Pair x _) = x+  (f ▵ g) x = f x `Pair` g x+  dis _ = Unit++instance Cartesian (,) () (->) where+  dup x = (x,x)+  exr (_,x) = x+  exl (x,_) = x+  (f ▵ g) x = (f x, g x)+  dis _ = ()++instance CoCartesian (⊕) Zero (->) where+  inl = Inj1+  inr = Inj2+  new = \case+  f ▿ g = \case+     Inj1 x -> f x+     Inj2 y -> g y+  jam = \case+     Inj1 x -> x+     Inj2 x -> x+

@@ -0,0 +1,178 @@+{-# 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+  EmptyR =.= _ = property True+  EmptyL =.= _ = property True+  _ =.= EmptyR = property True+  _ =.= EmptyL = property True+  (a :▵ b) =.= c = case findSplit c of+    (a',b') -> (a =.= a') * (b =.= b')+  (a :▿ b) =.= c = case findSplit' c of+    (a',b') -> (a =.= a') * (b =.= b')+  c =.= (a :▵ b) = case findSplit c of+    (a',b') -> (a =.= a') * (b =.= b')+  c =.= (a :▿ b) = case findSplit' c of+    (a',b') -> (a =.= a') * (b =.= b')+  Zero =.= c = testZero c+  c =.= Zero = testZero c+  (Diag x) =.= (Diag y) = x =.= y++testZero :: (Additive s, TestEqual s) => M s a b -> Property+testZero = \case+     EmptyL -> property True+     EmptyR -> property True+     Zero -> property True+     Diag s -> s =.= zero+     a :▵ b -> testZero a * testZero b+     a :▿ b -> testZero a * testZero b++instance Ring s => Scalable s (M s a b) where+  s *^ c = case c of+    EmptyR -> EmptyR+    EmptyL -> EmptyL+    Zero -> Zero+    Diag x -> Diag (s*x)+    a :▿ b -> (s *^ a) :▿ (s *^ b)+    a :▵ b -> (s *^ a) :▵ (s *^ b)+  +instance Ring s => Category (M s) where+  EmptyL . EmptyR = Zero -- adding zero elements together for each position in the matrix+  EmptyR . _ = EmptyR+  _ . EmptyL = EmptyL+  Zero . _ = Zero+  _ . Zero = Zero+  Diag s . m = s *^ m+  m . Diag s = s *^ m+  (a1 :▵ a2) . b = (a1 . b) :▵ (a2 . b)+  a . (b1 :▿ b2) = (a . b1) :▿ (a . b2)+  (a1 :▿ a2) . (b1 :▵ b2) = a1 . b1 + a2 . b2++  type Obj (M s) = Trivial+  id = Diag one++instance Ring s => Monoidal (⊕) Zero (M s) where+  (⊗) = cartesianCross -- a potential optimisation is that two diagonals will be a new diagonal. Represent diagonals as (sparse) vectors?+  assoc = cartesianAssoc+  assoc_ = cartesianAssoc_+  unitorR = cartesianUnitor+  unitorR_ = id ▿ new++instance Ring s => Symmetric (⊕) Zero (M s)+instance Ring s => Braided (⊕) Zero (M s) where+  swap = (zero ▵ id) ▿ (id ▵ zero)+instance Ring s => Cartesian (⊕) Zero (M s) where+  (▵) = (:▵)+  dis = EmptyR+  exl = id ▿ Zero+  exr = Zero ▿ id++instance Ring s => CoCartesian (⊕) Zero (M s) where+  (▿) = (:▿)+  new = EmptyL+  inl = id ▵ Zero+  inr = Zero ▵ id++instance Additive s => Additive (M s a b) where+  zero = Zero+  Zero + a = a+  a + Zero = a+  EmptyL + _ = EmptyL+  _ + EmptyL = EmptyL+  EmptyR + _ = EmptyR+  _ + EmptyR = EmptyR+  (a :▵ b) + m  = (a + d) :▵ (b + c) where (d,c) = findSplit  m+  m  + (a :▵ b) = (a + d) :▵ (b + c) where (d,c) = findSplit  m+  (a :▿ b) + m  = (a + d) :▿ (b + c) where (d,c) = findSplit' m+  m  + (a :▿ b) = (a + d) :▿ (b + c) where (d,c) = findSplit' m+  Diag s + Diag t = Diag (s + t)++instance Group s => Group (M s a b) where+  negate = \case+    EmptyL -> EmptyL+    EmptyR -> EmptyR+    Zero -> Zero+    Diag d -> Diag (negate d)+    f :▵ g -> negate f :▵ negate g+    f :▿ g -> negate f :▿ negate g++findSplit :: M s a (b ⊕ c) -> (M s a b, M s a c)+findSplit EmptyL = (EmptyL, EmptyL)+findSplit Zero = (Zero,Zero)+findSplit (Diag s) = (Diag s:▿Zero,Zero :▿ Diag s)+findSplit (a :▵ b) = (a,b)+findSplit ((findSplit -> (a1,a2)) :▿ (findSplit -> (b1,b2))) = (a1:▿b1,a2:▿b2)++findSplit' :: M s (b ⊕ c) a -> (M s b a, M s c a)+findSplit' EmptyR = (EmptyR, EmptyR)+findSplit' Zero = (Zero,Zero)+findSplit' (Diag s) = (Diag s:▵Zero,Zero :▵ Diag s)+findSplit' (a :▿ b) = (a,b)+findSplit' ((findSplit' -> (a1,a2)) :▵ (findSplit' -> (b1,b2))) = (a1:▵b1,a2:▵b2)+++transpose :: M s a b -> M s b a+transpose = \case+  EmptyL -> EmptyR+  EmptyR -> EmptyL+  Zero -> Zero+  (Diag s) -> Diag s+  (a :▿ b) -> transpose a :▵ transpose b+  (a :▵ b) -> transpose a :▿ transpose b++genMorphism :: Arbitrary s => Ring s => Repr (⊗) One (⊕) Zero a -> Repr (⊗) One (⊕) Zero b -> Gen (M s a b)+genMorphism RZero _ = pure EmptyL+genMorphism _ RZero = pure EmptyR+genMorphism (RPlus x y) b = transpose <$> ((▵) <$> (genMorphism b x) <*> (genMorphism b y))+genMorphism ROne (RPlus x y) = (▵) <$> genMorphism ROne x <*> genMorphism ROne y+genMorphism ROne ROne = Diag <$> arbitrary+genMorphism x _ = error ("genMorphism: " <> show x)+++prop_block_matrix :: Property+prop_block_matrix =+  laws_bicartesian @(M Int)+  (testableCat+     (\k -> forallSumType @(⊗) @One @(⊕) @Zero (\t -> k t))+     (\tx ty k -> property $ do+         x <- genMorphism tx ty+         unProperty (k x))+     (\_ _ -> Dict)+     RPlus+     RZero)

@@ -0,0 +1,23 @@+{-# LANGUAGE UndecidableInstances #-}+module Algebra.Category.Endo where++import Prelude (Semigroup(..), Monoid(..))+import Algebra.Category+import Algebra.Classes++newtype Endo cat a = Endo (cat a a)++instance (Category cat, Obj cat a) => Semigroup (Endo cat a) where+  Endo f <> Endo g = Endo (f . g)++instance (Category cat, Obj cat a) => Monoid (Endo cat a) where+  mempty = Endo id++instance (Category cat, Obj cat a) => Multiplicative (Endo cat a) where+  Endo f * Endo g = Endo (f . g)+  one = Endo id++instance (Dagger cat, Obj cat a) => Division (Endo cat a) where+  recip (Endo m) = Endo (dagger m)++

@@ -0,0 +1,287 @@+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ConstrainedClassMethods #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE PolyKinds #-}++module Algebra.Category.Laws where++import qualified Algebra.CategoryRecords as R+-- import Algebra.CategoryRecords (MonoidalRec(MonoidalRec))+import Algebra.Category+import Algebra.Category.Op++import Algebra.Classes (nameLaw, TestEqual(..), product)+import Algebra.Category.Objects+import Data.Kind+import Data.Constraint+import Test.QuickCheck+import Prelude (Show(..),($))+++law_id_comp :: forall {k} (f :: k -> k -> Type) a b. (Category f, TestEqual (f a b), O2 f a b) => f a b -> Property+law_id_comp n = nameLaw "id/comp" (id . n =.= n)++forallMorphism' :: forall f x i. TestableCat x i (Obj f) f -> (forall a b. (O2 f a b, TT f a b) => f a b -> Property) -> Property+forallMorphism' (TestableCat {..}) p+  = genObj (\t1 -> +    genObj (\t2 ->+    genMorph' t1 t2 (\f -> p f)))+++law_comp_id :: forall {k} (f :: k -> k -> Type) a b. (Category f, TestEqual (f a b), O2 f a b) => f a b -> Property+law_comp_id n = nameLaw "comp/id" (n . id =.= n)++law_comp_assoc :: forall {k} (f :: k -> k -> Type) a b c d. (Category f, TestEqual (f a d), O4 f a b c d) => f c d -> f b c -> f a b -> Property+law_comp_assoc n m o = nameLaw "comp/assoc" (n . (m . o) =.= (n . m) . o)++laws_category :: forall f x i. (Category f) => TestableCat x i (Obj f) f -> Property+laws_category tc@TestableCat {..}+  = product [forallMorphism' @f tc (\f -> property (law_id_comp f))+            ,forallMorphism' @f tc (\f -> property (law_comp_id f))+            ,genObj $ \t1 -> genObj $ \t2 -> genObj $ \t3 -> genObj $ \t4 ->+             genMorph t1 t2 $ \ h -> genMorph t2 t3 $ \ g -> genMorph t3 t4 $ \ f ->+             (f . (g . h) =.= (f . g) . h) \\ getTestable t1 t4]+++type TT f x y = TestEqual (f x y)+type GenObj obj o f = ((forall a. obj a => o a -> Property) -> Property)++data TestableCat x i obj f = forall o. TestableCat+  {genObj :: GenObj obj o f+  ,genMorph' :: forall a b. o a -> o b -> (TT f a b => f a b -> Property) -> Property+  ,genMorph :: forall a b. o a -> o b -> (f a b -> Property) -> Property+  ,getTestable :: forall a b. o a -> o b -> Dict (TT f a b)+  ,getTestable' :: forall a. o a -> Dict (TT f a a)+  ,(×) :: forall a b. o a -> o b -> o (a `x` b)+  ,unitObj :: o i+  }++testableCat :: forall f x i o obj. GenObj obj o f -> (forall a b. o a -> o b -> (f a b -> Property) -> Property) -> ( forall a b. o a -> o b -> Dict (TT f a b)) -> (forall a b. o a -> o b -> o (x a b)) -> o i -> TestableCat x i obj f+testableCat genObj genMorph getTestable (×) unitObj = TestableCat{..}+  where genMorph' :: forall a b. o a -> o b -> (TT f a b => f a b -> Property) -> Property+        genMorph' a b k = genMorph a b $ \f -> k f \\ getTestable a b+        getTestable' :: forall a. o a -> Dict (TT f a a)+        getTestable' a = getTestable a a+++law_parallel_composition :: forall {k} {cat :: k -> k -> Type}+                                     {x :: k -> k -> k} {a :: k} {c :: k} {b1 :: k} {b2 :: k}+                                     {b3 :: k} {d :: k} {i :: k} obj.+                              (obj (x a c), obj (x b1 b2), obj (x b3 d), obj a,+                               obj b1, obj b3, obj c, obj b2, obj d, Category cat, Obj cat ~ obj,+                               TestEqual (cat (x a c) (x b3 d))) =>+                              R.MonoidalRec x i obj cat -> cat b1 b3 -> cat b2 d -> cat a b1 -> cat c b2 -> Property+law_parallel_composition R.MonoidalRec{..} e f g h = nameLaw "cross-comp" ((e ⊗ f) ∘ (g ⊗ h) =.= (e ∘ g) ⊗ (f ∘ h))++law_assoc_inv :: forall {k} (a::k) (b::k) (c::k) x i obj (cat :: k -> k -> Type) o.+  (obj a, obj b, obj c, Con' x obj, TestEqual (cat (x (x a b) c) (x (x a b) c)), Category cat, Obj cat ~ obj)+  => R.MonoidalRec x i obj cat -> o a -> o b -> o c -> Property+law_assoc_inv R.MonoidalRec{..} _ _ _ = nameLaw "assoc-inv" (assoc_ @a @b @c ∘ assoc =.= id)+  ++law_unitorR_inv :: forall {k} (cat :: k -> k -> Type) x i {b :: k} {con :: k -> Constraint} {o}.+                     (Monoidal x i cat, Obj cat ~ con, Con' x con, con ~ Obj cat,  con b, con i,+                      TestEqual (cat (x b i) (x b i))) =>+                     o b -> Property+law_unitorR_inv _ = nameLaw "unitor-inv" ((unitorR :: b `cat` (b `x` i)) ∘ unitorR_ =.= id)+++law_unitorL_inv :: forall {k} {cat :: k -> k -> Type}+                            {x :: k -> k -> k} {b :: k} {i :: k} {con :: k -> Constraint} {o}.+                     (Category cat, Obj cat ~ con, Con' x con, con ~ Obj cat,  con b, con i,+                      TestEqual (cat (x i b) (x i b))) =>+                     R.MonoidalRec x i con cat -> o b -> Property+law_unitorL_inv  R.MonoidalRec{..} _ = nameLaw "unitor_-inv" (unitorL @b ∘ unitorL_ =.= id)+  +law_monoidal_triangle :: forall {k} (cat :: k -> k -> Type) (x :: k -> k -> k) (i :: k) a c obj o. (obj ~ Obj cat, Monoidal x i cat, obj a, obj c, obj i, Con' x obj, TestEqual (cat (x a c) (x a (x i c))))+  => o a -> o c -> Property+law_monoidal_triangle _ _ = nameLaw "monoidal-triangle"+   ((assoc . (unitorR ⊗ id)) =.=  ((id ⊗ unitorL) :: (cat (x a c) (x a (x i c)))))++law_monoidal_pentagon :: forall {k} (cat :: k -> k -> Type) (x :: k -> k -> k) (i :: k) a b c d obj o.+   (obj ~ Obj cat, Monoidal x i cat, obj a, obj b, obj c, obj d, Con' x obj, (TestEqual (cat (x (x (x a b) c) d) (x a (x b (x c d))))))+  => o a -> o b -> o c -> o d -> Property+law_monoidal_pentagon _ _ _ _ = nameLaw "monoidal-pentagon"+   (assoc . assoc =.=  ((id ⊗ assoc) . assoc . (assoc ⊗ id)+                        :: (cat (x (x (x a b) c) d) (x a (x b (x c d))))))+++laws_monoidal :: forall {k} (cat :: k -> k -> Type) x i (obj :: k -> Constraint).+                 (obj ~ Obj cat, Con' x obj, Monoidal x i cat, obj i) +                 => TestableCat x i obj cat -> Property+laws_monoidal  t@TestableCat{..}   = product+   [ laws_category t+   , genObj $ \t1 -> genObj $ \t2 -> genObj $ \t3 ->+     genObj $ \t4 -> genObj $ \t5 -> genObj $ \t6 ->+     genMorph t1 t2 $ \e -> genMorph t2 t3 $ \f ->+     genMorph t4 t5 $ \g -> genMorph t5 t6 $ \h ->+     law_parallel_composition m f h e g+     \\ getTestable (t1 × t4) (t3 × t6)+   , genObj $ \a -> genObj $ \b -> genObj $ \c -> law_assoc_inv m  a b c+     \\ getTestable' ((a × b) × c)+   , genObj $ \a -> genObj $ \b -> genObj $ \c -> law_assoc_inv mOp a b c+     \\ getTestable' ((a × b) × c)+   , genObj $ \a -> law_unitorR_inv @cat @x a \\ getTestable' (a × unitObj) +   , genObj $ \a -> law_unitorR_inv @(Op cat) @x a  \\ getTestable' (a × unitObj)+   , genObj $ \a -> law_unitorL_inv m   a  \\ getTestable' (unitObj × a)+   , genObj $ \a -> law_unitorL_inv mOp a  \\ getTestable' (unitObj × a)+   , genObj $ \a -> genObj $ \b -> law_monoidal_triangle @cat @x a b+     \\ getTestable (a × b) (a × (unitObj × b))+   , genObj $ \a -> genObj $ \b -> genObj $ \c -> genObj $ \d ->+       law_monoidal_pentagon @cat @x a b c d+       \\ getTestable (((a × b) × c) × d) (a × (b × (c × d))) +   ]+   where m :: R.MonoidalRec x i obj cat +         m@R.MonoidalRec{} = monoidalRec @x+         mOp :: R.MonoidalRec x i obj (Op cat)+         mOp = monoidalRec @x+         -- running the test on the op category mean that we test the reverse compositions.++law_swap_inv :: forall {k} (a::k) (b::k) x i obj (cat :: k -> k -> Type) o.+  (obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b, TestEqual (cat (x b a) (x b a)))+  => R.BraidedRec x i obj cat -> o a -> o b -> Property+law_swap_inv R.BraidedRec{..} _ _ = nameLaw "swap-inv" (swap_ @a @b ∘ swap =.= id)++law_braided_hexagon1 :: forall {k} (cat :: k -> k -> Type) x i a b c obj o.+   (obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj, (TestEqual (cat (x (x a b) c) (x b (x c a)))))+  => o a -> o b -> o c -> Property+law_braided_hexagon1 _ _ _ = nameLaw "braided-hexagon-1"+   (assoc . swap . assoc =.= ((id ⊗ swap) . assoc . (swap ⊗ id)+      :: cat ((a `x` b) `x` c) (b `x` (c `x` a))))++law_braided_hexagon2 :: forall {k} (cat :: k -> k -> Type) x i a b c obj o.+   (obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj, (TestEqual (cat (x a (x b c)) (x (x c a) b))))+  => o a -> o b -> o c -> Property+law_braided_hexagon2 _ _ _ = nameLaw "braided-hexagon-2"+   (assoc_ . swap . assoc_ =.= ((swap ⊗ id) . assoc_ . (id ⊗ swap) +      :: cat (a `x` (b `x` c)) ((c `x` a) `x` b)))++law_braided_triangle :: forall {k} (cat :: k -> k -> Type) (x :: k -> k -> k) (i :: k) a obj o. (obj ~ Obj cat, Braided x i cat, obj a, obj i, Con' x obj, TestEqual (cat (x a i) a))+  => o a -> Property+law_braided_triangle _ = nameLaw "monoidal-triangle"+   (unitorL_ . swap =.=  (unitorR_ :: (cat (x a i) a)))+++laws_braided :: forall {k} {x :: k -> k -> k}+                          {obj :: k -> Constraint} +                          {i :: k} +                          (cat :: k -> k -> Type).+                 (obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) +                 => TestableCat x i obj cat -> Property+laws_braided  t@TestableCat{..}   = product+   [ laws_monoidal t+   , genObj $ \a -> genObj $ \b -> law_swap_inv m   a b  \\ getTestable' (b × a)+   , genObj $ \a -> genObj $ \b -> law_swap_inv mOp a b  \\ getTestable' (b × a)+   , genObj $ \a -> law_braided_triangle @cat @x a \\ getTestable (a × unitObj) a+   , genObj $ \a -> genObj $ \b -> genObj $ \c ->+       law_braided_hexagon1 @cat @x a b c \\ getTestable ((a × b) × c) (b × (c × a))+   , genObj $ \a -> genObj $ \b -> genObj $ \c ->+       law_braided_hexagon2 @cat @x a b c \\ getTestable (a × (b × c)) ((c × a) × b)+   ]+   where m :: R.BraidedRec x i obj cat +         m@R.BraidedRec{} = braidedRec @x+         mOp :: R.BraidedRec x i obj (Op cat)+         mOp = braidedRec @x+         -- running the test on the op category mean that we test the reverse compositions.++law_swap_invol :: forall {k} (a::k) (b::k) x i obj (cat :: k -> k -> Type) o.+  (obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b, TestEqual (cat (x b a) (x b a)))+  => R.BraidedRec x i obj cat -> o a -> o b -> Property+law_swap_invol R.BraidedRec{..} _ _ = nameLaw "swap-invol" (swap @a @b ∘ swap =.= id)+++laws_symmetric :: forall {k} {x :: k -> k -> k}+                          {obj :: k -> Constraint} +                          {i :: k} +                          (cat :: k -> k -> Type).+                 (obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) +                 => TestableCat x i obj cat -> Property+laws_symmetric  t@TestableCat{..}   = product+   [ laws_braided t+   , genObj $ \a -> genObj $ \b -> law_swap_invol m a b+      \\ getTestable' (b × a) +   ]+   where m :: R.BraidedRec x i obj cat +         m@R.BraidedRec{} = braidedRec @x+++law_dup_commut :: forall {k} {cat :: k -> k -> Type}+                                     {x :: k -> k -> k}  {a :: k}+                                     {b :: k} {i :: k} obj.+                              (obj a, obj b, Category cat, Obj cat ~ obj,+                               TestEqual (cat a (x b b)), Cartesian x i cat, Con' x obj) =>+                              R.CartesianRec x i obj cat -> cat a b -> Property+law_dup_commut R.CartesianRec{..} f = nameLaw "dup/cross" ((f ⊗ f) . dup =.= dup . f)++law_projections :: forall {k} {con :: k -> Constraint} {x :: k -> k -> k}+                      {b :: k} {c :: k} {cat :: k -> k -> Type} {i :: k} {p}.+               (con (x b c), con b, con c, Obj cat (x b c), Con' x con,+                TestEqual (cat (x b c) (x b c)), Category cat) =>+               R.CartesianRec x i con cat -> p b -> p c -> Property+law_projections R.CartesianRec{..} _ _ = nameLaw "projections" (exl ▵ exr  =.= id @k @cat @(b `x` c))++++laws_cartesian_extra :: forall {k} (x :: k -> k -> k)+                          {obj :: k -> Constraint} +                          (i :: k )+                          (cat :: k -> k -> Type).+                 (obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) +                 => TestableCat x i obj cat -> Property+laws_cartesian_extra  t@TestableCat{..}   = product+   [ genObj $ \t1 -> genObj $ \t2 -> genMorph t1 t2 $ \f -> law_dup_commut m f  \\ getTestable t1 (t2 × t2)+   , genObj $ \t1 -> genObj $ \t2 -> law_projections m t1 t2  \\ getTestable' (t1 × t2)+   ]+   where m :: R.CartesianRec x i obj cat +         m@R.CartesianRec{..} = cartesianRec++laws_cartesian :: forall {k} (x :: k -> k -> k)+                          {obj :: k -> Constraint} +                          (i :: k )+                          (cat :: k -> k -> Type).+                 (obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) +                 => TestableCat x i obj cat -> Property+laws_cartesian  t@TestableCat{..} = product+   [ laws_symmetric t , laws_cartesian_extra t]++laws_cocartesian :: forall {k} {x :: k -> k -> k}+                          {obj :: k -> Constraint} +                          {i :: k} +                          {cat :: k -> k -> Type}.+                 (obj ~ Obj cat, Con' x obj, CoCartesian x i cat, obj i) +                 => TestableCat x i obj cat -> Property+laws_cocartesian  t = laws_cartesian (opTestable t)+++opTestable :: TestableCat x i obj cat -> TestableCat x i obj (Op cat)+opTestable TestableCat{..} = testableCat+                               genObj (\a b k -> genMorph b a $ \f -> k (Op f))+                               (\a b -> Dict \\ getTestable b a)+                               (×) unitObj++laws_bicartesian :: forall {k} {x :: k -> k -> k}+                          {obj :: k -> Constraint} +                          {i :: k} +                          (cat :: k -> k -> Type).+                 (obj ~ Obj cat, Con' x obj, BiCartesian x i cat, obj i) +                 => TestableCat x i obj cat -> Property+laws_bicartesian  t = product [ laws_symmetric t+                              , laws_cartesian_extra t+                              , laws_cartesian_extra (opTestable t)]

@@ -0,0 +1,40 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Algebra.Category.NatTrans where++import Algebra.Category+import Prelude (Functor(..))+import Algebra.Types++import Data.Kind++newtype NatTrans (f :: Type -> Type) (g :: Type -> Type) = NatTrans (forall x. f x -> g x)++instance Category NatTrans where+  type Obj NatTrans = Functor+  NatTrans f . NatTrans g = NatTrans (f ∘ g)+  id = NatTrans id++instance Monoidal (∘) Id NatTrans where+  assoc_ = NatTrans (Comp . Comp . fmap fromComp . fromComp)+  unitorR_ = NatTrans (fmap fromId . fromComp)+  NatTrans f ⊗ NatTrans g = NatTrans (Comp . f . fmap g . fromComp)+  assoc =  NatTrans (Comp . fmap Comp . fromComp . fromComp)+  unitorR = NatTrans (Comp . fmap Id)+  unitorL = NatTrans (Comp . Id)+  unitorL_ = NatTrans (fromId . fromComp)++instance Monoidal (⊗) One NatTrans where+  assoc = NatTrans (\(FunctorProd (FunctorProd x y) z) -> FunctorProd x (FunctorProd y z))+  assoc_ = NatTrans (\(FunctorProd x (FunctorProd y z)) -> (FunctorProd (FunctorProd x y) z))+  unitorR = NatTrans (\x -> FunctorProd x FunctorOne)+  unitorR_ = NatTrans (\(FunctorProd x _) -> x)+  unitorL = NatTrans (FunctorProd FunctorOne)+  unitorL_ = NatTrans (\(FunctorProd _ x) -> x)+  NatTrans f ⊗ NatTrans g = NatTrans (\(FunctorProd x y) ->  FunctorProd (f x) (g y))+  

@@ -0,0 +1,162 @@+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Algebra.Category.Objects where++import Algebra.Classes+import Algebra.Types+import Prelude (Int, Ord (..),otherwise,($),Show, Semigroup(..),show)+import Data.Kind+import Data.Constraint+import Test.QuickCheck+import Test.QuickCheck.Property+import Control.Applicative++type TimesCon con = forall a b. (con a, con b) => con (a⊗b) :: Constraint+type DualCon con = forall a. (con a) => con (Dual a) :: Constraint+type PlusCon con = forall a b. (con a, con b) => con (a⊕b) :: Constraint+type Con' x con = forall a b. (con a, con b) => con (a `x` b) :: Constraint+type UnCon o con = forall a. (con a) => con (o a) :: Constraint++type TimesCon1 con = forall x a b. (con (a (b x))) => con ((a⊗b) x) :: Constraint+type PlusCon1 con = forall {k} (x :: k) a b. (con (a x), con (b x)) => con ((a⊕b) x) :: Constraint+type OneCon1 (con :: Type -> Constraint) = forall x. con x => con (One x) :: Constraint+type ZeroCon1 con = forall x. con x => con (Zero x) :: Constraint+-- type LConTensor con = forall a b. con (a⊗b) => con a :: Constraint+-- type RConTensor con = forall a b. con (a⊗b) => con a :: Constraint++reprCon :: forall con a x i t o. (Con' x con, Con' t con, con i, con o) => Repr x i t o a -> Dict (con a)+reprCon = \case+  RPlus a b -> Dict \\ reprCon @con a \\ reprCon @con b+  RTimes a b -> Dict \\ reprCon @con a \\ reprCon @con b+  RZero -> Dict+  ROne -> Dict++reprCon1Comp :: forall (z :: Type) con (a :: Type -> Type) b. CompClosed con -> con z => CRepr a -> CRepr b -> Dict (con (a (b z)))+reprCon1Comp c@CompClosed{} a b = Dict \\ reprCon1 @(b z) c a \\ reprCon1 @z c b++reprCon1 :: forall (z :: Type) (con :: Type -> Constraint) a. con z => CompClosed con -> CRepr a -> Dict (con (a z))+reprCon1 c@CompClosed{..} = \case+  RPlus a b -> plus1Closed \\ reprCon1 @z c a \\ reprCon1 @z c b+  RTimes a b -> times1Closed \\ reprCon1Comp @z c a b+  RZero -> zero1Closed+  ROne -> one1Closed+++type ProdObj :: forall {k}. (k -> Constraint) -> Constraint+class ProdObj (con :: k -> Constraint) where+  objprod :: (con a, con b) => Dict (con (a⊗b))+  objfstsnd :: forall z a b. (z ~ (a⊗b), con z) => Dict (con a, con b)+  objone :: Dict (con One)++type DualObj :: forall {k}. (k -> Constraint) -> Constraint+class ProdObj con => DualObj (con :: k -> Constraint) where+  objdual :: con a => Dict (con (Dual a))+  objdual' :: forall z a. (z ~ Dual a, con z) => Dict (con a)+++objFstSnd :: forall con a b. ProdObj con => Dict (con (a ⊗ b)) -> Dict (con a, con b)+objFstSnd Dict = objfstsnd @con @(a ⊗ b)++{-++type SumObj :: forall {k}. (k -> Constraint) -> Constraint+class SumObj (con :: k -> Constraint) where -- TensorClosed constraint causes problems in the Free module. (probably GHC bug)+  objsum :: (con a, con b) => Dict (con (a⊕b))+  objleftright :: forall z a b. (z ~ (a⊕b), con z) => Dict (con a, con b)+  objzero :: Dict (con Zero)+++objSumProxy :: (SumObj con, con a, con b) => proxy1 a -> proxy2 b -> Dict (con (a⊕b))+objSumProxy _ _  = objsum++objProdProxy :: (ProdObj con, con a, con b) => proxy1 a -> proxy2 b -> Dict (con (a⊗b))+objProdProxy _ _  = objprod++instance ProdObj Trivial where+  objprod = Dict+  objfstsnd = Dict+  objone = Dict++instance SumObj Trivial where+  objsum = Dict+  objleftright = Dict+  objzero = Dict++instance ProdObj Finite where+  objprod = Dict+  objfstsnd = finiteFstsnd+  objone = Dict++instance SumObj Finite where+  objsum = Dict+  objleftright = finiteLeftRight+  objzero = Dict++-}++type Trivial :: k -> Constraint+class Trivial x+instance Trivial x++++data Some1  f where+  Some1 :: f x -> Some1 f++sizedArbRepr :: Int -> Gen (Some1 (Repr x i t o))+sizedArbRepr n+  | n <= 1 = frequency [(1,pure(Some1 RZero)), (3,pure(Some1 ROne))]+  | otherwise = do+      Some1 l <- sizedArbRepr  (n `div` 2)+      Some1 r <- sizedArbRepr  (n `div` 2)+      elements [Some1 (RPlus l r),Some1 (RTimes l r)]++sizedArbSum :: Int -> Gen (Some1 (Repr x i t o))+sizedArbSum n+  | n <= 1 = frequency [(1,pure(Some1 RZero)), (3,pure(Some1 ROne))]+  | otherwise = do+      Some1 l <- sizedArbSum  (n `div` 2)+      Some1 r <- sizedArbSum  (n `div` 2)+      elements [Some1 (RPlus l r)]+++isArbitrary1 :: CRepr x -> Dict (Arbitrary1 x)+isArbitrary1 = reprCon++isCoArbitrary :: MRepr x -> Dict (CoArbitrary x)+isCoArbitrary = reprCon++instance Arbitrary (Some1 (Repr x i t o)) where+  arbitrary = sized sizedArbRepr++forallSumType :: forall {k} x i t o. (forall (a :: k). Repr x i t o a -> Property) -> Property+forallSumType gen = MkProperty $ do+  Some1 t <- (sized sizedArbSum :: Gen (Some1 (Repr x i t o)))+  unProperty (counterexample ("obj: " <> show t) (property (gen t)))++forallType :: forall {k} x i t o. (forall (a :: k). Repr x i t o a -> Property) -> Property+forallType gen = MkProperty $ do+  Some1 t <- (arbitrary :: Gen (Some1 (Repr x i t o)))+  unProperty (counterexample ("obj: " <> show t) (property (gen t)))++++arbitrary2' :: forall f a b proxy. Arbitrary (f a b) => proxy a -> proxy b -> Gen (f a b)+arbitrary2' _ _ = arbitrary++forallMorphism :: forall f a b x i t o. (Show (f a b), Arbitrary (f a b))+               => Repr x i t o a -> Repr x i t o b -> (f a b -> Property) -> Property+forallMorphism t1 t2 = forAll (arbitrary2' t1 t2)+

@@ -0,0 +1,70 @@+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Algebra.Category.Op where++import Algebra.Category+import Algebra.Classes+import Algebra.Category.Objects+import Prelude (Show)+import Test.QuickCheck++newtype Op k a b = Op {fromOp :: k b a}++deriving instance Additive (f b a) => Additive (Op f a b)+deriving instance Group (f b a) => Group (Op f a b)+deriving instance Arbitrary (f b a) => Arbitrary (Op f a b)+deriving instance Show (f b a) => Show (Op f a b)+deriving instance TestEqual (f b a) => TestEqual (Op f a b)++instance Category k => Category (Op k) where+  type Obj (Op k) = Obj k+  id = Op id+  Op f . Op g = Op (g . f)++instance Monoidal x i k => Monoidal x i (Op k) where+  Op f ⊗ Op g = Op (f ⊗ g)+  assoc = Op assoc_+  assoc_ = Op assoc+  unitorR = Op unitorR_+  unitorR_ = Op unitorR+  unitorL = Op unitorL_+  unitorL_ = Op unitorL++instance Cartesian x i k => CoCartesian x i (Op k) where+  inl = Op exl+  inr = Op exr+  new = Op dis+  jam = Op dup+  Op f ▿ Op g = Op (f ▵ g)++instance CoCartesian x i k => Cartesian x i (Op k) where+  exl = Op inl+  exr = Op inr+  dis = Op new+  dup = Op jam+  Op f ▵ Op g = Op (f ▿ g)++instance Braided x i k => Braided x i (Op k) where+  swap = Op swap+  swap_ = Op swap_++instance Symmetric x i k => Symmetric x i (Op k) where++instance (con ~ Obj k, Con' x con, UnCon r con, UnCon l con, con i, Autonomous x i r l k, Braided x i k) => Autonomous x i l r (Op k) where+  turn = swap . Op turn'+  turn' = Op turn . swap++instance (con ~ Obj k, Con' x con, UnCon d con, con i, Compact x i d k, Braided x i k) => Compact x i d (Op k) where++

@@ -0,0 +1,108 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeFamilies #-}++module Algebra.Category.Relation where++import Algebra.Classes+import Algebra.Types+import Algebra.Category+import Prelude (Bool(..), Eq(..),(&&),flip, ($))++newtype Rel s a b = Rel (a -> b -> s)++instance Additive s => Additive (Rel s a b) where+  Rel f + Rel g = Rel (f + g)+  zero = Rel zero++indicate :: Ring s => Bool -> s+indicate = \case+  True -> one+  False -> zero++instance Ring s => Category (Rel s) where+  type Obj (Rel s) = Finite+  Rel p . Rel q = Rel (\i j -> sum [p k j * q i k | k <- inhabitants])+  id = Rel (\_ _ -> one)++instance Ring s => Autonomous (⊗) One Dual Dual (Rel s) where+  turn = Rel (\_ (DualType i `Pair` j) -> indicate (i == j)) +  turn' =  Rel (\(i `Pair` DualType j) _ -> indicate (i == j))+instance Ring s => Compact (⊗) One Dual (Rel s)+instance Ring s => Symmetric (⊗) One (Rel s)+instance Ring s => Braided (⊗) One (Rel s) where+  swap = Rel (\(i `Pair` j) (k `Pair` l) -> indicate (i == l && j == k))++instance Ring s => Dagger (Rel s) where+  dagger (Rel r) = Rel (flip r)++instance Ring s => Monoidal (⊗) One (Rel s) where+  unitorR = Rel (\i (i' `Pair` _) -> indicate (i == i'))+  unitorR_ = dagger unitorR+  Rel p ⊗ Rel q = Rel (\(i `Pair` j) (k `Pair` l) -> p i k * q j l)+  assoc = Rel (\((i `Pair` j) `Pair` k) (i' `Pair` (j' `Pair` k')) -> indicate (i == i' && j == j' && k == k'))+  assoc_ = dagger assoc++instance Ring s => Cartesian (⊗) One (Rel s) where+  dis = Rel (\_ _ -> one)+  dup = Rel (\i (j `Pair` k) -> indicate (i == j && i == k))++instance Ring s => CoCartesian (⊗) One (Rel s) where+  new = dagger dis+  jam = dagger dup++instance Ring s => Monoidal (⊕) Zero (Rel s) where+  Rel p ⊗ Rel q = Rel $ \case+    (Inj1 i) -> \case+      (Inj1 j) -> p i j+      (Inj2 _) -> zero+    (Inj2 i) -> \case+      (Inj1 _) -> zero+      (Inj2 j) -> q i j+  unitorR = Rel $ \i -> \case+    Inj1 j -> indicate (i == j)+    Inj2 j -> case j of+  assoc = Rel $ \case+    (Inj1 (Inj1 i)) -> \case+      Inj1 j -> indicate (i == j)+      _ -> zero+    (Inj1 (Inj2 i)) -> \case+      Inj2 (Inj1 j) -> indicate (i == j)+      _ -> zero+    (Inj2 i) -> \case+      Inj2 (Inj2 j) -> indicate (i == j)+      _ -> zero+  unitorR_ = dagger unitorR+  assoc_ = dagger assoc++instance Ring s => Symmetric (⊕) Zero (Rel s)+instance Ring s => Braided (⊕) Zero (Rel s) where+  swap = Rel $ \case+    (Inj1 i) -> \case+      (Inj1 _) -> zero+      (Inj2 j) -> indicate (i == j)+    (Inj2 i) -> \case+      (Inj2 _) -> zero+      (Inj1 j) -> indicate (i == j)+    +instance Ring s => CoCartesian (⊕) Zero (Rel s) where+  Rel p ▿ Rel q = Rel $ \case+    (Inj1 i) -> \j -> p i j+    (Inj2 i) -> \j -> q i j+  inl = Rel $ \i -> \case+    (Inj1 j) -> indicate (i == j)+    _ -> zero+  inr = Rel $ \i -> \case+    (Inj2 j) -> indicate (i == j)+    _ -> zero+  new = Rel $ \case+  jam = Rel $ \case+    (Inj1 i) -> \j -> indicate (i == j)+    (Inj2 i) -> \j -> indicate (i == j)++instance Ring s => Cartesian (⊕) Zero (Rel s) where+  exl = dagger inl+  exr = dagger inr+  dup = dagger jam+  

@@ -0,0 +1,53 @@+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ConstrainedClassMethods #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE PolyKinds #-}++module Algebra.CategoryRecords where+++data CategoryRec con cat = CategoryRec{+  (∘)      :: forall a b c. (con a, con b, con c) => b `cat` c -> a `cat` b -> a `cat` c+  ,id :: forall a. con a => a `cat` a+  }+   +data MonoidalRec x i con cat = MonoidalRec+  {(⊗) :: forall a b c d. (con a, con b, con c, con d) => (a `cat` b) -> (c `cat` d) -> (a `x` c) `cat` (b `x` d)+  ,assoc     :: forall a b c. (con a, con b, con c) => ((a `x` b) `x` c) `cat` (a `x` (b `x` c))+  ,assoc_    :: forall a b c. (con a, con b, con c) => (a `x` (b `x` c)) `cat` ((a `x` b) `x` c)+  ,unitorR   :: forall a. (con a,con i) => a `cat` (a `x` i)+  ,unitorR_  :: forall a. (con a,con i) => (a `x` i) `cat` a+  ,unitorL   :: forall a. (con a, con i) => a `cat` (i `x` a)+  ,unitorL_  :: forall a. (con a, con i) => (i `x` a) `cat` a+  }++data BraidedRec x i con cat = BraidedRec+  {swap, swap_ :: forall a b. (con a, con b) => (a `x` b) `cat` (b `x` a)+  }++data CartesianRec x i con cat = CartesianRec+  {exl   ::   forall a b. (con a, con b)                     =>    (a `x` b) `cat` a+  ,exr   ::   forall a b. (con a, con b)                     =>    (a `x` b) `cat` b+  ,dis   ::   forall a.  con a                       =>    a `cat` i+  ,dup   ::   forall a. con a                        =>    a `cat` (a `x` a)+  ,(▵)   ::   forall a b c. (con a,con b, con c) =>    (a `cat` b) -> (a `cat` c) -> a `cat` (b `x` c)+  +  }+

@@ -1,3 +1,6 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -6,9 +9,9 @@ {-# LANGUAGE MultiParamTypeClasses, ConstraintKinds, FlexibleContexts, FlexibleInstances, DeriveGeneric #-} module Algebra.Classes where -import Prelude (Int,Integer,Float,Double, (==), Monoid(..), Ord(..), Foldable,-                foldMap, Char,-                 Real(..), Enum(..), snd, Rational, Functor(..), Eq(..), Bool(..), Semigroup(..), Show(..), uncurry)+import Prelude (Integer,Float,Double, (==), Monoid(..), Ord(..), Ordering(..), Foldable,+                foldMap, (||), (&&), ($),+                 Enum(..), snd, Rational, Functor(..), Eq(..), Bool(..), Semigroup(..), Show(..), uncurry, otherwise,String)  import qualified Prelude import qualified Data.Ratio@@ -19,6 +22,7 @@ import Data.Binary import Data.Complex import GHC.Generics+import GHC.Int import Test.QuickCheck import Control.Applicative @@ -27,49 +31,26 @@ infixl 6 - infixl 6 + -infixl 7 * infixr 7 *^+infixr 7 *<++infixl 7 * infixl 7 /-infixl 7 `mod` infixl 7 `div`+infixl 7 `mod`+infixl 7 `quot`+infixl 7 `rem`+ infixr 8 ^ infixr 8 ^++infixr 8 ^/+infixr 8 **+infixr 8 ^?  type Natural = Integer -newtype Sum a = Sum {fromSum :: a} deriving Generic--instance Binary a => Binary (Sum a)--instance Additive a => Monoid (Sum a) where-  mempty = Sum zero-  mappend = (<>)--instance Additive a => Semigroup (Sum a) where-  (<>) (Sum x) (Sum y) = Sum (x + y)--newtype Product a = Product {fromProduct :: a}--instance Multiplicative a => Semigroup (Product a) where-  (<>) (Product x) (Product y) = Product (x * y)--instance Multiplicative a => Monoid (Product a) where-  mempty = Product one-  mappend = (<>)--newtype Exponential a = Exponential {fromExponential :: a}--instance Additive a => Multiplicative (Exponential a) where-  Exponential a * Exponential b = Exponential (a + b)-  one = Exponential zero-  Exponential a ^+ n = Exponential (times n a)--instance Group a => Division (Exponential a) where-  recip (Exponential a) = Exponential (negate a)-  Exponential a / Exponential b = Exponential (a - b)--timesDefault :: (Additive a2, Prelude.Integral a1) => a1 -> a2 -> a2-timesDefault n0 = if n0 < 0 then Prelude.error "Algebra.Classes.times: negative number of times" else go n0+timesDefault :: (Additive a1, Additive a2, Prelude.Integral a1) => a1 -> a2 -> a2+timesDefault n0 = if n0 < zero then Prelude.error "Algebra.Classes.times: negative number of times" else go n0     where go 0 _ = zero           go n x = if r == 0 then y + y else x + y + y             where (m,r) = n `Prelude.divMod` 2@@ -82,9 +63,15 @@   times :: Natural -> a -> a   times = timesDefault -class (Arbitrary a, Show a) => TestEqual a where+class (Show a) => TestEqual a where   (=.=) :: a -> a -> Property +law_refl :: TestEqual a => a -> Property+law_refl x = nameLaw "=.=-reflexive" (x =.= x)++laws_testEqual :: forall a. Arbitrary a => TestEqual a => Property+laws_testEqual = property (law_refl @a)+ infix 0 =.=  instance Multiplicative Property where@@ -94,27 +81,61 @@ nameLaw :: Testable prop => Prelude.String -> prop -> Property nameLaw x p = label x (counterexample x p) -law_zero_plus :: forall a. (Additive a, TestEqual a) => a -> Property-law_zero_plus n = nameLaw "zero/plus" (zero + n =.= n)+law_assoc :: forall a. (TestEqual a) => String -> (a -> a -> a) -> a -> a -> a -> Property+law_assoc opName (⊕) m n o = nameLaw (opName <> "-assoc") (n ⊕ (m ⊕ o) =.= (n ⊕ m) ⊕ o) -law_plus_zero :: (Additive a, TestEqual a) => a -> Property-law_plus_zero n = nameLaw "plus/zero" (n + zero =.= n)+law_left_id :: forall a. (TestEqual a) => String -> (a -> a -> a) -> a -> a ->  Property+law_left_id opName (⊕) z n = nameLaw (opName <> "-leftId") (z ⊕ n =.= n) -law_plus_assoc :: (Additive a, TestEqual a) => a -> a -> a -> Property-law_plus_assoc m n o = nameLaw "plus/assoc" (n + (m + o) =.= (n + m) + o)+law_right_id :: forall a. (TestEqual a) => String -> (a -> a -> a) -> a -> a ->  Property+law_right_id opName (⊕) z n = nameLaw (opName <> "-rightId") (n ⊕ z =.= n) +laws_monoid :: forall a. (Arbitrary a, TestEqual a) => String -> (a -> a -> a) -> a -> Property+laws_monoid opName (⊕) z = product+   [property (law_left_id @a opName (⊕) z)+   ,property (law_right_id @a opName (⊕) z)+   ,property (law_assoc @a opName (⊕))]++law_commutative :: (TestEqual a) => String -> (a -> a -> a) -> a -> a -> Property+law_commutative opName (⊕) m n = nameLaw (opName <> "-comm") (m ⊕ n =.= n ⊕ m)++laws_comm_monoid :: forall a. (Arbitrary a, TestEqual a) => String -> (a -> a -> a) -> a -> Property+laws_comm_monoid opName (⊕) z = laws_monoid opName (⊕) z * property (law_commutative opName (⊕)) +                                          + law_times :: (TestEqual a, Additive a) => Positive Integer -> a -> Property law_times (Positive m) n = nameLaw "times" (times m n =.= timesDefault m n) -laws_additive :: forall a. (Additive a, TestEqual a) => Property-laws_additive = product [property (law_zero_plus @a)-                        ,property (law_plus_zero @a)-                        ,property (law_plus_assoc @a)+laws_additive :: forall a. Arbitrary a => (Additive a, TestEqual a) => Property+laws_additive = product [property (laws_monoid @a "plus" (+) zero)                         ,property (law_times @a)] -instance TestEqual Int where (=.=) = (===)+law_exp_pos :: (TestEqual a, Multiplicative a) => a -> Property+law_exp_pos n = nameLaw "positive exponent" $ do+  m <- choose (0,5) -- for dense polynomials, elevating to a large power can be very expensive.+  pure (n ^+ m =.= positiveExponentDefault n m) +laws_multiplicative :: forall a. Arbitrary a => (Multiplicative a, TestEqual a) => Property+laws_multiplicative = product [property (laws_monoid @a "mul" (*) one)+                              ,property (law_exp_pos @a)] +law_fromInteger :: forall a. (TestEqual a, Ring a) => Integer -> Property+law_fromInteger m = nameLaw "fromInteger" (fromInteger @a m =.= fromIntegerDefault m)++laws_ring :: forall a. Arbitrary a => (Ring a, TestEqual a) => Property+laws_ring = product [property (law_fromInteger @a)+                    ,laws_group @a+                    ,laws_module @a @a+                    ,laws_multiplicative @a]++instance TestEqual Int where (=.=) = (===)+instance TestEqual Double where+  x =.= y = counterexample (show x <> interpret res <> show y) res+   where+    res = (Prelude.abs (x-y) < 0.01)+    interpret True  = " == "  +    interpret False = " /= "+ sum :: (Foldable t, Additive a) => t a -> a sum xs = fromSum (foldMap Sum xs) @@ -138,6 +159,19 @@   zero = 0   times n x = Prelude.fromIntegral n * x +instance Additive Int32 where+  (+) = (Prelude.+)+  zero = 0+  times n x = Prelude.fromIntegral n * x+instance Additive Int16 where+  (+) = (Prelude.+)+  zero = 0+  times n x = Prelude.fromIntegral n * x+instance Additive Int8 where+  (+) = (Prelude.+)+  zero = 0+  times n x = Prelude.fromIntegral n * x+ instance Additive CInt where   (+) = (Prelude.+)   zero = 0@@ -153,16 +187,25 @@   zero = 0   times n x = Prelude.fromIntegral n * x +instance Additive Bool where+  (+) = (Prelude.||)+  zero = False+ instance Additive Float where   (+) = (Prelude.+)   zero = 0   times n x = Prelude.fromIntegral n * x -instance (Ord k,Additive v) => Additive (Map k v) where+instance (Ord k,AbelianAdditive v) => Additive (Map k v) where   (+) = M.unionWith (+)   zero = M.empty   times n = fmap (times n) +instance (Additive v) => Additive (k -> v) where+  (+) = liftA2 (+)+  zero = pure zero+  times n = fmap (times n)+ class Additive r => DecidableZero r where   isZero :: r -> Bool @@ -186,32 +229,43 @@   isZero = (== 0) instance DecidableZero Float where   isZero = (== 0)-instance (Ord k,DecidableZero v) => DecidableZero (Map k v) where+instance (Prelude.Integral x, DecidableZero x) => DecidableZero (Data.Ratio.Ratio x) where+  isZero x = isZero (Data.Ratio.numerator x)+instance (Ord k,DecidableZero v,AbelianAdditive v) => DecidableZero (Map k v) where   isZero = Prelude.all isZero+instance DecidableZero x => DecidableZero (Complex x) where+  isZero (x :+ y) = isZero x && isZero y  class Additive a => AbelianAdditive a   -- just a law. -law_plus_comm :: (TestEqual a, Additive a) => a -> a -> Property-law_plus_comm m n = nameLaw "plus/comm" (m + n =.= n + m)--laws_abelian_additive :: forall a. (Group a, TestEqual a) => Property-laws_abelian_additive = laws_additive @a .&&. product [property (law_plus_comm @a)]+laws_abelian_additive :: forall a. (Arbitrary a, AbelianAdditive a, TestEqual a) => Property+laws_abelian_additive = laws_comm_monoid @a "plus" (+) zero  instance AbelianAdditive Integer instance AbelianAdditive CInt instance AbelianAdditive Int+instance AbelianAdditive Int8+instance AbelianAdditive Int16+instance AbelianAdditive Int32+instance AbelianAdditive Word8+instance AbelianAdditive Word16+instance AbelianAdditive Word32+instance AbelianAdditive Bool instance AbelianAdditive Double instance AbelianAdditive Float instance (Ord k,AbelianAdditive v) => AbelianAdditive (Map k v)+instance (AbelianAdditive v) => AbelianAdditive (k -> v)  multDefault :: Group a => Natural -> a -> a multDefault n x = if n < 0 then negate (times (negate n) x) else times n x  class Additive a => Group a where-  {-# MINIMAL (negate | (-)) #-}+  {-# MINIMAL (negate | (-) | subtract) #-}   (-) :: a -> a -> a   a - b = a + negate b+  subtract :: a -> a -> a+  subtract b a = a - b   negate :: a -> a   negate b = zero - b   mult :: Integer -> a -> a@@ -224,13 +278,12 @@ law_mult m n = nameLaw "mult" (mult m n =.= multDefault m n)  -laws_group :: forall a. (Group a, TestEqual a) => Property+laws_group :: forall a. Arbitrary a => (Group a, TestEqual a) => Property laws_group = laws_additive @a .&&. product [property (law_negate_minus @a)                                            ,property (law_mult @a)] -laws_abelian_group :: forall a. (Group a, TestEqual a) => Property-laws_abelian_group = laws_group @a .&&. product [property (law_plus_comm @a)]-+laws_abelian_group :: forall a. Arbitrary a => (Group a, TestEqual a) => Property+laws_abelian_group = laws_group @a * product [property (law_commutative @a "plus" (+))]  instance Group Integer where   (-) = (Prelude.-)@@ -244,14 +297,22 @@   (-) = (Prelude.-)   negate = Prelude.negate -instance Group Word32 where+instance Group Int32 where   (-) = (Prelude.-)   negate = Prelude.negate+instance Group Int16 where+  (-) = (Prelude.-)+  negate = Prelude.negate+instance Group Int8 where+  (-) = (Prelude.-)+  negate = Prelude.negate +instance Group Word32 where+  (-) = (Prelude.-)+  negate = Prelude.negate instance Group Word16 where   (-) = (Prelude.-)   negate = Prelude.negate- instance Group Word8 where   (-) = (Prelude.-)   negate = Prelude.negate@@ -264,16 +325,51 @@   (-) = (Prelude.-)   negate = Prelude.negate -instance (Ord k,Group v) => Group (Map k v) where+instance (Ord k,Group v,AbelianAdditive v) => Group (Map k v) where   -- This definition does not work:   -- (-) = M.unionWith (-)   -- because if a key is not present on the lhs. then the rhs won't be negated.   negate = fmap negate --- | Module-class (AbelianAdditive a, PreRing scalar) => Module scalar a where-  (*^) :: scalar -> a -> a+instance (Group v) => Group (k -> v) where+  negate = fmap negate+  (-) = liftA2 (-) +-- | Functorial scaling. Compared to (*^) this operator disambiguates+-- the scalar type, by using the functor structure and using the+-- multiplicative instance for scalars.+(*<) :: (Functor f, Multiplicative a) => a -> f a -> f a+s *< v = (s*) <$> v++-- | Any instance must preserve the following invariants: 1. if+-- Multiplicative a and Scalable a a, then (*) = (*^) for a.+-- 2. Scalable must define a partial order relation, in particular,+-- instances of the form (Scalable s a) => Scalable s (T ... a ...)+-- are acceptable, and should be declared overlappable.++class Scalable s a where+  (*^) :: s -> a -> a++instance {-# Overlappable #-} Scalable s a => Scalable s (Map k a) where+  s *^ x = fmap (s *^) x++instance {-# Overlappable #-} Scalable s a => Scalable s (k -> a) where+  s *^ x = fmap (s *^) x++-- | "Most natural" scaling. Also disambiguates the scalar type, but using a fundep.+class Scalable' a where+  type Scalar a+  (!*^) :: Scalar a -> a -> a++  +-- | A prefix variant of (*^), useful when using type applications.+-- scale :: forall s a. Scalable s a => s -> a -> a+-- scale = (*^)++type SemiModule s a = (AbelianAdditive a, SemiRing s, Scalable s a)++type Module s a = (SemiModule s a, Group s, Group a)+ law_module_zero :: forall s a. (Module s a, TestEqual a) => s -> Property law_module_zero s = nameLaw "module/zero" (s *^ zero =.= zero @a) @@ -289,7 +385,7 @@ law_module_mul :: forall s a. (Module s a, TestEqual a) => s -> s -> a -> Property law_module_mul s t x = nameLaw "module/mul/assoc" ((s * t) *^ x =.= s *^ t *^ x) -laws_module :: forall s a. (Module s a, TestEqual a, Arbitrary s, Show s) => Property+laws_module :: forall s a. Arbitrary a => (Module s a, TestEqual a, Arbitrary s, Show s) => Property laws_module = laws_additive @a .&&. product [property (law_module_zero @s @a)                                             ,property (law_module_one @s @a)                                             ,property (law_module_sum @s @a)@@ -304,37 +400,42 @@           collapse (a,_) (_,b) = (a,b)  -instance Module Integer Integer where+instance Scalable Integer Integer where   (*^) = (*) -instance Module Int Int where-  (*^) = (*)+instance Scalable Int Int where (*^) = (*) -instance Module CInt CInt where-  (*^) = (*)+instance Scalable Int8 Int8 where (*^) = (*)+instance Scalable Int16 Int16 where (*^) = (*)+instance Scalable Int32 Int32 where (*^) = (*) -instance Module Double Double where+instance Scalable Word8 Word8 where (*^) = (*)+instance Scalable Word16 Word16 where (*^) = (*)+instance Scalable Word32 Word32 where (*^) = (*)++instance Scalable CInt CInt where   (*^) = (*) -instance Module Float Float where+instance Scalable Double Double where   (*^) = (*) -instance (Ord k, Module a b) => Module a (Map k b) where-  s *^ m = fmap (s *^) m+instance Scalable Float Float where+  (*^) = (*)  -- | Multiplicative monoid class Multiplicative a where   (*) :: a -> a -> a   one :: a   (^+) :: a -> Natural -> a+  (^+) = positiveExponentDefault -  x0 ^+ n0 = if n0 < 0 then Prelude.error "Algebra.Classes.^: negative exponent" else go x0 n0+positiveExponentDefault :: Multiplicative a => a -> Natural -> a+positiveExponentDefault x0 n0 = if n0 < 0 then Prelude.error "Algebra.Classes.^+: negative exponent" else go x0 n0     where go _ 0 = one           go x n = if r == 0 then y * y else x * y * y             where (m,r) = n `Prelude.divMod` 2                   y = go x m - product :: (Multiplicative a, Foldable f) => f a -> a product xs = fromProduct (foldMap Product xs) @@ -363,6 +464,21 @@   one = 1   (^+) = (Prelude.^) +instance Multiplicative Int32 where+  (*) = (Prelude.*)+  one = 1+  (^+) = (Prelude.^)++instance Multiplicative Int16 where+  (*) = (Prelude.*)+  one = 1+  (^+) = (Prelude.^)++instance Multiplicative Int8 where+  (*) = (Prelude.*)+  one = 1+  (^+) = (Prelude.^)+ instance Multiplicative Int where   (*) = (Prelude.*)   one = 1@@ -378,6 +494,9 @@   one = 1   (^+) = (Prelude.^) +instance Multiplicative Bool where+  (*) = (Prelude.&&)+  one = True   type SemiRing a = (Multiplicative a, AbelianAdditive a)@@ -393,6 +512,14 @@ instance Ring Integer where   fromInteger = Prelude.fromInteger +instance Ring Int8 where fromInteger = Prelude.fromInteger+instance Ring Int16 where fromInteger = Prelude.fromInteger+instance Ring Int32 where fromInteger = Prelude.fromInteger++instance Ring Word8 where fromInteger = Prelude.fromInteger+instance Ring Word16 where fromInteger = Prelude.fromInteger+instance Ring Word32 where fromInteger = Prelude.fromInteger+ instance Ring CInt where   fromInteger = Prelude.fromInteger @@ -439,72 +566,80 @@   fromRational = Prelude.fromRational  -class Ring a => EuclideanDomain a where-    {-# MINIMAL (stdUnit | normalize) , (divMod | (div , mod)) #-}+class (Ring a, DecidableZero a) => EuclideanDomain a where+    {-# MINIMAL (stdUnit | normalize) , (quotRem | (quot , rem)) #-}     stdAssociate    :: a -> a     stdUnit         :: a -> a     normalize       :: a -> (a, a) -    div, mod        :: a -> a -> a-    divMod          :: a -> a -> (a,a)+    quot, rem        :: a -> a -> a+    quotRem          :: a -> a -> (a,a) -    stdAssociate x  =  x `div` stdUnit x+    stdAssociate x  =  x `quot` stdUnit x     stdUnit x       =  snd (normalize x)     normalize x     =  (stdAssociate x, stdUnit x) -    n `divMod` d    =  (n `div` d, n `mod` d)-    n `div` d       =  q  where (q,_) = divMod n d-    n `mod` d       =  r  where (_,r) = divMod n d+    n `quotRem` d    =  (n `quot` d, n `rem` d)+    n `quot` d       =  q  where (q,_) = quotRem n d+    n `rem` d       =  r  where (_,r) = quotRem n d +gcd             :: EuclideanDomain a => a -> a -> a+{-# NOINLINE [1] gcd #-}+gcd x y         =  gcd' (stdAssociate x) (stdAssociate y)+ where+   gcd'             :: (EuclideanDomain a) => a -> a -> a+   gcd' a b | isZero b  =  a+            | otherwise  =  gcd' b (a `rem` b) +-- | @'lcm' x y@ is the smallest positive integer that both @x@ and @y@ divide.+lcm :: (EuclideanDomain a) => a -> a -> a+{-# SPECIALISE lcm :: Int -> Int -> Int #-}+{-# NOINLINE [1] lcm #-}+lcm x y | isZero x || isZero y = zero+        | otherwise =  stdAssociate ((x `quot` (gcd x y)) * y)+ instance  EuclideanDomain Integer  where-    div             =  Prelude.div-    mod             =  Prelude.mod+    quot             =  Prelude.quot+    rem             =  Prelude.rem     stdAssociate x  =  Prelude.abs x     stdUnit x       =  if x < 0 then -1 else 1  instance  EuclideanDomain CInt  where-    div             =  Prelude.div-    mod             =  Prelude.mod+    quot             =  Prelude.quot+    rem             =  Prelude.rem     stdAssociate x  =  Prelude.abs x     stdUnit x       =  if x < 0 then -1 else 1  instance  EuclideanDomain Int  where-    div             =  Prelude.div-    mod             =  Prelude.mod+    quot             =  Prelude.quot+    rem             =  Prelude.rem     stdAssociate x  =  Prelude.abs x     stdUnit x       =  if x < 0 then -1 else 1 -class (Real a, Enum a, EuclideanDomain a) => Integral a  where-    quot, rem       :: a -> a -> a-    quotRem         :: a -> a -> (a,a)++-- Note: base.Integral has "Real", superclass, which also defines "toRational"+class (Ord a, Ring a, Enum a, EuclideanDomain a) => Integral a  where+    div, mod       :: a -> a -> a+    divMod         :: a -> a -> (a,a)     toInteger       :: a -> Integer -    n `quot` d      =  q  where (q,_) = quotRem n d-    n `rem` d       =  r  where (_,r) = quotRem n d-    quotRem n d     =  if Prelude.signum r == - Prelude.signum d then (q+one, r-d) else qr-      where qr@(q,r) = divMod n d+    n `div` d      =  q  where (q,_) = divMod n d+    n `mod` d       =  r  where (_,r) = divMod n d+    divMod n d     =  if stdUnit r == negate (stdUnit d) then (q+one, r-d) else qr+      where qr@(q,r) = quotRem n d  instance  Integral Integer  where-    quot      =  Prelude.quot-    rem       =  Prelude.rem+    div      =  Prelude.div+    mod       =  Prelude.mod     toInteger = Prelude.toInteger --gcd             :: (Integral a) => a -> a -> a-{-# NOINLINE [1] gcd #-}-gcd x y         =  gcd' (stdAssociate x) (stdAssociate y)- where-   gcd'             :: (Eq a, Integral a) => a -> a -> a-   gcd' a 0  =  a-   gcd' a b  =  gcd' b (a `rem` b)--{- -}--+instance  Integral Int  where+    div      =  Prelude.div+    mod       =  Prelude.mod+    toInteger = Prelude.toInteger ------------------------------ Ratio instances+---------------------------------------+-- Data.Ratio.Ratio instances instance Prelude.Integral a => Additive (Data.Ratio.Ratio a) where   zero = Prelude.fromInteger 0   (+) = (Prelude.+)@@ -524,18 +659,18 @@   recip = Prelude.recip   (/) = (Prelude./)   (^) = (Prelude.^^)-instance Prelude.Integral a => Module (Data.Ratio.Ratio a) (Data.Ratio.Ratio a) where+instance Prelude.Integral a => Scalable (Data.Ratio.Ratio a) (Data.Ratio.Ratio a) where   (*^) = (*) instance Prelude.Integral a => Ring (Data.Ratio.Ratio a) where   fromInteger = Prelude.fromInteger instance Prelude.Integral a => Field (Data.Ratio.Ratio a) where   fromRational = Prelude.fromRational +instance Scalable Rational Double where+    r *^ d = fromRational r * d  ---------------------- -- Complex instances-instance Module Rational Double where-    r *^ d = fromRational r * d instance Additive a => Additive (Complex a) where     (x:+y) + (x':+y')   =  (x+x') :+ (y+y')     zero = zero :+ zero@@ -546,10 +681,10 @@     (x:+y) - (x':+y')   =  (x-x') :+ (y-y')     negate (x:+y)       =  negate x :+ negate y instance AbelianAdditive a => AbelianAdditive (Complex a)-instance Ring a => Module (Complex a) (Complex a) where+instance Ring a => Scalable (Complex a) (Complex a) where   (*^) = (*)-instance Ring a => Module a (Complex a) where-  s *^ (x :+ y) =  (s *^ x :+ s *^ y)+instance {-# Overlappable #-} Scalable s a => Scalable s (Complex a) where+  s *^ x = fmap (s *^) x instance Ring a => Ring (Complex a) where     fromInteger n  =  fromInteger n :+ zero @@ -561,28 +696,6 @@ instance Field a => Field (Complex a) where     fromRational a =  fromRational a :+ zero -{-data Expr a where-  Embed :: a -> Expr a-  Add :: Expr a -> Expr a -> Expr a-  Mul :: Expr a -> Expr a -> Expr a-  Zero :: Expr a-  One :: Expr a-  deriving (Prelude.Show)---instance Additive (Expr a) where-  zero = Zero-  Zero + x = x-  x + Zero = x-  x + y = Add x y--instance Multiplicative (Expr a) where-  one = One-  One * x = x-  x * One = x-  x * y = Mul x y--}- -- Syntax  ifThenElse :: Bool -> t -> t -> t@@ -590,22 +703,285 @@ ifThenElse False _ a = a  +class Division a => Roots a where+  {-# MINIMAL root | (^/) #-}+  sqrt :: a -> a+  sqrt = root 2+  {-# INLINE sqrt #-} --- >>> times 5 (Embed "x")--- Add (Add (Embed "x") (Add (Embed "x") (Embed "x"))) (Add (Embed "x") (Embed "x"))+  root :: Integer -> a -> a+  root n x = x ^/ (1 Data.Ratio.% n) +  (^/) :: a -> Rational -> a+  x ^/ y = root (Data.Ratio.denominator y) (x ^ Data.Ratio.numerator y) --- >>> (Embed "x")--- Zero+type Algebraic a = (Roots a, Field a) +instance Roots Float where+  sqrt = Prelude.sqrt+  x ^/ y = x ** fromRational y -{--Note: the following is not quite what we intuitively want, because+instance Roots Double where+  sqrt = Prelude.sqrt+  x ^/ y = x ** fromRational y -class Field a => AlgebraicallyClosed  a where-  sqrt :: a -> (a,a)+-- | Class providing transcendental functions+class Algebraic a => Transcendental a where +    pi                  :: a+    exp, log            :: a -> a+    (**), logBase       :: a -> a -> a+    sin, cos, tan       :: a -> a+    asin, acos, atan    :: a -> a+    sinh, cosh, tanh    :: a -> a+    asinh, acosh, atanh :: a -> a -AlgebraicallyClosed numbers have two square roots.+    -- | @'log1p' x@ computes @'log' (1 + x)@, but provides more precise+    -- results for small (absolute) values of @x@ if possible.+    --+    -- @since 4.9.0.0+    log1p               :: a -> a --}+    -- | @'expm1' x@ computes @'exp' x - 1@, but provides more precise+    -- results for small (absolute) values of @x@ if possible.+    --+    -- @since 4.9.0.0+    expm1               :: a -> a +    -- | @'log1pexp' x@ computes @'log' (1 + 'exp' x)@, but provides more+    -- precise results if possible.+    --+    -- Examples:+    --+    -- * if @x@ is a large negative number, @'log' (1 + 'exp' x)@ will be+    --   imprecise for the reasons given in 'log1p'.+    --+    -- * if @'exp' x@ is close to @-1@, @'log' (1 + 'exp' x)@ will be+    --   imprecise for the reasons given in 'expm1'.+    --+    -- @since 4.9.0.0+    log1pexp            :: a -> a++    -- | @'log1mexp' x@ computes @'log' (1 - 'exp' x)@, but provides more+    -- precise results if possible.+    --+    -- Examples:+    --+    -- * if @x@ is a large negative number, @'log' (1 - 'exp' x)@ will be+    --   imprecise for the reasons given in 'log1p'.+    --+    -- * if @'exp' x@ is close to @1@, @'log' (1 - 'exp' x)@ will be+    --   imprecise for the reasons given in 'expm1'.+    --+    -- @since 4.9.0.0+    log1mexp            :: a -> a++    {-# INLINE (**) #-}+    {-# INLINE logBase #-}+    {-# INLINE tan #-}+    {-# INLINE tanh #-}+    x ** y              =  exp (log x * y)+    logBase x y         =  log y / log x+    tan  x              =  sin  x / cos  x+    tanh x              =  sinh x / cosh x++    {-# INLINE log1p #-}+    {-# INLINE expm1 #-}+    {-# INLINE log1pexp #-}+    {-# INLINE log1mexp #-}+    log1p x = log (one + x)+    expm1 x = exp x - one+    log1pexp x = log1p (exp x)+    log1mexp x = log1p (negate (exp x))++(^?) :: Transcendental a => a -> a -> a+(^?) = (**)++instance Transcendental Double where+  pi = Prelude.pi+  exp = Prelude.exp+  log = Prelude.log+  (**) = (Prelude.**)+  logBase = Prelude.logBase+  sin = Prelude.sin+  cos = Prelude.cos+  tan = Prelude.tan+  asin = Prelude.asin+  acos = Prelude.acos+  atan = Prelude.atan+  sinh = Prelude.sinh+  cosh = Prelude.cosh+  tanh = Prelude.tanh+  asinh = Prelude.asinh+  acosh = Prelude.acosh+  atanh = Prelude.atanh++instance Transcendental Float where+  pi = Prelude.pi+  exp = Prelude.exp+  log = Prelude.log+  (**) = (Prelude.**)+  logBase = Prelude.logBase+  sin = Prelude.sin+  cos = Prelude.cos+  tan = Prelude.tan+  asin = Prelude.asin+  acos = Prelude.acos+  atan = Prelude.atan+  sinh = Prelude.sinh+  cosh = Prelude.cosh+  tanh = Prelude.tanh+  asinh = Prelude.asinh+  acosh = Prelude.acosh+  atanh = Prelude.atanh++++instance (Prelude.RealFloat a, Ord a, Algebraic a) => Roots (Complex a) where+    root n x = mkPolar (root n ρ) (θ / fromInteger n)+      where (ρ,θ) = polar x+    sqrt z@(x:+y)+      | z == zero = zero+      | otherwise +                     =  u :+ (if y < 0 then -v else v)+                      where (u,v) = if x < 0 then (v',u') else (u',v')+                            v'    = Prelude.abs y / (u'*2)+                            u'    = sqrt ((magnitude z + Prelude.abs x) / 2)+++instance  (Prelude.RealFloat a, Transcendental a) => AlgebraicallyClosed (Complex a) where+  imaginaryUnit = 0 :+ 1+  rootOfUnity n i = exp (0 :+ 2*pi*fromInteger i/fromInteger n)+  ++instance  (Prelude.RealFloat a, Transcendental a) => Transcendental (Complex a) where+    {-# SPECIALISE instance Transcendental (Complex Float) #-}+    {-# SPECIALISE instance Transcendental (Complex Double) #-}+    pi             =  pi :+ 0+    exp (x:+y)     =  expx * cos y :+ expx * sin y+                      where expx = exp x+    log z          =  log (magnitude z) :+ phase z++    x ** y = case (x,y) of+      (_ , (0:+0))  -> 1 :+ 0+      ((0:+0), (exp_re:+_)) -> case compare exp_re 0 of+                 GT -> 0 :+ 0+                 LT -> inf :+ 0+                 EQ -> nan :+ nan+      ((re:+im), (exp_re:+_))+        | (Prelude.isInfinite re || Prelude.isInfinite im) -> case compare exp_re 0 of+                 GT -> inf :+ 0+                 LT -> 0 :+ 0+                 EQ -> nan :+ nan+        | otherwise -> exp (log x * y)+      where+        inf = 1/0+        nan = 0/0++    sin (x:+y)     =  sin x * cosh y :+ cos x * sinh y+    cos (x:+y)     =  cos x * cosh y :+ (- sin x * sinh y)+    tan (x:+y)     =  (sinx*coshy:+cosx*sinhy)/(cosx*coshy:+(-sinx*sinhy))+                      where sinx  = sin x+                            cosx  = cos x+                            sinhy = sinh y+                            coshy = cosh y++    sinh (x:+y)    =  cos y * sinh x :+ sin  y * cosh x+    cosh (x:+y)    =  cos y * cosh x :+ sin y * sinh x+    tanh (x:+y)    =  (cosy*sinhx:+siny*coshx)/(cosy*coshx:+siny*sinhx)+                      where siny  = sin y+                            cosy  = cos y+                            sinhx = sinh x+                            coshx = cosh x++    asin z@(x:+y)  =  y':+(-x')+                      where  (x':+y') = log (((-y):+x) + sqrt (1 - z*z))+    acos z         =  y'':+(-x'')+                      where (x'':+y'') = log (z + ((-y'):+x'))+                            (x':+y')   = sqrt (1 - z*z)+    atan z@(x:+y)  =  y':+(-x')+                      where (x':+y') = log (((1-y):+x) / sqrt (1+z*z))++    asinh z        =  log (z + sqrt (1+z*z))+    -- Take care to allow (-1)::Complex, fixing #8532+    acosh z        =  log (z + (sqrt (z+1)) * (sqrt (z-1)))+    atanh z        =  0.5 * log ((1.0+z) / (1.0-z))+++class Algebraic a => AlgebraicallyClosed a where+  imaginaryUnit :: a+  imaginaryUnit = rootOfUnity 2 1+  -- | rootOfUnity n give the nth roots of unity. The 2nd argument specifies which one is demanded+  rootOfUnity :: Integer -> Integer -> a++----------------+-- The following should go in Morphism.Monoids but sum/product depend on it.++newtype Sum a = Sum {fromSum :: a} deriving (Generic,Ord,Eq,Show)++instance Binary a => Binary (Sum a)++instance Additive a => Monoid (Sum a) where+  mempty = Sum zero+  mappend = (<>)++instance Additive a => Semigroup (Sum a) where+  (<>) (Sum x) (Sum y) = Sum (x + y)+++newtype Product a = Product {fromProduct :: a} deriving (Generic,Ord,Eq,Show)++instance Multiplicative a => Semigroup (Product a) where+  (<>) (Product x) (Product y) = Product (x * y)++instance Multiplicative a => Monoid (Product a) where+  mempty = Product one+  mappend = (<>)++---------------------+-- Functor application, useful for "deriving via".++newtype App f x = App (f x) deriving (Functor, Applicative) -- should be somewhere in base but can't find it.++instance (Applicative f, AbelianAdditive a) => AbelianAdditive (App f a) where+instance (Applicative f, Additive a) => Additive (App f a) where+  (+) = liftA2 (+)+  zero = pure zero+instance (Applicative f, Group a) => Group (App f a) where+  (-) = liftA2 (-)+  negate = fmap negate++instance (Applicative f, Multiplicative a) => Multiplicative (App f a) where+  (*) = liftA2 (*)+  one = pure one++instance (Applicative f, Scalable s a) =>  Scalable (App f s) (App f a) where+  (*^) = liftA2 (*^)++instance (Applicative f, Division s) => Division (App f s) where+  recip = fmap recip+  (/) = liftA2 (/)++instance (Applicative f, Roots s) => Roots (App f s) where+  x ^/ r = (^/ r) <$> x+  root i = fmap (root i)++instance (Applicative f, Field s) => Field (App f s) where+  fromRational x = pure (fromRational x)+  +instance (Applicative f, Transcendental s) => Transcendental (App f s) where+  pi = pure pi+  exp = fmap exp+  log = fmap log +  sin = fmap sin +  cos = fmap cos +  asin = fmap asin +  acos = fmap acos +  atan = fmap atan +  sinh = fmap sinh +  cosh = fmap cosh +  asinh = fmap asinh +  acosh = fmap acosh +  atanh = fmap atanh +  +instance (Applicative f, Ring a) => Ring (App f a) where+  fromInteger x = pure (fromInteger x)

@@ -1,5 +1,8 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-}-{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveFoldable #-}@@ -25,49 +28,117 @@  module Algebra.Linear where -import Algebra.Classes hiding ((*<))-import Prelude (cos,sin,Floating(..),Functor(..),Show(..),Eq(..),Int,fst,($),Ord,Double)+import Algebra.Classes+import Algebra.Category.Laws (laws_bicartesian,testableCat)+import Prelude (Show(..),Eq(..),($),Ord,error,flip,IO,Bool,Int,Functor,fmap+               ,return) import Control.Applicative import Data.Foldable hiding (sum,product) import Data.Traversable import Control.Monad.State import Algebra.Category--infixr 7 *<+import Algebra.Types+import Data.Constraint+import Algebra.Category.Relation+import Algebra.Category.Objects+import Data.Functor.Rep+import Data.Distributive+import Test.QuickCheck hiding (collect, tabulate)  type VectorSpace scalar a = (Field scalar, Module scalar a, Group a) -- Because of the existence of bases, vector spaces can always be made representable (Traversable, Applicative) functors. -- So we'd be better off using the following definition:  -- | Representation of vector as traversable functor-type VectorR v = (Applicative v,Traversable v) -- ... but this is missing the link with *^ for module.  We should be--- able to add forall s. PreRing s => Module s (v s), but GHC does not--- like it. (In fact, QuantifiedConstraints is very buggy in ghc 8.6)+-- able to add forall s. PreRing s => Module s (v s), but this creates+-- problems when defining instances. +class (Finite (Rep v),Representable v, Foldable v, Applicative v) => VectorR v where+  vectorSplit :: (v ~ (f ⊗ g)) => Dict (VectorR f, VectorR g)+  vectorSplit = error "vectorSplit: not product type"+  vectorCut :: (v ~ (f ⊕ g)) => Dict (VectorR f, VectorR g)+  vectorCut = error "vectorCut: not sum type"++instance (VectorR v, VectorR w) => VectorR (v ⊗ w) where+  -- vectorSplit = Dict++instance (VectorR v, VectorR w) => VectorR (v ∘ w) where+  -- vectorCut = Dict++instance (VectorR One)+instance (VectorR Id)++{-instance SumObj VectorR where+  objsum = Dict+  objleftright = vectorCut+  objzero = Dict++instance ProdObj VectorR where+  objprod = Dict+  objfstsnd = vectorSplit+  objone = Dict+-}++ class VectorR v => InnerProdSpace v where   inner :: Field s => v s -> v s -> s  -------------------------------------------------------------- -- Construction of finite vectors -data VZero a = VZero deriving (Functor,Foldable,Traversable,Show,Eq,Ord)-instance Applicative VZero where-  pure _ = VZero-  VZero <*> VZero = VZero+type VZero x = Zero x -data VNext v a = VNext !(v a) !a deriving (Functor,Foldable,Traversable,Show,Eq,Ord)+data VNext v a = VNext {vnextInit :: !(v a), vnextLast :: !a} deriving (Functor,Foldable,Traversable,Show,Eq,Ord)++instance Distributive v => Distributive (VNext v) where+  collect f x = VNext (collect (vnextInit . f) x) (vnextLast . f <$> x)+instance Representable a => Representable (VNext a) where+  type Rep (VNext a) = One ⊕ (Rep a)+  index (VNext xs x) = \case+    Inj1 _ -> x+    Inj2 i -> index xs i+  tabulate f = VNext (tabulate (f . Inj2)) (f (Inj1 Unit))+instance VectorR a => VectorR (VNext a) where++data V f a where+  V0 :: V One a+  (:/) :: !(V f a) -> !a -> V (VNext f) a++deriving instance Functor (V f)+deriving instance Foldable (V f)+deriving instance Traversable (V f)+deriving instance Show a => Show (V f a)+deriving instance Eq a => Eq (V f a)++class (Foldable f,Applicative f) => IsVec f where+  reifyVec :: f a -> V f a++instance IsVec One where+  reifyVec FunctorOne = V0++instance IsVec f => IsVec (VNext f) where+  reifyVec (VNext xs x) = reifyVec xs :/ x++fromV :: V f a -> f a+fromV V0 = FunctorOne+fromV (xs :/ x) = VNext (fromV xs) x++instance IsVec f => Applicative (V f) where+  pure x = reifyVec (pure x)+  fs <*> xs = reifyVec (fromV fs <*> fromV xs)+ instance Applicative v => Applicative (VNext v) where   pure x = VNext (pure x) x   VNext fs f <*> VNext xs x = VNext (fs <*> xs) (f x)  -type V1' = VNext VZero+type V1' = VNext One type V2' = VNext V1' type V3' = VNext V2'  pattern V1' :: a -> V1' a-pattern V1' x = VNext VZero x+pattern V1' x = VNext FunctorOne x pattern V2' :: forall a. a -> a -> V2' a pattern V2' x y = VNext (V1' x) y pattern V3' :: forall a. a -> a -> a -> V3' a@@ -77,8 +148,12 @@ -- Euclidean spaces with a (inner product)  -- | Make a Euclidean vector out of a traversable functor. (The p)-newtype Euclid f a = Euclid {fromEuclid :: f a} deriving (Functor,Foldable,Traversable,Show,Eq,Ord,Applicative)+newtype Euclid f a = Euclid {fromEuclid :: f a}+  deriving (Functor,Foldable,Traversable,Show,Eq,Ord,Applicative) +deriving via App f a instance (Applicative f, Additive a) => Additive (Euclid f a)+deriving via App f a instance (Applicative f, Group a) => Group (Euclid f a)+ type V3 = Euclid V3' type V2 = Euclid V2' @@ -87,16 +162,8 @@ pattern V3 :: forall a. a -> a -> a -> Euclid V3' a pattern V3 x y z = Euclid (V3' x y z) -instance (Applicative f,Additive a) => Additive (Euclid f a) where-  zero = pure zero-  x + y =  (+) <$> x <*> y-instance (Applicative f,AbelianAdditive a) => AbelianAdditive (Euclid f a) where-instance (Applicative f,Group a) => Group (Euclid f a) where-  negate x = negate <$> x-  x - y = (-) <$> x <*> y--instance (Applicative f,Module s a) => Module s (Euclid f a) where-  s *^ t = (s*^) <$> t+instance (Functor f, Scalable s a) => Scalable s (Euclid f a) where+  s *^ Euclid t = Euclid (((s*^) <$>) t)  pureMat :: (Applicative v, Applicative w) => s -> Mat s v w pureMat x = Mat (pure (pure x))@@ -109,14 +176,20 @@   negate x = matFlat (negate <$> flatMat x)   x - y = matFlat ((-) <$> flatMat x <*> flatMat y) -instance (Applicative f, Applicative g,Module s a) => Module s (Mat a f g) where+instance (Functor f, Functor g,Scalable s a) => Scalable s (Mat a f g) where   s *^ Mat t = Mat (((s*^) <$>) <$> t) - -- | Hadamard product (⊙) :: Applicative v => Multiplicative s => v s -> v s -> v s x ⊙ y = (*) <$> x <*> y +instance Distributive f => Distributive (Euclid f) where+  collect f = Euclid . collect (fromEuclid . f)+instance Representable f => Representable (Euclid f) where+  type Rep (Euclid f) = Rep f+  index (Euclid x) = index x+  tabulate f = Euclid (tabulate f)+instance VectorR f => VectorR (Euclid f) instance (VectorR f) => InnerProdSpace (Euclid f) where   inner x y = sum (x ⊙ y) -- fixme @@ -126,20 +199,16 @@ sqNorm :: Field s => InnerProdSpace v => v s -> s sqNorm x = inner x x -norm :: Field s => InnerProdSpace v => Floating s => v s  -> s+norm :: Algebraic s => InnerProdSpace v => v s  -> s norm = sqrt . sqNorm -normalize :: (VectorSpace s (v s)) => Floating s => InnerProdSpace v => v s -> v s+normalize :: (VectorSpace s (v s)) => Algebraic s => InnerProdSpace v => v s -> v s normalize v = recip (norm v) *^ v  -- | Cross product in 3 dimensions https://en.wikipedia.org/wiki/Cross_product (×) :: Ring a => V3 a -> V3 a -> V3 a (V3 a1 a2 a3) × (V3 b1 b2 b3) = V3 (a2*b3 - a3*b2)  (negate (a1*b3 - a3*b1)) (a1*b2 - a2*b1) -index :: Applicative v => Traversable v => v Int-index = fst (runState (sequenceA (pure increment)) zero)-  where increment = do x <- get; put (x+1); return x- type SqMat v s = Mat s v v  -- | Matrix type. (w s) is a column. (v s) is a row.@@ -158,10 +227,49 @@   instance Ring s => Category (Mat s) where-  type Con v = VectorR v+  type Obj (Mat s) = VectorR   (.) = matMul-  id = identity+  id = fromRel id +fromRel :: (VectorR a, VectorR b) => Rel s (Rep a) (Rep b) -> Mat s a b+fromRel (Rel f) = Mat (tabulate (\i -> tabulate (\j -> f i j)))+  +instance Ring s => Monoidal (∘) Id (Mat s) where+  assoc = fromRel assoc+  assoc_ = fromRel assoc_+  unitorR = fromRel unitorR+  unitorR_ = fromRel unitorR_+  Mat f ⊗ Mat g = Mat (Comp (fmap (\x -> fmap Comp  (fmap (\y -> liftA2 (liftA2 (*)) (fmap pure x) (pure y)) g)) f))+++instance Ring s => Symmetric (∘) Id (Mat s) where+instance Ring s => Braided (∘) Id (Mat s) where+  swap = fromRel swap++instance Ring s => Monoidal (⊗) One (Mat s) where+  assoc = fromRel assoc+  assoc_ = fromRel assoc_+  unitorR = fromRel unitorR+  unitorR_ = fromRel unitorR_+  Mat f ⊗ Mat g = Mat (FunctorProd+                        ((flip FunctorProd (pure zero)) <$> f)+                        (FunctorProd (pure zero) <$> g))++instance Ring s => Cartesian (⊗) One (Mat s) where+  Mat f ▵ Mat g = Mat (FunctorProd <$> f <*> g)+  dis = fromRel dis++instance Ring s => Braided (⊗) One (Mat s) where+  swap = fromRel swap+instance Ring s => Symmetric (⊗) One (Mat s) where++instance Ring s => CoCartesian (⊗) One (Mat s) where+  inl = fromRel inl+  inr = fromRel inr+  new = fromRel new+  jam = fromRel jam+  Mat f ▿ Mat g = Mat (FunctorProd f g)+   type Mat3x3 s = SqMat V3 s type Mat2x2 s = SqMat V2 s @@ -174,57 +282,48 @@                                            (V3 b e h)                                            (V3 c f i)) --- | Vector scaling. If Module a (f a), then (*^) must be the same as (*<).-(*<) :: (Functor f, Multiplicative b) => b -> f b -> f b-s *< v = (s*) <$> v --(<+>) :: (Applicative f, Additive b) => f b -> f b -> f b-u <+> v = (+) <$> u <*> v---matVecMul :: forall s v w. (Ring s, Foldable v,Applicative v,Applicative w) => Mat s v w -> v s -> w s-matVecMul (Mat m) x = foldr (<+>) (pure zero) ((*<) <$> x <*> m) -- If GHC gets fixed: use VectorR constraint instead of Applicative, and add instead of foldr.--rotation2d :: (Group a,Floating a) => a -> Mat2x2 a+rotation2d :: Transcendental a => a -> Mat2x2 a rotation2d θ = transpose $ Mat $ V2 (V2 (cos θ) (-sin θ))                                     (V2 (sin θ)  (cos θ))  -- >>> rotation2d (pi/2) -- Mat {fromMat = V2' (V2' 6.123233995736766e-17 (-1.0)) (V2' 1.0 6.123233995736766e-17)} + crossProductMatrix :: Group a => V3 a -> Mat3x3 a crossProductMatrix (V3 a1 a2 a3) = Mat3x3 zero  (-a3) a2                                           a3    zero  (-a1)                                           (-a2) a1    zero --- | Tensor product-(⊗) :: (Applicative v, Applicative w, Multiplicative s)-    => w s -> v s -> Mat s w v-v1 ⊗ v2 = tensorWith (*) v2 v1--tensorWith :: (Applicative v, Applicative w)+outerWith :: (Applicative v, Applicative w)            => (s -> t -> u) -> w s -> v t -> Mat u v w-tensorWith f v1 v2 = matFlat (f <$> Flat (pure v1) <*> Flat (pure <$> v2))+outerWith f v1 v2 = matFlat (f <$> Flat (pure v1) <*> Flat (pure <$> v2)) -identity :: Traversable v => Ring s => Applicative v => SqMat v s-identity = tensorWith (\x y -> if x == y then one else zero) index index -diagonal :: Traversable v => Ring s => Applicative v => v s -> SqMat v s-diagonal v = tensorWith (\x (y,a) -> if x == y then a else zero) index ((,) <$> index <*> v)+-- | Outer product +outer :: (Applicative v, Applicative w, Multiplicative s)+    => Euclid w s -> Euclid v s -> Mat s (Euclid w) (Euclid v)+v1 `outer` v2 = outerWith (*) v2 v1 ++diagonal :: Eq (Rep v) => Representable v => Ring s => Applicative v => v s -> SqMat v s+diagonal v = outerWith (\x (y,a) -> if x == y then a else zero) (tabulate id) ((,) <$> (tabulate id) <*> v)+ -- | 3d rotation around given axis-rotation3d :: Ring a => Floating a => a -> V3 a -> Mat3x3 a-rotation3d θ u = cos θ *^ identity ++rotation3d :: Transcendental a => a -> V3 a -> Mat3x3 a+rotation3d θ u = cos θ *^ id +                  sin θ *^ crossProductMatrix u +-                 (1 - cos θ) *^ (u ⊗ u)+                 (1 - cos θ) *^ (u `outer` u) + -- | 3d rotation mapping the direction of 'from' to that of 'to'-rotationFromTo :: (Floating a, Module a a,Field a)+rotationFromTo :: forall a. (Algebraic a)                => V3 a -> V3 a -> Mat3x3 a-rotationFromTo from to = c *^ identity + s *^ crossProductMatrix v + (1-c) *^ (v ⊗ v)+rotationFromTo from to = c *^ id + s *^ crossProductMatrix v + (1-c) *^ (v `outer` v)   where y = to         x = from+        v :: V3 a         v = x × y -- axis of rotation         c = inner x y -- cos of angle         s = norm v -- sin of angle@@ -232,26 +331,53 @@ -- >>> let u = (V3 (1::Double) 0 0); v = (V3 0 1 1); in (rotationFromTo u v) `matVecMul` u -- Euclid {fromEuclid = VNext (VNext (VNext VZero 0.0) 1.4142135623730951) 1.4142135623730951} -transpose :: Applicative g => Traversable f => Mat a f g -> Mat a g f-transpose = Mat . sequenceA . fromMat+-- | Transposition as distribution+transpose :: Functor f => Distributive g => Mat a f g -> Mat a g f+transpose = Mat . distribute . fromMat -matMul :: (Traversable u, Ring s, Applicative w, Applicative v, Applicative u) => Mat s u w -> Mat s v u -> Mat s v w+instance Ring s => Dagger (Mat s) where+  dagger = transpose++matMul :: (Foldable u, Ring s, Applicative w, Applicative v, Applicative u) => Mat s u w -> Mat s v u -> Mat s v w matMul a (Mat b) = Mat (matVecMul a <$> b)  +(<+>) :: (Applicative f, Additive b) => f b -> f b -> f b+u <+> v = (+) <$> u <*> v++matVecMul :: forall s v w. (Ring s, Foldable v,Applicative v,Applicative w) => Mat s v w -> v s -> w s+matVecMul (Mat m) x = foldr (<+>) (pure zero) ((*<) <$> x <*> m)+ -- >>> let t1 = rotation2d (1::Double) in matMul (transpose t1) t1 -- Mat {fromMat = VNext (VNext VZero (VNext (VNext VZero 1.0) 0.0)) (VNext (VNext VZero 0.0) 1.0)} +instance (Arbitrary s, Arbitrary1 a, Arbitrary1 b) => Arbitrary (Mat s a b) where+  arbitrary = Mat <$> liftArbitrary arbitrary1+instance (TestEqual s, Arbitrary s, Arbitrary1 a, Arbitrary1 b,Show (a (b s)), VectorR b, VectorR a) => TestEqual (Mat s a b) where+  Mat m =.= Mat n = product (product <$> ( liftA2 (=.=) <$> m <*> n))  --- The group of Orthogonal matrices, using "Multiplicative" for respecting conventions a bit better-newtype OrthoMat v s = OrthoMat (SqMat v s) -instance (Ring s, Applicative v, Traversable v) => Multiplicative (OrthoMat v s) where-  one = OrthoMat id-  OrthoMat m * OrthoMat n = OrthoMat (m . n)--instance (Ring s, Applicative v, Traversable v) => Division (OrthoMat v s) where-  recip (OrthoMat m) = OrthoMat (transpose m)+prop_linear_with_functor_laws :: Property+prop_linear_with_functor_laws =+  laws_bicartesian @(Mat Int)+  (testableCat+     (\k -> forallType @(∘) @Id @(⊗) @One (\t -> k t+       \\ reprCon @VectorR t))+     (\tx ty k -> forallMorphism tx ty k+       \\ reprCon1Comp @Int showCompClosed tx ty+       \\ reprCon @Arbitrary1 tx+       \\ reprCon @Arbitrary1 ty)+     (\a b -> Dict+       \\ reprCon1Comp @Int showCompClosed a b+       \\ reprCon @Arbitrary1 a+       \\ reprCon @Arbitrary1 b+       \\ reprCon @VectorR a+       \\ reprCon @VectorR b)+     RPlus+     RZero)  +return []+runTests :: IO Bool+runTests = $quickCheckAll

@@ -0,0 +1,66 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Algebra.Morphism.Affine where++import Prelude (Eq(..), Ord(..), Functor(..), id,Bool(..),Show,otherwise)+import Algebra.Classes+import Algebra.Linear+import qualified Data.Map as M+import Data.Either+import Control.Applicative++import Algebra.Morphism.LinComb (LinComb(..))+import qualified Algebra.Morphism.LinComb as LC+++data Affine x c = Affine c (LinComb x c)+  deriving (Functor, Eq, Ord,Show)++instance Multiplicative c => Scalable c (Affine x c) where+  k *^ x = k *< x++instance (Ord x, AbelianAdditive c,DecidableZero c) => AbelianAdditive (Affine x c)+instance (Ord x, AbelianAdditive c,Group c,DecidableZero c) => Group (Affine x c) where+  negate = fmap negate+instance (Ord x, AbelianAdditive c,DecidableZero c) => Additive (Affine x c) where+  (Affine c1 xs1) + (Affine c2 xs2) = Affine (c1 + c2) (xs1 + xs2)+  zero = Affine zero zero++splitVar :: Ord x => Additive c => x -> Affine x c -> (c, Affine x c)+splitVar x (Affine c0 (LinComb m)) = (M.findWithDefault zero x m, Affine c0 (LinComb (M.delete x m)))++-- | @solve x f@ solves the equation @f == 0@ for x.+-- Let f = k x + e.  If k == 0, return Left e. Otherwise, x and return Right -e/k. (The value of x)+solve :: (Ord scalar, Eq scalar, Field scalar, Ord x,DecidableZero scalar)+      => x -> Affine x scalar -> Either (Affine x scalar) (Bool,Affine x scalar)+solve x f = if k == zero then Left e else Right (k>zero,recip k *^ negate e) +  where (k,e) = splitVar x f++-- | Constant affine expression+constant :: (AbelianAdditive c, DecidableZero c) => Ord x => c -> Affine x c+constant c = Affine c zero++isConstant :: Eq c => Ord x => DecidableZero c => Affine x c -> Either x c+isConstant (Affine k x) = case LC.toList x of+  [] -> Right k+  ((v,_):_) -> Left v++var :: Multiplicative c => Additive c => v -> Affine v c+var x = Affine zero (LC.var x)++eval :: forall x c v. (Additive x, Scalable x x) => (c -> x) -> (v -> x) -> Affine v c -> x+eval fc fv (Affine c p) = fc c + LC.eval fc fv p++subst :: (Ord x, AbelianAdditive c, DecidableZero c, Multiplicative c) => (v -> Affine x c) -> Affine v c -> Affine x c+subst f (Affine c p) = constant c + LC.eval id f p ++mapVars :: Ord x => (v -> x) -> Affine v c -> Affine x c+mapVars f (Affine k e) = Affine k (LC.mapVars f e)++traverseVars :: Ord x => Applicative f => (v -> f x) -> Affine v c -> f (Affine x c)+traverseVars f (Affine k e) = Affine k <$> LC.traverseVars f e

@@ -0,0 +1,52 @@+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses, ConstraintKinds, FlexibleContexts, FlexibleInstances, DeriveGeneric #-}++module Algebra.Morphism.Exponential where++import Prelude (Show,Eq,Ord,Integer,Functor,Foldable)+import Data.Traversable+import Algebra.Classes++newtype Exp a = Exp a deriving (Show,Eq,Ord,Foldable,Traversable,Functor)++fromExp :: Exp a -> a+fromExp (Exp x) = x++instance Additive a => Multiplicative (Exp a) where+  Exp a * Exp b = Exp (a + b)+  one = Exp zero+  Exp a ^+ n = Exp (times n a)++instance Group a => Division (Exp a) where+  recip (Exp a) = Exp (negate a)+  Exp a / Exp b = Exp (a - b)++instance Field a => Roots (Exp a) where+  root n (Exp x) = Exp (x / fromInteger n)+++newtype Log a = Log a deriving (Show,Eq,Ord)++fromLog :: Log a -> a+fromLog (Log x) = x++instance Multiplicative a => Additive (Log a) where+  Log a + Log b = Log (a * b)+  zero = Log one+  times n (Log a) = Log (a ^+ n)++instance Multiplicative a => Scalable Integer (Log a) where+  n *^ Log x = Log (x ^+ n)+  +instance Division a => Group (Log a) where+  negate (Log a) = Log (recip a)+  Log a - Log b = Log (a / b)++-- instance Roots a => Field (Log a) where+-- fromRational x = Log (root (denominator x) (fromInteger (numerator x)))+

@@ -0,0 +1,86 @@+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Algebra.Morphism.LinComb where++import Prelude hiding (Num(..), sum)+-- import Data.List (intercalate,and,filter)+import Algebra.Classes+import qualified Data.Map as M+-- import Data.Function (on)+-- import Data.Monoid+-- import Control.Applicative+-- import Data.Traversable++-- | Normalised linear combinations as maps from variables to+-- coefficients (zero coefficient never present in the map)+newtype LinComb x c = LinComb (M.Map x c)+  deriving (Functor,AbelianAdditive,Eq,Ord,Show,Traversable,Foldable)+deriving instance {-# Overlappable #-} Scalable s a => Scalable s (LinComb k a)++fromLinComb :: LinComb x c -> M.Map x c+fromLinComb (LinComb x) = x+eval :: forall d x c v. Scalable d x => Additive x => (c -> d) -> (v -> x) -> LinComb v c -> x+eval fc fv p = sum [ fc c *^ fv v | (v, c) <- toList p ]++normalise :: DecidableZero c => LinComb x c -> LinComb x c+normalise (LinComb x) = LinComb (M.filter (not . isZero) x)++instance (AbelianAdditive c,DecidableZero c,Ord e) => Additive (LinComb e c) where+  zero = LinComb zero+  LinComb x + LinComb y = normalise (LinComb (x+y))++instance (AbelianAdditive c,Group c,DecidableZero c,Ord e) => Group (LinComb e c) where+  negate = fmap negate+  LinComb x - LinComb y = normalise (LinComb (x-y))++-- Alternative instances for non-normalised version:+-- instance (Eq e, Eq c, Additive c) => Eq (LinComb e c) where+--    (==) = (==) `on` toList++-- instance (Ord e, Ord c, Additive c) => Ord (LinComb e c) where+--    compare = compare `on` toList++toList :: LinComb k a -> [(k, a)]+toList = {- filter ((/= zero) . snd)  no need to filter zeros because normalised -} M.assocs . fromLinComb ++var :: Multiplicative c => x -> LinComb x c+var x = LinComb (M.singleton x one)++-- | Convert from list without testing coefficients+unsafeFromList :: Ord v => [(v,c)] -> LinComb v c+unsafeFromList = LinComb . M.fromList++fromList :: DecidableZero c => Additive c => Ord v => [(v,c)] -> LinComb v c+fromList = normalise . LinComb . M.fromListWith (+)++instance (AbelianAdditive c, Eq c, DecidableZero c, Ord e) => DecidableZero (LinComb e c) where+  isZero (LinComb p) = p == M.empty  ++-- instance (Show c, Show e, Eq c, Multiplicative c) => Show (LinComb e c) where+--   show (LinComb xs) = intercalate "+" ([(if coef /= one then show coef else mempty) <> show m  | (m,coef) <- M.toList xs])++-- | Substitution by evaluation+subst :: DecidableZero c => AbelianAdditive c => Scalable c c => Ord v => (x -> LinComb v c) -> LinComb x c -> LinComb v c+subst f = eval id f++-- | transform variables. coefficients are not touched+mapVars :: Ord x => (t -> x) -> LinComb t c -> LinComb x c+mapVars f (LinComb m) = unsafeFromList [(f x, e) | (x,e) <- M.assocs m]++-- | Multiplies elements, assuming multiplication is monotonous.+mulVarsMonotonic :: Multiplicative x => x -> LinComb x c -> LinComb x c+mulVarsMonotonic x (LinComb m) = LinComb (M.mapKeysMonotonic (x *) m) ++-- | transform variables with effect. coefficients are not touched+traverseVars :: Applicative f => Ord x => (v -> f x) -> LinComb v c -> f (LinComb x c)+traverseVars f e = unsafeFromList <$> traverse (\(x,c) -> (,c) <$> f x) (toList e)++-- | transform variables and coefficients with effect.+bitraverse :: Applicative f => Ord x => (v -> f x) -> (c -> f d) -> LinComb v c -> f (LinComb x d)+bitraverse f g e = unsafeFromList <$> traverse (\(x,c) -> (,) <$> f x <*> g c) (toList e)

@@ -0,0 +1,55 @@+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Algebra.Morphism.Pointwise where++import Prelude (Functor(..), (.))+import Control.Applicative+import Algebra.Classes++-- | Function type where all functions are run pointwise.+newtype Pointwise x a = Pointwise (x -> a) deriving (Functor, Additive, Group, AbelianAdditive, Applicative)++fromPointwise :: Pointwise x a -> x -> a+fromPointwise (Pointwise x) = x++instance Multiplicative a => Multiplicative (Pointwise x a) where+  one  = pure one+  (*) = liftA2 (*)++instance Division a => Division (Pointwise x a) where+  recip  = fmap recip+  (/) = liftA2 (/)++instance Roots a => Roots (Pointwise x a) where+  root n  = fmap (root n)++instance Transcendental a => Transcendental (Pointwise x a) where+  pi = pure pi+  log = fmap log+  sin = fmap sin+  cos = fmap cos+  asin = fmap asin+  acos = fmap acos+  atan = fmap atan+  sinh = fmap sinh+  cosh = fmap cosh+  asinh = fmap asinh+  acosh = fmap acosh+  atanh = fmap atanh+  exp = fmap exp++instance Multiplicative a => Scalable (Pointwise x a) (Pointwise x a) where+  (*^) = (*)++instance Ring a => Ring (Pointwise x a) where+  fromInteger = pure . fromInteger++instance Field a => Field (Pointwise x a) where+  fromRational = pure . fromRational+

@@ -0,0 +1,126 @@+{-# LANGUAGE MultiParamTypeClasses #-}+module Algebra.Morphism.Ratio where++import Algebra.Classes+import Prelude (Ord(..), Eq(..),Integer,Show(..), error, otherwise, (.), Int, ($))+import Text.Show (showParen, showString)+import qualified Data.Ratio+------------------------------------------------------------------------+-- Divide by zero and arithmetic overflow+------------------------------------------------------------------------++-- We put them here because they are needed relatively early+-- in the libraries before the Exception type has been defined yet.++{-# NOINLINE divZeroError #-}+divZeroError :: a+divZeroError = error "division by zero"++{-# NOINLINE ratioZeroDenominatorError #-}+ratioZeroDenominatorError :: a+ratioZeroDenominatorError = error "ratioZeroDenomException"++{-# NOINLINE overflowError #-}+overflowError :: a+overflowError = error "overflowException"++{-# NOINLINE underflowError #-}+underflowError :: a+underflowError = error "underflowException"+++data  Ratio a = !a :% !a  deriving Eq -- ^ @since 2.01++type Rational = Ratio Integer++--------------------------------------------------------------+-- Instances for @Ratio@+--------------------------------------------------------------++-- | @since 2.0.1+instance  (Integral a)  => Ord (Ratio a)  where+    {-# SPECIALIZE instance Ord Rational #-}+    (x:%y) <= (x':%y')  =  x * y' <= x' * y+    (x:%y) <  (x':%y')  =  x * y' <  x' * y++-- | @since 2.0.1+instance  EuclideanDomain a  => Additive (Ratio a)  where+  zero = zero :% one+  (x:%y) + (x':%y')   =  reduce (x*y' + x'*y) (y*y')++instance EuclideanDomain a => Multiplicative (Ratio a) where+  one = one :% one+  (x:%y) * (x':%y')   =  reduce (x * x') (y * y')++instance EuclideanDomain a => Group (Ratio a) where+    (x:%y) - (x':%y')   =  reduce (x*y' - x'*y) (y*y')+    negate (x:%y)       =  (negate x) :% y++    -- abs (x:%y)          =  abs x :% y+    -- signum (x:%_)       =  signum x :% 1+    -- fromInteger x       =  fromInteger x :% 1++instance EuclideanDomain a => AbelianAdditive (Ratio a)+instance EuclideanDomain a => Ring (Ratio a)+instance EuclideanDomain a => Scalable (Ratio a) (Ratio a) where+  (*^) = (*)+  +-- | @since 2.0.1+instance  (EuclideanDomain a)  => Division (Ratio a)  where+    {-# SPECIALIZE instance Division Rational #-}+    (x:%y) / (x':%y')   =  (x*y') % (y*x')+    -- recip (x:%y)+    --     | isZero x =  ratioZeroDenominatorError+    --     | x < 0         = negate y :% negate x+    --     | otherwise     = y :% x++instance EuclideanDomain a => Field (Ratio a) where+    fromRational x =  fromInteger (Data.Ratio.numerator x) % fromInteger (Data.Ratio.denominator x)++-- | @since 2.0.1+-- instance  (Integral a)  => Real (Ratio a)  where+--     {-# SPECIALIZE instance Real Rational #-}+--     toRational (x:%y)   =  toInteger x :% toInteger y++-- -- | @since 2.0.1+-- instance  (Integral a)  => RealFrac (Ratio a)  where+--     {-# SPECIALIZE instance RealFrac Rational #-}+--     properFraction (x:%y) = (fromInteger (toInteger q), r:%y)+--                           where (q,r) = quotRem x y+--     round r =+--       let+--         (n, f) = properFraction r+--         x = if r < 0 then -1 else 1+--       in+--         case (compare (abs f) 0.5, odd n) of+--           (LT, _) -> n+--           (EQ, False) -> n+--           (EQ, True) -> n + x+--           (GT, _) -> n + x++-- | @since 2.0.1+instance  (Show a)  => Show (Ratio a)  where+    {-# SPECIALIZE instance Show Rational #-}+    showsPrec p (x:%y)  =  showParen (p > ratioPrec) $+                           showsPrec ratioPrec1 x .+                           showString " % " .+                           showsPrec ratioPrec1 y++++-- | 'reduce' is a subsidiary function used only in this module.+-- It normalises a ratio by dividing both numerator and denominator by+-- their greatest common divisor.+reduce ::  (EuclideanDomain a) => a -> a -> Ratio a+{-# SPECIALISE reduce :: Integer -> Integer -> Rational #-}+reduce x y | isZero y = ratioZeroDenominatorError+           | otherwise = (x `quot` d) :% (y `quot` d)+             where d = gcd x y++(%) :: EuclideanDomain a => a -> a -> Ratio a+x % y =  reduce (x * sign) a+  where (a,sign) = normalize y++ratioPrec, ratioPrec1 :: Int+ratioPrec  = 7  -- Precedence of ':%' constructor+ratioPrec1 = ratioPrec + 1

@@ -0,0 +1,219 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE EmptyDataDeriving #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeOperators #-}++module Algebra.Types where++import Data.Kind+import Data.Constraint (Dict(..))+import Data.Functor.Rep+import Data.Distributive+import GHC.Generics hiding (Rep)+import Test.QuickCheck hiding (tabulate,collect)++class SumKind k where+  data (a::k) ⊕ (b::k) :: k+  data Zero :: k++class ProdKind k where+  data (a::k) ⊗ (b::k) :: k+  data One :: k++class DualKind k where+  data Dual (a::k) :: k++data Repr x i t o :: k -> Type where+  RPlus :: Repr x i t o  a -> Repr x i t o b -> Repr x i t o (a `t` b)+  RTimes :: Repr x i t o a -> Repr x i t o b -> Repr x i t o (a `x` b)+  ROne :: Repr x i t o i+  RZero :: Repr x i t o o++instance Show (Repr x i t o a) where+  showsPrec d = \case+    RZero -> showString "0"+    ROne -> showString "1"+    RPlus x y -> showParen (d>=2) (showsPrec 2 x . showString " + " . showsPrec 2 y)+    RTimes x y -> showParen (d>=3) (showsPrec 3 x . showString " × " . showsPrec 3 y)++type CRepr = Repr (∘) Id (⊗) One+type MRepr = Repr (⊗) One (⊕) Zero++instance SumKind Type where+  data x ⊕ y = Inj1 x | Inj2 y deriving (Eq,Ord,Show,Generic)+  data Zero deriving (Eq,Ord,Show)++instance ProdKind Type where+  data x ⊗ y = Pair {π1 :: x, π2 :: y} deriving (Eq,Ord,Show,Generic)+  data One = Unit deriving (Eq,Ord,Enum,Bounded,Show)++instance DualKind Type where+  data Dual x = DualType {fromDualType :: x} deriving (Eq,Ord,Show,Generic)++instance Finite a => Finite (Dual a) where+instance Finite a => Bounded (Dual a) where+  minBound = DualType minBound+  maxBound = DualType maxBound+instance Finite a => Enum (Dual a) where+  toEnum = DualType . toEnum+  fromEnum = fromEnum . fromDualType++inhabitants :: Finite a => [a]+inhabitants = [minBound..maxBound]++class (Enum a, Bounded a, Eq a, Ord a) => Finite a where+  typeSize :: Int+  typeSize = fromEnum (maxBound @a) - fromEnum (minBound @a) + 1+  finiteFstsnd :: forall α β. (a ~ (α⊗β)) => Dict (Finite α, Finite β)+  finiteFstsnd = error "finiteFstsnd: not a product type"+  finiteLeftRight :: forall α β. (a ~ (α⊕β)) => Dict (Finite α, Finite β)+  finiteLeftRight = error "finiteFstsnd: not a sum type"+++fromZero :: forall a. Finite a => Int -> a+fromZero i = toEnum (i + fromEnum (minBound @a))++instance (Bounded x, Bounded y) => Bounded (x⊕y) where+  minBound = Inj1 minBound+  maxBound = Inj2 maxBound++instance (Finite x, Finite y) => Enum (x⊕y) where+  toEnum i = if i < typeSize @x then Inj1 (toEnum i) else Inj2 (toEnum (i-typeSize @x))+  fromEnum = \case+     Inj1 x -> fromEnum x+     Inj2 x -> fromEnum x + typeSize @x++instance (Finite x, Finite y) => Finite (x⊕y) where+  finiteLeftRight = Dict+instance (Finite x, Finite y) => Enum (x⊗y) where+  toEnum k = Pair (toEnum i) (toEnum j)+    where (j,i) = k `divMod` typeSize @x+  fromEnum (Pair x y) = fromEnum x + fromEnum y * (typeSize @x)+instance (Finite x, Finite y) => Finite (x⊗y) where+  finiteFstsnd = Dict+instance Finite Bool+instance Finite One++instance (Bounded x, Bounded y) => Bounded (x⊗y) where+  minBound = minBound `Pair` minBound+  maxBound = maxBound `Pair` maxBound+  +  +instance Enum Zero where+  toEnum = error "toEnum: Zero"+  fromEnum = \case+instance Bounded Zero where+  minBound = error "minBound: Zero"+  maxBound = error "maxBound: Zero"+instance Finite Zero where+  typeSize = 0++instance CoArbitrary One where+  coarbitrary _ = id+instance CoArbitrary Zero where+  coarbitrary _ = id+instance (CoArbitrary f, CoArbitrary g) => CoArbitrary (f ⊕ g) where+instance (CoArbitrary f, CoArbitrary g) => CoArbitrary (f ⊗ g) where++newtype (f ∘ g) x = Comp {fromComp :: (f (g x))} deriving (Foldable, Generic1, Eq)+deriving instance (Functor f, Functor g) => Functor (f ∘ g)+deriving instance (Traversable f, Traversable g) => Traversable (f ∘ g)+newtype Id x = Id {fromId :: x} deriving (Foldable, Traversable, Functor, Generic1, Eq)++instance SumKind (Type -> Type) where+  data (f ⊕ g) x = FunctorInj1 (f x) | FunctorInj2 (g x) deriving (Foldable, Traversable, Functor,Generic1,Eq)+  data Zero x deriving (Foldable, Traversable, Functor,Generic1,Eq)++instance ProdKind (Type -> Type) where+  data (f ⊗ g) x = FunctorProd {prodFst :: f x, prodSnd :: g x} deriving (Foldable, Traversable, Functor,Generic1,Eq)+  data One x = FunctorOne deriving (Foldable, Traversable, Functor, Generic1, Eq)++instance DualKind (Type -> Type) where+  data Dual f x = FunctorDual {fromFunctorDual :: f x} deriving (Foldable, Traversable, Functor, Generic1, Show, Eq)++deriving instance Show (One (x :: Type))+deriving instance Show x => Show (Id (x :: Type))+deriving instance (Show (a x), Show (b x)) => Show ((a⊗b) (x :: Type))+deriving instance (Show (a (b x))) => Show ((a∘b) (x :: Type))++data CompClosed (con :: Type -> Constraint) = CompClosed {+  zero1Closed :: forall (x :: Type). Dict (con (One x)),+  plus1Closed :: forall a b (x :: Type). (con (a x), con (b x)) => Dict (con ((a⊗b) x)),+  one1Closed :: forall (x :: Type). con x => Dict (con (Id x)),+  times1Closed :: forall (a :: Type -> Type) b (x :: Type). (con (a (b x))) => Dict (con ((a∘b) x))+                          }+++showCompClosed :: CompClosed Show+showCompClosed = CompClosed Dict Dict Dict Dict++instance Distributive One where+  distribute _ = FunctorOne+instance Distributive Id where+  distribute = Id . fmap fromId+instance Representable One where+  type Rep One = Zero+  index FunctorOne = \case+  tabulate _ = FunctorOne+instance Representable Id where+  type Rep Id = One+  index (Id x) _ = x+  tabulate f = Id (f Unit)+instance (Distributive v, Distributive w) => Distributive (v ∘ w) where+  distribute = Comp . fmap distribute . distribute . fmap fromComp+instance (Representable v, Representable w) => Representable (v ∘ w) where+  type Rep (v ∘ w) = Rep v ⊗ Rep w+  index (Comp f) (i `Pair` j) = (f `index` i) `index` j+  tabulate f = Comp (tabulate (\i -> tabulate (\j -> f (i `Pair` j))))+instance (Distributive v, Distributive w) => Distributive (v ⊗ w) where+  collect f x = FunctorProd (collect (prodFst . f) x) (collect (prodSnd . f) x)+instance (Representable v, Representable w) => Representable (v ⊗ w) where+  type Rep (v ⊗ w) = Rep v ⊕ Rep w+  index (FunctorProd x y) = \case+    Inj1 i -> index x i+    Inj2 i -> index y i+  tabulate f = FunctorProd (tabulate (f . Inj1)) (tabulate (f . Inj2))++instance Arbitrary1 Id where+  liftArbitrary = fmap Id+instance Arbitrary1 One where+  liftArbitrary _ = pure FunctorOne+instance (Arbitrary1 f, Arbitrary1 g) => Arbitrary1 (f ⊗ g) where+  liftArbitrary g = FunctorProd <$> liftArbitrary g <*> liftArbitrary g+instance (Arbitrary1 f, Arbitrary1 g) => Arbitrary1 (f ∘ g) where+  liftArbitrary g = Comp <$> liftArbitrary (liftArbitrary g)++instance Applicative Id where+  pure = Id+  Id f <*> Id x = Id (f x)+  +instance Applicative One where+  pure _ = FunctorOne+  _ <*> _ = FunctorOne++instance (Applicative f, Applicative g) => Applicative (f ∘ g) where+  Comp f <*> Comp x = Comp ((fmap (<*>) f) <*> x)+  pure x = Comp (pure (pure x))++instance (Applicative f, Applicative g) => Applicative (f ⊗ g) where+  FunctorProd f g <*> FunctorProd x y = FunctorProd (f <*> x) (g <*> y)+  pure x = FunctorProd (pure x) (pure x)++instance (Applicative f) => Applicative (Dual f) where+  FunctorDual f <*> FunctorDual x = FunctorDual (f <*> x)+  pure x = FunctorDual (pure x)+

@@ -1,5 +1,5 @@ name:           gasp-version:        1.3.0.0+version:        1.4.0.0 category:       Algebra synopsis:       A framework of algebraic classes description:@@ -9,7 +9,7 @@ author:         Jean-Philippe Bernardy maintainer:     jeanphilippe.bernardy@gmail.com Cabal-Version:  1.12-tested-with:    GHC==8.4.1+tested-with:    GHC==9.2.1 build-type:     Simple source-repository head   type: git@@ -22,10 +22,34 @@   build-depends: containers   build-depends: binary   build-depends: mtl+  build-depends: constraints+  build-depends: distributive, adjunctions+    -- for representable functors+       build-depends: QuickCheck    exposed-modules:++               Algebra.Classes-       Algebra.Linear-       Algebra.Category+       Algebra.Types+       +       Algebra.Morphism.Affine+       Algebra.Morphism.Exponential+       Algebra.Morphism.LinComb+       Algebra.Morphism.Ratio+       Algebra.Morphism.Pointwise +       Algebra.Category+       Algebra.Category.Laws+       Algebra.Category.Objects+                  +       Algebra.Category.Relation+       Algebra.Category.Endo+       Algebra.Category.Op+       Algebra.Category.NatTrans+       Algebra.Category.BlockMatrix+                  +       Algebra.CategoryRecords+    +       Algebra.Linear