0 | module Pipeline.Category
 1 |
 2 | import Control.Category
 3 | import Pipeline.Basic
 4 | import Data.Category.Graded
 5 | import public Data.Vect
 6 | import public Data.Vect.Utils
 7 | import public Data.Vect.Quantifiers
 8 |
 9 | -- Pipelines parameterised over a category we first declare the objects and arrows of the category
10 | parameters {0 obj : Type} {0 arr : obj -> obj -> Type}
11 |
12 |   -- An implementation is a list of paired-up morphisms
13 |   public export 0
14 |   ImplCat : Vect (2 + n) obj -> Type
15 |   ImplCat xs = All (uncurry arr) (pairUp xs)
16 |
17 |   -- Running the pipeline requires evidence that the morphisms form a category and an implementation
18 |   -- for each morphism
19 |   export
20 |   RunCat : {auto cat : Category {obj} arr} -> (p : Vect (2 + n) obj) -> ImplCat p -> Vect.head p `arr` Vect.last p
21 |   RunCat [x, y] [f] = f
22 |   RunCat (x :: y :: z :: xs) (f :: c) = RunCat (y :: z :: xs) c . f
23 |
24 | -- This ensures the functor `f` is strong wrt to the monoid `mon`
25 | export
26 | interface CoprodStrength (mon : Monoid a) (f : a -> Type) | f where
27 |   constructor MkFCoprod
28 |   left : {x, y : _} -> f x -> f (x <+> y)
29 |   right : {x, y : _} -> f y -> f (x <+> y)
30 |
31 | -- The identity functor is strong wrt to Either as a monoid on types
32 | export
33 | CoprodStrength EitherMon (\x => x) using EitherSem where
34 |   left = Left
35 |   right = Right
36 |
37 | -- The OneOf functor is strong wrt to the free monoid on types
38 | export
39 | CoprodStrength AnyMon OneOf using AnySem where
40 |   left = Any.left
41 |   right = Any.right
42 |
43 | -- The following is to avoid clashes between `.` as function composition and `.` as morphism composition
44 | %hide Basics.(.)
45 |
46 | export
47 | [Set] Category Fn where
48 |   id x = x
49 |   (.) f g x = f (g x)
50 |
51 | -- Given any monoid and a strong functor, we can build the graded category using the monoid given
52 | -- and GradedCorproduct morphisms indexed by `f` using the grade given by the monoid
53 | public export %hint
54 | MkInst : {0 gr : Type} -> {f : gr -> Type} -> (mon : Monoid gr) => (fc : CoprodStrength mon f) => GradedCat mon (GradedCoproductMonad {e = gr} f)
55 | MkInst {fc = MkFCoprod ll rr} = MkGradedCat Right
56 |   (\m1, m2 => (mapFst ll . m1) @{Set} >=> (mapFst rr . m2) @{Set})
57 |
58 | -- This is merely a fold but we write it inductively explicitly so that it evaluates nicesly when asking for the
59 | -- types of `runGradedCat`
60 | public export
61 | foldGrades : Monoid gr => Vect (S n) gr -> gr
62 | foldGrades (x :: []) = x
63 | foldGrades (x :: (y :: xs)) = x <+> foldGrades (y :: xs)
64 |
65 | -- The common parameters to run pipelines in a graded category, we parameterised everything by
66 | -- the grade, the objects and the graded morphisms
67 | parameters {0 gr : Type}  {0 obj : Type} {0 arr : gr -> obj -> obj -> Type}
68 |
69 |   -- An implementation needs both the layers of the pipeline, and the grades of each morphism.
70 |   -- For each triple of `source`, `target` and `grade` we build the graded morphism `source -[grade]> target`
71 |   -- as the type of the implementation of the corresponding stage
72 |   public export 0
73 |   ImplGr : forall n. Vect (2 + n) obj -> Vect (S n) gr -> Type
74 |   ImplGr layers grades = All (\arg => arr (fst arg) (fst (snd arg)) (snd (snd arg))) (zip grades (pairUp layers))
75 |
76 |   -- To run a graded pipeline we need evidence that the grade is a monoid, that the category is a graded category
77 |   -- and we need a graded implementation of the pipeline. The resulting morphism is a graded morphism from the
78 |   -- start of the pipeline, to the end, except that all the grades are accumulated using `foldGrades` as a result
79 |   -- of composing each graded morphism from the implementation.
80 |   export
81 |   RunGrCat : forall n. {auto mon : Monoid gr} -> (cat : GradedCat mon arr) -> (p : Vect (2 + n) obj) -> (grades : Vect (S n) gr) ->
82 |                  ImplGr p grades -> arr (foldGrades grades) (Vect.head p) (Vect.last p)
83 |   RunGrCat cat [x, y] [gr] [f] = f
84 |   RunGrCat cat (x :: y :: z :: xs) (gr1 :: (g :: gs)) (f :: c :: cs) =
85 |     f #> RunGrCat cat (y :: z :: xs) (g :: gs) (c :: cs)
86 |