
   0 | module Data.Coproduct
   1 | 
   2 | import Control.Function
   3 | 
   4 | import Data.List
   5 | import Data.Fin
   6 | import public Data.Ops
   7 | 
   8 | %default total
   9 | 
  10 | ||| co-products
  11 | public export
  12 | data (+) : Type -> Type -> Type where
  13 |   ||| Left choice
  14 |   (<+) : a -> a + b
  15 |   ||| Right choice
  16 |   (+>) : b -> a + b
  17 | 
  18 | ||| Eliminator for co-products
  19 | public export
  20 | choice : (a -> c) -> (b -> c) -> a + b -> c
  21 | choice f g (<+ x) = f x
  22 | choice f g (+> x) = g x
  23 | 
  24 | public export
  25 | dchoice : {0 a, b : Type} -> {0 m : a + b -> Type} ->
  26 |           (l : (x : a) -> m (<+ x)) ->
  27 |           (r : (x : b) -> m (+> x)) ->
  28 |           (e : a + b) -> m e
  29 | dchoice l r (<+ x) = l x
  30 | dchoice l r (+> x) = r x
  31 | 
  32 | public export
  33 | dia : a + a -> a
  34 | dia (<+ x) = x
  35 | dia (+> x) = x
  36 | 
  37 | public export
  38 | assocL : (a + b) + c -> a + (b + c)
  39 | assocL (<+ (<+ x)) = <+ x
  40 | assocL (<+ (+> x)) = +> (<+ x)
  41 | assocL (+> x) = +> (+> x)
  42 | 
  43 | public export
  44 | assocR : a + (b + c) -> (a + b) + c
  45 | assocR (<+ x) = <+ (<+ x)
  46 | assocR (+> (<+ x)) = <+ (+> x)
  47 | assocR (+> (+> x)) = +> x
  48 | 
  49 | ||| Co-product is a bifunctor
  50 | public export
  51 | Bifunctor (+) where
  52 |   bimap f g (<+ x) = <+ (f x)
  53 |   bimap f g (+> x) = +> (g x)
  54 | 
  55 | public export
  56 | Functor (Coproduct.(+) a) where
  57 |   map = bimap id
  58 | 
  59 | public export
  60 | Applicative (Coproduct.(+) a) where
  61 |   pure = (+>)
  62 |   (<*>) (<+ e) _ = <+ e
  63 |   (<*>) (+> f) (<+ x) = <+ x
  64 |   (<*>) (+> f) (+> x) = +> f x
  65 | 
  66 | public export
  67 | Monad (Coproduct.(+) a) where
  68 |   join (<+ x) = <+ x
  69 |   join (+> x) = x
  70 | 
  71 | public export
  72 | Alternative (Coproduct.(+) Unit) where
  73 |   empty = <+ ()
  74 |   (<|>) (<+ x) y = y
  75 |   (<|>) (+> x) _ = +> x
  76 | 
  77 | export
  78 | Show a => Show b => Show (a + b) where
  79 |   show (<+ l) = show l
  80 |   show (+> r) = show r
  81 | 
  82 | ||| Left choice is injective
  83 | export
  84 | Injective (<+) where
  85 |   injective Refl = Refl
  86 | 
  87 | ||| Right choice is injective
  88 | export
  89 | Injective (+>) where
  90 |   injective Refl = Refl
  91 | 
  92 | ||| A sum of `n` values of type `a`
  93 | public export
  94 | Sum : (n : Nat) -> (a : Type) -> Type
  95 | Sum Z y = Void
  96 | Sum (S Z) y = y
  97 | Sum (S x) y = y + Sum x y
  98 | 
  99 | public export
 100 | SumList : List Type -> Type
 101 | SumList [] = Void
 102 | SumList (x :: xs) = x + SumList xs
 103 | 
 104 | public export
 105 | match : {a : _} -> SumList a -> SumList b -> SumList (a ++ b)
 106 | match {a = []} x y = y
 107 | match {a = (ty :: xs)} (<+ x) y = <+ x
 108 | match {a = (ty :: xs)} (+> x) y = +> match x y
 109 | 
 110 | export
 111 | split : {a : _} -> SumList (a ++ b) -> SumList a + SumList b
 112 | split {a = []} x = +> x
 113 | split {a = (y :: xs)} (<+ x) = <+ <+ x
 114 | split {a = (y :: xs)} (+> x) = case split x of
 115 |                                     (<+ z) => <+ (+> z)
 116 |                                     (+> z) => +> z
 117 | 
 118 | ||| A selector is a pair of a fin n and a value of type a the Fin allows to
 119 | ||| pick where in a sum of `n` values of `a` the value fit.
 120 | public export
 121 | Selector : Nat -> Type -> Type
 122 | Selector n a = (Fin n, a)
 123 | 
 124 | ||| Convert from a selector to a sum of a
 125 | public export
 126 | finToSum : {0 n : Nat} -> Selector n a -> Sum n a
 127 | finToSum {n = S Z} (FZ, y) = y
 128 | finToSum {n = S Z} (FS x, y) = y
 129 | 
 130 | ||| Diagonal operator on a sum of `n` values of `a`
 131 | export
 132 | diagonal : (n : Nat) -> Sum n a -> a
 133 | diagonal 0 x = void x
 134 | diagonal (S 0) x = x
 135 | diagonal (S (S k)) (<+ x) = x
 136 | diagonal (S (S k)) (+> x) = diagonal (S k) x
 137 | 
 138 | ||| Convert a sum of n values of a into a pair that records which values of `a` was in the sum in a fin
 139 | export
 140 | sumToSelector : {n : Nat} -> Sum n a -> (Fin n, a)
 141 | sumToSelector x {n = Z} = void x
 142 | sumToSelector x {n = (S Z)} = (FZ, x)
 143 | sumToSelector (<+ x) {n = (S (S k))} = (FZ, x)
 144 | sumToSelector (+> x) {n = (S (S k))} = mapFst FS $ sumToSelector {n = S k} x
 145 | 
 146 | ||| A dependent choice from `n` values of `a`
 147 | public export
 148 | ChoiceN : (n : Nat) -> (ty : a -> Type) -> Sum n a -> Type
 149 | ChoiceN Z ty _ = Void
 150 | ChoiceN (S Z) ty v = ty v
 151 | ChoiceN (S (S n)) ty idx =
 152 |   Coproduct.choice (ty) (\x => ChoiceN (S n) ty x) idx
 153 | 
 154 | export
 155 | diaChoice : {n : Nat} -> {0 b : Type} ->
 156 |             (c : Sum n a) -> b -> ChoiceN n {a} (const b) c
 157 | diaChoice {n = 0} c x = c
 158 | diaChoice {n = (S 0)} c x = x
 159 | diaChoice {n = (S (S k))} (<+ y) x = x
 160 | diaChoice {n = (S (S k))} (+> y) x = diaChoice y x
 161 | 
 162 | public export
 163 | fromMaybe : Maybe a -> () + a
 164 | fromMaybe = maybe (<+ ()) (+>)
 165 | 
 166 | public export
 167 | swap : a + b -> b + a
 168 | swap (<+ x) = +> x
 169 | swap (+> x) = <+ x
 170 | 
 171 | ||| Extract the left value
 172 | public export
 173 | alwaysLeft : a + Void -> a
 174 | alwaysLeft (<+ x) = x
 175 | 
 176 | ||| Extract the right value
 177 | public export
 178 | alwaysRight : Void + b -> b
 179 | alwaysRight (+> x) = x
 180 | 
 181 |