0 | module Data.Product
  1 |
  2 | import public Data.Ops
  3 | import Data.Vect
  4 |
  5 | %default total
  6 | %hide Prelude.(&&)
  7 | %hide Builtin.DPair.DPair.fst
  8 | %hide Builtin.DPair.DPair.snd
  9 |
 10 | ||| Pairs of types
 11 | public export
 12 | record (*) (a, b : Type) where
 13 |   constructor (&&)
 14 |   p1 : a
 15 |   p2 : b
 16 |
 17 | public export
 18 | (.π1) : a * b -> a
 19 | (.π1) = p1
 20 |
 21 | public export
 22 | π1 : a * b -> a
 23 | π1 = p1
 24 |
 25 | public export
 26 | (.π2) : a * b -> b
 27 | (.π2) = p2
 28 |
 29 | public export
 30 | π2 : a * b -> b
 31 | π2 = p2
 32 |
 33 | %pair Data.Product.(*) p1 p2
 34 | %name Data.Product.(*) p1, p2
 35 |
 36 | public export
 37 | elim : (a -> a') -> (b -> b') -> (a' -> b' -> c) -> a * b -> c
 38 | elim f g m x = f x.π1 `m` g x.π2
 39 |
 40 | public export
 41 | depCurry : {0 a, b : Type} ->
 42 |            {0 c : a -> b -> Type} ->
 43 |            ((x : a) -> (y : b) -> c x y) -> (p : a * b) -> c p.π1 p.π2
 44 | depCurry f x = f x.π1 x.π2
 45 |
 46 | public export
 47 | bi : (a -> x) -> (b -> y) -> a * b -> x * y
 48 | bi f1 f2 p = elim f1 f2 (&&) p
 49 |
 50 | ||| Map each element of the pair and combine the results into one
 51 | public export
 52 | merge : (a -> c) -> (b -> c) -> (c -> c -> c) -> a * b -> c
 53 | merge = elim
 54 |
 55 | ||| Map each element of the pair and combine the results into one using
 56 | ||| the monoid on `c`
 57 | public export
 58 | merge' : Monoid c => (a -> c) -> (b -> c) -> a * b -> c
 59 | merge' f g = merge f g (<+>)
 60 |
 61 | public export
 62 | Show a => Show b => Show (a * b) where
 63 |   show (a && b) = "\{show a} & \{show b}"
 64 |
 65 | ||| Swap the two elements of a product
 66 | public export
 67 | swap : a * b -> b * a
 68 | swap x = x.π2 && x.π1
 69 |
 70 | ||| Convert from a product to a pair
 71 | public export
 72 | toPair : a * b -> (a, b)
 73 | toPair x = (x.π1, x.π2)
 74 |
 75 | ||| Convert from a pair to a product
 76 | public export
 77 | fromPair : (a, b) -> (a * b)
 78 | fromPair x = fst x && snd x
 79 |
 80 | ||| Products have a bifunctor insttance
 81 | public export
 82 | Bifunctor (*) where
 83 |   bimap = bi
 84 |
 85 | ||| Duplicate an element
 86 | public export
 87 | dup : a -> a * a
 88 | dup x = x && x
 89 |
 90 | public export
 91 | distribute : a * b -> c * d -> (a * c) * (b * d)
 92 | distribute x y = (x.π1 && y.π1) && (x.π2 && y.π2)
 93 |
 94 | export
 95 | fork : (a -> b) -> (a -> c) -> a -> b * c
 96 | fork f g x = f x && g x
 97 |
 98 | export
 99 | split : (a * b) * c -> (a * c) * (b * c)
100 | split ((a && b) && c) = (a && c) && (b && c)
101 |
102 | ||| Like bimap but with two arguments
103 | export
104 | through : (a -> b -> c) -> (x -> y -> z) -> (a * x) -> (b * y) -> (c * z)
105 | through f g x y = f x.π1 y.π1 && g x.π2 y.π2
106 |
107 | ||| From arity 2 to arity 1 with pair
108 | public export
109 | curry : (a * b -> c) -> a -> b -> c
110 | curry f a b = f (a && b)
111 |
112 | ||| From arity 2 to arity 1 with pair
113 | public export
114 | uncurry : (a -> b -> c) -> a * b -> c
115 | uncurry f x = f x.π1 x.π2
116 |
117 | public export
118 | shuffle : (a * x) * (b * y) -> (a * b) * (x * y)
119 | shuffle ((a && x) && (b && y)) = (a && b) && (x && y)
120 |
121 | public export
122 | proj1Pair : (0 a, b : _) -> (a && b).π1 === a
123 | proj1Pair _ _ = Refl
124 |
125 | public export
126 | proj2Pair : (0 a, b : _) -> (a && b).π2 === b
127 | proj2Pair _ _ = Refl
128 |
129 | public export
130 | (^) : Type -> Nat -> Type
131 | (^) a Z = Unit
132 | (^) a (S 1) = a
133 | (^) a (S n) = a * a ^ n
134 |
135 | public export
136 | assocL : (a * b) * c -> a * (b * c)
137 | assocL x = x.π1.π1 && (x.π1.π2 && x.π2)
138 |
139 | public export
140 | assocR : a * (b * c) -> (a * b) * c
141 | assocR x = (x.π1 && x.π2.π1) && x.π2.π2
142 |
143 | public export
144 | FreeProd : List Type -> Type
145 | FreeProd [] = Unit
146 | FreeProd (x :: []) = x
147 | FreeProd (x :: (y :: xs)) = x * FreeProd (y :: xs)
148 |
149 | namespace Pair
150 |   -- Cartesian product of pairs
151 |   public export
152 |   cartesian : (a, b) -> (x, y) -> ((a, x), (b, y))
153 |   cartesian (z, v) (w, s) = ((z, w), (v, s))
154 |
155 | ||| A product of n values of type a
156 | public export
157 | Prod : (n : Nat) -> (a : Type) -> Type
158 | Prod Z x = Unit
159 | Prod (S Z) x = x
160 | Prod (S n) x = x * Prod n x
161 |
162 | ||| Convert a vector of n elements into a product of n values of type a
163 | export
164 | toProduct : Vect n a -> Prod n a
165 | toProduct [] {n = Z} = ()
166 | toProduct (x :: []) {n = S 0} = x
167 | toProduct (x :: xs) {n = S (S k)} = x && toProduct xs
168 |
169 | public export
170 | projIdentity : (x : a * b) -> (x.π1 && x.π2) === x
171 | projIdentity (a && b) = Refl
172 |
173 | public export
174 | fst : a * b -> a
175 | fst = .π1
176 |
177 | public export
178 | snd : a * b -> b
179 | snd = .π2
180 |