0 | ||| This module defines tensor products, which are later used to define
 1 | ||| the concept of profunctor strength. The two primary tensor products
 2 | ||| in `Idr` are the product (`Pair`) and the coproduct (`Either`).
 3 | module Data.Tensor
 4 |
 5 | %default total
 6 |
 7 |
 8 | ------------------------------------------------------------------------------
 9 | -- Tensor products
10 | ------------------------------------------------------------------------------
11 |
12 |
13 | ||| A bifunctor that admits an *associator*, i.e. a bifunctor that is
14 | ||| associative up to isomorphism.
15 | |||
16 | ||| Laws:
17 | ||| * `mapFst assocl . assocl . assocl = assocl . mapSnd assocl`
18 | public export
19 | interface Bifunctor ten => Associative ten where
20 |   assocl : a `ten` (b `ten` c) -> (a `ten` b) `ten` c
21 |   assocl = assoc.leftToRight
22 |
23 |   assocr : (a `ten` b) `ten` c -> a `ten` (b `ten` c)
24 |   assocr = assoc.rightToLeft
25 |
26 |   assoc : a `ten` (b `ten` c) <=> (a `ten` b) `ten` c
27 |   assoc = MkEquivalence assocl assocr
28 |
29 |
30 | ||| A bifunctor that admits a swap map, i.e. a bifunctor that is
31 | ||| symmetric up to isomorphism.
32 | |||
33 | ||| The bifunctor `ten` is generally also associative.
34 | public export
35 | interface Bifunctor ten => Symmetric ten where
36 |   swap' : a `ten` b -> b `ten` a
37 |   swap' = symmetric.leftToRight
38 |
39 |   symmetric : a `ten` b <=> b `ten` a
40 |   symmetric = MkEquivalence swap' swap'
41 |
42 |
43 | ||| A tensor product is an associative bifunctor that has an identity element
44 | ||| up to isomorphism. Tensor products constitute the monoidal structure of a
45 | ||| monoidal category.
46 | |||
47 | ||| Laws:
48 | ||| * `mapSnd unitl.leftToRight = mapFst unitr.leftToRight . assocl`
49 | public export
50 | interface Associative ten => Tensor ten i | ten where
51 |   unitl : i `ten` a <=> a
52 |   unitr : a `ten` i <=> a
53 |
54 |
55 | ------------------------------------------------------------------------------
56 | -- Cartesian monoidal structure
57 | ------------------------------------------------------------------------------
58 |
59 |
60 | public export
61 | Associative Pair where
62 |   assocl (x,(y,z)) = ((x,y),z)
63 |   assocr ((x,y),z) = (x,(y,z))
64 |
65 | public export
66 | Symmetric Pair where
67 |   swap' = swap
68 |
69 | public export
70 | Tensor Pair () where
71 |   unitl = MkEquivalence snd ((),)
72 |   unitr = MkEquivalence fst (,())
73 |
74 |
75 | ------------------------------------------------------------------------------
76 | -- Cocartesian monoidal structure
77 | ------------------------------------------------------------------------------
78 |
79 |
80 | public export
81 | Associative Either where
82 |   assocl (Left x) = Left (Left x)
83 |   assocl (Right (Left x)) = Left (Right x)
84 |   assocl (Right (Right x)) = Right x
85 |
86 |   assocr (Left (Left x)) = Left x
87 |   assocr (Left (Right x)) = Right (Left x)
88 |   assocr (Right x) = Right (Right x)
89 |
90 | public export
91 | Symmetric Either where
92 |   swap' = either Right Left
93 |
94 | public export
95 | Tensor Either Void where
96 |   unitl = MkEquivalence (either absurd id) Right
97 |   unitr = MkEquivalence (either id absurd) Left
98 |