packages feed

linear-smc 2.0.2 → 2.2.2

raw patch · 7 files changed

+630/−322 lines, 7 filesdep ~arraydep ~base

Dependency ranges changed: array, base

Files

Control/Category/Constrained.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE AllowAmbiguousTypes #-}@@ -21,7 +22,7 @@ import Data.Kind import Data.Constraint import Data.Type.Equality-+import Data.Array(Ix)  type O2 k a b = (Obj k a, Obj k b) type O3 k a b c =@@ -77,6 +78,8 @@  type a ⊗ b = (a,b) infixr 7 ⊗+type TensorClosed (con :: Type -> Constraint) =+  forall x y. (con x, con y) => con (x ⊗ y) :: Constraint   class ({-<-}ProdObj (Obj k),{->-}Category k) => Monoidal k where@@ -238,3 +241,17 @@ data Order a b where   LT, GT :: Order a b   EQ :: Order a a++newtype Atom s = Atom s deriving (Bounded, Eq, Ord, Enum,Ix)+newtype Dual a = Dual a+++class (ProdObj con) => AutonomousObj con where+  objDual :: forall a. (con a) => Dict (con (Dual a))+  dualObj :: forall z a. (z ~ Dual a, con z) => Dict (con a)++type Unit = ()++class ({-<-}AutonomousObj (Obj cat), {->-}Monoidal cat) => Autonomous cat where+  turn   :: {-<-}Obj cat a => {->-} Unit `cat` (Dual a ⊗ a)+  turn'  :: {-<-}Obj cat a => {->-} (a ⊗ Dual a) `cat` Unit
Control/Category/FreeCartesian.hs view
@@ -1,6 +1,6 @@+{-# LANGUAGE EmptyCase #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE QuantifiedConstraints #-}-{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE AllowAmbiguousTypes #-}@@ -22,114 +22,173 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE LinearTypes #-} -module Control.Category.FreeCartesian where+module Control.Category.FreeCartesian (Cat, π1, π2, embed, (▴), toSMC) where -import Prelude hiding ((.),id,curry)+import Prelude hiding ((.),id,curry,Ordering(..)) import Control.Category.Constrained-import Data.Kind+import Unsafe.Coerce+-- import Control.Category.InitialSMC (type TensorClosed)+ +data Trie  k con a b where+  (:▴:) :: (con b, con c) => Trie k con a b -> Trie k con a c -> Trie k con a (b,c) -- fork+  Z :: Trie  k con a a -- Stop+  (:.) :: (con a, con b) => k a b -> Trie k con b c -> Trie k con a c -- Embed+  L :: Trie  k con  a c -> Trie  k con (a,b) c -- (∘ π₁)+  R :: Trie  k con  b c -> Trie  k con (a,b) c -- (∘ π₂)+  -- composition, with the invariant that the 1st argument is a fork (so b is a product object) (unsimplified). (If it were not a fork, then the composition can be linearized)+  -- Furthermore, the 2nd argument must feed both components to an 'embed', or to the final output.+  -- The 1st argument isn't simplified. Because: 1. simplifying isn't going to help comparision. 2. this way we simplify only one of the copies.+  (:∘) :: (con b) => Trie k con a b -> Trie k con b c -> Trie k con a c -instance (forall x y. (con x, con y) => Show (k x y)) => Show  (Cat k con a b) where-  show x = showsPrec (-1) x ""-  showsPrec d = \case-    I -> showString "id"-    P1 -> showString "π₁"-    P2 -> showString "π₂"-    Embed s -> showString (show s)-    f :.: g -> showParen (d >  0) (showsPrec 0 f . showString " ∘ " . showsPrec 0 g)-    f :▵: g -> showParen (d > -1) (showsPrec 2 f . showString " ▵ " . showsPrec 2 g)+compareTries :: Trie cat con a b -> Trie cat con a c -> Order b c+compareTries Z Z = EQ+compareTries (L f) (L g) = compareTries f g+compareTries (R f) (R g) = compareTries f g+compareTries (_ :. f) (_ :. g) = compareTries f (unsafeCoerceSource g)+  -- same source: because of linearity, if the source is fully+  -- consumed, there can only be a single way in which the source is+  -- transformed.+compareTries (x :∘ f) (y :∘ g) = case compareTries x y of+  EQ -> compareTries f g+  LT -> LT+  GT -> GT+compareTries ((:▴:) x _) ((:▴:) y _) = case compareTries x y of+  EQ -> unsafeCoerce EQ -- the first component of the forks are equal. We maintain the invariant ① that both components are going to be used.+  -- Because of linearity, this means that the 1st component fully determines the output pair.+  LT -> LT+  GT -> GT+compareTries Z _ = LT+compareTries _ Z = GT+compareTries (L {}) _ = LT+compareTries _ (L {})= GT+compareTries (R {}) _ = LT+compareTries _ (R {})= GT+compareTries ((:. ) {}) _ = LT+compareTries _ ((:. ) {})= GT+compareTries ((:∘) {}) _ = LT+compareTries _ ((:∘) {})= GT -showDbg :: Int -> Cat k con a b -> ShowS-showDbg d = \case-    Embed _ -> showString "?"-    I -> showString "id"-    f :.: g -> showParen (d /= 0) (showDbg 0 f . showString " ∘ " . showDbg 0 g)-    f :▵: g -> showParen True (showDbg 2 f . showString " ▵ " . showDbg 2 g)-    P2 -> showString "π₂"-    P1 -> showString "π₁"+pshows :: Show a => a -> ShowS+pshows x = showParen True (shows x) +instance (ProdObj con, forall x y. (con x, con y) => Show (k x y)) => Show  (Trie k con a b) where+  showsPrec _d = \case+    f :▴: g -> showString "⟨" . shows f . showString "," . shows g . showString "⟩"+    m :∘ f -> pshows m . showString "." . shows f+    L k -> showString "1" . shows k+    R k  -> showString "2" . shows k+    φ :. k -> shows φ . shows k+    Z -> showString "!" -parens :: [Char] -> [Char]-parens x = "(" <> x <> ")"+type Cat k con a b = forall c. Trie k con b c -> Trie k con a c -mapGenerators :: (con a, con b) => (forall x y. (con x, con y) => k x y -> k' x y) -> Cat k con a b -> Cat k' con a b-mapGenerators f = \case-  I -> I-  Embed g -> Embed (f g)-  a :.: b -> mapGenerators f a :.: mapGenerators f b-  P1 -> P1-  P2 -> P2-  a :▵: b -> mapGenerators f a :▵: mapGenerators f b-  x -> error (showDbg 0 x " (Free.mapGenerators)")+embed  :: {-<-}(con a, con b) => {->-}k a b -> Cat k {-<-}con{->-} a b+embed φ = (φ :.) -type Cat = FreeCartesian+π1  :: {-<-}con b => {->-} Cat k {-<-}con{->-} (a ⊗ b) a+π1 = L -data FreeCartesian k {-<-} (con :: Type -> Constraint) {->-} a b where-  I      :: FreeCartesian k {-<-}con{->-} a a-  (:.:)  :: {-<-}con b => {->-} FreeCartesian k {-<-}con{->-} b c -> FreeCartesian k {-<-}con{->-} a b-         -> FreeCartesian k {-<-}con{->-} a c-  Embed  :: {-<-}(con a, con b) => {->-}k a b -> FreeCartesian k {-<-}con{->-} a b-  (:▵:)  :: {-<-}(con a, con b, con c) => {->-}FreeCartesian k {-<-}con {->-}a b -> FreeCartesian k {-<-}con{->-} a c-         -> FreeCartesian k {-<-}con{->-} a (b ⊗ c)-  P1     :: {-<-}con b => {->-} FreeCartesian k {-<-}con{->-} (a ⊗ b) a-  P2     :: {-<-}con a => {->-} FreeCartesian k {-<-}con{->-} (a ⊗ b) b {-<-}+π2     :: {-<-}con a => {->-} Cat k {-<-}con{->-} (a ⊗ b) b {-<-}+π2 = R -assocRight :: (Cat k obj x y) -> (Cat k obj x y)-assocRight (a :.: (assocRight -> (b :.: c))) = (a :.: b) :.: c-assocRight x = x+(▴) :: (con a, con b, con d, TensorClosed con) => (Cat k con a b) -> (Cat k con a d) -> (Cat k con a (b ⊗ d))+f ▴ g = \case Z -> h+              e -> h :∘ e+     where h = f Z :▴: g Z -rightView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c-rightView (assocRight -> (a :.: b)) = a :.: b-rightView x = I :.: x -assocLeft :: (Cat k obj x y) -> (Cat k obj x y)-assocLeft ((assocLeft -> (a :.: b)) :.: c) = a :.: (b :.: c)-assocLeft x = x+-- -- | Make a branch with a possible continuation.+-- -- We do not create (M f Z).+-- toBranch :: (con a, con b, TensorClosed con) => FreeCartesian  k con a b -> Cat k con a b+-- toBranch = \case+--   I -> id+--   (f :.: g) -> toBranch g . toBranch f+--   (Embed φ) -> (φ :.)+--   P1 -> L+--   P2 -> R+--   (f :▵: g) -> \case Z -> h+--                      e -> h :∘ e+--      where h = toTrie f :▴: toTrie g    -leftView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c-leftView (assocLeft -> (a :.: b)) = a :.: b-leftView x = x :.: I+-- toTrie :: (con a, con b, TensorClosed con) => FreeCartesian  k con a b -> Trie k con a b+-- toTrie f = toBranch f Z -pattern (:>:) ::  (obj x, obj y) => (obj b)  => Cat k obj b y -> Cat k obj x b -> Cat k obj x y-pattern f :>: g <- (rightView -> f :.: g)-  where f :>: g = f . g+-- | Insert a morphism (normalised)+ee :: (con a, TensorClosed con,con b, con d, Obj k ~ con, Monoidal k)+  => k a b -> Trie  k con  b d -> (forall c. con c => Trie k con a c -> k c d -> ξ) -> ξ+ee φ Z k = k Z φ -- A morphism at the end of computation. It's connected to the output directly, so because of linearity it will be fully consumed. So we can extract it.+ee φ f k = k (φ :. f) id -pattern (:<:) ::  (obj x, obj y) => (obj b) => (Cat k obj b y) -> (Cat k obj x b) -> Cat k obj x y-pattern f :<: g <- (leftView -> f :.: g)-  where f :<: g = f . g+-- | Insert a fork (normalised). Precondition: f is a Fork.+trieComp :: (con a, TensorClosed con,con b, con d, Obj k ~ con, Monoidal k)+  => Trie k con a b -> Trie k con  b d -> (forall c. con c => Trie k con a c -> k c d -> ξ) -> ξ+trieComp f Z k = normalize f k -- Nothing after, so we expand the fork, so that it can be merged with other branches.+trieComp f g k = k (f :∘ g) id -evalCartesian :: forall k a b con f.-              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),-               con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>-              (forall α β. (con α, con β) => k α β -> f α β)  ->-              Cat k (Obj k) a b -> f a b-evalCartesian embed = \case-  I -> id-  (f :.: g) -> evalCartesian embed f . evalCartesian embed g-  (Embed φ) -> embed φ-  P1 -> exl-  P2 -> exr-  f :▵: g -> evalCartesian embed f ▵ evalCartesian embed g-  +unsafeCoerceSource :: k a b -> k a' b+unsafeCoerceSource = unsafeCoerce -instance Category (Cat k con) where-  type Obj (Cat k con) = con-  id = I-  I ∘ x = x-  x ∘ I = x-  P1 ∘ (f :▵: _) = f-  P2 ∘ (_ :▵: g) = g-  x ∘ y = x :.: y- +-- | Normalised fork, in the case where the heads of the components are not themselves forks.+-- Attempt a merge and return Right if successful, otherwise Left and the ordering of componets.+fork2 :: forall a b c con k ξ. (con a, con b, con c, Monoidal k, TensorClosed con, con ~ Obj k)+  => Trie k con a b -> Trie k con a c -> (forall x. con x => Trie k con a x -> k x (b⊗c) -> ξ) -> Either (Order b c) ξ+fork2 (φ :. f) (_ :. g) k = Right $ fork f (unsafeCoerceSource g) $ \fg s -> ee φ fg $ \φfg t -> k φfg (s . t)+   -- same source ⇒ same morphism. -- (φ∘f ▵ φ∘g) = φ ∘ (f▵g)+fork2 (L Z) (R Z) k  = Right $ k Z id -- π₁ ▵ π₂ = id+fork2 (R Z) (L Z) k  = Right $ k Z swap -- π₂ ▵ π₁ = swap+fork2 (R f) (R g) k  = objprod @con @a // Right $ fork f g $ \fg s -> k (R fg) s -- (π₂∘f ▵ π₂∘g) = π₂ ∘ (f▵g)+fork2 (L f) (L g) k  = objprod @con @a // Right $ fork f g $ \fg s -> k (L fg) s -- shared start+fork2 (x :∘ f) (y :∘ g) k = case compareTries x y of+  EQ -> Right $ fork f g $ \fg s -> trieComp x fg $ \ xfg t -> k xfg (s . t) -- shared start+  LT -> Left LT -- not equal starts, return ordering+  GT -> Left GT+fork2 f g _ = Left (compareTries f g) -- guaranteed not equal morphisms; we return their ordering. -instance ({-<-}ProdObj con, con (), forall a b. (con a, con b) => con (a,b), {->-}Monoidal k) =>  Monoidal (FreeCartesian k {-<-}con{->-}) {-<-}where-  f × g = cartesianCross f g-  assoc = cartesianAssoc-  assoc' = cartesianAssoc'-  swap = cartesianSwap-  unitor = cartesianUnitor-  unitor' = cartesianUnitor'{->-}-instance ({-<-}ProdObj con, con (), forall a b. (con a, con b) => con (a,b),{->-} Monoidal k) => Cartesian (FreeCartesian k {-<-}con{->-}) {-<-}where-  exl = P1-  exr = P2-  dup = id :▵: id-  (▵) = (:▵:){->-}+-- | Normalised fork:+-- 1. Leaves are merged as much as possible.+-- 2. Fork combinators are right associated. (The first component of a fork can never itself be a fork)+-- 3. Leaves are sorted so that equal (heads) can be discovered.+-- (This performs rather badly on a long chain of forks--- but this+-- won't normally happen because we don't have very deeply nested+-- tuples, typically.)+fork :: forall a b c con k ξ. (con a, con b, con c, Monoidal k, TensorClosed con, con ~ Obj k)+  => Trie k con a b -> Trie k con a c -> (forall x. con x => Trie k con a x -> k x (b⊗c) -> ξ) -> ξ+fork (f :▴: g) h k = -- fork on left: reassociate+  fork g h $ \gh s -> fork f gh $ \fgh t -> k fgh (assoc' . (id×s) . t)+fork f (g :▴: h) k =  -- fork on right: attempt merging 1st and 2nd positions+  case fork2 f g $ \fg s ->+    -- attempt sucessful in the contiuation:+       fork fg h $ \lfgh t -> k lfgh (assoc . (s × id)  . t) of+    Right r -> r+    Left c -> case c of+      EQ -> error "fork: missed equality"+      LT -> k (f :▴: (g :▴: h)) id -- already in normal form+      GT ->  -- wrong order, swap necessary (so we're bubble-sorting the chain of forks)+        fork f h $ \fh s ->+        fork g fh $ \gfh t ->+        k gfh (assoc . (swap × id) . assoc' . (id × s) . t)+fork f g k = case fork2 f g k of+  Right r -> r -- sucessful reduction+  Left c -> case c of+    EQ -> error "fork: missed equality"+    LT -> k (f :▴: g) id+    GT -> k (g :▴: f) swap++-- | Recursively normalise. If the input is SMC equivalent in the+-- sense of the paper, the result is Z plus the SMC equivalent+-- morphism.+normalize :: forall a b con k ξ. (Obj k ~ con, Monoidal k, con a, con b, TensorClosed con)+  => Trie k con a b -> (forall c. con c => Trie k con a c -> k c b -> ξ) -> ξ+normalize t0 k = case t0 of+  Z -> k Z id+  f :▴: g -> normalize f $ \f' s -> normalize g $ \g' t -> (fork f' g') $ \f'g u -> k f'g ((s × t) . u)+  L f -> objprod @con @a // normalize f $ \f' s -> k (L f') s+  R f -> objprod @con @a // normalize f $ \f' s -> k (R f') s+  f :∘ g -> normalize g $ \g' s -> trieComp f g' $ \fg' t -> k fg' (s . t)+  φ :. f -> normalize f $ \f' s -> ee φ f' $ \φf' t -> k φf' (s . t)++toSMC :: forall a b con k. (Obj k ~ con, Monoidal k, con a, con b, TensorClosed con) => Cat k con a b -> k a b+toSMC t = normalize (t Z) $ \f g -> case f of+  Z -> g+  _ -> error "toSMC: normalisation process failed"+
Control/Category/Linear.hs view
@@ -25,212 +25,9 @@   -- pattern (:::),   encode, decode, (!:),   -- Helpers for cartesian categories-  ignore, copy, discard+  ignore, copy, discard,+  extract -- debug ) where --import Data.Kind (Type)--import Prelude hiding ((.),id,curry,LT,GT,EQ)-import Control.Category.Constrained-import Control.Category.FreeCartesian as Cartesian-import Unsafe.Coerce-import qualified Control.Category.FreeSMC as SMC------ Linear patterns don't really work, and some version of GHC do not accept this declaration at all. Disabled for now.--- pattern (:::) :: forall con (k :: Type -> Type -> Type) r a b.---                    (Obj k r, Obj k a, Obj k b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) =>---                    P k r a ⊸ P k r b ⊸ P k r (a, b)--- pattern x ::: y <- (split @con -> (x,y))---   where x ::: y = merge @con (x,y)---- infixr ::: -- GHC does not always see this change. rm -r dist/dante. T_T (ghc 8.8.4)---type P :: (Type -> Type -> Type) -> Type -> Type -> Type--ignore      :: (Monoidal k, {-<-} O3 k r a (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-}) => P k r () ⊸ P k r a ⊸ P k r a-mkUnit     :: {-<-}forall k con a r. (Obj k r, Monoidal k, con (), con a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)     => {->-} P k r a ⊸ (P k r a , P k r ())-split    :: {-<-}forall con a b r k. (O3 k r a b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}P k r (a ⊗ b) ⊸ (P k r a, P k r b)-merge    :: {-<-}forall  con a b r k. (O3 k r a b, Monoidal k, con(), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}(P k r a , P k r b) ⊸ P k r (a ⊗ b)-encode   :: {-<-} O3 k r a b => {->-}  (a `k` b) -> (P k r a ⊸ P k r b)-decode   :: {-<-} forall a b k con. (con (), con ~ Obj k, Monoidal k, con a, con b, (forall α β. (con α, con β) => con (α,β))) => {->-} (forall r. {-<-}Obj k r =>{->-} P k r a ⊸ P k r b) -> (a `k` b)--(!:) :: forall  con a b r k. (O3 k r a b, Monoidal k, con(), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)-       => P k r a ⊸ P k r b ⊸ P k r (a,b)-x !: y = merge (x,y)---data P k r a     where-  Y :: FreeCartesian k {-<-} (Obj k) {->-} r a -> P k r a-fromP :: P k r a -> FreeCartesian k {-<-} (Obj k) {->-} r a-fromP (Y f) = f--  -encode φ (Y f)    = Y (Embed φ ∘ f) -- put φ after f.-mkUnit            = split ∘ (encode unitor)-ignore f g        = encode unitor' (merge (g,f))-split (Y f)       = (Y (exl ∘ f), Y (exr ∘ f)) -merge (Y f, Y g)  = Y (f ▵ g)---decode f          = SMC.evalM (reduce (extract f))-extract           :: {-<-} (Obj k a, Obj k b) => {->-} (forall r. {-<-} Obj k r => {->-} P k r a ⊸ P k r b) -> FreeCartesian k {-<-} (Obj k) {->-} a b-extract f         = fromP (f (Y id))--------------------------------------------------------------------------- If the underlying category is cartesian, we have additionally:---  -copy  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-} ) => P k r a ⊸ P k r (a ⊗ a)-copy  = encode dup-discard  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k, con () {->-} ) => P k r a ⊸ P k r ()-discard  = encode dis-------type FreeSMC = SMC.Cat---- haskell-src-exts does not like the ' before constructors. It does not honour extensions either.-type Null = '[]-type Cons x xs = x ': xs--type family Prod (xs :: [Type])  where-  Prod Null = ()-  Prod (Cons x ys) = x ⊗ Prod ys---data Merge k {-<-}con{->-} a xs where-  (:+)   :: {-<-}(con x, con (Prod xs)) => {->-}FreeCartesian k {-<-}con{->-} a x -> Merge k {-<-}con{->-} a xs-         -> Merge k {-<-}con{->-}  a (Cons x xs)-  Nil    :: Merge k {-<-}con{->-} a Null--infixr :+----- | expose does two things:--- 1. push abstract morphisms (E, X) into the already processed part--- 2. turn f ▵ g into a Merge--expose  ::  (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b) => {->-}Cat cat {-<-}con{->-} a b ->-            (  forall x. con (Prod x) => FreeSMC cat con (Prod x) b -> Merge cat con a x -> k) -> k-expose (f1 :▵: f2) k      =  expose f1 $ \g1 fs1 ->-                             expose f2 $ \g2 fs2 ->-                             appendSorted fs1 fs2 $ \g fs ->-                             k ((g1 × g2) ∘ g) fs-expose (Embed ϕ :<: f) k  =  expose f $ \g fs ->-                             k (SMC.Embed ϕ ∘ g) fs-expose x k                = k unitor' (x :+ Nil)---- | Merge L/R pair--reduceStep  ::  {-<-}(ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con (Prod xs)) =>{->-} Merge cat {-<-}con{->-} a xs ->-                (  forall zs. {-<-}con (Prod zs) => {->-}FreeSMC cat {-<-}con{->-} (Prod zs) (Prod xs)  ->-                  Merge cat {-<-}con{->-} a zs -> k) -> k--- There exists at least one pair of the form L :<: f and R :<: f if--- already maximally exposed. So we do not handle the base cases here.---- If R :<: f is the first in the order, then L :<: f also exists;--- and it should be first, so the case (R :<: f) :+ (L :<: f) isn't a possible merge.-reduceStep ((P1 :<: f₁) :+ (P2 :<: f₂) :+ rest) k-  | EQ <- compareMorphisms f₁ f₂ =-  expose f₁               $ \g f' -> -- expose any fork (▵) in f₁-  appendSorted f' rest    $ \g' rest' -> -- insert the exposed stuff in a sorted way-  k (assoc ∘ (g × id) ∘ g') rest'-reduceStep (f :+ rest) k =-  reduceStep rest                    $ \g rest' ->-  appendSorted (f :+ Nil) rest'  $ \g' rest'' ->-  k ((unitor' × g) ∘ g') rest''-  -appendSorted  :: {-<-}(ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con (Prod xs), con (Prod ys)) => {->-} Merge cat {-<-}con{->-} a xs -> Merge cat {-<-}con{->-} a ys ->-                 (  forall zs. {-<-}con(Prod zs)=> {->-}FreeSMC cat {-<-}con{->-}  (Prod zs)-                                                                                   (Prod xs ⊗ Prod ys)  ->-                    Merge cat{-<-}con{->-} a zs -> k) -> k-appendSorted  Nil        ys         k = k (swap ∘  unitor)  ys-appendSorted  xs         Nil        k = k          unitor   xs-appendSorted  (x :+ xs)  (y :+ ys)  k =-  case compareMorphisms x y of-    GT  ->   appendSorted (x :+ xs) ys $ \a zs ->-             k (assoc ∘ (swap × id) ∘  assoc' ∘ (id × a))  (y :+ zs)-    _   ->   appendSorted xs (y :+ ys) $ \a zs ->-             k (                       assoc' ∘ (id × a))  (x :+ zs)---- | intermediate result-data R cat con a b where-  St :: con (Prod b)-    => FreeSMC k con (Prod b) c -- already processed part (SMC here)-    -> Merge k con a b -- maximally exposed and sorted merge tree (see 'expose' below)-    -> R k con a c---- | Perform 1 reduction step, assumes input is already maximally exposed and sorted. -reductionStep :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b) => R cat con a b -> R cat con a b-reductionStep (St r1 (f :+ Nil)) = expose f $ \ready m -> St (r1 . unitor . ready) m  -- single morphism to analyse-reductionStep (St r1 m) = reduceStep m $ \r2 m' -> St (r1 . r2) m' -- L/R pair to find and reduce---- | Perform all reduction steps and return intermediate states-reductionSteps  :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), -               con a, con b) => R cat con a b -> [R cat con a b]-reductionSteps st@(St _ Nil) = [st] -- done; and all the input is discarded-reductionSteps st@(St _ (I :+ Nil)) = [st] -- done!-reductionSteps st = st : reductionSteps (reductionStep st)--freeToR :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (),-           con x) => Cat k con a x -> R k con a x-freeToR f = St unitor' (f :+ Nil)--rToFree :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b)-        => R cat con a b -> FreeSMC cat con a b-rToFree (St done Nil) = unsafeCoerce done--- why is the above safe? (St _ Nil) means that the whole input is--- discarded/the whole expression has no free variable. In other--- words, the input is the unit type. So we can coerce. ------ Other explanation:--- Our input is (f id), with f : (r `k` a) ⊸ r `k` b--- We know that (f id) starts with discard.  Because f is linear, (f--- id) can discard its input only if the input type is the unit in the--- first place, hence a=().-rToFree (St done (I :+ Nil)) = done . unitor--reduce  :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (),-             con a, con b) => Cartesian.Cat cat con a b -> FreeSMC cat con a b-reduce = rToFree . last . reductionSteps . freeToR---- Invariant: same source!-compareMorphisms :: (con a, con b, con c) => Cat cat con a b -> Cat cat con a c -> Order b c-compareMorphisms I I = EQ-compareMorphisms I _ = LT-compareMorphisms _ I = GT-compareMorphisms (f Cartesian.:>: g) (f' Cartesian.:>: g') =-  case compareAtoms g g' of-    LT -> LT-    GT -> GT-    EQ -> compareMorphisms f f'---- Invariant: same source!-compareAtoms :: (con a, con b, con c) => Cat cat con a b -> Cat cat con a c -> Order b c-compareAtoms P1 P1 = EQ-compareAtoms P2 P2 = EQ-compareAtoms (Embed _) (Embed _) = unsafeCoerce EQ -- Same source -> same Atoms-compareAtoms (f :▵: g) (f' :▵: g') = case compareMorphisms f f' of-  LT -> LT-  GT -> GT-  EQ -> case compareMorphisms g g' of-    LT -> LT-    GT -> GT-    EQ -> EQ-compareAtoms P1 _ = LT-compareAtoms _ P1 = GT-compareAtoms P2 _ = LT-compareAtoms _ P2 = GT-compareAtoms (Embed _) _ = LT-compareAtoms _ (Embed _) = GT-compareAtoms f g = error ("compareAtoms:\n" ++ showDbg 0 f "\n" ++ showDbg 0 g "" )+import Control.Category.Linear.Internal
+ Control/Category/Linear/Internal.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE UnicodeSyntax #-}+++module Control.Category.Linear.Internal where++import Data.Kind (Type)++import Prelude hiding ((.),id,curry,LT,GT,EQ)+import Control.Category.Constrained+import Control.Category.FreeCartesian as FC+-- import Control.Category.Show as Show+-- import qualified Control.Category.InitialSMC as Init++-- Linear patterns don't really work, and some version of GHC do not accept this declaration at all. Disabled for now.+-- pattern (:::) :: forall con (k :: Type -> Type -> Type) r a b.+--                    (Obj k r, Obj k a, Obj k b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) =>+--                    P k r a ⊸ P k r b ⊸ P k r (a, b)+-- pattern x ::: y <- (split @con -> (x,y))+--   where x ::: y = merge @con (x,y)++-- infixr ::: -- GHC does not always see this change. rm -r dist/dante. T_T (ghc 8.8.4)+++type P :: (Type -> Type -> Type) -> Type -> Type -> Type++++split    :: {-<-}forall con a b r k. (O3 k r a b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}P k r (a ⊗ b) ⊸ (P k r a, P k r b)+merge    :: {-<-}forall  con a b r k. (O3 k r a b, Monoidal k, con(), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}(P k r a , P k r b) ⊸ P k r (a ⊗ b)+encode   :: {-<-} (O3 k r a b, TensorClosed con, con ~ Obj k) => {->-}  (a `k` b) -> (P k r a ⊸ P k r b)++(!:) :: forall  con a b r k. (O3 k r a b, Monoidal k, con(), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)+       => P k r a ⊸ P k r b ⊸ P k r (a,b)+x !: y = merge (x,y)+++data P k r a     where+  Y :: Cat k {-<-} (Obj k) {->-} r a -> P k r a+fromP :: P k r a -> Cat k {-<-} (Obj k) {->-} r a+fromP (Y f) = f++  +encode φ (Y f)    = Y (f ∘ embed φ) -- put φ after f.+split (Y f)       = (Y (f ∘ π1), Y (f ∘ π2)) +merge (Y f, Y g)  = Y (f ▴ g)++decode   :: {-<-} forall a b k con. (con (), con ~ Obj k, Monoidal k, con a, con b, (forall α β. (con α, con β) => con (α,β))) => {->-} (forall r. {-<-}Obj k r =>{->-} P k r a ⊸ P k r b) -> (a `k` b)+decode f          = toSMC (extract f)++extract           :: {-<-} (Obj k a, Obj k b) => {->-} (forall r. {-<-} Obj k r => {->-} P k r a ⊸ P k r b) -> Cat k {-<-} (Obj k) {->-} a b+extract f         = fromP (f (Y id))++ignore      :: (Monoidal k, {-<-} O3 k r a (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-}) => P k r () ⊸ P k r a ⊸ P k r a+ignore f g  = encode unitor' (merge (g,f))++mkUnit   :: {-<-}forall k con a r. (Obj k r, Monoidal k, con (), con a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)         => {->-}P k r a ⊸ (P k r a, P k r ())+mkUnit x = split (encode unitor x) ++---------------------------------------------------------------------+-- If the underlying category is cartesian, we have additionally:+  +copy  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-} ) => P k r a ⊸ P k r (a ⊗ a)+copy  = encode dup+discard  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k, con () {->-} ) => P k r a ⊸ P k r ()+discard  = encode dis
+ Control/Category/StructuredObject.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE UnicodeSyntax #-}++module Control.Category.StructuredObject where++import Control.Category.Constrained+import Prelude hiding (id, (.))+import Data.Array (Ix)+import Data.Constraint (Dict(..),Constraint)++-- representation for the objects+data Repr s a where+  RUnit :: Repr s ()+  RPair :: Repr s a -> Repr s b -> Repr s (a,b)+  RAtom :: Repr s (Atom s)+  RDual :: Repr s a -> Repr s (Dual a)++-----------------+-- OO+class OO s a where+  type Sub s t a+  getRepr :: Repr s a+  subOO :: forall c b. (OO s a, a ~ (c ⊗ b)) => Dict (OO s c, OO s b)+  subOO = error "not a product"+  dualOO :: forall z. (OO s a, a ~ Dual z) => Dict (OO s z)+  dualOO = error "not a dual"+  toList :: a -> [s]++type Structured s con = forall x. con x => OO s x :: Constraint++type Basic s = (Bounded s, Enum s, Ix s)++instance OO s () where+  type Sub s t () = ()+  getRepr = RUnit+  toList () = []+instance Basic s => OO s (Atom s) where+  type Sub s t (Atom s) = Atom t+  getRepr = RAtom+  toList (Atom x) = [x]+instance OO s a => OO s (Dual a) where+  type Sub s t (Dual a) = Dual (Sub s t a)+  getRepr = RDual getRepr+  dualOO = Dict+  toList (Dual a) = toList a++mapRepr :: forall t s a. Repr s a -> Repr t (Sub s t a)+mapRepr RAtom = RAtom+mapRepr RUnit = RUnit+mapRepr (RPair q r) = RPair (mapRepr q) (mapRepr r)+mapRepr (RDual r) = RDual (mapRepr r)++instance (OO s a, OO s b) => OO s (a⊗b) where+  toList (a,b) = toList a <> toList b+  type Sub s t (a,b) = (Sub s t a,Sub s t b)+  getRepr = RPair getRepr getRepr+  subOO = Dict++instance ProdObj (OO s) where+  prodobj = Dict+  objprod = subOO+  objunit = Dict++instance AutonomousObj (OO s) where+  objDual = Dict+  dualObj :: forall z a con. (z ~ Dual a, con z, con ~ OO s) => Dict (con a)+  dualObj = dualOO @s @z+++
+ Control/Category/Tensors.hs view
@@ -0,0 +1,207 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UnicodeSyntax #-}+module Control.Category.Tensors (R,+                                 constant, zeroTensor, delta, contract, deriv, juggleDown, juggleUp, plus, (⋆),+                                 tensorEval, tensorEval1, tensorEmbed, tensorEmbed1,+                                 affinity, derivUsingAffinity,++                                 TensorCategory(..), CoordinateCategory(..), AutonomousObj(..),+                                 Group(..), VectorSpace(..), Dual(..)) where++import Data.Kind+import Control.Category.Constrained+import Control.Category.StructuredObject+import Control.Category.Linear.Internal+import qualified Control.Category.FreeCartesian as FC+import Control.Category.FreeCartesian ((▴))+import Prelude hiding (id, (.), Num(..), uncurry)++class Group v where+  (+)     :: v -> v -> v+  zero    :: v+  negate  :: v -> v++class Group v => VectorSpace scalar v where+  (*^)  ::  scalar -> v -> v++type DualClosed (con :: Type -> Constraint) =+  forall x. (con x) => con (Dual x) :: Constraint+++class Autonomous cat => TensorCategory v cat where+  metric          :: {-<-}(O2 cat v Unit) =>{->-} (v ⊗ v) `cat` Unit+  cometric        :: {-<-}(O2 cat v Unit) =>{->-} Unit `cat` (v ⊗ v)+  derivSemantics  :: {-<-}O3 cat a b v =>{->-} (a `cat` b) -> ((v ⊗ a) `cat` b)+  default derivSemantics  :: {-<-}(O3 cat a b v, Obj cat ~ con, TensorClosed con, GroupCat cat, v ~ Atom s, OO s a, OO s b, CoordinateCategory v cat, con ()) =>{->-} (a `cat` b) -> ((v ⊗ a) `cat` b)+  derivSemantics = derivUsingAffinity+++juggleDown :: (con ~ Obj cat, TensorClosed con, DualClosed con, AutonomousObj con, TensorCategory v cat, con v, con ())+  => Dual v `cat` v+juggleDown = compactHelper2 cometric++juggleUp :: (con ~ Obj cat, TensorClosed con, DualClosed con, AutonomousObj con, TensorCategory v cat, con v, con ())+  => v `cat` Dual v+juggleUp = compactHelper1 metric++compactHelper1 :: (Autonomous k, Obj k ~ con, DualClosed con, TensorClosed con, con a, con b, con ()) => k (a ⊗ b) () -> k a (Dual b)+compactHelper1 f = unitor' ∘ (id × f) ∘ assoc . (swap × id) . assoc' . (id × turn) ∘ unitor++compactHelper2 :: (Autonomous k, Obj k ~ con, DualClosed con, TensorClosed con, con a, con b, con ()) => k () (a ⊗ b) -> k (Dual a) b+compactHelper2 f = unitor' ∘ swap ∘ ((turn' ∘ swap) × id) ∘ assoc' ∘ (id × f) ∘ unitor+++shuf ::+  ( Monoidal k+  , con ~ Obj k+  , TensorClosed con+  , con a, con s, con b+  ) => (a ⊗ (s ⊗ b)) `k` (s ⊗ (a ⊗ b))+shuf = assoc ∘ (swap × id) ∘ assoc'++++class TensorCategory v cat => CoordinateCategory v cat  where+  partialDerivative :: O3 cat a b v => (a `cat` b) -> ((v ⊗ a) `cat` b)+  christoffel     :: {-<-}(Obj cat v)=>{->-} (v ⊗ v) `cat` v+++derivUsingAffinity :: forall a b v s k con.+  (AutonomousObj con, TensorClosed con, OO s a, OO s b, v ~ Atom s,+   con a, con b, con v, con (),+   GroupCat k, CoordinateCategory v k, Obj k ~ con )+  => k a b -> k (v ⊗ a) b+derivUsingAffinity t = partialDerivative t + negate (t ∘ affinity) + (affinity ∘ (id × t))+++type AdditiveCat scalar (cat :: Type -> Type -> Type) = forall a b. VectorSpace scalar (a `cat` b)+type GroupCat (cat :: Type -> Type -> Type) = forall a b. Group (a `cat` b)++data S cat r where+  Compose  :: {-<-}Obj cat x => {->-} (x `cat` Unit) -> FC.Cat cat {-<-}(Obj cat){->-} r x -> S cat r+  Plus   :: (Bool -> S cat r) ⊸ S cat r+type R cat r = P cat r Unit ⊸ S cat r++++constant      :: (Monoidal cat, AdditiveCat scalar cat {-<-},con r, con a, Autonomous cat, Obj cat ~ con, DualClosed con, TensorClosed con, con (){->-})+  => scalar -> R cat r+constant s (Y u) = Compose (s *^ id) u+++++zeroTensor = tensorEmbed1 zero++plus f u = Plus (\b -> f b u) ++Compose t1 q1  ⋆- Compose t2 q2  = Compose (unitor' ∘ (t1 × t2)) (q1 ▴ q2)+Plus f         ⋆- t              = Plus (\c -> f c ⋆- t)+t              ⋆- Plus f         = Plus (\c -> t ⋆- f c)++deriv'         :: {-<-} forall v cat con r. (con v, TensorClosed con, con ~ Obj cat, con r, con (), Monoidal cat, ProdObj con) =>{->-} (TensorCategory v cat) => P cat r v ⊸ S cat r ⊸ S cat r+deriv'  (Y i)  (Compose t q)  = Compose (derivSemantics t) (i ▴ q)+deriv'  p      (Plus f )      = Plus (\c -> deriv' p (f c) )+++deriv i r u = deriv' i (r u)++cartesianToMonoidal  :: {-<-}(Obj cat~con,Monoidal cat, ProdObj con, TensorClosed con, con (), con a, con b) => {->-} FC.Cat cat {-<-}con{->-} a b -> a `cat` b+cartesianToMonoidal = FC.toSMC++tensorEval0'   :: ({-<-}Obj cat ~ con, con a, TensorClosed con, ProdObj con, con (), {->-}Monoidal cat, GroupCat  cat) => S cat a -> a `cat` Unit+tensorEval0' u = case u of+  (Compose t q)  -> t ∘ cartesianToMonoidal q+  Plus f         -> tensorEval0' (f True) + tensorEval0' (f False)++tensorEval1 f          = tensorEval0' (uncurry f (Y (FC.embed unitor)))+tensorEval f         = unitor' . swap . (tensorEval1 (uncurry f) × id) . assoc' . (id × turn) . unitor+tensorEmbed1 f (Y q) (Y u) = Compose (f ∘ unitor') (q ▴ u)+tensorEmbed t i j     = tensorEmbed1 (turn' ∘ (t × id)) (merge (i,j))+++delta'         :: {-<-}(Autonomous cat, TensorClosed obj, DualClosed obj, Obj cat ~ obj, obj a, obj (), obj r) => {->-}P cat r a ⊸ P cat r (Dual a) ⊸ S cat r+delta' (Y i) (Y j) = Compose turn' (i ▴ j)++delta i j u = eatU u (delta' i j)++type U cat r = P cat r Unit++eatU :: (con ~ Obj cat, TensorClosed con, ProdObj con, con r, con (), Monoidal cat) => U cat r ⊸ S cat r ⊸ S cat r+eatU (Y f) (Compose φ g) = Compose (φ ∘ unitor') (g ▴ f)+eatU p (Plus f) = Plus (\b -> eatU p (f b))+++tensorEmbed   :: ({-<-}Obj cat ~ con, con a, con b, TensorClosed con, DualClosed con, ProdObj con, con (), {->-}Autonomous cat) => (a `cat` b) -> (forall r. {-<-} con r => {->-} P cat r a ⊸ P cat r (Dual b) ⊸ R cat r)+tensorEmbed1  :: ({-<-}Obj cat ~ con, con a, TensorClosed con, ProdObj con, con (), {->-}Monoidal cat) => (a `cat` Unit) -> (forall r. {-<-}  con r => {->-} P cat r a ⊸ R cat r)++tensorEval    :: ({-<-}Obj cat ~ con, con a, con b, DualClosed con, TensorClosed con, ProdObj con, con (), {->-}Autonomous cat, GroupCat  cat) => (forall r. {-<-} con r => {->-} P cat r a ⊸ P cat r (Dual b) ⊸ R cat r) -> a `cat` b+tensorEval1    :: ({-<-}Obj cat ~ con, con a, TensorClosed con, ProdObj con, con (), {->-}Monoidal cat, GroupCat cat) => (forall r. {-<-} con r => {->-} P cat r a ⊸ R cat r) -> a `cat` Unit++zeroTensor    :: (GroupCat cat, Autonomous cat{-<-}, Obj cat ~ con, con r, con a,  DualClosed con, TensorClosed con, con (){->-}) => P cat r a ⊸ R cat r++plus          :: (Bool -> R cat r) ⊸ R cat r+(⋆)           :: (Monoidal cat {-<-}, O2 cat r (), TensorClosed con, con ~ Obj cat {->-}) => R cat r ⊸ R cat r ⊸ R cat r+(⋆-)      :: (Monoidal cat, {-<-} O2 cat r (), TensorClosed con, con ~ Obj cat {->-}) => S cat r ⊸ S cat r ⊸ S cat r+(f ⋆ g) u = dupU u & \(u1,u2) -> f u1 ⋆- g u2++dupU :: (Monoidal cat,con ~ Obj cat, TensorClosed con, ProdObj con, con r, con Unit) => U cat r ⊸ (U cat r,U cat r)+dupU = split ∘ (encode unitor)++delta         :: {-<-}(Autonomous cat, TensorClosed obj, DualClosed obj, Obj cat ~ obj, obj a, obj (), obj r) => {->-}P cat r a ⊸ P cat r (Dual a) ⊸ R cat r+contract :: {-<-}(Autonomous cat, con ~ Obj cat, con a, con r, con (), con (Dual a), TensorClosed con, DualClosed con) => {->-}(P cat r (Dual a) ⊸ P cat r a ⊸ R cat r) ⊸ R cat r+contract f u = uncurry (uncurry f) (encode ((turn × id) . unitor) u) ++deriv         :: {-<-}forall v cat con r.  (con v, TensorClosed con, con ~ Obj cat, con r, con (), Monoidal cat, ProdObj con) =>{->-} (TensorCategory v cat) => P cat r v ⊸ R cat r ⊸ R cat r++uncurry   :: (Monoidal cat {-<-} , O3 cat r a b, con (), TensorClosed con, con ~ Obj cat{->-})  =>  (P cat r a ⊸ P cat r b ⊸ k) ⊸ (P cat r (a⊗b) ⊸ k)+uncurry f p = split p & \case (a,b) -> f a b++(&) ::  a ⊸ (a ⊸ b) ⊸ b+x & f = f x+++affinity :: forall v a s k con.+            (con ~ Obj k, OO s a, con a, con v, con (), v ~ Atom s,+             TensorClosed con, AutonomousObj con, GroupCat k,+             TensorCategory (Atom s) k,CoordinateCategory (Atom s) k)+         => k (Atom s ⊗ a) a+affinity = aff getRepr++aff :: forall s k con a.+       (con ~ Obj k, con a, con (Atom s), con (),+        TensorClosed con, AutonomousObj con, TensorCategory (Atom s) k,+        GroupCat k, CoordinateCategory (Atom s) k)+    => Repr s a -> k (Atom s ⊗ a) a+aff = \case+  RAtom -> christoffel+  RUnit -> zero+  RPair p q ->+    objprod @con @a //+    ((aff p × id) ∘ assoc') + ((id × aff q) ∘ shuf)+  RDual q ->+    dualObj @con @a //+    negate (unitor' . swap .+           (turn' × id) .+           assoc' . (id × swap) . assoc .+           ((( aff q × id) . assoc' . (id × (swap . turn) ) . unitor) × id))
linear-smc.cabal view
@@ -1,8 +1,31 @@-Cabal-Version:  3.0-name:           linear-smc-version:        2.0.2-category:       control+cabal-version:      3.0+-- The cabal-version field refers to the version of the .cabal specification,+-- and can be different from the cabal-install (the tool) version and the+-- Cabal (the library) version you are using. As such, the Cabal (the library)+-- version used must be equal or greater than the version stated in this field.+-- Starting from the specification version 2.2, the cabal-version field must be+-- the first thing in the cabal file.++-- Initial package description 'linear-smc' generated by+-- 'cabal init'. For further documentation, see:+--   http://haskell.org/cabal/users-guide/+--+-- The name of the package.+name:               linear-smc++-- The package version.+-- See the Haskell package versioning policy (PVP) for standards+-- guiding when and how versions should be incremented.+-- https://pvp.haskell.org+-- PVP summary:     +-+------- breaking API changes+--                  | | +----- non-breaking API additions+--                  | | | +--- code changes with no API change+version:            2.2.2++-- A short (one-line) description of the package. synopsis:       Build SMC morphisms using linear types++-- A longer description of the package. description:   A number of domain specific languages, such as circuits or   data-science workflows, are best expressed as diagrams of boxes@@ -12,26 +35,61 @@   allows one to program SMCs with linear functions instead of SMC   combinators. This is done without resorting to template haskell or compiler plugins.   The rationale, design and implementation of this library is provided by the paper  "Evaluating Linear Functions to Symmetric Monoidal Categories", by Jean-Philippe Bernardy and Arnaud Spiwack, appearing at Haskell Symposium 2021.-license:        LGPL-3.0-or-later-license-file:   LICENSE-author:         Jean-Philippe Bernardy-maintainer:     jeanphilippe.bernardy@gmail.com-tested-with:    GHC==9.0.2-build-type:     Simple +-- The license under which the package is released.+license:            LGPL-3.0-or-later++-- The file containing the license text.+license-file:       LICENSE++-- The package author(s).+author:             Jean-Philippe Bernardy++-- An email address to which users can send suggestions, bug reports, and patches.+maintainer:         jeanphilippe.bernardy@gmail.com++-- A copyright notice.+-- copyright:+category:           Math+build-type:         Simple++-- Extra source files to be distributed with the package, such as examples, or a tutorial module.+-- extra-source-files:++common warnings+    ghc-options: -Wall+ library-  build-depends:       base >=4.13 && < 666-  build-depends: constraints >= 0.13.4 && < 666+    -- Import common warning flags.+    import:           warnings -  default-language: Haskell2010-  exposed-modules:-    Control.Category.Constrained-    Control.Category.Linear-  other-modules:-    Control.Category.FreeSMC-    Control.Category.FreeCartesian-    +    -- Modules exported by the library.+    exposed-modules:+      Control.Category.Constrained+      Control.Category.Linear+      Control.Category.Tensors+    other-modules:+      Control.Category.FreeSMC+      Control.Category.FreeCartesian+      Control.Category.Linear.Internal+      Control.Category.StructuredObject+    -- Modules included in this library but not exported.+    -- other-modules: +    -- LANGUAGE extensions used by modules in this package.+    -- other-extensions:++    -- Other library packages from which modules are imported.+    build-depends: constraints >= 0.13.4 && < 666+    build-depends: array >= 0.5 && < 666+    build-depends:    base >=4.16.4.0 && < 666++    -- Directories containing source files.+    hs-source-dirs:   .++    -- Base language which the package is written in.+    default-language: Haskell2010+ Test-Suite test-unitary   build-depends: constraints   build-depends: array >= 0.5.4 && < 666@@ -39,4 +97,3 @@   type:       exitcode-stdio-1.0   main-is:    examples/Unitary.hs   build-depends: base-