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