linear-smc 1.0.0 → 1.0.1

raw patch · 4 files changed

+44/−64 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Control/Category/Constrained.hs +1/−8
• Control/Category/FreeSMC.hs +22/−39
• Control/Category/Linear.hs +20/−16
• linear-smc.cabal +1/−1

@@ -1,25 +1,18 @@ {-# 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@@ -215,7 +208,7 @@   -- etc.  instance Category (FUN x) where-  id = \x -> x+  id x = x   f ∘ g = \x -> f (g x)  instance Monoidal (FUN m) where

@@ -2,17 +2,13 @@ {-# 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 #-}@@ -29,7 +25,7 @@ import Data.Kind import Data.Type.Equality -data Sho a b = Sho {fromSho :: Int -> ShowS}+newtype Sho a b = Sho {fromSho :: Int -> ShowS}  instance Show (Sho a b) where   showsPrec d (Sho f) = f d@@ -144,10 +140,10 @@ 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 (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@@ -177,27 +173,27 @@     A -> A'     A' -> A -assocRight :: (Cat k obj x y) -> (Cat k obj x y)+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 :: (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 :: 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 :: (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 (:>:) ::  (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 (:<:) ::  (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 @@ -208,7 +204,7 @@  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)+               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@@ -221,7 +217,7 @@  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)+               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@@ -237,20 +233,20 @@ 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)+           => 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 (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)+           => 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)+evalUnitor' (IL x) = evalUnitor' x × id+evalUnitor' (IR x) = id × evalUnitor' x -- eval Dup = dup -- eval Apply = apply -- eval (Curry f) = curry (eval f)@@ -280,13 +276,13 @@   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 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)+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)+monoidalSimplify = mkSimplifier monoidalRules  monoidalRules :: forall k con. ProtoSimplifier k con monoidalRules  (.) = \ x y -> Alt (after x y) where@@ -359,19 +355,6 @@ 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

@@ -3,20 +3,14 @@ {-# 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 #-}@@ -24,12 +18,11 @@ {-# 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, (!:),+  encode, decode, (!:),   -- Helpers for cartesian categories   ignore, copy, discard ) where@@ -184,6 +177,7 @@ -- | 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) @@ -193,6 +187,16 @@  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 (),@@ -223,13 +227,13 @@     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 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 "" ) 

@@ -1,6 +1,6 @@ Cabal-Version:  3.0 name:           linear-smc-version:        1.0.0+version:        1.0.1 category:       control synopsis:       Build SMC morphisms using linear types description: