{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RebindableSyntax #-}

module Algebra.Linear where

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
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
-- ... but this is missing the link with *^ for module.  We should be
-- 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 = [Char] -> Dict (VectorR f, VectorR g)
forall a. HasCallStack => [Char] -> a
error [Char]
"vectorSplit: not product type"
  vectorCut :: (v ~ (f ⊕ g)) => Dict (VectorR f, VectorR g)
  vectorCut = [Char] -> Dict (VectorR f, VectorR g)
forall a. HasCallStack => [Char] -> a
error [Char]
"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

type VZero x = Zero x

data VNext v a = VNext {forall (v :: * -> *) a. VNext v a -> v a
vnextInit :: !(v a), forall (v :: * -> *) a. VNext v a -> a
vnextLast :: !a} deriving ((forall a b. (a -> b) -> VNext v a -> VNext v b)
-> (forall a b. a -> VNext v b -> VNext v a) -> Functor (VNext v)
forall a b. a -> VNext v b -> VNext v a
forall a b. (a -> b) -> VNext v a -> VNext v b
forall (v :: * -> *) a b. Functor v => a -> VNext v b -> VNext v a
forall (v :: * -> *) a b.
Functor v =>
(a -> b) -> VNext v a -> VNext v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (v :: * -> *) a b.
Functor v =>
(a -> b) -> VNext v a -> VNext v b
fmap :: forall a b. (a -> b) -> VNext v a -> VNext v b
$c<$ :: forall (v :: * -> *) a b. Functor v => a -> VNext v b -> VNext v a
<$ :: forall a b. a -> VNext v b -> VNext v a
Functor,(forall m. Monoid m => VNext v m -> m)
-> (forall m a. Monoid m => (a -> m) -> VNext v a -> m)
-> (forall m a. Monoid m => (a -> m) -> VNext v a -> m)
-> (forall a b. (a -> b -> b) -> b -> VNext v a -> b)
-> (forall a b. (a -> b -> b) -> b -> VNext v a -> b)
-> (forall b a. (b -> a -> b) -> b -> VNext v a -> b)
-> (forall b a. (b -> a -> b) -> b -> VNext v a -> b)
-> (forall a. (a -> a -> a) -> VNext v a -> a)
-> (forall a. (a -> a -> a) -> VNext v a -> a)
-> (forall a. VNext v a -> [a])
-> (forall a. VNext v a -> Bool)
-> (forall a. VNext v a -> Int)
-> (forall a. Eq a => a -> VNext v a -> Bool)
-> (forall a. Ord a => VNext v a -> a)
-> (forall a. Ord a => VNext v a -> a)
-> (forall a. Num a => VNext v a -> a)
-> (forall a. Num a => VNext v a -> a)
-> Foldable (VNext v)
forall a. Eq a => a -> VNext v a -> Bool
forall a. Num a => VNext v a -> a
forall a. Ord a => VNext v a -> a
forall m. Monoid m => VNext v m -> m
forall a. VNext v a -> Bool
forall a. VNext v a -> Int
forall a. VNext v a -> [a]
forall a. (a -> a -> a) -> VNext v a -> a
forall m a. Monoid m => (a -> m) -> VNext v a -> m
forall b a. (b -> a -> b) -> b -> VNext v a -> b
forall a b. (a -> b -> b) -> b -> VNext v a -> b
forall (v :: * -> *) a.
(Foldable v, Eq a) =>
a -> VNext v a -> Bool
forall (v :: * -> *) a. (Foldable v, Num a) => VNext v a -> a
forall (v :: * -> *) a. (Foldable v, Ord a) => VNext v a -> a
forall (v :: * -> *) m. (Foldable v, Monoid m) => VNext v m -> m
forall (v :: * -> *) a. Foldable v => VNext v a -> Bool
forall (v :: * -> *) a. Foldable v => VNext v a -> Int
forall (v :: * -> *) a. Foldable v => VNext v a -> [a]
forall (v :: * -> *) a.
Foldable v =>
(a -> a -> a) -> VNext v a -> a
forall (v :: * -> *) m a.
(Foldable v, Monoid m) =>
(a -> m) -> VNext v a -> m
forall (v :: * -> *) b a.
Foldable v =>
(b -> a -> b) -> b -> VNext v a -> b
forall (v :: * -> *) a b.
Foldable v =>
(a -> b -> b) -> b -> VNext v a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (v :: * -> *) m. (Foldable v, Monoid m) => VNext v m -> m
fold :: forall m. Monoid m => VNext v m -> m
$cfoldMap :: forall (v :: * -> *) m a.
(Foldable v, Monoid m) =>
(a -> m) -> VNext v a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> VNext v a -> m
$cfoldMap' :: forall (v :: * -> *) m a.
(Foldable v, Monoid m) =>
(a -> m) -> VNext v a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> VNext v a -> m
$cfoldr :: forall (v :: * -> *) a b.
Foldable v =>
(a -> b -> b) -> b -> VNext v a -> b
foldr :: forall a b. (a -> b -> b) -> b -> VNext v a -> b
$cfoldr' :: forall (v :: * -> *) a b.
Foldable v =>
(a -> b -> b) -> b -> VNext v a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> VNext v a -> b
$cfoldl :: forall (v :: * -> *) b a.
Foldable v =>
(b -> a -> b) -> b -> VNext v a -> b
foldl :: forall b a. (b -> a -> b) -> b -> VNext v a -> b
$cfoldl' :: forall (v :: * -> *) b a.
Foldable v =>
(b -> a -> b) -> b -> VNext v a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> VNext v a -> b
$cfoldr1 :: forall (v :: * -> *) a.
Foldable v =>
(a -> a -> a) -> VNext v a -> a
foldr1 :: forall a. (a -> a -> a) -> VNext v a -> a
$cfoldl1 :: forall (v :: * -> *) a.
Foldable v =>
(a -> a -> a) -> VNext v a -> a
foldl1 :: forall a. (a -> a -> a) -> VNext v a -> a
$ctoList :: forall (v :: * -> *) a. Foldable v => VNext v a -> [a]
toList :: forall a. VNext v a -> [a]
$cnull :: forall (v :: * -> *) a. Foldable v => VNext v a -> Bool
null :: forall a. VNext v a -> Bool
$clength :: forall (v :: * -> *) a. Foldable v => VNext v a -> Int
length :: forall a. VNext v a -> Int
$celem :: forall (v :: * -> *) a.
(Foldable v, Eq a) =>
a -> VNext v a -> Bool
elem :: forall a. Eq a => a -> VNext v a -> Bool
$cmaximum :: forall (v :: * -> *) a. (Foldable v, Ord a) => VNext v a -> a
maximum :: forall a. Ord a => VNext v a -> a
$cminimum :: forall (v :: * -> *) a. (Foldable v, Ord a) => VNext v a -> a
minimum :: forall a. Ord a => VNext v a -> a
$csum :: forall (v :: * -> *) a. (Foldable v, Num a) => VNext v a -> a
sum :: forall a. Num a => VNext v a -> a
$cproduct :: forall (v :: * -> *) a. (Foldable v, Num a) => VNext v a -> a
product :: forall a. Num a => VNext v a -> a
Foldable,Functor (VNext v)
Foldable (VNext v)
(Functor (VNext v), Foldable (VNext v)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> VNext v a -> f (VNext v b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    VNext v (f a) -> f (VNext v a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> VNext v a -> m (VNext v b))
-> (forall (m :: * -> *) a.
    Monad m =>
    VNext v (m a) -> m (VNext v a))
-> Traversable (VNext v)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (v :: * -> *). Traversable v => Functor (VNext v)
forall (v :: * -> *). Traversable v => Foldable (VNext v)
forall (v :: * -> *) (m :: * -> *) a.
(Traversable v, Monad m) =>
VNext v (m a) -> m (VNext v a)
forall (v :: * -> *) (f :: * -> *) a.
(Traversable v, Applicative f) =>
VNext v (f a) -> f (VNext v a)
forall (v :: * -> *) (m :: * -> *) a b.
(Traversable v, Monad m) =>
(a -> m b) -> VNext v a -> m (VNext v b)
forall (v :: * -> *) (f :: * -> *) a b.
(Traversable v, Applicative f) =>
(a -> f b) -> VNext v a -> f (VNext v b)
forall (m :: * -> *) a. Monad m => VNext v (m a) -> m (VNext v a)
forall (f :: * -> *) a.
Applicative f =>
VNext v (f a) -> f (VNext v a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> VNext v a -> m (VNext v b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> VNext v a -> f (VNext v b)
$ctraverse :: forall (v :: * -> *) (f :: * -> *) a b.
(Traversable v, Applicative f) =>
(a -> f b) -> VNext v a -> f (VNext v b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> VNext v a -> f (VNext v b)
$csequenceA :: forall (v :: * -> *) (f :: * -> *) a.
(Traversable v, Applicative f) =>
VNext v (f a) -> f (VNext v a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
VNext v (f a) -> f (VNext v a)
$cmapM :: forall (v :: * -> *) (m :: * -> *) a b.
(Traversable v, Monad m) =>
(a -> m b) -> VNext v a -> m (VNext v b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> VNext v a -> m (VNext v b)
$csequence :: forall (v :: * -> *) (m :: * -> *) a.
(Traversable v, Monad m) =>
VNext v (m a) -> m (VNext v a)
sequence :: forall (m :: * -> *) a. Monad m => VNext v (m a) -> m (VNext v a)
Traversable,Int -> VNext v a -> ShowS
[VNext v a] -> ShowS
VNext v a -> [Char]
(Int -> VNext v a -> ShowS)
-> (VNext v a -> [Char])
-> ([VNext v a] -> ShowS)
-> Show (VNext v a)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall (v :: * -> *) a.
(Show a, Show (v a)) =>
Int -> VNext v a -> ShowS
forall (v :: * -> *) a.
(Show a, Show (v a)) =>
[VNext v a] -> ShowS
forall (v :: * -> *) a. (Show a, Show (v a)) => VNext v a -> [Char]
$cshowsPrec :: forall (v :: * -> *) a.
(Show a, Show (v a)) =>
Int -> VNext v a -> ShowS
showsPrec :: Int -> VNext v a -> ShowS
$cshow :: forall (v :: * -> *) a. (Show a, Show (v a)) => VNext v a -> [Char]
show :: VNext v a -> [Char]
$cshowList :: forall (v :: * -> *) a.
(Show a, Show (v a)) =>
[VNext v a] -> ShowS
showList :: [VNext v a] -> ShowS
Show,VNext v a -> VNext v a -> Bool
(VNext v a -> VNext v a -> Bool)
-> (VNext v a -> VNext v a -> Bool) -> Eq (VNext v a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (v :: * -> *) a.
(Eq a, Eq (v a)) =>
VNext v a -> VNext v a -> Bool
$c== :: forall (v :: * -> *) a.
(Eq a, Eq (v a)) =>
VNext v a -> VNext v a -> Bool
== :: VNext v a -> VNext v a -> Bool
$c/= :: forall (v :: * -> *) a.
(Eq a, Eq (v a)) =>
VNext v a -> VNext v a -> Bool
/= :: VNext v a -> VNext v a -> Bool
Eq,Eq (VNext v a)
Eq (VNext v a) =>
(VNext v a -> VNext v a -> Ordering)
-> (VNext v a -> VNext v a -> Bool)
-> (VNext v a -> VNext v a -> Bool)
-> (VNext v a -> VNext v a -> Bool)
-> (VNext v a -> VNext v a -> Bool)
-> (VNext v a -> VNext v a -> VNext v a)
-> (VNext v a -> VNext v a -> VNext v a)
-> Ord (VNext v a)
VNext v a -> VNext v a -> Bool
VNext v a -> VNext v a -> Ordering
VNext v a -> VNext v a -> VNext v a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (v :: * -> *) a. (Ord a, Ord (v a)) => Eq (VNext v a)
forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> Bool
forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> Ordering
forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> VNext v a
$ccompare :: forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> Ordering
compare :: VNext v a -> VNext v a -> Ordering
$c< :: forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> Bool
< :: VNext v a -> VNext v a -> Bool
$c<= :: forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> Bool
<= :: VNext v a -> VNext v a -> Bool
$c> :: forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> Bool
> :: VNext v a -> VNext v a -> Bool
$c>= :: forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> Bool
>= :: VNext v a -> VNext v a -> Bool
$cmax :: forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> VNext v a
max :: VNext v a -> VNext v a -> VNext v a
$cmin :: forall (v :: * -> *) a.
(Ord a, Ord (v a)) =>
VNext v a -> VNext v a -> VNext v a
min :: VNext v a -> VNext v a -> VNext v a
Ord)

instance Distributive v => Distributive (VNext v) where
  collect :: forall (f :: * -> *) a b.
Functor f =>
(a -> VNext v b) -> f a -> VNext v (f b)
collect a -> VNext v b
f f a
x = v (f b) -> f b -> VNext v (f b)
forall (v :: * -> *) a. v a -> a -> VNext v a
VNext ((a -> v b) -> f a -> v (f b)
forall (g :: * -> *) (f :: * -> *) a b.
(Distributive g, Functor f) =>
(a -> g b) -> f a -> g (f b)
forall (f :: * -> *) a b. Functor f => (a -> v b) -> f a -> v (f b)
collect (VNext v b -> v b
forall (v :: * -> *) a. VNext v a -> v a
vnextInit (VNext v b -> v b) -> (a -> VNext v b) -> a -> v b
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. a -> VNext v b
f) f a
x) (VNext v b -> b
forall (v :: * -> *) a. VNext v a -> a
vnextLast (VNext v b -> b) -> (a -> VNext v b) -> a -> b
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. a -> VNext v b
f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
x)
instance Representable a => Representable (VNext a) where
  type Rep (VNext a) = One ⊕ (Rep a)
  index :: forall a. VNext a a -> Rep (VNext a) -> a
index (VNext a a
xs a
x) = \case
    Inj1 One
_ -> a
x
    Inj2 Rep a
i -> a a -> Rep a -> a
forall a. a a -> Rep a -> a
forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
index a a
xs Rep a
i
  tabulate :: forall a. (Rep (VNext a) -> a) -> VNext a a
tabulate Rep (VNext a) -> a
f = a a -> a -> VNext a a
forall (v :: * -> *) a. v a -> a -> VNext v a
VNext ((Rep a -> a) -> a a
forall a. (Rep a -> a) -> a a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate (Rep (VNext a) -> a
(One ⊕ Rep a) -> a
f ((One ⊕ Rep a) -> a) -> (Rep a -> One ⊕ Rep a) -> Rep a -> a
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. Rep a -> One ⊕ Rep a
forall x y. y -> x ⊕ y
Inj2)) (Rep (VNext a) -> a
f (One -> One ⊕ Rep a
forall x y. x -> x ⊕ y
Inj1 One
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 :: forall a. One a -> V One a
reifyVec One a
R:OneFUNx a
FunctorOne = V One a
forall a. V One a
V0

instance IsVec f => IsVec (VNext f) where
  reifyVec :: forall a. VNext f a -> V (VNext f) a
reifyVec (VNext f a
xs a
x) = f a -> V f a
forall a. f a -> V f a
forall (f :: * -> *) a. IsVec f => f a -> V f a
reifyVec f a
xs V f a -> a -> V (VNext f) a
forall (f :: * -> *) a. V f a -> a -> V (VNext f) a
:/ a
x

fromV :: V f a -> f a
fromV :: forall (f :: * -> *) a. V f a -> f a
fromV V f a
V0 = f a
One a
forall x. One x
FunctorOne
fromV (V f a
xs :/ a
x) = f a -> a -> VNext f a
forall (v :: * -> *) a. v a -> a -> VNext v a
VNext (V f a -> f a
forall (f :: * -> *) a. V f a -> f a
fromV V f a
xs) a
x

instance IsVec f => Applicative (V f) where
  pure :: forall a. a -> V f a
pure a
x = f a -> V f a
forall a. f a -> V f a
forall (f :: * -> *) a. IsVec f => f a -> V f a
reifyVec (a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
  V f (a -> b)
fs <*> :: forall a b. V f (a -> b) -> V f a -> V f b
<*> V f a
xs = f b -> V f b
forall a. f a -> V f a
forall (f :: * -> *) a. IsVec f => f a -> V f a
reifyVec (V f (a -> b) -> f (a -> b)
forall (f :: * -> *) a. V f a -> f a
fromV V f (a -> b)
fs f (a -> b) -> f a -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> V f a -> f a
forall (f :: * -> *) a. V f a -> f a
fromV V f a
xs)

instance Applicative v => Applicative (VNext v) where
  pure :: forall a. a -> VNext v a
pure a
x = v a -> a -> VNext v a
forall (v :: * -> *) a. v a -> a -> VNext v a
VNext (a -> v a
forall a. a -> v a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x) a
x
  VNext v (a -> b)
fs a -> b
f <*> :: forall a b. VNext v (a -> b) -> VNext v a -> VNext v b
<*> VNext v a
xs a
x = v b -> b -> VNext v b
forall (v :: * -> *) a. v a -> a -> VNext v a
VNext (v (a -> b)
fs v (a -> b) -> v a -> v b
forall a b. v (a -> b) -> v a -> v b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> v a
xs) (a -> b
f a
x)


type V1' = VNext One
type V2' = VNext V1'
type V3' = VNext V2'

pattern V1' :: a -> V1' a
pattern $mV1' :: forall {r} {a}. V1' a -> (a -> r) -> ((# #) -> r) -> r
$bV1' :: forall a. a -> V1' a
V1' x = VNext FunctorOne x
pattern V2' :: forall a. a -> a -> V2' a
pattern $mV2' :: forall {r} {a}. V2' a -> (a -> a -> r) -> ((# #) -> r) -> r
$bV2' :: forall a. a -> a -> V2' a
V2' x y = VNext (V1' x) y
pattern V3' :: forall a. a -> a -> a -> V3' a
pattern $mV3' :: forall {r} {a}. V3' a -> (a -> a -> a -> r) -> ((# #) -> r) -> r
$bV3' :: forall a. a -> a -> a -> V3' a
V3' x y z = VNext (V2' x y) z

--------------------------------------------
-- Euclidean spaces with a (inner product)

-- | Make a Euclidean vector out of a traversable functor. (The p)
newtype Euclid f a = Euclid {forall {k} (f :: k -> *) (a :: k). Euclid f a -> f a
fromEuclid :: f a}
  deriving ((forall a b. (a -> b) -> Euclid f a -> Euclid f b)
-> (forall a b. a -> Euclid f b -> Euclid f a)
-> Functor (Euclid f)
forall a b. a -> Euclid f b -> Euclid f a
forall a b. (a -> b) -> Euclid f a -> Euclid f b
forall (f :: * -> *) a b.
Functor f =>
a -> Euclid f b -> Euclid f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Euclid f a -> Euclid f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Euclid f a -> Euclid f b
fmap :: forall a b. (a -> b) -> Euclid f a -> Euclid f b
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Euclid f b -> Euclid f a
<$ :: forall a b. a -> Euclid f b -> Euclid f a
Functor,(forall m. Monoid m => Euclid f m -> m)
-> (forall m a. Monoid m => (a -> m) -> Euclid f a -> m)
-> (forall m a. Monoid m => (a -> m) -> Euclid f a -> m)
-> (forall a b. (a -> b -> b) -> b -> Euclid f a -> b)
-> (forall a b. (a -> b -> b) -> b -> Euclid f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Euclid f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Euclid f a -> b)
-> (forall a. (a -> a -> a) -> Euclid f a -> a)
-> (forall a. (a -> a -> a) -> Euclid f a -> a)
-> (forall a. Euclid f a -> [a])
-> (forall a. Euclid f a -> Bool)
-> (forall a. Euclid f a -> Int)
-> (forall a. Eq a => a -> Euclid f a -> Bool)
-> (forall a. Ord a => Euclid f a -> a)
-> (forall a. Ord a => Euclid f a -> a)
-> (forall a. Num a => Euclid f a -> a)
-> (forall a. Num a => Euclid f a -> a)
-> Foldable (Euclid f)
forall a. Eq a => a -> Euclid f a -> Bool
forall a. Num a => Euclid f a -> a
forall a. Ord a => Euclid f a -> a
forall m. Monoid m => Euclid f m -> m
forall a. Euclid f a -> Bool
forall a. Euclid f a -> Int
forall a. Euclid f a -> [a]
forall a. (a -> a -> a) -> Euclid f a -> a
forall m a. Monoid m => (a -> m) -> Euclid f a -> m
forall b a. (b -> a -> b) -> b -> Euclid f a -> b
forall a b. (a -> b -> b) -> b -> Euclid f a -> b
forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Euclid f a -> Bool
forall (f :: * -> *) a. (Foldable f, Num a) => Euclid f a -> a
forall (f :: * -> *) a. (Foldable f, Ord a) => Euclid f a -> a
forall (f :: * -> *) m. (Foldable f, Monoid m) => Euclid f m -> m
forall (f :: * -> *) a. Foldable f => Euclid f a -> Bool
forall (f :: * -> *) a. Foldable f => Euclid f a -> Int
forall (f :: * -> *) a. Foldable f => Euclid f a -> [a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Euclid f a -> a
forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Euclid f a -> m
forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Euclid f a -> b
forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Euclid f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => Euclid f m -> m
fold :: forall m. Monoid m => Euclid f m -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Euclid f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Euclid f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Euclid f a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Euclid f a -> m
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Euclid f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Euclid f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Euclid f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Euclid f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Euclid f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Euclid f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Euclid f a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Euclid f a -> b
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Euclid f a -> a
foldr1 :: forall a. (a -> a -> a) -> Euclid f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Euclid f a -> a
foldl1 :: forall a. (a -> a -> a) -> Euclid f a -> a
$ctoList :: forall (f :: * -> *) a. Foldable f => Euclid f a -> [a]
toList :: forall a. Euclid f a -> [a]
$cnull :: forall (f :: * -> *) a. Foldable f => Euclid f a -> Bool
null :: forall a. Euclid f a -> Bool
$clength :: forall (f :: * -> *) a. Foldable f => Euclid f a -> Int
length :: forall a. Euclid f a -> Int
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Euclid f a -> Bool
elem :: forall a. Eq a => a -> Euclid f a -> Bool
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Euclid f a -> a
maximum :: forall a. Ord a => Euclid f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Euclid f a -> a
minimum :: forall a. Ord a => Euclid f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => Euclid f a -> a
sum :: forall a. Num a => Euclid f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => Euclid f a -> a
product :: forall a. Num a => Euclid f a -> a
Foldable,Functor (Euclid f)
Foldable (Euclid f)
(Functor (Euclid f), Foldable (Euclid f)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Euclid f a -> f (Euclid f b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Euclid f (f a) -> f (Euclid f a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Euclid f a -> m (Euclid f b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Euclid f (m a) -> m (Euclid f a))
-> Traversable (Euclid f)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *). Traversable f => Functor (Euclid f)
forall (f :: * -> *). Traversable f => Foldable (Euclid f)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Euclid f (m a) -> m (Euclid f a)
forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Euclid f (f a) -> f (Euclid f a)
forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Euclid f a -> m (Euclid f b)
forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Euclid f a -> f (Euclid f b)
forall (m :: * -> *) a. Monad m => Euclid f (m a) -> m (Euclid f a)
forall (f :: * -> *) a.
Applicative f =>
Euclid f (f a) -> f (Euclid f a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Euclid f a -> m (Euclid f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Euclid f a -> f (Euclid f b)
$ctraverse :: forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Euclid f a -> f (Euclid f b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Euclid f a -> f (Euclid f b)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Euclid f (f a) -> f (Euclid f a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Euclid f (f a) -> f (Euclid f a)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Euclid f a -> m (Euclid f b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Euclid f a -> m (Euclid f b)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Euclid f (m a) -> m (Euclid f a)
sequence :: forall (m :: * -> *) a. Monad m => Euclid f (m a) -> m (Euclid f a)
Traversable,Int -> Euclid f a -> ShowS
[Euclid f a] -> ShowS
Euclid f a -> [Char]
(Int -> Euclid f a -> ShowS)
-> (Euclid f a -> [Char])
-> ([Euclid f a] -> ShowS)
-> Show (Euclid f a)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> Euclid f a -> ShowS
forall k (f :: k -> *) (a :: k).
Show (f a) =>
[Euclid f a] -> ShowS
forall k (f :: k -> *) (a :: k). Show (f a) => Euclid f a -> [Char]
$cshowsPrec :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> Euclid f a -> ShowS
showsPrec :: Int -> Euclid f a -> ShowS
$cshow :: forall k (f :: k -> *) (a :: k). Show (f a) => Euclid f a -> [Char]
show :: Euclid f a -> [Char]
$cshowList :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
[Euclid f a] -> ShowS
showList :: [Euclid f a] -> ShowS
Show,Euclid f a -> Euclid f a -> Bool
(Euclid f a -> Euclid f a -> Bool)
-> (Euclid f a -> Euclid f a -> Bool) -> Eq (Euclid f a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (f :: k -> *) (a :: k).
Eq (f a) =>
Euclid f a -> Euclid f a -> Bool
$c== :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
Euclid f a -> Euclid f a -> Bool
== :: Euclid f a -> Euclid f a -> Bool
$c/= :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
Euclid f a -> Euclid f a -> Bool
/= :: Euclid f a -> Euclid f a -> Bool
Eq,Eq (Euclid f a)
Eq (Euclid f a) =>
(Euclid f a -> Euclid f a -> Ordering)
-> (Euclid f a -> Euclid f a -> Bool)
-> (Euclid f a -> Euclid f a -> Bool)
-> (Euclid f a -> Euclid f a -> Bool)
-> (Euclid f a -> Euclid f a -> Bool)
-> (Euclid f a -> Euclid f a -> Euclid f a)
-> (Euclid f a -> Euclid f a -> Euclid f a)
-> Ord (Euclid f a)
Euclid f a -> Euclid f a -> Bool
Euclid f a -> Euclid f a -> Ordering
Euclid f a -> Euclid f a -> Euclid f a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (f :: k -> *) (a :: k). Ord (f a) => Eq (Euclid f a)
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Bool
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Ordering
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Euclid f a
$ccompare :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Ordering
compare :: Euclid f a -> Euclid f a -> Ordering
$c< :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Bool
< :: Euclid f a -> Euclid f a -> Bool
$c<= :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Bool
<= :: Euclid f a -> Euclid f a -> Bool
$c> :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Bool
> :: Euclid f a -> Euclid f a -> Bool
$c>= :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Bool
>= :: Euclid f a -> Euclid f a -> Bool
$cmax :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Euclid f a
max :: Euclid f a -> Euclid f a -> Euclid f a
$cmin :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Euclid f a -> Euclid f a -> Euclid f a
min :: Euclid f a -> Euclid f a -> Euclid f a
Ord,Functor (Euclid f)
Functor (Euclid f) =>
(forall a. a -> Euclid f a)
-> (forall a b. Euclid f (a -> b) -> Euclid f a -> Euclid f b)
-> (forall a b c.
    (a -> b -> c) -> Euclid f a -> Euclid f b -> Euclid f c)
-> (forall a b. Euclid f a -> Euclid f b -> Euclid f b)
-> (forall a b. Euclid f a -> Euclid f b -> Euclid f a)
-> Applicative (Euclid f)
forall a. a -> Euclid f a
forall a b. Euclid f a -> Euclid f b -> Euclid f a
forall a b. Euclid f a -> Euclid f b -> Euclid f b
forall a b. Euclid f (a -> b) -> Euclid f a -> Euclid f b
forall a b c.
(a -> b -> c) -> Euclid f a -> Euclid f b -> Euclid f c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (f :: * -> *). Applicative f => Functor (Euclid f)
forall (f :: * -> *) a. Applicative f => a -> Euclid f a
forall (f :: * -> *) a b.
Applicative f =>
Euclid f a -> Euclid f b -> Euclid f a
forall (f :: * -> *) a b.
Applicative f =>
Euclid f a -> Euclid f b -> Euclid f b
forall (f :: * -> *) a b.
Applicative f =>
Euclid f (a -> b) -> Euclid f a -> Euclid f b
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> Euclid f a -> Euclid f b -> Euclid f c
$cpure :: forall (f :: * -> *) a. Applicative f => a -> Euclid f a
pure :: forall a. a -> Euclid f a
$c<*> :: forall (f :: * -> *) a b.
Applicative f =>
Euclid f (a -> b) -> Euclid f a -> Euclid f b
<*> :: forall a b. Euclid f (a -> b) -> Euclid f a -> Euclid f b
$cliftA2 :: forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> Euclid f a -> Euclid f b -> Euclid f c
liftA2 :: forall a b c.
(a -> b -> c) -> Euclid f a -> Euclid f b -> Euclid f c
$c*> :: forall (f :: * -> *) a b.
Applicative f =>
Euclid f a -> Euclid f b -> Euclid f b
*> :: forall a b. Euclid f a -> Euclid f b -> Euclid f b
$c<* :: forall (f :: * -> *) a b.
Applicative f =>
Euclid f a -> Euclid f b -> Euclid f a
<* :: forall a b. Euclid f a -> Euclid f b -> Euclid f a
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'

pattern V2 :: forall a. a -> a -> Euclid V2' a
pattern $mV2 :: forall {r} {a}. Euclid V2' a -> (a -> a -> r) -> ((# #) -> r) -> r
$bV2 :: forall a. a -> a -> Euclid V2' a
V2 x y = Euclid (V2' x y)
pattern V3 :: forall a. a -> a -> a -> Euclid V3' a
pattern $mV3 :: forall {r} {a}.
Euclid V3' a -> (a -> a -> a -> r) -> ((# #) -> r) -> r
$bV3 :: forall a. a -> a -> a -> Euclid V3' a
V3 x y z = Euclid (V3' x y z)

instance (Functor f, Scalable s a) => Scalable s (Euclid f a) where
  s
s *^ :: s -> Euclid f a -> Euclid f a
*^ Euclid f a
t = f a -> Euclid f a
forall {k} (f :: k -> *) (a :: k). f a -> Euclid f a
Euclid (((s
ss -> a -> a
forall s a. Scalable s a => s -> a -> a
*^) (a -> a) -> f a -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) f a
t)

pureMat :: (Applicative v, Applicative w) => s -> Mat s v w
pureMat :: forall (v :: * -> *) (w :: * -> *) s.
(Applicative v, Applicative w) =>
s -> Mat s v w
pureMat s
x = v (w s) -> Mat s v w
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (w s -> v (w s)
forall a. a -> v a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s -> w s
forall a. a -> w a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
x))

instance (Applicative f,Applicative g,Additive a) => Additive (Mat a f g) where
  zero :: Mat a f g
zero = a -> Mat a f g
forall (v :: * -> *) (w :: * -> *) s.
(Applicative v, Applicative w) =>
s -> Mat s v w
pureMat a
forall a. Additive a => a
zero
  Mat a f g
x + :: Mat a f g -> Mat a f g -> Mat a f g
+ Mat a f g
y = Flat f g a -> Mat a f g
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
Flat w v s -> Mat s w v
matFlat (a -> a -> a
forall a. Additive a => a -> a -> a
(+) (a -> a -> a) -> Flat f g a -> Flat f g (a -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mat a f g -> Flat f g a
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> Flat w v s
flatMat Mat a f g
x Flat f g (a -> a) -> Flat f g a -> Flat f g a
forall a b. Flat f g (a -> b) -> Flat f g a -> Flat f g b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mat a f g -> Flat f g a
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> Flat w v s
flatMat Mat a f g
y)
instance (Applicative f,Applicative g,AbelianAdditive a) => AbelianAdditive (Mat a f g) where
instance (Applicative f,Applicative g,Group a) => Group (Mat a f g) where
  negate :: Mat a f g -> Mat a f g
negate Mat a f g
x = Flat f g a -> Mat a f g
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
Flat w v s -> Mat s w v
matFlat (a -> a
forall a. Group a => a -> a
negate (a -> a) -> Flat f g a -> Flat f g a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mat a f g -> Flat f g a
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> Flat w v s
flatMat Mat a f g
x)
  Mat a f g
x - :: Mat a f g -> Mat a f g -> Mat a f g
- Mat a f g
y = Flat f g a -> Mat a f g
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
Flat w v s -> Mat s w v
matFlat ((-) (a -> a -> a) -> Flat f g a -> Flat f g (a -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mat a f g -> Flat f g a
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> Flat w v s
flatMat Mat a f g
x Flat f g (a -> a) -> Flat f g a -> Flat f g a
forall a b. Flat f g (a -> b) -> Flat f g a -> Flat f g b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mat a f g -> Flat f g a
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> Flat w v s
flatMat Mat a f g
y)

instance (Functor f, Functor g,Scalable s a) => Scalable s (Mat a f g) where
  s
s *^ :: s -> Mat a f g -> Mat a f g
*^ Mat f (g a)
t = f (g a) -> Mat a f g
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (((s
ss -> a -> a
forall s a. Scalable s a => s -> a -> a
*^) (a -> a) -> g a -> g a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (g a -> g a) -> f (g a) -> f (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g a)
t)

-- | Hadamard product
(⊙) :: Applicative v => Multiplicative s => v s -> v s -> v s
v s
x ⊙ :: forall (v :: * -> *) s.
(Applicative v, Multiplicative s) =>
v s -> v s -> v s
⊙ v s
y = s -> s -> s
forall a. Multiplicative a => a -> a -> a
(*) (s -> s -> s) -> v s -> v (s -> s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v s
x v (s -> s) -> v s -> v s
forall a b. v (a -> b) -> v a -> v b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> v s
y

instance Distributive f => Distributive (Euclid f) where
  collect :: forall (f :: * -> *) a b.
Functor f =>
(a -> Euclid f b) -> f a -> Euclid f (f b)
collect a -> Euclid f b
f = f (f b) -> Euclid f (f b)
forall {k} (f :: k -> *) (a :: k). f a -> Euclid f a
Euclid (f (f b) -> Euclid f (f b))
-> (f a -> f (f b)) -> f a -> Euclid f (f b)
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (a -> f b) -> f a -> f (f b)
forall (g :: * -> *) (f :: * -> *) a b.
(Distributive g, Functor f) =>
(a -> g b) -> f a -> g (f b)
forall (f :: * -> *) a b. Functor f => (a -> f b) -> f a -> f (f b)
collect (Euclid f b -> f b
forall {k} (f :: k -> *) (a :: k). Euclid f a -> f a
fromEuclid (Euclid f b -> f b) -> (a -> Euclid f b) -> a -> f b
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. a -> Euclid f b
f)
instance Representable f => Representable (Euclid f) where
  type Rep (Euclid f) = Rep f
  index :: forall a. Euclid f a -> Rep (Euclid f) -> a
index (Euclid f a
x) = f a -> Rep f -> a
forall a. f a -> Rep f -> a
forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
index f a
x
  tabulate :: forall a. (Rep (Euclid f) -> a) -> Euclid f a
tabulate Rep (Euclid f) -> a
f = f a -> Euclid f a
forall {k} (f :: k -> *) (a :: k). f a -> Euclid f a
Euclid ((Rep f -> a) -> f a
forall a. (Rep f -> a) -> f a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate Rep f -> a
Rep (Euclid f) -> a
f)
instance VectorR f => VectorR (Euclid f)
instance (VectorR f) => InnerProdSpace (Euclid f) where
  inner :: forall s. Field s => Euclid f s -> Euclid f s -> s
inner Euclid f s
x Euclid f s
y = Euclid f s -> s
forall (t :: * -> *) a. (Foldable t, Additive a) => t a -> a
sum (Euclid f s
x Euclid f s -> Euclid f s -> Euclid f s
forall (v :: * -> *) s.
(Applicative v, Multiplicative s) =>
v s -> v s -> v s
⊙ Euclid f s
y) -- fixme

(·) :: Field s => InnerProdSpace v => v s -> v s -> s
· :: forall s (v :: * -> *).
(Field s, InnerProdSpace v) =>
v s -> v s -> s
(·) = v s -> v s -> s
forall s. Field s => v s -> v s -> s
forall (v :: * -> *) s.
(InnerProdSpace v, Field s) =>
v s -> v s -> s
inner

sqNorm :: Field s => InnerProdSpace v => v s -> s
sqNorm :: forall s (v :: * -> *). (Field s, InnerProdSpace v) => v s -> s
sqNorm v s
x = v s -> v s -> s
forall s. Field s => v s -> v s -> s
forall (v :: * -> *) s.
(InnerProdSpace v, Field s) =>
v s -> v s -> s
inner v s
x v s
x

norm :: Algebraic s => InnerProdSpace v => v s  -> s
norm :: forall s (v :: * -> *). (Algebraic s, InnerProdSpace v) => v s -> s
norm = s -> s
forall a. Roots a => a -> a
sqrt (s -> s) -> (v s -> s) -> v s -> s
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. v s -> s
forall s (v :: * -> *). (Field s, InnerProdSpace v) => v s -> s
sqNorm

normalize :: (VectorSpace s (v s)) => Algebraic s => InnerProdSpace v => v s -> v s
normalize :: forall s (v :: * -> *).
(VectorSpace s (v s), Algebraic s, InnerProdSpace v) =>
v s -> v s
normalize v s
v = s -> s
forall a. Division a => a -> a
recip (v s -> s
forall s (v :: * -> *). (Algebraic s, InnerProdSpace v) => v s -> s
norm v s
v) s -> v s -> v s
forall s a. Scalable s a => s -> a -> a
*^ v s
v

-- | Cross product in 3 dimensions https://en.wikipedia.org/wiki/Cross_product
(×) :: Ring a => V3 a -> V3 a -> V3 a
(V3 a
a1 a
a2 a
a3) × :: forall a. Ring a => V3 a -> V3 a -> V3 a
× (V3 a
b1 a
b2 a
b3) = a -> a -> a -> Euclid V3' a
forall a. a -> a -> a -> Euclid V3' a
V3 (a
a2a -> a -> a
forall a. Multiplicative a => a -> a -> a
*a
b3 a -> a -> a
forall a. Group a => a -> a -> a
- a
a3a -> a -> a
forall a. Multiplicative a => a -> a -> a
*a
b2)  (a -> a
forall a. Group a => a -> a
negate (a
a1a -> a -> a
forall a. Multiplicative a => a -> a -> a
*a
b3 a -> a -> a
forall a. Group a => a -> a -> a
- a
a3a -> a -> a
forall a. Multiplicative a => a -> a -> a
*a
b1)) (a
a1a -> a -> a
forall a. Multiplicative a => a -> a -> a
*a
b2 a -> a -> a
forall a. Group a => a -> a -> a
- a
a2a -> a -> a
forall a. Multiplicative a => a -> a -> a
*a
b1)

type SqMat v s = Mat s v v

-- | Matrix type. (w s) is a column. (v s) is a row.
newtype Mat s w v = Mat {forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> w (v s)
fromMat :: w (v s)} deriving Int -> Mat s w v -> ShowS
[Mat s w v] -> ShowS
Mat s w v -> [Char]
(Int -> Mat s w v -> ShowS)
-> (Mat s w v -> [Char])
-> ([Mat s w v] -> ShowS)
-> Show (Mat s w v)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall k (s :: k) k (w :: k -> *) (v :: k -> k).
Show (w (v s)) =>
Int -> Mat s w v -> ShowS
forall k (s :: k) k (w :: k -> *) (v :: k -> k).
Show (w (v s)) =>
[Mat s w v] -> ShowS
forall k (s :: k) k (w :: k -> *) (v :: k -> k).
Show (w (v s)) =>
Mat s w v -> [Char]
$cshowsPrec :: forall k (s :: k) k (w :: k -> *) (v :: k -> k).
Show (w (v s)) =>
Int -> Mat s w v -> ShowS
showsPrec :: Int -> Mat s w v -> ShowS
$cshow :: forall k (s :: k) k (w :: k -> *) (v :: k -> k).
Show (w (v s)) =>
Mat s w v -> [Char]
show :: Mat s w v -> [Char]
$cshowList :: forall k (s :: k) k (w :: k -> *) (v :: k -> k).
Show (w (v s)) =>
[Mat s w v] -> ShowS
showList :: [Mat s w v] -> ShowS
Show

-- | View of the matrix as a composition of functors.
newtype Flat w v s = Flat {forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
Flat w v s -> w (v s)
fromFlat :: w (v s)} deriving (Int -> Flat w v s -> ShowS
[Flat w v s] -> ShowS
Flat w v s -> [Char]
(Int -> Flat w v s -> ShowS)
-> (Flat w v s -> [Char])
-> ([Flat w v s] -> ShowS)
-> Show (Flat w v s)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall k (w :: k -> *) k (v :: k -> k) (s :: k).
Show (w (v s)) =>
Int -> Flat w v s -> ShowS
forall k (w :: k -> *) k (v :: k -> k) (s :: k).
Show (w (v s)) =>
[Flat w v s] -> ShowS
forall k (w :: k -> *) k (v :: k -> k) (s :: k).
Show (w (v s)) =>
Flat w v s -> [Char]
$cshowsPrec :: forall k (w :: k -> *) k (v :: k -> k) (s :: k).
Show (w (v s)) =>
Int -> Flat w v s -> ShowS
showsPrec :: Int -> Flat w v s -> ShowS
$cshow :: forall k (w :: k -> *) k (v :: k -> k) (s :: k).
Show (w (v s)) =>
Flat w v s -> [Char]
show :: Flat w v s -> [Char]
$cshowList :: forall k (w :: k -> *) k (v :: k -> k) (s :: k).
Show (w (v s)) =>
[Flat w v s] -> ShowS
showList :: [Flat w v s] -> ShowS
Show,(forall a b. (a -> b) -> Flat w v a -> Flat w v b)
-> (forall a b. a -> Flat w v b -> Flat w v a)
-> Functor (Flat w v)
forall a b. a -> Flat w v b -> Flat w v a
forall a b. (a -> b) -> Flat w v a -> Flat w v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
a -> Flat w v b -> Flat w v a
forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
(a -> b) -> Flat w v a -> Flat w v b
$cfmap :: forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
(a -> b) -> Flat w v a -> Flat w v b
fmap :: forall a b. (a -> b) -> Flat w v a -> Flat w v b
$c<$ :: forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
a -> Flat w v b -> Flat w v a
<$ :: forall a b. a -> Flat w v b -> Flat w v a
Functor,(forall m. Monoid m => Flat w v m -> m)
-> (forall m a. Monoid m => (a -> m) -> Flat w v a -> m)
-> (forall m a. Monoid m => (a -> m) -> Flat w v a -> m)
-> (forall a b. (a -> b -> b) -> b -> Flat w v a -> b)
-> (forall a b. (a -> b -> b) -> b -> Flat w v a -> b)
-> (forall b a. (b -> a -> b) -> b -> Flat w v a -> b)
-> (forall b a. (b -> a -> b) -> b -> Flat w v a -> b)
-> (forall a. (a -> a -> a) -> Flat w v a -> a)
-> (forall a. (a -> a -> a) -> Flat w v a -> a)
-> (forall a. Flat w v a -> [a])
-> (forall a. Flat w v a -> Bool)
-> (forall a. Flat w v a -> Int)
-> (forall a. Eq a => a -> Flat w v a -> Bool)
-> (forall a. Ord a => Flat w v a -> a)
-> (forall a. Ord a => Flat w v a -> a)
-> (forall a. Num a => Flat w v a -> a)
-> (forall a. Num a => Flat w v a -> a)
-> Foldable (Flat w v)
forall a. Eq a => a -> Flat w v a -> Bool
forall a. Num a => Flat w v a -> a
forall a. Ord a => Flat w v a -> a
forall m. Monoid m => Flat w v m -> m
forall a. Flat w v a -> Bool
forall a. Flat w v a -> Int
forall a. Flat w v a -> [a]
forall a. (a -> a -> a) -> Flat w v a -> a
forall m a. Monoid m => (a -> m) -> Flat w v a -> m
forall b a. (b -> a -> b) -> b -> Flat w v a -> b
forall a b. (a -> b -> b) -> b -> Flat w v a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Eq a) =>
a -> Flat w v a -> Bool
forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Num a) =>
Flat w v a -> a
forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Ord a) =>
Flat w v a -> a
forall (w :: * -> *) (v :: * -> *) m.
(Foldable w, Foldable v, Monoid m) =>
Flat w v m -> m
forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
Flat w v a -> Bool
forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
Flat w v a -> Int
forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
Flat w v a -> [a]
forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
(a -> a -> a) -> Flat w v a -> a
forall (w :: * -> *) (v :: * -> *) m a.
(Foldable w, Foldable v, Monoid m) =>
(a -> m) -> Flat w v a -> m
forall (w :: * -> *) (v :: * -> *) b a.
(Foldable w, Foldable v) =>
(b -> a -> b) -> b -> Flat w v a -> b
forall (w :: * -> *) (v :: * -> *) a b.
(Foldable w, Foldable v) =>
(a -> b -> b) -> b -> Flat w v a -> b
$cfold :: forall (w :: * -> *) (v :: * -> *) m.
(Foldable w, Foldable v, Monoid m) =>
Flat w v m -> m
fold :: forall m. Monoid m => Flat w v m -> m
$cfoldMap :: forall (w :: * -> *) (v :: * -> *) m a.
(Foldable w, Foldable v, Monoid m) =>
(a -> m) -> Flat w v a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Flat w v a -> m
$cfoldMap' :: forall (w :: * -> *) (v :: * -> *) m a.
(Foldable w, Foldable v, Monoid m) =>
(a -> m) -> Flat w v a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Flat w v a -> m
$cfoldr :: forall (w :: * -> *) (v :: * -> *) a b.
(Foldable w, Foldable v) =>
(a -> b -> b) -> b -> Flat w v a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Flat w v a -> b
$cfoldr' :: forall (w :: * -> *) (v :: * -> *) a b.
(Foldable w, Foldable v) =>
(a -> b -> b) -> b -> Flat w v a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Flat w v a -> b
$cfoldl :: forall (w :: * -> *) (v :: * -> *) b a.
(Foldable w, Foldable v) =>
(b -> a -> b) -> b -> Flat w v a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Flat w v a -> b
$cfoldl' :: forall (w :: * -> *) (v :: * -> *) b a.
(Foldable w, Foldable v) =>
(b -> a -> b) -> b -> Flat w v a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Flat w v a -> b
$cfoldr1 :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
(a -> a -> a) -> Flat w v a -> a
foldr1 :: forall a. (a -> a -> a) -> Flat w v a -> a
$cfoldl1 :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
(a -> a -> a) -> Flat w v a -> a
foldl1 :: forall a. (a -> a -> a) -> Flat w v a -> a
$ctoList :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
Flat w v a -> [a]
toList :: forall a. Flat w v a -> [a]
$cnull :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
Flat w v a -> Bool
null :: forall a. Flat w v a -> Bool
$clength :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v) =>
Flat w v a -> Int
length :: forall a. Flat w v a -> Int
$celem :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Eq a) =>
a -> Flat w v a -> Bool
elem :: forall a. Eq a => a -> Flat w v a -> Bool
$cmaximum :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Ord a) =>
Flat w v a -> a
maximum :: forall a. Ord a => Flat w v a -> a
$cminimum :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Ord a) =>
Flat w v a -> a
minimum :: forall a. Ord a => Flat w v a -> a
$csum :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Num a) =>
Flat w v a -> a
sum :: forall a. Num a => Flat w v a -> a
$cproduct :: forall (w :: * -> *) (v :: * -> *) a.
(Foldable w, Foldable v, Num a) =>
Flat w v a -> a
product :: forall a. Num a => Flat w v a -> a
Foldable)
flatMat :: Mat s w v -> Flat w v s
flatMat :: forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> Flat w v s
flatMat (Mat w (v s)
x) = (w (v s) -> Flat w v s
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
w (v s) -> Flat w v s
Flat w (v s)
x)
matFlat :: Flat w v s -> Mat s w v
matFlat :: forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
Flat w v s -> Mat s w v
matFlat (Flat w (v s)
x) = (w (v s) -> Mat s w v
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat w (v s)
x)

instance (Applicative w, Applicative v) => Applicative (Flat w v) where
  pure :: forall a. a -> Flat w v a
pure a
x = w (v a) -> Flat w v a
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
w (v s) -> Flat w v s
Flat (v a -> w (v a)
forall a. a -> w a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> v a
forall a. a -> v a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x))
  Flat w (v (a -> b))
f <*> :: forall a b. Flat w v (a -> b) -> Flat w v a -> Flat w v b
<*> Flat w (v a)
a = w (v b) -> Flat w v b
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
w (v s) -> Flat w v s
Flat ((v (a -> b) -> v a -> v b
forall a b. v (a -> b) -> v a -> v b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
(<*>) (v (a -> b) -> v a -> v b) -> w (v (a -> b)) -> w (v a -> v b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> w (v (a -> b))
f) w (v a -> v b) -> w (v a) -> w (v b)
forall a b. w (a -> b) -> w a -> w b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> w (v a)
a)


instance Ring s => Category (Mat s) where
  type Obj (Mat s) = VectorR
  . :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) =>
Mat s b c -> Mat s a b -> Mat s a c
(.) = Mat s b c -> Mat s a b -> Mat s a c
forall (u :: * -> *) s (w :: * -> *) (v :: * -> *).
(Foldable u, Ring s, Applicative w, Applicative v,
 Applicative u) =>
Mat s u w -> Mat s v u -> Mat s v w
matMul
  id :: forall (a :: * -> *). Obj (Mat s) a => Mat s a a
id = Rel s (Rep a) (Rep a) -> Mat s a a
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep a) (Rep a)
forall a. Obj (Rel s) a => Rel s a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id

fromRel :: (VectorR a, VectorR b) => Rel s (Rep a) (Rep b) -> Mat s a b
fromRel :: forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel (Rel Rep a -> Rep b -> s
f) = a (b s) -> Mat s a b
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat ((Rep a -> b s) -> a (b s)
forall a. (Rep a -> a) -> a a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate (\Rep a
i -> (Rep b -> s) -> b s
forall a. (Rep b -> a) -> b a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate (\Rep b
j -> Rep a -> Rep b -> s
f Rep a
i Rep b
j)))
  
instance Ring s => Monoidal (∘) Id (Mat s) where
  assoc :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) =>
Mat s ((a ∘ b) ∘ c) (a ∘ (b ∘ c))
assoc = Rel s (Rep ((a ∘ b) ∘ c)) (Rep (a ∘ (b ∘ c)))
-> Mat s ((a ∘ b) ∘ c) (a ∘ (b ∘ c))
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep ((a ∘ b) ∘ c)) (Rep (a ∘ (b ∘ c)))
Rel s ((Rep a ⊗ Rep b) ⊗ Rep c) (Rep a ⊗ (Rep b ⊗ Rep c))
forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x (x a b) c) (x a (x b c))
assoc
  assoc_ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) =>
Mat s (a ∘ (b ∘ c)) ((a ∘ b) ∘ c)
assoc_ = Rel s (Rep (a ∘ (b ∘ c))) (Rep ((a ∘ b) ∘ c))
-> Mat s (a ∘ (b ∘ c)) ((a ∘ b) ∘ c)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep (a ∘ (b ∘ c))) (Rep ((a ∘ b) ∘ c))
Rel s (Rep a ⊗ (Rep b ⊗ Rep c)) ((Rep a ⊗ Rep b) ⊗ Rep c)
forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x a (x b c)) (x (x a b) c)
assoc_
  unitorR :: forall (a :: * -> *).
(Obj (Mat s) a, Obj (Mat s) Id) =>
Mat s a (a ∘ Id)
unitorR = Rel s (Rep a) (Rep (a ∘ Id)) -> Mat s a (a ∘ Id)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep a) (Rep (a ∘ Id))
Rel s (Rep a) (Rep a ⊗ One)
forall a. (Obj (Rel s) a, Obj (Rel s) One) => Rel s a (a ⊗ One)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR
  unitorR_ :: forall (a :: * -> *).
(Obj (Mat s) a, Obj (Mat s) Id) =>
Mat s (a ∘ Id) a
unitorR_ = Rel s (Rep (a ∘ Id)) (Rep a) -> Mat s (a ∘ Id) a
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep (a ∘ Id)) (Rep a)
Rel s (Rep a ⊗ One) (Rep a)
forall a. (Obj (Rel s) a, Obj (Rel s) One) => Rel s (a ⊗ One) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x a i) a
unitorR_
  Mat a (b s)
f ⊗ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *) (d :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c, Obj (Mat s) d) =>
Mat s a b -> Mat s c d -> Mat s (a ∘ c) (b ∘ d)
⊗ Mat c (d s)
g = (∘) a c ((∘) b d s) -> Mat s (a ∘ c) (b ∘ d)
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (a (c ((∘) b d s)) -> (∘) a c ((∘) b d s)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp ((b s -> c ((∘) b d s)) -> a (b s) -> a (c ((∘) b d s))
forall a b. (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b s
x -> (b (d s) -> (∘) b d s) -> c (b (d s)) -> c ((∘) b d s)
forall a b. (a -> b) -> c a -> c b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b (d s) -> (∘) b d s
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp  ((d s -> b (d s)) -> c (d s) -> c (b (d s))
forall a b. (a -> b) -> c a -> c b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\d s
y -> (d s -> d s -> d s) -> b (d s) -> b (d s) -> b (d s)
forall a b c. (a -> b -> c) -> b a -> b b -> b c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ((s -> s -> s) -> d s -> d s -> d s
forall a b c. (a -> b -> c) -> d a -> d b -> d c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 s -> s -> s
forall a. Multiplicative a => a -> a -> a
(*)) ((s -> d s) -> b s -> b (d s)
forall a b. (a -> b) -> b a -> b b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> d s
forall a. a -> d a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b s
x) (d s -> b (d s)
forall a. a -> b a
forall (f :: * -> *) a. Applicative f => a -> f a
pure d s
y)) c (d s)
g)) a (b s)
f))


instance Ring s => Symmetric (∘) Id (Mat s) where
instance Ring s => Braided (∘) Id (Mat s) where
  swap :: forall (a :: * -> *) (b :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b) =>
Mat s (a ∘ b) (b ∘ a)
swap = Rel s (Rep (a ∘ b)) (Rep (b ∘ a)) -> Mat s (a ∘ b) (b ∘ a)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep (a ∘ b)) (Rep (b ∘ a))
Rel s (Rep a ⊗ Rep b) (Rep b ⊗ Rep a)
forall a b. (Obj (Rel s) a, Obj (Rel s) b) => Rel s (a ⊗ b) (b ⊗ a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap

instance Ring s => Monoidal (⊗) One (Mat s) where
  assoc :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) =>
Mat s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc = Rel s (Rep ((a ⊗ b) ⊗ c)) (Rep (a ⊗ (b ⊗ c)))
-> Mat s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep ((a ⊗ b) ⊗ c)) (Rep (a ⊗ (b ⊗ c)))
Rel s ((Rep a ⊕ Rep b) ⊕ Rep c) (Rep a ⊕ (Rep b ⊕ Rep c))
forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x (x a b) c) (x a (x b c))
assoc
  assoc_ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) =>
Mat s (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc_ = Rel s (Rep (a ⊗ (b ⊗ c))) (Rep ((a ⊗ b) ⊗ c))
-> Mat s (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep (a ⊗ (b ⊗ c))) (Rep ((a ⊗ b) ⊗ c))
Rel s (Rep a ⊕ (Rep b ⊕ Rep c)) ((Rep a ⊕ Rep b) ⊕ Rep c)
forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s (a ⊕ (b ⊕ c)) ((a ⊕ b) ⊕ c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x a (x b c)) (x (x a b) c)
assoc_
  unitorR :: forall (a :: * -> *).
(Obj (Mat s) a, Obj (Mat s) One) =>
Mat s a (a ⊗ One)
unitorR = Rel s (Rep a) (Rep (a ⊗ One)) -> Mat s a (a ⊗ One)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep a) (Rep (a ⊗ One))
Rel s (Rep a) (Rep a ⊕ Zero)
forall a. (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s a (a ⊕ Zero)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR
  unitorR_ :: forall (a :: * -> *).
(Obj (Mat s) a, Obj (Mat s) One) =>
Mat s (a ⊗ One) a
unitorR_ = Rel s (Rep (a ⊗ One)) (Rep a) -> Mat s (a ⊗ One) a
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep (a ⊗ One)) (Rep a)
Rel s (Rep a ⊕ Zero) (Rep a)
forall a. (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s (a ⊕ Zero) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x a i) a
unitorR_
  Mat a (b s)
f ⊗ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *) (d :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c, Obj (Mat s) d) =>
Mat s a b -> Mat s c d -> Mat s (a ⊗ c) (b ⊗ d)
⊗ Mat c (d s)
g = (⊗) a c ((⊗) b d s) -> Mat s (a ⊗ c) (b ⊗ d)
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (a ((⊗) b d s) -> c ((⊗) b d s) -> (⊗) a c ((⊗) b d s)
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd
                        (((b s -> d s -> (⊗) b d s) -> d s -> b s -> (⊗) b d s
forall a b c. (a -> b -> c) -> b -> a -> c
flip b s -> d s -> (⊗) b d s
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd (s -> d s
forall a. a -> d a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
forall a. Additive a => a
zero)) (b s -> (⊗) b d s) -> a (b s) -> a ((⊗) b d s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a (b s)
f)
                        (b s -> d s -> (⊗) b d s
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd (s -> b s
forall a. a -> b a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
forall a. Additive a => a
zero) (d s -> (⊗) b d s) -> c (d s) -> c ((⊗) b d s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c (d s)
g))

instance Ring s => Cartesian (⊗) One (Mat s) where
  Mat a (b s)
f ▵ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) =>
Mat s a b -> Mat s a c -> Mat s a (b ⊗ c)
▵ Mat a (c s)
g = a ((⊗) b c s) -> Mat s a (b ⊗ c)
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (b s -> c s -> (⊗) b c s
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd (b s -> c s -> (⊗) b c s) -> a (b s) -> a (c s -> (⊗) b c s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a (b s)
f a (c s -> (⊗) b c s) -> a (c s) -> a ((⊗) b c s)
forall a b. a (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a (c s)
g)
  dis :: forall (a :: * -> *). Obj (Mat s) a => Mat s a One
dis = Rel s (Rep a) (Rep One) -> Mat s a One
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep a) (Rep One)
Rel s (Rep a) Zero
forall a. Obj (Rel s) a => Rel s a Zero
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a i
dis

instance Ring s => Braided (⊗) One (Mat s) where
  swap :: forall (a :: * -> *) (b :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b) =>
Mat s (a ⊗ b) (b ⊗ a)
swap = Rel s (Rep (a ⊗ b)) (Rep (b ⊗ a)) -> Mat s (a ⊗ b) (b ⊗ a)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep (a ⊗ b)) (Rep (b ⊗ a))
Rel s (Rep a ⊕ Rep b) (Rep b ⊕ Rep a)
forall a b. (Obj (Rel s) a, Obj (Rel s) b) => Rel s (a ⊕ b) (b ⊕ a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap
instance Ring s => Symmetric (⊗) One (Mat s) where

instance Ring s => CoCartesian (⊗) One (Mat s) where
  inl :: forall (a :: * -> *) (b :: * -> *).
O2 (Mat s) a b =>
Mat s a (a ⊗ b)
inl = Rel s (Rep a) (Rep (a ⊗ b)) -> Mat s a (a ⊗ b)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep a) (Rep (a ⊗ b))
Rel s (Rep a) (Rep a ⊕ Rep b)
forall a b. O2 (Rel s) a b => Rel s a (a ⊕ b)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(CoCartesian x i cat, O2 cat a b) =>
cat a (x a b)
inl
  inr :: forall (a :: * -> *) (b :: * -> *).
O2 (Mat s) a b =>
Mat s b (a ⊗ b)
inr = Rel s (Rep b) (Rep (a ⊗ b)) -> Mat s b (a ⊗ b)
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep b) (Rep (a ⊗ b))
Rel s (Rep b) (Rep a ⊕ Rep b)
forall a b. O2 (Rel s) a b => Rel s b (a ⊕ b)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(CoCartesian x i cat, O2 cat a b) =>
cat b (x a b)
inr
  new :: forall (a :: * -> *). Obj (Mat s) a => Mat s One a
new = Rel s (Rep One) (Rep a) -> Mat s One a
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep One) (Rep a)
Rel s Zero (Rep a)
forall a. Obj (Rel s) a => Rel s Zero a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat i a
new
  jam :: forall (a :: * -> *). Obj (Mat s) a => Mat s (a ⊗ a) a
jam = Rel s (Rep (a ⊗ a)) (Rep a) -> Mat s (a ⊗ a) a
forall (a :: * -> *) (b :: * -> *) s.
(VectorR a, VectorR b) =>
Rel s (Rep a) (Rep b) -> Mat s a b
fromRel Rel s (Rep (a ⊗ a)) (Rep a)
Rel s (Rep a ⊕ Rep a) (Rep a)
forall a. Obj (Rel s) a => Rel s (a ⊕ a) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat (x a a) a
jam
  Mat b (a s)
f ▿ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) =>
Mat s b a -> Mat s c a -> Mat s (b ⊗ c) a
▿ Mat c (a s)
g = (⊗) b c (a s) -> Mat s (b ⊗ c) a
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (b (a s) -> c (a s) -> (⊗) b c (a s)
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd b (a s)
f c (a s)
g)
  
type Mat3x3 s = SqMat V3 s
type Mat2x2 s = SqMat V2 s

pattern Mat2x2 :: forall s. s -> s -> s -> s -> Mat s V2 V2
pattern $mMat2x2 :: forall {r} {s}.
Mat s V2 V2 -> (s -> s -> s -> s -> r) -> ((# #) -> r) -> r
$bMat2x2 :: forall s. s -> s -> s -> s -> Mat s V2 V2
Mat2x2 a b c d = Mat (V2 (V2 a c)
                                 (V2 b d))

pattern Mat3x3 :: forall s. s -> s -> s -> s -> s -> s -> s -> s -> s -> Mat s V3 V3
pattern $mMat3x3 :: forall {r} {s}.
Mat s V3 V3
-> (s -> s -> s -> s -> s -> s -> s -> s -> s -> r)
-> ((# #) -> r)
-> r
$bMat3x3 :: forall s. s -> s -> s -> s -> s -> s -> s -> s -> s -> Mat s V3 V3
Mat3x3 a b c d e f g h i = Mat (V3 (V3 a d g)
                                           (V3 b e h)
                                           (V3 c f i))


rotation2d :: Transcendental a => a -> Mat2x2 a
rotation2d :: forall a. Transcendental a => a -> Mat2x2 a
rotation2d a
θ = Mat a V2 V2 -> Mat a V2 V2
forall (f :: * -> *) (g :: * -> *) a.
(Functor f, Distributive g) =>
Mat a f g -> Mat a g f
transpose (Mat a V2 V2 -> Mat a V2 V2) -> Mat a V2 V2 -> Mat a V2 V2
forall a b. (a -> b) -> a -> b
$ V2 (V2 a) -> Mat a V2 V2
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (V2 (V2 a) -> Mat a V2 V2) -> V2 (V2 a) -> Mat a V2 V2
forall a b. (a -> b) -> a -> b
$ V2 a -> V2 a -> V2 (V2 a)
forall a. a -> a -> Euclid V2' a
V2 (a -> a -> V2 a
forall a. a -> a -> Euclid V2' a
V2 (a -> a
forall a. Transcendental a => a -> a
cos a
θ) (-a -> a
forall a. Transcendental a => a -> a
sin a
θ))
                                    (a -> a -> V2 a
forall a. a -> a -> Euclid V2' a
V2 (a -> a
forall a. Transcendental a => a -> a
sin a
θ)  (a -> a
forall a. Transcendental a => a -> a
cos a
θ))

-- >>> 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 :: forall a. Group a => V3 a -> Mat3x3 a
crossProductMatrix (V3 a
a1 a
a2 a
a3) = a -> a -> a -> a -> a -> a -> a -> a -> a -> Mat a V3 V3
forall s. s -> s -> s -> s -> s -> s -> s -> s -> s -> Mat s V3 V3
Mat3x3 a
forall a. Additive a => a
zero  (-a
a3) a
a2
                                          a
a3    a
forall a. Additive a => a
zero  (-a
a1)
                                          (-a
a2) a
a1    a
forall a. Additive a => a
zero

outerWith :: (Applicative v, Applicative w)
           => (s -> t -> u) -> w s -> v t -> Mat u v w
outerWith :: forall (v :: * -> *) (w :: * -> *) s t u.
(Applicative v, Applicative w) =>
(s -> t -> u) -> w s -> v t -> Mat u v w
outerWith s -> t -> u
f w s
v1 v t
v2 = Flat v w u -> Mat u v w
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
Flat w v s -> Mat s w v
matFlat (s -> t -> u
f (s -> t -> u) -> Flat v w s -> Flat v w (t -> u)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v (w s) -> Flat v w s
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
w (v s) -> Flat w v s
Flat (w s -> v (w s)
forall a. a -> v a
forall (f :: * -> *) a. Applicative f => a -> f a
pure w s
v1) Flat v w (t -> u) -> Flat v w t -> Flat v w u
forall a b. Flat v w (a -> b) -> Flat v w a -> Flat v w b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> v (w t) -> Flat v w t
forall {k} {k} (w :: k -> *) (v :: k -> k) (s :: k).
w (v s) -> Flat w v s
Flat (t -> w t
forall a. a -> w a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> w t) -> v t -> v (w t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v t
v2))


-- | Outer product 
outer :: (Applicative v, Applicative w, Multiplicative s)
    => Euclid w s -> Euclid v s -> Mat s (Euclid w) (Euclid v)
Euclid w s
v1 outer :: forall (v :: * -> *) (w :: * -> *) s.
(Applicative v, Applicative w, Multiplicative s) =>
Euclid w s -> Euclid v s -> Mat s (Euclid w) (Euclid v)
`outer` Euclid v s
v2 = (s -> s -> s)
-> Euclid v s -> Euclid w s -> Mat s (Euclid w) (Euclid v)
forall (v :: * -> *) (w :: * -> *) s t u.
(Applicative v, Applicative w) =>
(s -> t -> u) -> w s -> v t -> Mat u v w
outerWith s -> s -> s
forall a. Multiplicative a => a -> a -> a
(*) Euclid v s
v2 Euclid w s
v1


diagonal :: Eq (Rep v) => Representable v => Ring s => Applicative v => v s -> SqMat v s
diagonal :: forall (v :: * -> *) s.
(Eq (Rep v), Representable v, Ring s, Applicative v) =>
v s -> SqMat v s
diagonal v s
v = (Rep v -> (Rep v, s) -> s)
-> v (Rep v) -> v (Rep v, s) -> Mat s v v
forall (v :: * -> *) (w :: * -> *) s t u.
(Applicative v, Applicative w) =>
(s -> t -> u) -> w s -> v t -> Mat u v w
outerWith (\Rep v
x (Rep v
y,s
a) -> if Rep v
x Rep v -> Rep v -> Bool
forall a. Eq a => a -> a -> Bool
== Rep v
y then s
a else s
forall a. Additive a => a
zero) ((Rep v -> Rep v) -> v (Rep v)
forall a. (Rep v -> a) -> v a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate Rep v -> Rep v
forall a. Obj (->) a => a -> a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id) ((,) (Rep v -> s -> (Rep v, s)) -> v (Rep v) -> v (s -> (Rep v, s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Rep v -> Rep v) -> v (Rep v)
forall a. (Rep v -> a) -> v a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate Rep v -> Rep v
forall a. Obj (->) a => a -> a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id) v (s -> (Rep v, s)) -> v s -> v (Rep v, s)
forall a b. v (a -> b) -> v a -> v b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> v s
v)

-- | 3d rotation around given axis
rotation3d :: Transcendental a => a -> V3 a -> Mat3x3 a
rotation3d :: forall a. Transcendental a => a -> V3 a -> Mat3x3 a
rotation3d a
θ V3 a
u = a -> a
forall a. Transcendental a => a -> a
cos a
θ a -> Mat3x3 a -> Mat3x3 a
forall s a. Scalable s a => s -> a -> a
*^ Mat3x3 a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
forall (a :: * -> *). Obj (Mat a) a => Mat a a a
id Mat3x3 a -> Mat3x3 a -> Mat3x3 a
forall a. Additive a => a -> a -> a
+
                 a -> a
forall a. Transcendental a => a -> a
sin a
θ a -> Mat3x3 a -> Mat3x3 a
forall s a. Scalable s a => s -> a -> a
*^ V3 a -> Mat3x3 a
forall a. Group a => V3 a -> Mat3x3 a
crossProductMatrix V3 a
u Mat3x3 a -> Mat3x3 a -> Mat3x3 a
forall a. Additive a => a -> a -> a
+
                 (a
1 a -> a -> a
forall a. Group a => a -> a -> a
- a -> a
forall a. Transcendental a => a -> a
cos a
θ) a -> Mat3x3 a -> Mat3x3 a
forall s a. Scalable s a => s -> a -> a
*^ (V3 a
u V3 a -> V3 a -> Mat3x3 a
forall (v :: * -> *) (w :: * -> *) s.
(Applicative v, Applicative w, Multiplicative s) =>
Euclid w s -> Euclid v s -> Mat s (Euclid w) (Euclid v)
`outer` V3 a
u)


-- | 3d rotation mapping the direction of 'from' to that of 'to'
rotationFromTo :: forall a. (Algebraic a)
               => V3 a -> V3 a -> Mat3x3 a
rotationFromTo :: forall a. Algebraic a => V3 a -> V3 a -> Mat3x3 a
rotationFromTo V3 a
from V3 a
to = a
c a -> Mat3x3 a -> Mat3x3 a
forall s a. Scalable s a => s -> a -> a
*^ Mat3x3 a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
forall (a :: * -> *). Obj (Mat a) a => Mat a a a
id Mat3x3 a -> Mat3x3 a -> Mat3x3 a
forall a. Additive a => a -> a -> a
+ a
s a -> Mat3x3 a -> Mat3x3 a
forall s a. Scalable s a => s -> a -> a
*^ V3 a -> Mat3x3 a
forall a. Group a => V3 a -> Mat3x3 a
crossProductMatrix V3 a
v Mat3x3 a -> Mat3x3 a -> Mat3x3 a
forall a. Additive a => a -> a -> a
+ (a
1a -> a -> a
forall a. Group a => a -> a -> a
-a
c) a -> Mat3x3 a -> Mat3x3 a
forall s a. Scalable s a => s -> a -> a
*^ (V3 a
v V3 a -> V3 a -> Mat3x3 a
forall (v :: * -> *) (w :: * -> *) s.
(Applicative v, Applicative w, Multiplicative s) =>
Euclid w s -> Euclid v s -> Mat s (Euclid w) (Euclid v)
`outer` V3 a
v)
  where y :: V3 a
y = V3 a
to
        x :: V3 a
x = V3 a
from
        v :: V3 a
        v :: V3 a
v = V3 a
x V3 a -> V3 a -> V3 a
forall a. Ring a => V3 a -> V3 a -> V3 a
× V3 a
y -- axis of rotation
        c :: a
c = V3 a -> V3 a -> a
forall s. Field s => Euclid V3' s -> Euclid V3' s -> s
forall (v :: * -> *) s.
(InnerProdSpace v, Field s) =>
v s -> v s -> s
inner V3 a
x V3 a
y -- cos of angle
        s :: a
s = V3 a -> a
forall s (v :: * -> *). (Algebraic s, InnerProdSpace v) => v s -> s
norm V3 a
v -- sin of angle

-- >>> 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}

-- | Transposition as distribution
transpose :: Functor f => Distributive g => Mat a f g -> Mat a g f
transpose :: forall (f :: * -> *) (g :: * -> *) a.
(Functor f, Distributive g) =>
Mat a f g -> Mat a g f
transpose = g (f a) -> Mat a g f
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (g (f a) -> Mat a g f)
-> (Mat a f g -> g (f a)) -> Mat a f g -> Mat a g f
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. f (g a) -> g (f a)
forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: * -> *) a. Functor f => f (g a) -> g (f a)
distribute (f (g a) -> g (f a))
-> (Mat a f g -> f (g a)) -> Mat a f g -> g (f a)
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. Mat a f g -> f (g a)
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
Mat s w v -> w (v s)
fromMat

instance Ring s => Dagger (Mat s) where
  dagger :: forall (a :: * -> *) (b :: * -> *).
O2 (Mat s) a b =>
Mat s a b -> Mat s b a
dagger = Mat s a b -> Mat s b a
forall (f :: * -> *) (g :: * -> *) a.
(Functor f, Distributive g) =>
Mat a f g -> Mat a g f
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 :: forall (u :: * -> *) s (w :: * -> *) (v :: * -> *).
(Foldable u, Ring s, Applicative w, Applicative v,
 Applicative u) =>
Mat s u w -> Mat s v u -> Mat s v w
matMul Mat s u w
a (Mat v (u s)
b) = v (w s) -> Mat s v w
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (Mat s u w -> u s -> w s
forall s (v :: * -> *) (w :: * -> *).
(Ring s, Foldable v, Applicative v, Applicative w) =>
Mat s v w -> v s -> w s
matVecMul Mat s u w
a (u s -> w s) -> v (u s) -> v (w s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v (u s)
b)


(<+>) :: (Applicative f, Additive b) => f b -> f b -> f b
f b
u <+> :: forall (f :: * -> *) b.
(Applicative f, Additive b) =>
f b -> f b -> f b
<+> f b
v = b -> b -> b
forall a. Additive a => a -> a -> a
(+) (b -> b -> b) -> f b -> f (b -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
u f (b -> b) -> f b -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f b
v

matVecMul :: forall s v w. (Ring s, Foldable v,Applicative v,Applicative w) => Mat s v w -> v s -> w s
matVecMul :: forall s (v :: * -> *) (w :: * -> *).
(Ring s, Foldable v, Applicative v, Applicative w) =>
Mat s v w -> v s -> w s
matVecMul (Mat v (w s)
m) v s
x = (w s -> w s -> w s) -> w s -> v (w s) -> w s
forall a b. (a -> b -> b) -> b -> v a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr w s -> w s -> w s
forall (f :: * -> *) b.
(Applicative f, Additive b) =>
f b -> f b -> f b
(<+>) (s -> w s
forall a. a -> w a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
forall a. Additive a => a
zero) (s -> w s -> w s
forall (f :: * -> *) a.
(Functor f, Multiplicative a) =>
a -> f a -> f a
(*<) (s -> w s -> w s) -> v s -> v (w s -> w s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v s
x v (w s -> w s) -> v (w s) -> v (w s)
forall a b. v (a -> b) -> v a -> v b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> v (w s)
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 :: Gen (Mat s a b)
arbitrary = a (b s) -> Mat s a b
forall {k} {k} (s :: k) (w :: k -> *) (v :: k -> k).
w (v s) -> Mat s w v
Mat (a (b s) -> Mat s a b) -> Gen (a (b s)) -> Gen (Mat s a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (b s) -> Gen (a (b s))
forall a. Gen a -> Gen (a a)
forall (f :: * -> *) a. Arbitrary1 f => Gen a -> Gen (f a)
liftArbitrary Gen (b s)
forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => Gen (f a)
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 a (b s)
m =.= :: Mat s a b -> Mat s a b -> Property
=.= Mat a (b s)
n = a Property -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product (b Property -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product (b Property -> Property) -> a (b Property) -> a Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (s -> s -> Property) -> b s -> b s -> b Property
forall a b c. (a -> b -> c) -> b a -> b b -> b c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 s -> s -> Property
forall a. TestEqual a => a -> a -> Property
(=.=) (b s -> b s -> b Property) -> a (b s) -> a (b s -> b Property)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a (b s)
m a (b s -> b Property) -> a (b s) -> a (b Property)
forall a b. a (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a (b s)
n))



prop_linear_with_functor_laws :: Property
prop_linear_with_functor_laws :: Property
prop_linear_with_functor_laws =
  forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, BiCartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
forall (cat :: (* -> *) -> (* -> *) -> *).
(VectorR ~ Obj cat, Con' (⊗) VectorR, BiCartesian (⊗) One cat,
 VectorR One) =>
TestableCat (⊗) One VectorR cat -> Property
laws_bicartesian @(Mat Int)
  (GenObj VectorR (Repr (∘) Id (⊗) One) (Mat Int)
-> (forall (a :: * -> *) (b :: * -> *).
    Repr (∘) Id (⊗) One a
    -> Repr (∘) Id (⊗) One b -> (Mat Int a b -> Property) -> Property)
-> (forall (a :: * -> *) (b :: * -> *).
    Repr (∘) Id (⊗) One a
    -> Repr (∘) Id (⊗) One b -> Dict (TT (Mat Int) a b))
-> (forall (a :: * -> *) (b :: * -> *).
    Repr (∘) Id (⊗) One a
    -> Repr (∘) Id (⊗) One b -> Repr (∘) Id (⊗) One (a ⊗ b))
-> Repr (∘) Id (⊗) One One
-> TestableCat (⊗) One VectorR (Mat Int)
forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (o :: k -> *) (obj :: k -> Constraint).
GenObj obj o f
-> (forall (a :: k) (b :: k).
    o a -> o b -> (f a b -> Property) -> Property)
-> (forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b))
-> (forall (a :: k) (b :: k). o a -> o b -> o (x a b))
-> o i
-> TestableCat x i obj f
testableCat
     (\forall (a :: * -> *).
VectorR a =>
Repr (∘) Id (⊗) One a -> Property
k -> forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
(forall (a :: k). Repr x i t o a -> Property) -> Property
forall (x :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (t :: (* -> *) -> (* -> *) -> * -> *) (o :: * -> *).
(forall (a :: * -> *). Repr x i t o a -> Property) -> Property
forallType @(∘) @Id @(⊗) @One (\Repr (∘) Id (⊗) One a
t -> Repr (∘) Id (⊗) One a -> Property
forall (a :: * -> *).
VectorR a =>
Repr (∘) Id (⊗) One a -> Property
k Repr (∘) Id (⊗) One a
t
       (VectorR a => Property) -> Dict (VectorR a) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: (* -> *) -> Constraint) (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 @VectorR Repr (∘) Id (⊗) One a
t))
     (\Repr (∘) Id (⊗) One a
tx Repr (∘) Id (⊗) One b
ty Mat Int a b -> Property
k -> Repr (∘) Id (⊗) One a
-> Repr (∘) Id (⊗) One b -> (Mat Int a b -> Property) -> Property
forall {k} (f :: k -> k -> *) (a :: k) (b :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(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 Repr (∘) Id (⊗) One a
tx Repr (∘) Id (⊗) One b
ty Mat Int a b -> Property
k
       (Show (a (b Int)) => Property)
-> Dict (Show (a (b Int))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall z (con :: * -> Constraint) (a :: * -> *) (b :: * -> *).
CompClosed con
-> con z => CRepr a -> CRepr b -> Dict (con (a (b z)))
reprCon1Comp @Int CompClosed Show
showCompClosed Repr (∘) Id (⊗) One a
tx Repr (∘) Id (⊗) One b
ty
       (Arbitrary1 a => Property) -> Dict (Arbitrary1 a) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: (* -> *) -> Constraint) (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 @Arbitrary1 Repr (∘) Id (⊗) One a
tx
       (Arbitrary1 b => Property) -> Dict (Arbitrary1 b) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: (* -> *) -> Constraint) (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 @Arbitrary1 Repr (∘) Id (⊗) One b
ty)
     (\Repr (∘) Id (⊗) One a
a Repr (∘) Id (⊗) One b
b -> Dict (TT (Mat Int) a b)
Show (a (b Int)) => Dict (TT (Mat Int) a b)
forall (a :: Constraint). a => Dict a
Dict
       (Show (a (b Int)) => Dict (TT (Mat Int) a b))
-> Dict (Show (a (b Int))) -> Dict (TT (Mat Int) a b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall z (con :: * -> Constraint) (a :: * -> *) (b :: * -> *).
CompClosed con
-> con z => CRepr a -> CRepr b -> Dict (con (a (b z)))
reprCon1Comp @Int CompClosed Show
showCompClosed Repr (∘) Id (⊗) One a
a Repr (∘) Id (⊗) One b
b
       (Arbitrary1 a => Dict (TT (Mat Int) a b))
-> Dict (Arbitrary1 a) -> Dict (TT (Mat Int) a b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: (* -> *) -> Constraint) (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 @Arbitrary1 Repr (∘) Id (⊗) One a
a
       (Arbitrary1 b => Dict (TT (Mat Int) a b))
-> Dict (Arbitrary1 b) -> Dict (TT (Mat Int) a b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: (* -> *) -> Constraint) (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 @Arbitrary1 Repr (∘) Id (⊗) One b
b
       (VectorR a => Dict (TT (Mat Int) a b))
-> Dict (VectorR a) -> Dict (TT (Mat Int) a b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: (* -> *) -> Constraint) (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 @VectorR Repr (∘) Id (⊗) One a
a
       (VectorR b => Dict (TT (Mat Int) a b))
-> Dict (VectorR b) -> Dict (TT (Mat Int) a b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: (* -> *) -> Constraint) (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 @VectorR Repr (∘) Id (⊗) One b
b)
     Repr (∘) Id (⊗) One a
-> Repr (∘) Id (⊗) One b -> Repr (∘) Id (⊗) One (a ⊗ b)
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k)
       (a1 :: k) (b :: k).
Repr x i t o a1 -> Repr x i t o b -> Repr x i t o (t a1 b)
forall (a :: * -> *) (b :: * -> *).
Repr (∘) Id (⊗) One a
-> Repr (∘) Id (⊗) One b -> Repr (∘) Id (⊗) One (a ⊗ b)
RPlus
     Repr (∘) Id (⊗) One One
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o o
RZero)


return []
runTests :: IO Bool
runTests :: IO Bool
runTests = $[Char]
[([Char], Property)]
Property
[([Char], Property)] -> (Property -> IO Result) -> IO Bool
Property -> IO Result
Property -> Property
forall prop. Testable prop => prop -> IO Result
forall prop. Testable prop => prop -> Property
prop_linear_with_functor_laws :: Property
property :: forall prop. Testable prop => prop -> Property
quickCheckResult :: forall prop. Testable prop => prop -> IO Result
runQuickCheckAll :: [([Char], Property)] -> (Property -> IO Result) -> IO Bool
quickCheckAll