0 | module Control.Category.Traced
 1 |
 2 | import Control.Category.Core
 3 | import Control.Category.Functor
 4 | import Control.Category.Monoidal
 5 | import Data.Morphisms
 6 |
 7 | %default total
 8 |
 9 | ------------------------------------------------------------
10 | -- Interface
11 | ------------------------------------------------------------
12 |
13 | ||| A *traced monoidal category* is a monoidal category equipped with
14 | ||| trace maps, maps which allow one to write loops in string diagrams.
15 | ||| The name "traced" comes from a connection to the trace of a matrix
16 | ||| in linear algebra, though the concept has far greater applications.
17 | |||
18 | ||| This is the interface-style definition of a traced monoidal category.
19 | ||| For the record-style definition, see `Control.Category.Records.TracedR`.
20 | |||
21 | ||| Laws:
22 | ||| * `tracel (mapr f . g) = f . tracel g`
23 | ||| * `tracer (mapl f . g) = f . tracer g`
24 | ||| * `tracel (f . mapr g) = tracel f . g`
25 | ||| * `tracer (f . mapl g) = tracer f . g`
26 | ||| * `tracel (unitl' . f . unitl) = f`
27 | ||| * `tracer (unitr' . f . unitr) = f`
28 | ||| * `tracel (tracel f) . assoc = tracel f`
29 | ||| * `tracer (tracer f) . assoc' = tracer f`
30 | ||| * `assoc . tracer (bimap f g) = bimap f (tracer g)`
31 | ||| * `assoc' . tracel (bimap f g) = bimap (tracel f) g`
32 | ||| * `tracel f = tracer f` for all `f : cat a a`
33 | |||
34 | ||| Note that these laws are for spherical traces, which are rather
35 | ||| restrictive. Some weaker versions of these laws may be appropriate
36 | ||| depending on the needs of the implementation.
37 | public export
38 | interface Monoidal cat ten i =>
39 |     Traced (0 cat : Hom obj) (ten : obj -> obj -> obj) (i : obj) | cat,ten where
40 |   constructor MkTraced
41 |   ||| The left trace.
42 |   tracel : {a,b,c : _} -> cat (a `ten` b) (a `ten` c) -> cat b c
43 |   ||| The right trace.
44 |   tracer : {a,b,c : _} -> cat (a `ten` c) (b `ten` c) -> cat a b
45 |
46 | ||| See `PreMonoidal`.
47 | public export
48 | PreTraced : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> Type
49 | PreTraced = Traced
50 |
51 |
52 | ||| Take the trace of an endomorphism, returning an endomorphism in
53 | ||| the unit object. Depending on what the unit object is, this may
54 | ||| or may not actually be useful.
55 | |||
56 | ||| The name comes from the fact that in the monoidal category of
57 | ||| vector spaces, this takes a square matrix `M` to the 1x1 matrix
58 | ||| `[ tr(M) ]`.
59 | public export
60 | trace : Traced cat ten i => {a : _} -> cat a a -> cat i i
61 | trace @{c@(MkTraced{})} f = tracer $ unitl' {ten} . f . unitl
62 |