constrained-categories 0.3.1.1 → 0.4.2.0
raw patch · 14 files changed
Files
- Control/Applicative/Constrained.hs +6/−4
- Control/Arrow/Constrained.hs +56/−24
- Control/Category/Constrained.hs +111/−20
- Control/Category/Constrained/Prelude.hs +2/−2
- Control/Category/Constrained/Reified.hs +1/−1
- Control/Category/Constrained/Reified/PolyPattern.hs +1/−1
- Control/Category/Discrete.hs +1/−1
- Control/Category/Hask.hs +1/−1
- Control/Functor/Constrained.hs +8/−11
- Control/Monad/Constrained.hs +6/−3
- Data/CategoryObject/Product.hs +49/−0
- Data/Foldable/Constrained.hs +4/−6
- Data/Traversable/Constrained.hs +2/−8
- constrained-categories.cabal +7/−3
Control/Applicative/Constrained.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Applicative.Constrained -- Copyright : (c) 2013 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-}@@ -29,6 +29,7 @@ ) where +import Control.Category.Constrained import Control.Functor.Constrained import Control.Arrow.Constrained @@ -36,7 +37,8 @@ import qualified Control.Category.Hask as Hask -class (Functor f r t, Cartesian r, Cartesian t) => Monoidal f r t where+class (Functor f r t, Cartesian r, Cartesian t, Object t (f (UnitObject r)))+ => Monoidal f r t where pureUnit :: UnitObject t `t` f (UnitObject r) fzipWith :: (ObjectPair r a b, Object r c, ObjectPair t (f a) (f b), Object t (f c)) => r (a, b) c -> t (f a, f b) (f c)@@ -91,8 +93,8 @@ constrainedFZipWith :: ( Category r, Category t, o a, o b, o (a,b), o c , o (f a, f b), o (f c) )- => ( r (a, b) c -> t (f a, f b) (f c) )- -> ConstrainedCategory r o (a, b) c -> ConstrainedCategory t o (f a, f b) (f c)+ => ( r (a, b) c -> t (f a, f b) (f c) )+ -> (o⊢r) (a, b) c -> (o⊢t) (f a, f b) (f c) constrainedFZipWith zf = constrained . zf . unconstrained
Control/Arrow/Constrained.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Arrow.Constrained -- Copyright : (c) 2013 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- -- Haskell's 'Arr.Arrow's, going back to [Hughes 2000], combine multiple ideas from -- category theory:@@ -33,6 +33,7 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UnicodeSyntax #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-}@@ -74,6 +75,7 @@ import GHC.Exts (Constraint) import Data.Tagged import Data.Void+import Data.CategoryObject.Product import Data.Coerce import Data.Type.Coercion@@ -82,6 +84,8 @@ import Control.Category.Discrete +import qualified Data.Functor.Contravariant as Hask+ infixr 1 >>>, <<< infixr 3 &&&, *** @@ -242,7 +246,7 @@ arr Refl = id instance EnhancedCat Coercion Discrete where arr Refl = id-instance Category f => EnhancedCat (ConstrainedCategory f o) Discrete where+instance Category f => EnhancedCat (o⊢f) Discrete where arr Refl = id -- | Many categories have as morphisms essentially /functions with extra properties/:@@ -260,9 +264,9 @@ ($) :: (Function f, Object f a, Object f b) => f a b -> a -> b f $ x = arr f x -instance (Function f) => EnhancedCat (->) (ConstrainedCategory f o) where+instance (Function f) => EnhancedCat (->) (o⊢f) where arr (ConstrainedMorphism q) = arr q-instance (EnhancedCat Discrete f) => EnhancedCat Discrete (ConstrainedCategory f o) where+instance (EnhancedCat Discrete f) => EnhancedCat Discrete (o⊢f) where arr (ConstrainedMorphism q) = arr q instance EnhancedCat (->) Coercion where@@ -305,71 +309,99 @@ unit = Hask.pure () const = Hask.const -constrainedArr :: (Category k, Category a, o b, o c )- => ( k b c -> a b c )- -> k b c -> ConstrainedCategory a o b c+instance (Morphism k, Morphism l) => Morphism (k×l) where+ (f:***:g) *** (h:***:i) = (f***h) :***: (g***i)+instance (PreArrow k, PreArrow l) => PreArrow (k×l) where+ (f:***:g) &&& (h:***:i) = (f&&&h) :***: (g&&&i)+ terminal = terminal :***: terminal+ fst = fst :***: fst+ snd = snd :***: snd++prodCatUnit :: ∀ k l . (WellPointed k, WellPointed l)+ => Tagged ((k×l) (ProductCatObj (UnitObject k) (UnitObject l))+ (ProductCatObj (UnitObject k) (UnitObject l)))+ (ProductCatObj (UnitObject k) (UnitObject l))+prodCatUnit = Tagged $ ProductCatObj uk ul+ where Tagged uk = unit :: Tagged (k (UnitObject k) (UnitObject k)) (UnitObject k)+ Tagged ul = unit :: Tagged (l (UnitObject l) (UnitObject l)) (UnitObject l)++instance (WellPointed k, WellPointed l) => WellPointed (k×l) where+ type PointObject (k×l) o = (PointObject k (LFactor o), PointObject l (RFactor o))+ unit = prodCatUnit+ const c = const (lfactorProj c) :***: const (rfactorProj c)++constrainedArr :: (Category k, Category a, o b, o c ) => ( k b c -> a b c )+ -> k b c -> (o⊢a) b c constrainedArr ar = constrained . ar constrainedFirst :: ( Category a, Cartesian a, ObjectPair a b d, ObjectPair a c d )- => ( a b c -> a (b, d) (c, d) )- -> ConstrainedCategory a o b c -> ConstrainedCategory a o (b, d) (c, d)+ => ( a b c -> a (b, d) (c, d) )+ -> (o⊢a) b c -> (o⊢a) (b, d) (c, d) constrainedFirst fs = ConstrainedMorphism . fs . unconstrained constrainedSecond :: ( Category a, Cartesian a, ObjectPair a d b, ObjectPair a d c )- => ( a b c -> a (d, b) (d, c) )- -> ConstrainedCategory a o b c -> ConstrainedCategory a o (d, b) (d, c)+ => ( a b c -> a (d, b) (d, c) )+ -> (o⊢a) b c -> (o⊢a) (d, b) (d, c) constrainedSecond sn = ConstrainedMorphism . sn . unconstrained +instance Morphism Hask.Op where+ first (Hask.Op f) = Hask.Op $ first f+ second (Hask.Op f) = Hask.Op $ second f+ Hask.Op f *** Hask.Op g = Hask.Op $ f *** g+instance MorphChoice Hask.Op where+ left (Hask.Op f) = Hask.Op $ left f+ right (Hask.Op f) = Hask.Op $ right f+ Hask.Op f +++ Hask.Op g = Hask.Op $ f +++ g -instance (Morphism a, o (UnitObject a)) => Morphism (ConstrainedCategory a o) where+instance (Morphism a, o (UnitObject a)) => Morphism (o⊢a) where first = constrainedFirst first second = constrainedSecond second ConstrainedMorphism a *** ConstrainedMorphism b = ConstrainedMorphism $ a *** b -instance (PreArrow a, o (UnitObject a)) => PreArrow (ConstrainedCategory a o) where+instance (PreArrow a, o (UnitObject a)) => PreArrow (o⊢a) where ConstrainedMorphism a &&& ConstrainedMorphism b = ConstrainedMorphism $ a &&& b terminal = ConstrainedMorphism terminal fst = ConstrainedMorphism fst snd = ConstrainedMorphism snd -instance (WellPointed a, o (UnitObject a)) => WellPointed (ConstrainedCategory a o) where- type PointObject (ConstrainedCategory a o) x = PointObject a x+instance (WellPointed a, o (UnitObject a)) => WellPointed (o⊢a) where+ type PointObject (o⊢a) x = PointObject a x globalElement x = ConstrainedMorphism $ globalElement x unit = cstrCatUnit const x = ConstrainedMorphism $ const x cstrCatUnit :: forall a o . (WellPointed a, o (UnitObject a))- => CatTagged (ConstrainedCategory a o) (UnitObject a)+ => CatTagged (o⊢a) (UnitObject a) cstrCatUnit = retag (unit :: CatTagged a (UnitObject a)) instance (EnhancedCat a k, o (UnitObject a))- => EnhancedCat (ConstrainedCategory a o) k where+ => EnhancedCat (o⊢a) k where arr = constrainedArr arr constrainedLeft :: ( CoCartesian k, ObjectSum k b d, ObjectSum k c d )- => ( k b c -> k (b+d) (c+d) )- -> ConstrainedCategory k o b c -> ConstrainedCategory k o (b+d) (c+d)+ => ( k b c -> k (b+d) (c+d) )+ -> (o⊢k) b c -> (o⊢k) (b+d) (c+d) constrainedLeft fs = ConstrainedMorphism . fs . unconstrained constrainedRight :: ( CoCartesian k, ObjectSum k b c, ObjectSum k b d )- => ( k c d -> k (b+c) (b+d) )- -> ConstrainedCategory k o c d -> ConstrainedCategory k o (b+c) (b+d)+ => ( k c d -> k (b+c) (b+d) )+ -> (o⊢k) c d -> (o⊢k) (b+c) (b+d) constrainedRight fs = ConstrainedMorphism . fs . unconstrained -instance (MorphChoice k, o (ZeroObject k)) => MorphChoice (ConstrainedCategory k o) where+instance (MorphChoice k, o (ZeroObject k)) => MorphChoice (o⊢k) where left = constrainedLeft left right = constrainedRight right ConstrainedMorphism a +++ ConstrainedMorphism b = ConstrainedMorphism $ a +++ b -instance (PreArrChoice k, o (ZeroObject k)) => PreArrChoice (ConstrainedCategory k o) where+instance (PreArrChoice k, o (ZeroObject k)) => PreArrChoice (o⊢k) where ConstrainedMorphism a ||| ConstrainedMorphism b = ConstrainedMorphism $ a ||| b initial = ConstrainedMorphism initial coFst = ConstrainedMorphism coFst coSnd = ConstrainedMorphism coSnd instance (SPDistribute k, o (ZeroObject k), o (UnitObject k))- => SPDistribute (ConstrainedCategory k o) where+ => SPDistribute (o⊢k) where distribute = ConstrainedMorphism distribute unDistribute = ConstrainedMorphism unDistribute boolAsSwitch = ConstrainedMorphism boolAsSwitch
Control/Category/Constrained.hs view
@@ -2,17 +2,19 @@ -- Module : Control.Category.Constrained -- Copyright : (c) 2013-2016 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- -- -- The most basic category theory tools are included partly in this -- module, partly in "Control.Arrow.Constrained". {-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE UnicodeSyntax #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ExplicitNamespaces #-}@@ -20,6 +22,7 @@ #if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE UndecidableSuperClasses #-} #endif+{-# LANGUAGE LambdaCase #-} module Control.Category.Constrained ( -- * The category class@@ -30,12 +33,17 @@ -- * Monoidal with coproducts , type (+)() , CoCartesian (..), ObjectSum+ -- * The standard function category+ , type Hask -- * Isomorphisms , Isomorphic (..) -- * Constraining a category , ConstrainedCategory (ConstrainedMorphism)+ , type (⊢)() , constrained, unconstrained , ConstrainedFunction+ -- * Product categories+ , ProductCategory(..), type (×)() -- * Global-element proxies , HasAgent (..) , genericAlg, genericAgentMap@@ -51,9 +59,16 @@ import Data.Tagged import Data.Monoid import Data.Void+import Data.CategoryObject.Product+#if MIN_VERSION_base(4,9,0)+import Data.Kind (Type)+#endif import Data.Type.Coercion import qualified Control.Category as Hask+import qualified Data.Functor.Contravariant as Hask (Op(..)) +import Data.Constraint.Trivial (Unconstrained)+ import Control.Category.Discrete -- | In mathematics, a category is defined as a class of /objects/, plus a class of@@ -69,8 +84,12 @@ -- /morphism type constructor/. From a mathematician's point of view this may -- seem a bit strange way to define the category, but it just turns out to -- be quite convenient for practical purposes.-class Category k where- type Object k o :: Constraint+#if MIN_VERSION_base(4,9,0)+class Category (k :: κ -> κ -> Type) where+#else+class Category (k :: κ -> κ -> *) where+#endif+ type Object k (o :: κ) :: Constraint type Object k o = () id :: Object k a => k a a (.) :: (Object k a, Object k b, Object k c) @@ -86,6 +105,21 @@ id = Prelude.id (.) = (Prelude..) +instance Category Hask.Op where+ id = Hask.id+ (.) = (Hask..)++-- | The category of all Haskell types, with (wrapped) Haskell functions as morphisms.+-- This is just a type-wrapper, morally equivalent to the @(->)@ category itself.+-- The difference is that 'Control.Functor.Constrained.Functor' instances in the '(->)'+-- category are automatically inherited from the standard 'Prelude.Functor' instances+-- that most packages define their type for. The benefit of that is that normal+-- Haskell code keeps working when the "Prelude" classes are replaced with the ones+-- from this library, but the downside is that you can't make /more gradual/ instances+-- when this is desired. This is where the 'Hask' category comes in: it only has functors+-- that are explicitly declared as such.+type Hask = Unconstrained⊢(->)+ -- | Analogue to 'asTypeOf', this does not actually do anything but can -- give the compiler type unification hints in a convenient manner. inCategoryOf :: (Category k) => k a b -> k c d -> k a b@@ -95,15 +129,22 @@ -- | A given category can be specialised, by using the same morphisms but adding -- extra constraints to what is considered an object. -- --- For instance, @'ConstrainedCategory' (->) 'Ord'@ is the category of all+-- For instance, @'Ord'⊢(->)@ is the category of all -- totally ordered data types (but with arbitrary functions; this does not require -- monotonicity or anything). newtype ConstrainedCategory (k :: * -> * -> *) (o :: * -> Constraint) (a :: *) (b :: *) = ConstrainedMorphism { unconstrainedMorphism :: k a b } +type o ⊢ k = ConstrainedCategory k o+ -- | Cast a morphism to its equivalent in a more constrained category, -- provided it connects objects that actually satisfy the extra constraint.-constrained :: (Category k, o a, o b) => k a b -> ConstrainedCategory k o a b+-- +-- In practice, it is often necessary to specify to what typeclass it should be+-- constrained. The most convenient way of doing that is with+-- <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeApplications type-applications syntax>.+-- E.g. @'constrained' \@Ord length@ is the 'length' function considered as a morphism in the subcategory of Hask in which all types are orderable. (Which makes it suitable for e.g. fmapping over a set.)+constrained :: ∀ o k a b . (Category k, o a, o b) => k a b -> (o⊢k) a b constrained = ConstrainedMorphism -- | \"Unpack\" a constrained morphism again (forgetful functor).@@ -112,11 +153,11 @@ -- morphisms that are actually 'Function's can just be applied -- to their objects with '$' right away, no need to go back to -- Hask first.-unconstrained :: (Category k) => ConstrainedCategory k o a b -> k a b+unconstrained :: ∀ o k a b . (Category k) => (o⊢k) a b -> k a b unconstrained = unconstrainedMorphism -instance (Category k) => Category (ConstrainedCategory k isObj) where- type Object (ConstrainedCategory k isObj) o = (Object k o, isObj o)+instance (Category k) => Category (isObj⊢k) where+ type Object (isObj⊢k) o = (Object k o, isObj o) id = ConstrainedMorphism id ConstrainedMorphism f . ConstrainedMorphism g = ConstrainedMorphism $ f . g @@ -214,8 +255,8 @@ swap :: ( ObjectPair k a b, ObjectPair k b a ) => k (a,b) (b,a) - attachUnit :: ( u ~ UnitObject k, ObjectPair k a u ) => k a (a,u)- detachUnit :: ( u ~ UnitObject k, ObjectPair k a u ) => k (a,u) a+ attachUnit :: ( unit ~ UnitObject k, ObjectPair k a unit ) => k a (a,unit)+ detachUnit :: ( unit ~ UnitObject k, ObjectPair k a unit ) => k (a,unit) a regroup :: ( ObjectPair k a b, ObjectPair k b c , ObjectPair k a (b,c), ObjectPair k (a,b) c ) => k (a, (b, c)) ((a, b), c)@@ -234,10 +275,17 @@ detachUnit = \(a, ()) -> a regroup = \(a, (b, c)) -> ((a, b), c) regroup' = \((a, b), c) -> (a, (b, c))++instance Cartesian Hask.Op where+ swap = Hask.Op $ \(a,b) -> (b,a)+ attachUnit = Hask.Op $ \(a, ()) -> a+ detachUnit = Hask.Op $ \a -> (a, ())+ regroup = Hask.Op $ \((a, b), c) -> (a, (b, c))+ regroup' = Hask.Op $ \(a, (b, c)) -> ((a, b), c) -instance (Cartesian f, o (UnitObject f)) => Cartesian (ConstrainedCategory f o) where- type PairObjects (ConstrainedCategory f o) a b = (PairObjects f a b)- type UnitObject (ConstrainedCategory f o) = UnitObject f+instance (Cartesian f, o (UnitObject f)) => Cartesian (o⊢f) where+ type PairObjects (o⊢f) a b = (PairObjects f a b)+ type UnitObject (o⊢f) = UnitObject f swap = ConstrainedMorphism swap attachUnit = ConstrainedMorphism attachUnit@@ -272,8 +320,8 @@ coSwap :: ( ObjectSum k a b, ObjectSum k b a ) => k (a+b) (b+a) - attachZero :: ( Object k a, z ~ ZeroObject k, ObjectSum k a z ) => k a (a+z)- detachZero :: ( Object k a, z ~ ZeroObject k, ObjectSum k a z ) => k (a+z) a+ attachZero :: ( Object k a, zero ~ ZeroObject k, ObjectSum k a zero ) => k a (a+zero)+ detachZero :: ( Object k a, zero ~ ZeroObject k, ObjectSum k a zero ) => k (a+zero) a coRegroup :: ( Object k a, Object k c, ObjectSum k a b, ObjectSum k b c , ObjectSum k a (b+c), ObjectSum k (a+b) c ) => k (a+(b+c)) ((a+b)+c)@@ -319,10 +367,31 @@ -- boolFromSwitch (Left x) = (False,x) -- boolFromSwitch (Right x) = (True,x) -- -instance (CoCartesian f, o (ZeroObject f)) => CoCartesian (ConstrainedCategory f o) where- type SumObjects (ConstrainedCategory f o) a b = (SumObjects f a b)- type ZeroObject (ConstrainedCategory f o) = ZeroObject f+instance CoCartesian Hask.Op where+ coSwap = Hask.Op $ \case Right a -> Left a+ Left a -> Right a+ attachZero = Hask.Op $ \case Left a -> a+ Right void -> absurd void+ detachZero = Hask.Op Left+ coRegroup = Hask.Op $ \case Left (Left a) -> Left a+ Left (Right a) -> (Right (Left a))+ Right a -> Right (Right a)+ coRegroup' = Hask.Op $ \case (Left a) -> Left (Left a)+ Right (Left a) -> Left (Right a)+ Right (Right a) -> Right a+ maybeFromSum = Hask.Op $ \case Nothing -> Left ()+ Just x -> Right x+ maybeAsSum = Hask.Op $ \case Left () -> Nothing+ Right x -> Just x+ boolFromSum = Hask.Op $ \case False -> Left ()+ True -> Right ()+ boolAsSum = Hask.Op $ \case Left () -> False+ Right () -> True +instance (CoCartesian f, o (ZeroObject f)) => CoCartesian (o⊢f) where+ type SumObjects (o⊢f) a b = (SumObjects f a b)+ type ZeroObject (o⊢f) = ZeroObject f+ coSwap = ConstrainedMorphism coSwap attachZero = ConstrainedMorphism attachZero detachZero = ConstrainedMorphism detachZero@@ -369,8 +438,8 @@ apply (f,x) = f x -instance (Curry f, o (UnitObject f)) => Curry (ConstrainedCategory f o) where- type MorphObjects (ConstrainedCategory f o) a c = ( MorphObjects f a c, f ~ (->) )+instance (Curry f, o (UnitObject f)) => Curry (o⊢f) where+ type MorphObjects (o⊢f) a c = ( MorphObjects f a c, f ~ (->) ) uncurry (ConstrainedMorphism f) = ConstrainedMorphism $ \(a,b) -> unconstrained (f a) b curry (ConstrainedMorphism f) = ConstrainedMorphism $ \a -> ConstrainedMorphism $ \b -> f (a, b) @@ -421,3 +490,25 @@ instance Category Coercion where id = Hask.id (.) = (Hask..)+++infixr 3 :***:++data ProductCategory k l p q = k (LFactor p) (LFactor q) :***: l (RFactor p) (RFactor q)++type (×) = ProductCategory++instance (Category k, Category l) => Category (k×l) where+ type Object (k×l) o = (IsProduct o, Object k (LFactor o), Object l (RFactor o))+ id = id:***:id+ (f:***:g) . (h:***:i) = (f.h):***:(g.i)++instance (Cartesian k, Cartesian l) => Cartesian (k×l) where+ type UnitObject (k×l) = ProductCatObj (UnitObject k) (UnitObject l)+ type PairObjects (k×l) a b = ( PairObjects k (LFactor a) (LFactor b)+ , PairObjects l (RFactor a) (RFactor b) )+ swap = swap :***: swap+ attachUnit = attachUnit :***: attachUnit+ detachUnit = detachUnit :***: detachUnit+ regroup = regroup :***: regroup+ regroup' = regroup' :***: regroup'
Control/Category/Constrained/Prelude.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Category.Constrained.Prelude -- Copyright : (c) 2013 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- {-# LANGUAGE ConstraintKinds #-}@@ -23,7 +23,7 @@ , Functor(..), (<$>), Applicative(..), (<*>), Monad(..), (=<<), filter , mapM, mapM_, sequence, sequence_ , Foldable, foldMap, fold, traverse_, concatMap- , Traversable, traverse )+ , Traversable, traverse, MonadFail(..) ) import Control.Category.Constrained hiding (ConstrainedMorphism) import Control.Functor.Constrained
Control/Category/Constrained/Reified.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Category.Constrained.Reified -- Copyright : (c) 2016 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- -- -- GADTs that mirror the class hierarchy from 'Category' to (at the moment) 'Cartesian',
Control/Category/Constrained/Reified/PolyPattern.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Category.Constrained.Reified.PolyPattern -- Copyright : (c) 2016 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- -- -- Pattern synonyms which allow you to deconstruct the various types
Control/Category/Discrete.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Category.Discrete -- Copyright : (c) 2018 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- -- {-# LANGUAGE GADTs #-}
Control/Category/Hask.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Category.Hask -- Copyright : (c) 2013 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- -- Re-exports of all the common category-theory inspired classes from the -- "base" package, i.e. basically endofunctors in the Hask category (with
Control/Functor/Constrained.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Functor.Constrained -- Copyright : (c) 2014 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- {-# LANGUAGE ConstraintKinds #-}@@ -19,9 +19,8 @@ module Control.Functor.Constrained- ( module Control.Category.Constrained- -- * Functors- , Functor(..)+ ( -- * Functors+ Functor(..) , (<$>) , constrainedFmap -- * [Co]product mapping@@ -42,7 +41,7 @@ import Control.Category.Discrete -class ( Category r, Category t, Object t (f (UnitObject r)) )+class ( Category r, Category t ) => Functor f r t | f r -> t, f t -> r where fmap :: (Object r a, Object t (f a), Object r b, Object t (f b)) => r a b -> t (f a) (f b)@@ -90,16 +89,14 @@ constrainedFmap :: (Category r, Category t, o a, o b, o (f a), o (f b)) - => ( r a b -> t (f a) (f b) ) - -> ConstrainedCategory r o a b -> ConstrainedCategory t o (f a) (f b)+ => ( r a b -> t (f a) (f b) ) + -> (o⊢r) a b -> (o⊢t) (f a) (f b) constrainedFmap q = constrained . q . unconstrained -instance (Functor [] k k, o [UnitObject k]) - => Functor [] (ConstrainedCategory k o) (ConstrainedCategory k o) where+instance (Functor [] k k) => Functor [] (o⊢k) (o⊢k) where fmap (ConstrainedMorphism f) = ConstrainedMorphism $ fmap f -instance (o (), o [()], o Void, o [Void]) => SumToProduct []- (ConstrainedCategory (->) o) (ConstrainedCategory (->) o) where+instance (o (), o Void, o [Void]) => SumToProduct [] (o⊢(->)) (o⊢(->)) where sum2product = ConstrainedMorphism sum2product mapEither (ConstrainedMorphism f) = ConstrainedMorphism $ mapEither f filter (ConstrainedMorphism f) = ConstrainedMorphism $ filter f
Control/Monad/Constrained.hs view
@@ -2,7 +2,7 @@ -- Module : Control.Monad.Constrained -- Copyright : (c) 2013 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-}@@ -36,6 +36,7 @@ ) where +import Control.Category.Constrained import Control.Applicative.Constrained import Data.Foldable.Constrained import Data.Traversable.Constrained@@ -43,11 +44,12 @@ import Prelude hiding ( id, const, fst, snd, (.), ($)- , Functor(..), Applicative(..), Monad(..), (=<<)+ , Functor(..), Applicative(..), Monad(..), MonadFail(..), (=<<) , uncurry, curry, filter , mapM, mapM_, sequence, sequence_ ) import qualified Control.Category.Hask as Hask+import qualified Control.Monad.Fail as HaskFail import Control.Arrow.Constrained @@ -131,7 +133,8 @@ class (MonadPlus m k) => MonadFail m k where fail :: (Object k (m a)) => k String (m a) -instance (Hask.MonadPlus m, Hask.Applicative m) => MonadFail m (->) where+instance (Hask.MonadPlus m, Hask.Applicative m, HaskFail.MonadFail m) + => MonadFail m (->) where fail = Hask.fail
+ Data/CategoryObject/Product.hs view
@@ -0,0 +1,49 @@+-- |+-- Module : Data.CategoryObject.Product+-- Copyright : (c) Justus Sagemüller 2021+-- License : GPL v3+-- +-- Maintainer : (@) jsag $ hvl.no+-- Stability : experimental+-- Portability : portable+-- ++{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleInstances #-}++module Data.CategoryObject.Product where+ +import Data.Semigroup+import Data.Monoid hiding ((<>))++data ProductCatObj a b = ProductCatObj a b++type family LFactor t where+ LFactor (ProductCatObj l r) = l+ LFactor (a,b) = (LFactor a, LFactor b)++type family RFactor t where+ RFactor (ProductCatObj l r) = r+ RFactor (a,b) = (RFactor a, RFactor b)++class IsProduct t where+ lfactorProj :: t -> LFactor t+ rfactorProj :: t -> RFactor t++instance IsProduct (ProductCatObj a b) where+ lfactorProj (ProductCatObj x _) = x+ rfactorProj (ProductCatObj _ y) = y++instance (IsProduct a, IsProduct b) => IsProduct (a,b) where+ lfactorProj (x,y) = (lfactorProj x, lfactorProj y)+ rfactorProj (x,y) = (rfactorProj x, rfactorProj y)+++instance (Semigroup a, Semigroup b) => Semigroup (ProductCatObj a b) where+ ProductCatObj x y <> ProductCatObj w z = ProductCatObj (x<>w) (y<>z)++instance (Monoid a, Monoid b) => Monoid (ProductCatObj a b) where+ mempty = ProductCatObj mempty mempty+ mappend (ProductCatObj x y) (ProductCatObj w z)+ = ProductCatObj (mappend x w) (mappend y z)
Data/Foldable/Constrained.hs view
@@ -2,7 +2,7 @@ -- Module : Data.Foldable.Constrained -- Copyright : (c) 2014 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-}@@ -19,8 +19,7 @@ module Data.Foldable.Constrained- ( module Control.Category.Constrained - , Foldable(..)+ ( Foldable(..) , fold , traverse_, mapM_, forM_, sequence_ , concatMap@@ -127,9 +126,8 @@ ffoldl f (i,Just a) = f(i,a) -instance ( Foldable f s t, WellPointed s, WellPointed t- , Functor f (ConstrainedCategory s o) (ConstrainedCategory t o) - ) => Foldable f (ConstrainedCategory s o) (ConstrainedCategory t o) where+instance ( Foldable f s t, WellPointed s, WellPointed t, Functor f (o⊢s) (o⊢t) )+ => Foldable f (o⊢s) (o⊢t) where foldMap (ConstrainedMorphism f) = ConstrainedMorphism $ foldMap f ffoldl (ConstrainedMorphism f) = ConstrainedMorphism $ ffoldl f
Data/Traversable/Constrained.hs view
@@ -2,7 +2,7 @@ -- Module : Data.Traversable.Constrained -- Copyright : (c) 2014 Justus Sagemüller -- License : GPL v3 (see COPYING)--- Maintainer : (@) sagemueller $ geo.uni-koeln.de+-- Maintainer : (@) jsag $ hvl.no -- {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-}@@ -19,8 +19,7 @@ module Data.Traversable.Constrained- ( module Control.Applicative.Constrained - , Traversable(..)+ ( Traversable(..) , forM , EndoTraversable , haskTraverse@@ -90,11 +89,6 @@ traverse f = arr mM where mM Nothing = constPure Nothing `inCategoryOf` f $ mempty mM (Just x) = fmap (arr Just) . f $ x---- data Stupid a = Stupid a--- instance Functor Stupid (ConstrainedCategory (->) Num) (->) where--- fmap (Stupid (ConstrainedMorphism f)) (Stupid a) = Stupid (f a)--- -- | Flipped version of 'traverse' / 'mapM'. forM :: forall s t k m a b l .
constrained-categories.cabal view
@@ -1,5 +1,5 @@ Name: constrained-categories-Version: 0.3.1.1+Version: 0.4.2.0 Category: control Synopsis: Constrained clones of the category-theory type classes, using ConstraintKinds. Description: Haskell has, and makes great use of, powerful facilities from category@@ -27,7 +27,7 @@ License: GPL-3 License-file: COPYING Author: Justus Sagemüller-Maintainer: (@) sagemueller $ geo.uni-koeln.de+Maintainer: (@) jsag $ hvl.no Homepage: https://github.com/leftaroundabout/constrained-categories Build-Type: Simple Cabal-Version: >=1.10@@ -40,10 +40,13 @@ Library Default-Language: Haskell2010- Build-Depends: base>=4.7 && <5+ Build-Depends: base>=4.8 && <5 , tagged , void , semigroups+ , contravariant+ , fail+ , trivial-constraint >= 0.4 && < 0.8 Default-Extensions: ConstraintKinds TypeFamilies FlexibleInstances@@ -61,4 +64,5 @@ Control.Category.Constrained.Reified.PolyPattern Data.Foldable.Constrained Data.Traversable.Constrained+ Data.CategoryObject.Product