
   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 | ||| Co-product is a bifunctor
  38 | public export
  39 | Bifunctor (+) where
  40 |   bimap f g (<+ x) = <+ (f x)
  41 |   bimap f g (+> x) = +> (g x)
  42 | 
  43 | public export
  44 | Functor (Coproduct.(+) a) where
  45 |   map = bimap id
  46 | 
  47 | public export
  48 | Applicative (Coproduct.(+) a) where
  49 |   pure = (+>)
  50 |   (<*>) (<+ e) _ = <+ e
  51 |   (<*>) (+> f) (<+ x) = <+ x
  52 |   (<*>) (+> f) (+> x) = +> f x
  53 | 
  54 | public export
  55 | Monad (Coproduct.(+) a) where
  56 |   join (<+ x) = <+ x
  57 |   join (+> x) = x
  58 | 
  59 | public export
  60 | Alternative (Coproduct.(+) Unit) where
  61 |   empty = <+ ()
  62 |   (<|>) (<+ x) y = y
  63 |   (<|>) (+> x) _ = +> x
  64 | 
  65 | export
  66 | Show a => Show b => Show (a + b) where
  67 |   show (<+ l) = show l
  68 |   show (+> r) = show r
  69 | 
  70 | ||| Left choice is injective
  71 | export
  72 | Injective (<+) where
  73 |   injective Refl = Refl
  74 | 
  75 | ||| Right choice is injective
  76 | export
  77 | Injective (+>) where
  78 |   injective Refl = Refl
  79 | 
  80 | ||| A sum of `n` values of type `a`
  81 | public export
  82 | Sum : (n : Nat) -> (a : Type) -> Type
  83 | Sum Z y = Void
  84 | Sum (S Z) y = y
  85 | Sum (S x) y = y + Sum x y
  86 | 
  87 | public export
  88 | SumList : List Type -> Type
  89 | SumList [] = Void
  90 | SumList (x :: xs) = x + SumList xs
  91 | 
  92 | public export
  93 | match : {a : _} -> SumList a -> SumList b -> SumList (a ++ b)
  94 | match {a = []} x y = y
  95 | match {a = (ty :: xs)} (<+ x) y = <+ x
  96 | match {a = (ty :: xs)} (+> x) y = +> match x y
  97 | 
  98 | export
  99 | split : {a : _} -> SumList (a ++ b) -> SumList a + SumList b
 100 | split {a = []} x = +> x
 101 | split {a = (y :: xs)} (<+ x) = <+ <+ x
 102 | split {a = (y :: xs)} (+> x) = case split x of
 103 |                                     (<+ z) => <+ (+> z)
 104 |                                     (+> z) => +> z
 105 | 
 106 | ||| A selector is a pair of a fin n and a value of type a the Fin allows to
 107 | ||| pick where in a sum of `n` values of `a` the value fit.
 108 | public export
 109 | Selector : Nat -> Type -> Type
 110 | Selector n a = (Fin n, a)
 111 | 
 112 | ||| Convert from a selector to a sum of a
 113 | public export
 114 | finToSum : {0 n : Nat} -> Selector n a -> Sum n a
 115 | finToSum {n = S Z} (FZ, y) = y
 116 | finToSum {n = S Z} (FS x, y) = y
 117 | 
 118 | ||| Diagonal operator on a sum of `n` values of `a`
 119 | export
 120 | diagonal : (n : Nat) -> Sum n a -> a
 121 | diagonal 0 x = void x
 122 | diagonal (S 0) x = x
 123 | diagonal (S (S k)) (<+ x) = x
 124 | diagonal (S (S k)) (+> x) = diagonal (S k) x
 125 | 
 126 | ||| Convert a sum of n values of a into a pair that records which values of `a` was in the sum in a fin
 127 | export
 128 | sumToSelector : {n : Nat} -> Sum n a -> (Fin n, a)
 129 | sumToSelector x {n = Z} = void x
 130 | sumToSelector x {n = (S Z)} = (FZ, x)
 131 | sumToSelector (<+ x) {n = (S (S k))} = (FZ, x)
 132 | sumToSelector (+> x) {n = (S (S k))} = mapFst FS $ sumToSelector {n = S k} x
 133 | 
 134 | ||| A dependent choice from `n` values of `a`
 135 | public export
 136 | ChoiceN : (n : Nat) -> (ty : a -> Type) -> Sum n a -> Type
 137 | ChoiceN Z ty _ = Void
 138 | ChoiceN (S Z) ty v = ty v
 139 | ChoiceN (S (S n)) ty idx =
 140 |   Coproduct.choice (ty) (\x => ChoiceN (S n) ty x) idx
 141 | 
 142 | export
 143 | diaChoice : {n : Nat} -> {0 b : Type} ->
 144 |             (c : Sum n a) -> b -> ChoiceN n {a} (const b) c
 145 | diaChoice {n = 0} c x = c
 146 | diaChoice {n = (S 0)} c x = x
 147 | diaChoice {n = (S (S k))} (<+ y) x = x
 148 | diaChoice {n = (S (S k))} (+> y) x = diaChoice y x
 149 | 
 150 | public export
 151 | fromMaybe : Maybe a -> () + a
 152 | fromMaybe = maybe (<+ ()) (+>)
 153 | 
 154 | public export
 155 | swap : a + b -> b + a
 156 | swap (<+ x) = +> x
 157 | swap (+> x) = <+ x
 158 | 
 159 | ||| Extract the left value
 160 | public export
 161 | alwaysLeft : a + Void -> a
 162 | alwaysLeft (<+ x) = x
 163 | 
 164 | ||| Extract the right value
 165 | public export
 166 | alwaysRight : Void + b -> b
 167 | alwaysRight (+> x) = x
 168 | 
 169 |