linear-smc (empty) → 1.0.0
raw patch · 7 files changed
+1503/−0 lines, 7 filesdep +arraydep +basedep +constraints
Dependencies added: array, base, constraints
Files
- Control/Category/Constrained.hs +247/−0
- Control/Category/FreeCartesian.hs +141/−0
- Control/Category/FreeSMC.hs +418/−0
- Control/Category/Linear.hs +235/−0
- LICENSE +166/−0
- examples/Unitary.hs +254/−0
- linear-smc.cabal +42/−0
+ Control/Category/Constrained.hs view
@@ -0,0 +1,247 @@+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RecursiveDo #-}+{-# LANGUAGE LinearTypes #-}++module Control.Category.Constrained where++import Prelude hiding ((.),id)+import Data.Kind+import Data.Constraint+import Data.Type.Equality+++type O2 k a b = (Obj k a, Obj k b)+type O3 k a b c =+ (Obj k a, Obj k b, Obj k c)+type O4 k a b c d =+ (Obj k a, Obj k b, Obj k c, Obj k d)++type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where+ All c '[] = ()+ All c (x ': xs) = (c x, All c xs)+ ++class Trivial a+instance Trivial a++instance ProdObj Trivial where+ prodobj = Dict+ objprod = Dict+ objunit = Dict+++class Category k where+ type Obj k :: Type -> Constraint {-<-}+ type Obj k = Trivial {->-}+ id :: Obj k a => a `k` a+ (∘) :: (Obj k a, Obj k b, Obj k c) =>+ (b `k` c) -> (a `k` b) -> a `k` c++infixl 8 .+infixl 8 ∘++(.) :: (Category k, O3 k a b c) => k b c -> k a b -> k a c+(.) = (∘)++class ProdObj con where+ prodobj :: (con a, con b) => Dict (con (a⊗b))+ objprod :: forall z a b. (z ~ (a⊗b), con z) => Dict (con a, con b)+ objunit :: Dict (con ())++objProd :: forall k a b z. (z ~ (a⊗b), Obj k z, Monoidal k) => Dict (Obj k a, Obj k b)+objProd = objprod++prodObj :: forall k a b. (Monoidal k, Obj k a, Obj k b) => Dict (Obj k (a⊗b))+prodObj = prodobj++unitObj :: forall k. (Monoidal k) => Dict (Obj k ())+unitObj = objunit+++infixr 0 //+(//) :: Dict c -> (c => k) -> k+Dict // k = k++type a ⊗ b = (a,b)+infixr 7 ⊗+++class ({-<-}ProdObj (Obj k),{->-}Category k) => Monoidal k where+ (×) :: {-<-}(Obj k a, Obj k b, Obj k c, Obj k d) =>{->-} (a `k` b) -> (c `k` d) -> (a ⊗ c) `k` (b ⊗ d)+ swap :: {-<-}(Obj k a, Obj k b) =>{->-} (a ⊗ b) `k` (b ⊗ a)+ assoc :: {-<-}(Obj k a, Obj k b, Obj k c) =>{->-} ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))+ assoc' :: {-<-}(Obj k a, Obj k b, Obj k c) =>{->-} (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)+ unitor :: {-<-}(Obj k a) =>{->-} a `k` (a ⊗ ())+ unitor' :: {-<-}(Obj k a) =>{->-} (a ⊗ ()) `k` a++class Monoidal k => Cartesian k where+ exl :: {-<-} forall a b. O2 k a b => {->-} (a ⊗ b) `k` a+ exr :: {-<-} forall a b. O2 k a b => {->-} (a ⊗ b) `k` b+ dis :: {-<-} forall a. Obj k a => {->-} a `k` ()+ dup :: {-<-} (Obj k a, Obj k (a⊗a)) => {->-} a `k` (a ⊗ a)+ (▵) :: {-<-} forall a b c. (Obj k a,Obj k b, Obj k c) => {->-} (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)++ {-<-}+ {-# MINIMAL exl,exr,dup | exl,exr,(▵) | dis,dup | dis,(▵) #-}+ dis = disDefault+ dup = id ▵ id+ exl = exlDefault+ exr = exrDefault+ (▵) = (▵!)+ {->-}++disDefault :: forall k a. (Cartesian k, Obj k a) => a `k` ()+disDefault = exr . unitor+ \\ prodObj @k @a @()+ \\ unitObj @k++exlDefault :: forall k a b. (Cartesian k, O2 k a b) => (a ⊗ b) `k` a+exlDefault = unitor' . (id × dis)+ \\ prodObj @k @a @b+ \\ prodObj @k @a @()+ \\ unitObj @k++exrDefault :: forall k a b. (Cartesian k, O2 k a b) => (a ⊗ b) `k` b+exrDefault = unitor' ∘ swap ∘ (dis × id)+ \\ prodObj @k @a @b+ \\ prodObj @k @b @()+ \\ prodObj @k @() @b+ \\ unitObj @k++(▵!) :: forall k a b c. (Cartesian k, O3 k a b c) => (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)+f ▵! g = (f × g) . dup+ \\ prodObj @k @a @a+ \\ prodObj @k @b @c++cartesianCross :: (Obj k (b1 ⊗ b2), Obj k b3, Obj k c, Obj k b1,+ Obj k b2, Cartesian k) =>+ k b1 b3 -> k b2 c -> k (b1 ⊗ b2) (b3 ⊗ c)+cartesianCross a b = (a . exl) ▵ (b . exr)+cartesianUnitor :: forall a k. (Obj k a, Obj k (), Cartesian k) => a `k` (a ⊗ ())+cartesianUnitor = id ▵ dis++cartesianUnitor' :: forall a k. (Obj k a, Obj k (), Cartesian k) => (a ⊗ ()) `k` a+cartesianUnitor' = exl++cartesianSwap :: forall a b k. (Obj k a, Obj k b, Cartesian k) => (a ⊗ b) `k` (b ⊗ a)+cartesianSwap = exr ▵ exl+ \\ prodObj @k @a @b++cartesianAssoc :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))+cartesianAssoc = (exl . exl) ▵ ((exr . exl) ▵ exr)+ \\ prodObj @k @(a,b) @c+ \\ prodObj @k @a @b+ \\ prodObj @k @b @c++cartesianAssoc' :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)+cartesianAssoc' = (exl ▵ (exl . exr)) ▵ (exr . exr)+ \\ prodObj @k @a @(b,c)+ \\ prodObj @k @a @b+ \\ prodObj @k @b @c++++class Monoidal k => CoCartesian k where+ inl :: {-<-} O2 k a b => {->-} a `k` (a ⊗ b)+ inr :: {-<-} O2 k a b => {->-} b `k` (a ⊗ b)+ new :: {-<-} forall a. (Obj k a) => {->-} () `k` a+ jam :: {-<-} Obj k a => {->-} (a⊗a) `k` a+ (▿) :: {-<-} forall a b c. (Obj k a,Obj k b, Obj k c) => {->-} (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a++ {-<-}+ jam = id ▿ id+ new = newDefault+ (▿) = (▿!)+ {->-}++jamDefault :: (Obj k a, CoCartesian k) => (a⊗a) `k` a+jamDefault = id ▿ id++newDefault :: forall k a. (Obj k a, CoCartesian k) => () `k` a+newDefault = unitor' . inr+ \\ prodObj @k @a @()+ \\ unitObj @k++(▿!) :: forall k a b c. (O3 k a b c, CoCartesian k) => (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a+f ▿! g = jam . (f × g)+ \\ prodObj @k @a @a+ \\ prodObj @k @b @c++transp :: forall a b c d k con . (con ~ Obj k, Monoidal k, O4 k a b c d, (forall α β. (con α, con β) => con (α,β)))+ => ((a,b) ⊗ (c,d)) `k` ((a,c) ⊗ (b,d))+transp = assoc' . (id × (assoc . (swap × id) . assoc')) . assoc++-- -- Poor man's infix arrows.+-- -- http://haskell.1045720.n5.nabble.com/Type-operators-in-GHC-td5154978i20.html+-- type a - (c :: * -> * -> *) = c a+-- type c > b = c b++-- infix 2 -+-- infix 1 >+++class Cartesian k => Closed k where+ -- expObj' :: forall a b. SObj k a -> SObj k b -> SObj k (a -> b)+ apply :: O2 k a b => ((a -> b) ⊗ a) `k` b+ curry :: O3 k a b c => ((a ⊗ b) `k` c) -> (a `k` (b -> c))+++class Invertible k where+ dual :: (a `k` b) -> b `k` a++type Hopf k = (Cartesian k, CoCartesian k)+ -- (laws unstated as usual...)+ -- jam . dup = id+ -- etc.++instance Category (FUN x) where+ id = \x -> x+ f ∘ g = \x -> f (g x)++instance Monoidal (FUN m) where+ (f × g) (a,b) = (f a, g b)+ assoc ((x,y),z) = (x,(y,z)) + assoc' (x,(y,z)) = ((x,y),z) + swap (x,y) = (y,x)+ unitor = (,())+ unitor' (x,()) = x++instance Cartesian (->) where+ exl = fst+ exr = snd+ (f ▵ g) x = (f x, g x)+ dup x = (x,x)++instance Closed (->) where+ apply (f,x) = f x+ curry = Prelude.curry++type Comparator k = forall a b b'. k a b -> k a b' -> Maybe (b :~: b')++class Category k => HasCompare k where+ compareMorphs :: Comparator k++-- | Equality-witnessing order type+data Order a b where+ LT, GT :: Order a b+ EQ :: Order a a
+ Control/Category/FreeCartesian.hs view
@@ -0,0 +1,141 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE LinearTypes #-}++module Control.Category.FreeCartesian where++import Prelude hiding ((.),id,curry)+import Control.Category.Constrained+import Data.Kind++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"+ E -> showString "ε"+ 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)++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 "π₁"+ E -> showString "ε"+++parens :: [Char] -> [Char]+parens x = "(" <> x <> ")"++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+ E -> E+ P1 -> P1+ P2 -> P2+ a :▵: b -> mapGenerators f a :▵: mapGenerators f b+ x -> error (showDbg 0 x " (Free.mapGenerators)")++type Cat = FreeCartesian++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 {-<-}+ E :: FreeCartesian k con a () {->-}++assocRight :: (Cat k obj x y) -> (Cat k obj x y)+assocRight (a :.: (assocRight -> (b :.: c))) = (a :.: b) :.: c+assocRight x = x++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++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++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++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++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+ E -> dis+ f :▵: g -> evalCartesian embed f ▵ evalCartesian embed g+ ++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+ ++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+ dis = E+ dup = id :▵: id+ (▵) = (:▵:){->-}
+ Control/Category/FreeSMC.hs view
@@ -0,0 +1,418 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Control.Category.FreeSMC where++import Prelude hiding ((.),id,curry)+import Control.Category.Constrained+import Data.Monoid+import Data.Kind+import Data.Type.Equality++data Sho a b = Sho {fromSho :: Int -> ShowS}++instance Show (Sho a b) where+ showsPrec d (Sho f) = f d++shoCon :: String -> Sho a b+shoCon name = Sho $ \_ -> showString name++instance Category Sho where+ type Obj Sho = Trivial+ id = shoCon "id"+ Sho f ∘ Sho g = Sho $ \d -> showParen (d /= 0) (f 0 . showString " ∘ " . g 0)++instance Monoidal Sho where+ swap = shoCon "swap"+ assoc = shoCon "assoc"+ assoc' = shoCon "assoc'"+ unitor = shoCon "unitor"+ unitor' = shoCon "unitor'"+ Sho f × Sho g = Sho $ \d -> showParen (d /= 0) (f 2 . showString " × " . g 2)++instance Cartesian Sho where+ dis = shoCon "dis"+ dup = shoCon "dup"+ exl = shoCon "exl"+ exr = shoCon "exr"+ Sho f ▵ Sho g = Sho $ \d -> showParen (d /= 0) (f 2 . showString " ▵ " . g 2)++class HasShow k where+ toShow :: k a b -> Sho a b++instance HasShow Sho where+ toShow = id+++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"+ S -> showString "swap"+ A -> showString "assoc"+ A' -> showString "assoc'"+ U a -> {-showString "[" .-} fromSho (evalUnitor (trivializeUnitor a)) 0 {-. showString "]"-}+ U' a -> {-showString "[" .-} fromSho (evalUnitor' (trivializeUnitor a)) 0 {-. showString "]"-}+ X 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)+++showDbg :: Int -> Cat k con a b -> ShowS+showDbg d = \case+ X _ -> 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)+ S -> showString "σ"+ A -> showString "α"+ A' -> showString "α'"+ U _ -> showString "ρ"+ U' a -> showString ("ρ'(" ++ show a ++ ")")++++parens :: [Char] -> [Char]+parens x = "("<> x <>")"++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+ X g -> X (f g)++ I -> I+ a :.: b -> mapGenerators f a :.: mapGenerators f b++ a :×: b -> mapGenerators f a :×: mapGenerators f b+ A -> A+ A' -> A'+ S -> S+ U x -> U x+ U' x -> U' x++ x -> error (showDbg 0 x " (Free.mapGenerators)")+++instance Show (Unitor con a b) where+ show UL = "⟨"+ show UR = "⟩"+ show (IL a) = "⟨" ++ show a+ show (IR a) = "⟩" ++ show a+data Unitor con a b where+ UL :: Unitor con a ((),a)+ UR :: Unitor con a (a,())+ IL :: (con a, con b, con c) => Unitor con a b -> Unitor con (a,c) (b,c)+ IR :: (con a, con b, con c) => Unitor con a b -> Unitor con (c,a) (c,b)++compareUnitors :: Unitor con a b -> Unitor con a b' -> Maybe (b :~: b')+compareUnitors UL UL = Just Refl+compareUnitors UR UR = Just Refl+compareUnitors (IL a) (IL b) = case compareUnitors a b of Nothing -> Nothing; Just Refl -> Just Refl+compareUnitors (IR a) (IR b) = case compareUnitors a b of Nothing -> Nothing; Just Refl -> Just Refl+compareUnitors _ _ = Nothing++trivializeUnitor :: Unitor con a b -> Unitor Trivial a b+trivializeUnitor UL = UL+trivializeUnitor UR = UR+trivializeUnitor (IL f) = IL (trivializeUnitor f)+trivializeUnitor (IR f) = IR (trivializeUnitor f)++commuteUnitors :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (),+ con a, con b) => Unitor con c b -> Unitor con a b -> Cat cat con a c+commuteUnitors UL UL = id+commuteUnitors UL UR = id+commuteUnitors UR UR = id+commuteUnitors UR UL = id+commuteUnitors (IL a) (IL b) = (commuteUnitors a b × id)+commuteUnitors (IR a) (IR b) = (id × commuteUnitors a b)+commuteUnitors (IR a) (IL b) = (U (IL b)) . (U' (IR a))+commuteUnitors (IL a) (IR b) = (U (IR b)) . (U' (IL a))+commuteUnitors UL (IR a) = U a . U' UL+commuteUnitors UR (IL a) = U a . U' UR+commuteUnitors (IR a) UL = U UL . U' a+commuteUnitors (IL a) UR = U UR . U' a+++data Cat k (con :: Type -> Constraint) a b where+ A :: (con a, con b, con c) => Cat k con ((a,b),c) (a,(b,c))+ A' :: (con a, con b, con c) => Cat k con (a,(b,c)) ((a,b),c)+ S :: (con a, con b) => Cat k con (a,b) (b,a) + Embed :: (con a, con b) => k a b -> Cat k con a b+ I :: Cat k con a a+ U :: Unitor con a b -> Cat k con a b+ U' :: Unitor con b a -> Cat k con a b++ (:.:) :: con b => (Cat k con b c) -> (Cat k con a b) -> (Cat k con a c)+ (:×:) :: (con a, con b, con c, con d) => (Cat k con a b) -> (Cat k con c d) -> (Cat k con (a ⊗ c) (b ⊗ d))+++instance Invertible (Cat k con) where+ dual :: Cat k con a b -> Cat k con b a+ dual = \case+ I -> I+ f :×: g -> dual f :×: dual g+ f :.: g -> dual g :.: dual f+ S -> S+ A -> A'+ A' -> A++assocRight :: (Cat k obj x y) -> (Cat k obj x y)+assocRight (a :.: (assocRight -> (b :.: c))) = (a :.: b) :.: c+assocRight x = x++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++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++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++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++-- pattern Uncurry :: (obj a1, obj a2, obj c, obj (a1×a2)) => Cat k obj a1 (a2 -> c) -> Cat k obj (a1 × a2) c+-- pattern Uncurry f <- Apply :<: (f :×: I)++++evalM :: forall k a b con.+ (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),+ con ~ Obj k, Monoidal k, Obj k a, Obj k b) => Cat k (Obj k) a b -> (k a b)+evalM I = id+evalM (f :×: g) = evalM f × evalM g+evalM (f :.: g) = evalM f . evalM g+evalM A = assoc+evalM A' = assoc'+evalM S = swap+evalM (U u) = evalUnitor u+evalM (U' u) = evalUnitor' u+evalM (Embed ϕ) = ϕ++evalCartesian :: forall k a b con.+ (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),+ con ~ Obj k, Cartesian k, Obj k a, Obj k b) => Cat k (Obj k) a b -> (k a b)+evalCartesian = \case+ I -> id+ (f :×: g) -> evalCartesian f × evalCartesian g+ (f :.: g) -> evalCartesian f . evalCartesian g+ (X ϕ) -> ϕ+ A -> assoc+ A' -> assoc'+ S -> swap+ (U u) -> evalUnitor u+ (U' u) -> evalUnitor' u+++evalUnitor :: forall k a b con.+ (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),+ con ~ Obj k, Monoidal k, Obj k a, Obj k b)+ => Unitor (Obj k) a b -> (k a b)+evalUnitor UR = unitor+evalUnitor UL = swap . unitor+evalUnitor (IL x) = (evalUnitor x × id)+evalUnitor (IR x) = (id × evalUnitor x)++evalUnitor' :: forall k a b con.+ (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),+ con ~ Obj k, Monoidal k, Obj k a, Obj k b)+ => Unitor (Obj k) b a -> (k a b)+evalUnitor' UR = unitor'+evalUnitor' UL = unitor' . swap+evalUnitor' (IL x) = (evalUnitor' x × id)+evalUnitor' (IR x) = (id × evalUnitor' x)+-- eval Dup = dup+-- eval Apply = apply+-- eval (Curry f) = curry (eval f)+---------------------------+-- Cat k obj - instances+++pattern X :: forall (k :: Type -> Type -> Type) (con :: Type -> Constraint) a b. () => (con a, con b) => k a b -> Cat k con a b+pattern X x = Embed x++instance Category (Cat k con) where+ type Obj (Cat k con) = con+ id = I+ I ∘ x = x+ x ∘ I = x+ x ∘ y = x :.: y++instance (ProdObj con, forall a b. (con a, con b) => con (a,b)) => Monoidal (Cat k con) where+ I × I = I+ U' a × I = U' (IL a)+ I × U' a = U' (IR a)+ f × g = f :×: g+ assoc = A+ assoc' = A'+ swap = S+ unitor = U UR+ unitor' = U' UR+++type Composer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b -> (Cat k con a c)+type PartialComposer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b -> Alt Maybe (Cat k con a c)+type ProtoSimplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => Composer k con -> PartialComposer k con+type Simplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => forall a b. (con a, con b) => (Cat k con a b) -> (Cat k con a b)++monoidalSimplify :: (con (), ProdObj con, forall α β. (con α, con β) => con (α,β)) => (con a, con b) => Cat k con a b -> Cat k con a b+monoidalSimplify = mkSimplifier (\x -> monoidalRules x)++monoidalRules :: forall k con. ProtoSimplifier k con+monoidalRules (.) = \ x y -> Alt (after x y) where+ after :: (con a, con b, con c) => Cat k con b c -> Cat k con a b -> Maybe (Cat k con a c)++ -- obvious simplifications+ S `after` S = Just id+ A' `after` A = Just id+ A `after` A' = Just id++ -- commute (or cancel) unitors+ U' x `after` U y = Just (commuteUnitors x y)++ -- push swaps to the right+ S `after` (f :×: g) = Just ((g × f) . S)++ -- swap individual strands+ S `after` A = Just (assoc' . (id × swap) . assoc . (swap × id))+ S `after` A' = Just (assoc . (swap × id) . assoc' . (id × swap))+ A `after` S = Just ((id × swap) . assoc . (swap × id) . assoc')+ A' `after` S = Just ((swap × id) . assoc' . (id × swap ) . assoc)++ -- push U' through S+ U' UR `after` S = Just (U' UL)+ U' UL `after` S = Just (U' UR)+ U' (IL a) `after` S = Just (swap . U' (IR a))+ U' (IR a) `after` S = Just (swap . U' (IL a))++ -- push U' into ×+ U' UR `after` ((f :×: I) :<: h) = Just (f . U' UR . h)+ U' (IL a) `after` ((f :×: g) :<: h) = Just (((U' a . f) × g) . h )+ U' (IR a) `after` ((f :×: g) :<: h) = Just ((f × (U' a . g)) . h )++ -- push U' through A'+ U' UR `after` A' = Just (id × U' UR)+ U' (IR a) `after` A' = Just (A' . (id × (id × U' a)))+ U' (IL (IR a)) `after` A' = Just (A' . (id × (U' a × id)) )+ U' (IL UR) `after` A' = Just (id × U' UL )+ U' (IL UL) `after` A' = Just (U' UL)+ U' (IL (IL a)) `after` A' = Just (A' . (U' a × id))++ -- push U' through A+ U' UL `after` A = Just (U' UL × id)+ U' (IL a) `after` A = Just (A . ((U' a × id) × id))+ U' (IR (IL a)) `after` A = Just (A . ((id × U' a) × id))+ U' (IR UL) `after` A = Just (U' UR × id)+ U' (IR UR) `after` A = Just (U' UR)+ U' (IR (IR a)) `after` A = Just (A . (id × U' a))++ -- compose strands + (f :×: g) `after` (h :×: i) = Just ((f . h) × (g . i))+++ -- failing the above, extract unitors+ ((f :>: U' a) :×: g) `after` h = Just ((f×g) . U' (IL a) . h )+ (f :×: (g :>: U' a)) `after` h = Just ((f × g) . U' (IR a) . h)++ h `after` ((f :>: U' a) :×: g) = Just (h . (f × g) . U' (IL a) )+ h `after` (f :×: (g :>: U' a)) = Just (h . (f × g) . U' (IR a) )+++ -- extract unitors from ▵:+ -- h `after` ((U a :<: f) :▵: g) = Just (h . U (IL a) . (f ▵ g) )+ -- h `after` (f :▵: (U a :<: g )) = Just (h . U (IR a) . (f ▵ g) )++ _ `after` _ = Nothing+++neverEqual :: Comparator k+neverEqual _ _ = Nothing+++++{-++closedCartesianRules :: forall k con. ProtoSimplifier k con+closedCartesianRules (.) = \ x y -> Alt (after x y) where+ after :: (con a, con b, con c) => Cat k con b c -> Cat k con a b -> Maybe (Cat k con a c)+ + -- Incomplete support for apply/curry simplifier+ Apply `after` (Curry f :×: I) = Just f+ -- Apply `after` (Curry (g :>: R) :▵: f) = Just (g . f)+ _ `after` _ = Nothing+-}+mkSimplifier :: forall k con. ProtoSimplifier k con -> Simplifier k con+mkSimplifier protoAfter = simplify where+ (...) :: Composer k con+ I ... g = g -- g is already normal.+ f ... I = f -- f is already normal.+ (f :>: g) ... (h :<: i) = case getAlt (g `after` h) of+ Nothing -> (f :>: g) :.: (h :<: i) -- no reaction. both subterms are normal. so we're done.+ Just j -> f ... j ... i --- reaction :: we must recurse. ("After" must return a normal term; j.)+ f ... g = f :.: g+ after :: PartialComposer k con+ after = protoAfter (...)++ simplify :: (con a, con b) => Cat k con a b -> Cat k con a b+ -- simplify (Curry f) = Curry (simplify f)+ simplify (f :×: g) = simplify f × simplify g+ simplify (f :.: g) = simplify f ... simplify g+ simplify x = x+++toDup :: (ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con b) => Cat k con a b -> Cat k con a b+toDup = \case+ I -> I+ (f :×: g) -> toDup f × toDup g+ (f :.: g) -> toDup f . toDup g+ X ϕ -> X ϕ+ A -> A+ A' -> A'+ S -> S+ (U u) -> U u+ (U' u) -> U' u+++toE :: (ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con b) => Cat k con a b -> Cat k con a b+toE = \case+ I -> I+ (f :×: g) -> toE f × toE g+ (f :.: g) -> toE f . toE g+ X ϕ -> X ϕ+ A -> A+ A' -> A'+ S -> S+ (U u) -> U u+ (U' u) -> U' u+
+ Control/Category/Linear.hs view
@@ -0,0 +1,235 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE UnicodeSyntax #-}++{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}++module Control.Category.Linear (+ -- Interface+ type P, unit, split, merge, pattern (:::),+ encode, decode, reduce, (!:),+ -- Helpers for cartesian categories+ ignore, copy, discard+) 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++++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++unit :: {-<-}forall k con r. (Obj k r, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}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.+unit = Y dis+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:+++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))+ +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 (E :<: _) k = k id Nil+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 :<: g) must be rejected.+reduceStep ((P1 :<: f₁) :+ (P2 :<: f₂) :+ rest) k+ | EQ <- compareMorphisms f₁ f₂ =+ expose f₁ $ \g f' -> -- expose any merge+ 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 _ (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 (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 E E = 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 (E) (_) = LT+compareAtoms (_) (E) = GT+compareAtoms f g = error ("compareAtoms:\n" ++ showDbg 0 f "\n" ++ showDbg 0 g "" )+
+ LICENSE view
@@ -0,0 +1,166 @@++ GNU LESSER GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.+++ This version of the GNU Lesser General Public License incorporates+the terms and conditions of version 3 of the GNU General Public+License, supplemented by the additional permissions listed below.++ 0. Additional Definitions.++ As used herein, "this License" refers to version 3 of the GNU Lesser+General Public License, and the "GNU GPL" refers to version 3 of the GNU+General Public License.++ "The Library" refers to a covered work governed by this License,+other than an Application or a Combined Work as defined below.++ An "Application" is any work that makes use of an interface provided+by the Library, but which is not otherwise based on the Library.+Defining a subclass of a class defined by the Library is deemed a mode+of using an interface provided by the Library.++ A "Combined Work" is a work produced by combining or linking an+Application with the Library. The particular version of the Library+with which the Combined Work was made is also called the "Linked+Version".++ The "Minimal Corresponding Source" for a Combined Work means the+Corresponding Source for the Combined Work, excluding any source code+for portions of the Combined Work that, considered in isolation, are+based on the Application, and not on the Linked Version.++ The "Corresponding Application Code" for a Combined Work means the+object code and/or source code for the Application, including any data+and utility programs needed for reproducing the Combined Work from the+Application, but excluding the System Libraries of the Combined Work.++ 1. Exception to Section 3 of the GNU GPL.++ You may convey a covered work under sections 3 and 4 of this License+without being bound by section 3 of the GNU GPL.++ 2. Conveying Modified Versions.++ If you modify a copy of the Library, and, in your modifications, a+facility refers to a function or data to be supplied by an Application+that uses the facility (other than as an argument passed when the+facility is invoked), then you may convey a copy of the modified+version:++ a) under this License, provided that you make a good faith effort to+ ensure that, in the event an Application does not supply the+ function or data, the facility still operates, and performs+ whatever part of its purpose remains meaningful, or++ b) under the GNU GPL, with none of the additional permissions of+ this License applicable to that copy.++ 3. Object Code Incorporating Material from Library Header Files.++ The object code form of an Application may incorporate material from+a header file that is part of the Library. You may convey such object+code under terms of your choice, provided that, if the incorporated+material is not limited to numerical parameters, data structure+layouts and accessors, or small macros, inline functions and templates+(ten or fewer lines in length), you do both of the following:++ a) Give prominent notice with each copy of the object code that the+ Library is used in it and that the Library and its use are+ covered by this License.++ b) Accompany the object code with a copy of the GNU GPL and this license+ document.++ 4. Combined Works.++ You may convey a Combined Work under terms of your choice that,+taken together, effectively do not restrict modification of the+portions of the Library contained in the Combined Work and reverse+engineering for debugging such modifications, if you also do each of+the following:++ a) Give prominent notice with each copy of the Combined Work that+ the Library is used in it and that the Library and its use are+ covered by this License.++ b) Accompany the Combined Work with a copy of the GNU GPL and this license+ document.++ c) For a Combined Work that displays copyright notices during+ execution, include the copyright notice for the Library among+ these notices, as well as a reference directing the user to the+ copies of the GNU GPL and this license document.++ d) Do one of the following:++ 0) Convey the Minimal Corresponding Source under the terms of this+ License, and the Corresponding Application Code in a form+ suitable for, and under terms that permit, the user to+ recombine or relink the Application with a modified version of+ the Linked Version to produce a modified Combined Work, in the+ manner specified by section 6 of the GNU GPL for conveying+ Corresponding Source.++ 1) Use a suitable shared library mechanism for linking with the+ Library. A suitable mechanism is one that (a) uses at run time+ a copy of the Library already present on the user's computer+ system, and (b) will operate properly with a modified version+ of the Library that is interface-compatible with the Linked+ Version.++ e) Provide Installation Information, but only if you would otherwise+ be required to provide such information under section 6 of the+ GNU GPL, and only to the extent that such information is+ necessary to install and execute a modified version of the+ Combined Work produced by recombining or relinking the+ Application with a modified version of the Linked Version. (If+ you use option 4d0, the Installation Information must accompany+ the Minimal Corresponding Source and Corresponding Application+ Code. If you use option 4d1, you must provide the Installation+ Information in the manner specified by section 6 of the GNU GPL+ for conveying Corresponding Source.)++ 5. Combined Libraries.++ You may place library facilities that are a work based on the+Library side by side in a single library together with other library+facilities that are not Applications and are not covered by this+License, and convey such a combined library under terms of your+choice, if you do both of the following:++ a) Accompany the combined library with a copy of the same work based+ on the Library, uncombined with any other library facilities,+ conveyed under the terms of this License.++ b) Give prominent notice with the combined library that part of it+ is a work based on the Library, and explaining where to find the+ accompanying uncombined form of the same work.++ 6. Revised Versions of the GNU Lesser General Public License.++ The Free Software Foundation may publish revised and/or new versions+of the GNU Lesser General Public License from time to time. Such new+versions will be similar in spirit to the present version, but may+differ in detail to address new problems or concerns.++ Each version is given a distinguishing version number. If the+Library as you received it specifies that a certain numbered version+of the GNU Lesser General Public License "or any later version"+applies to it, you have the option of following the terms and+conditions either of that published version or of any later version+published by the Free Software Foundation. If the Library as you+received it does not specify a version number of the GNU Lesser+General Public License, you may choose any version of the GNU Lesser+General Public License ever published by the Free Software Foundation.++ If the Library as you received it specifies that a proxy can decide+whether future versions of the GNU Lesser General Public License shall+apply, that proxy's public statement of acceptance of any version is+permanent authorization for you to choose that version for the+Library.
+ examples/Unitary.hs view
@@ -0,0 +1,254 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RecursiveDo #-}+{-# LANGUAGE UnicodeSyntax #-}+{-# LANGUAGE LinearTypes #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}++import Control.Category.Constrained+import Control.Category.Linear++import Data.Complex+import Data.List (transpose, intercalate)+import Data.Constraint+import Control.Monad+import System.Exit (exitFailure)+import Prelude hiding (id,(.),not)+import Data.Array+import Numeric++type COMPLEX = Complex Double+++data U a b = U {fromM :: Array (a,b) COMPLEX}++class (Bounded a, Ix a, Eq a) => Finite a where+ inhabitants :: [a]+ subFinite :: forall c b. (Finite (c ⊗ b), a ~ (c ⊗ b)) => Dict (Finite c, Finite b)+instance Finite () where+ inhabitants = [()]+ subFinite = error "Finite ()"+instance Finite Bool where+ inhabitants = inhabitants'+ subFinite = error "Finite Bool"++inhabitants' :: forall a. (Bounded a, Enum a) => [a]+inhabitants' = [minBound..maxBound]++pad :: Int -> String -> String+pad n xs = replicate (n - length xs) ' ' ++ xs++padAll :: [String] -> [String]+padAll xs = map (pad m) xs+ where m = maximum (map length xs)++showMat :: [[String]] -> String+showMat = unlines . map (intercalate " ") . transpose . map padAll . transpose ++showCOMPLEX :: RealFloat a => Complex a -> String+showCOMPLEX (x :+ y) = (showFFloat (Just 1) x . showString "+i" . showFFloat (Just 1) y ) ""++instance (Finite a, Finite b) => Show (a `U` b) where+ show (U f) = showMat [[showCOMPLEX (f ! (i,j)) | i <- inhabitants] | j <- inhabitants]+++instance (Finite a, Finite b) => Finite (a,b) where+ inhabitants = [(x,y) | x <- inhabitants, y <- inhabitants]+ subFinite = Dict++instance ProdObj Finite where+ prodobj = Dict+ objprod = subFinite+ objunit = Dict++summation :: (Num a, Finite t) => (t -> a) -> a+summation f = sum [f x | x <- inhabitants]++tabulate :: (Finite a, Finite b) => (a -> b -> COMPLEX) -> a `U` b+tabulate f = U ( array ( (minBound,minBound),+ (maxBound,maxBound))+ [((i,j),f i j) | i <- inhabitants, j <- inhabitants])++instance Category U where+ type Obj U = Finite+ id = tabulate delta -- identity matrix+ U g ∘ U f = tabulate (\i j -> summation+ (\k -> f!(i,k) * g!(k,j))) -- matrix multiplication++instance Monoidal U where+ U f × U g = tabulate (\(a,c) (b,d) -> f ! (a,b) * g ! (c,d)) -- kroneckerProduct+ unitor = tabulate (\x (y,()) -> delta x y)+ unitor' = tabulate (\(y,()) x -> delta x y)+ assoc = tabulate (\ ((x,y),z) (x',(y',z')) ->+ delta ((x,y),z) ((x',y'),z'))+ assoc' = tabulate (\ (x',(y',z')) ((x,y),z) ->+ delta ((x,y),z) ((x',y'),z'))+ swap = tabulate $ \(x,y) (y',x') -> delta (x,y) (x',y')+ +-- This is indeed a tensor product.+-- Assume z with two untangled parts: z[(i,k)] = x[i] + y[k]+-- Consider: ((f×g) · z) (j,l)+-- = ∑i ∑k (f×g)(j,l)(i,k) z[i,k]+-- = ∑i ∑k f(j,i) * g(l,k) * (x[i] + y[k])+-- = ∑i ∑k f(j,i) * g(l,k) * x[i] + ∑i ∑k f(j,i) * g(l,k) * y[k]+-- = ∑i f(j,i) * x[i] * ∑k g(l,k) + ∑k g(l,k) * y[k] * ∑i f(j,i)+-- = ∑i f(j,i) * x[i] * 1 + ∑k g(l,k) * y[k] * 1+-- = (f · x)(j) + (g · y)(l)+++-- instance Cartesian (U) where+-- dup = tabulate $ \i (j,k) -> if i==j && i==k then one else 0+-- exl = tabulate $ \(i,_) k -> if i==k then 1 else 0+-- exr = tabulate $ \(_,i) k -> if i==k then 1 else 0++-- instance CoCartesian (U) where+-- jam = tabulate $ \(j,k) i -> if i==j && i==k then 1 else 0+-- inl = tabulate $ \k (i,_) -> if i==k then 1 else 0+-- inr = tabulate $ \k (_,i) -> if i==k then 1 else 0++-- instance Frobenius COMPLEX (U) where+-- scale c = tabulate $ \i j -> c * delta i j++++vsq2 :: COMPLEX+vsq2 = 1 / sqrt 2++-- Hadamard (H) gate+h :: Finite r => P U r Bool ⊸ P U r Bool+h = encode (tabulate m) where+ m :: Bool -> Bool -> COMPLEX+ m True True = -vsq2+ m _ _ = vsq2+++decoded_h :: U Bool Bool+decoded_h = decode h++-- >>> decoded_h+-- 0.7071067811865475 :+ 0.0 0.7071067811865475 :+ 0.0+-- 0.7071067811865475 :+ 0.0 (-0.7071067811865475) :+ (-0.0)++i :: COMPLEX+i = 0 :+ 1++t :: Finite r => P (U) r Bool ⊸ P (U) r Bool+t = encode (tabulate m) where+ m :: Bool -> Bool -> COMPLEX+ m True True = exp (i*pi/4)+ m False False = 1+ m _ _ = 0++hermitianConjugate :: (Finite a, Finite b) => b `U` a -> a `U` b +hermitianConjugate (U f) = tabulate (\i j -> conjugate (f ! (j,i)))++conjugateTranspose :: {-<-}(Finite a, Finite b) =>{->-} U b a -> U a b+conjugateTranspose = hermitianConjugate ++-- Lets' not show the type; it works also for M matrices.++invert :: {-<-} (Finite a, Finite b) => {->-} (forall s. {-<-} Finite s => {->-} P U s a ⊸ P U s b) -> (forall r. {-<-} Finite r => {->-} P U r b ⊸ P U r a)+invert f = encode (conjugateTranspose (decode f))++t' :: Finite r => P U r Bool ⊸ P U r Bool+t' = invert t++t'decoded :: U Bool Bool+t'decoded = decode t'++-- >>> t'decoded+-- 1.0 :+ (-0.0) 0.0 :+ (-0.0)+-- 0.0 :+ (-0.0) 0.7071067811865476 :+ (-0.7071067811865475)++ctrl :: Finite a => (forall r. Finite r => P (U) r a ⊸ P (U) r a) ->+ (forall r. Finite r => P (U) r Bool ⊸ P (U) r a ⊸ P (U) r (Bool,a))+ctrl f x y = encode (ctrlMat (decode f)) (x !: y)++ctrlMat :: Finite a => U a a -> U (Bool,a) (Bool,a)+ctrlMat (U f) = tabulate (\(cIn,x) (cOut,y) ->+ case (cIn,cOut) of+ (True,True) -> f!(x,y) -- if the control is active, transform using f+ (False,False) -> delta x y -- otherwise identity + _ -> 0) -- never transform the control+++delta :: (Eq a) => a -> a -> COMPLEX+delta x y = if x == y then 1 else 0+++not :: Finite r => P (U) r Bool ⊸ P (U) r Bool+not = encode ((tabulate $ \x y -> 1 - delta x y))++(&) :: a ⊸ (a ⊸ b) ⊸ b+x & f = f x++ctrlneg' :: U (Bool,Bool) (Bool,Bool)+ctrlneg' = decode (\p -> split p & \(x,y) -> ctrl not x y)++-- >>> ctrlneg'+-- 1.0 :+ 0.0 0.0 :+ 0.0 0.0 :+ 0.0 0.0 :+ 0.0+-- 0.0 :+ 0.0 1.0 :+ 0.0 0.0 :+ 0.0 0.0 :+ 0.0+-- 0.0 :+ 0.0 0.0 :+ 0.0 0.0 :+ 0.0 1.0 :+ 0.0+-- 0.0 :+ 0.0 0.0 :+ 0.0 1.0 :+ 0.0 0.0 :+ 0.0+++++second :: (t ⊸ b) ⊸ (a, t) ⊸ (a, b)+second f (x,y) = (x,f y)++first :: (t ⊸ b) ⊸ (t, a) ⊸ (b, a)+first f (x,y) = (f x,y)+++toffoli2 :: (Obj k r, Obj k (b, b), Obj k b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) =>+ (P k r b ⊸ P k r b)+ -> (P k r b ⊸ P k r b)+ -> (P k r b ⊸ P k r b)+ -> (P k r b ⊸ P k r b ⊸ (P k r (b,b)))+ -> ((P k r b, P k r b), P k r b)+ ⊸ P k r ((b, b), b)++toffoli2 {-<-} hadam tGate tInv cnot {->-} ((c1,c2),x) =+ cnot c1 (hadam x) & split & \(c1,x) ->+ cnot c2 (tInv x) & split & \(c2,x) ->+ cnot c1 (tGate x) & split & \(c1,x) ->+ cnot c2 (tInv x) & split & \(c2,x) ->+ cnot c2 (tGate c1) & split & \(c2,y) ->+ (cnot (tGate c2) (tInv y)) !: (hadam (tGate x))+ +toffU :: Finite r => P U r ((Bool, Bool), Bool) ⊸ P (U) r ((Bool, Bool), Bool)+toffU = toffoli2 h t t' (ctrl not) . first split . split+++toffoli'' :: U ((Bool, Bool), Bool) ((Bool, Bool), Bool)+toffoli'' = decode toffU++result :: String+result = "1.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0\n\+ \0.0+i0.0 1.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0\n\+ \0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 1.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0\n\+ \0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 1.0+i0.0 0.0+i0.0 0.0+i0.0\n\+ \0.0+i0.0 0.0+i0.0 1.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0\n\+ \0.0+i0.0 0.0+i0.0 0.0+i0.0 1.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0\n\+ \0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 1.0+i-0.0\n\+ \0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 0.0+i0.0 1.0+i-0.0 0.0+i0.0\n"++main :: IO ()+main = unless (show (toffoli'') == result) exitFailure++-- Local Variables:+-- dante-target: "test-unitary"+-- End:
+ linear-smc.cabal view
@@ -0,0 +1,42 @@+Cabal-Version: 3.0+name: linear-smc+version: 1.0.0+category: control+synopsis: Build SMC morphisms using linear types+description:+ A number of domain specific languages, such as circuits or+ data-science workflows, are best expressed as diagrams of boxes+ connected by wires.+ A faithful abstraction of box-and-wires is Symmetric Monoidal Categories (SMCs)+ This library+ 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.1+build-type: Simple++library+ build-depends: base >=4.13 && < 666+ build-depends: constraints++ default-language: Haskell2010+ exposed-modules:+ Control.Category.Constrained+ Control.Category.Linear+ other-modules:+ Control.Category.FreeSMC+ Control.Category.FreeCartesian+ ++Test-Suite test-unitary+ build-depends: constraints+ build-depends: array+ default-language: Haskell2010+ type: exitcode-stdio-1.0+ main-is: examples/Unitary.hs+ build-depends: base+