Constrained.hs (1383B)
1 module Lude.Algebra.Category.Constrained ( 2 Constrained (..), 3 ) where 4 5 import Lude.Algebra.Category.Core 6 import Lude.Constraint.Core 7 import Lude.Haskell 8 9 -------------------------------------------------------------------------------- 10 11 -- | The full subcategory of objects satisfying the given constraint 12 -- 13 -- Note the significance of "full" here: This category contains *all* morphisms 14 -- between objects that satisfy the constraint, so it can not express categories 15 -- that also constrain morphisms in some way (e.g., pointed objects with 16 -- point-preserving morphisms). 17 type Constrained :: forall {k}. Predicate k -> Cat k -> Cat k 18 data Constrained c p a b = (c a, c b) => Constrain {unConstrain :: a `p` b} 19 20 instance (Categorical p) => Categorical (Constrained c p) where 21 type Obj (Constrained c p) = Obj p :&: c 22 identity = Constrain identity 23 compose (Constrain f) (Constrain g) = Constrain (compose f g) 24 witnessMor (Constrain f) = MkEvidence \\ witnessMor f 25 26 instance (Categorical p) => Functorial (Constrained c p a) where 27 type Dom (Constrained c p a) = Constrained c p 28 type Cod (Constrained c p a) = Function 29 map = compose 30 31 instance (Categorical p) => Functorial (Constrained c p) where 32 type Dom (Constrained c p) = Dual (Constrained c p) 33 type Cod (Constrained c p) = (Constrained c p) ==> Function 34 map (MkDual f) = Naturally (. f)