diff --git a/Algebra/Category.hs b/Algebra/Category.hs --- a/Algebra/Category.hs +++ b/Algebra/Category.hs @@ -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 + diff --git a/Algebra/Category/BlockMatrix.hs b/Algebra/Category/BlockMatrix.hs new file mode 100644 --- /dev/null +++ b/Algebra/Category/BlockMatrix.hs @@ -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) diff --git a/Algebra/Category/Endo.hs b/Algebra/Category/Endo.hs new file mode 100644 --- /dev/null +++ b/Algebra/Category/Endo.hs @@ -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) + + diff --git a/Algebra/Category/Laws.hs b/Algebra/Category/Laws.hs new file mode 100644 --- /dev/null +++ b/Algebra/Category/Laws.hs @@ -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)] diff --git a/Algebra/Category/NatTrans.hs b/Algebra/Category/NatTrans.hs new file mode 100644 --- /dev/null +++ b/Algebra/Category/NatTrans.hs @@ -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)) + diff --git a/Algebra/Category/Objects.hs b/Algebra/Category/Objects.hs new file mode 100644 --- /dev/null +++ b/Algebra/Category/Objects.hs @@ -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) + diff --git a/Algebra/Category/Op.hs b/Algebra/Category/Op.hs new file mode 100644 --- /dev/null +++ b/Algebra/Category/Op.hs @@ -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 + + diff --git a/Algebra/Category/Relation.hs b/Algebra/Category/Relation.hs new file mode 100644 --- /dev/null +++ b/Algebra/Category/Relation.hs @@ -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 + diff --git a/Algebra/CategoryRecords.hs b/Algebra/CategoryRecords.hs new file mode 100644 --- /dev/null +++ b/Algebra/CategoryRecords.hs @@ -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) + + } + diff --git a/Algebra/Classes.hs b/Algebra/Classes.hs --- a/Algebra/Classes.hs +++ b/Algebra/Classes.hs @@ -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) diff --git a/Algebra/Linear.hs b/Algebra/Linear.hs --- a/Algebra/Linear.hs +++ b/Algebra/Linear.hs @@ -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 diff --git a/Algebra/Morphism/Affine.hs b/Algebra/Morphism/Affine.hs new file mode 100644 --- /dev/null +++ b/Algebra/Morphism/Affine.hs @@ -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 diff --git a/Algebra/Morphism/Exponential.hs b/Algebra/Morphism/Exponential.hs new file mode 100644 --- /dev/null +++ b/Algebra/Morphism/Exponential.hs @@ -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))) + diff --git a/Algebra/Morphism/LinComb.hs b/Algebra/Morphism/LinComb.hs new file mode 100644 --- /dev/null +++ b/Algebra/Morphism/LinComb.hs @@ -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) diff --git a/Algebra/Morphism/Pointwise.hs b/Algebra/Morphism/Pointwise.hs new file mode 100644 --- /dev/null +++ b/Algebra/Morphism/Pointwise.hs @@ -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 + diff --git a/Algebra/Morphism/Ratio.hs b/Algebra/Morphism/Ratio.hs new file mode 100644 --- /dev/null +++ b/Algebra/Morphism/Ratio.hs @@ -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 diff --git a/Algebra/Types.hs b/Algebra/Types.hs new file mode 100644 --- /dev/null +++ b/Algebra/Types.hs @@ -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) + diff --git a/gasp.cabal b/gasp.cabal --- a/gasp.cabal +++ b/gasp.cabal @@ -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