
   0 | module Data.SOP.NS
   1 | 
   2 | import Data.List.Elem
   3 | import Data.SOP.Interfaces
   4 | import Data.SOP.NP
   5 | import Data.SOP.Utils
   6 | 
   7 | import Decidable.Equality
   8 | 
   9 | %default total
  10 | 
  11 | ||| An n-ary sum.
  12 | |||
  13 | ||| The sum is parameterized by a type constructor f and indexed by a
  14 | ||| type-level list xs. The length of the list determines the number of choices
  15 | ||| in the sum and if the i-th element of the list is of type x, then the i-th
  16 | ||| choice of the sum is of type f x.
  17 | |||
  18 | ||| The constructor names are chosen to resemble Peano-style natural numbers,
  19 | ||| i.e., Z is for "zero", and S is for "successor". Chaining S and Z chooses
  20 | ||| the corresponding component of the sum.
  21 | |||
  22 | ||| Note that empty sums (indexed by an empty list) have no non-bottom
  23 | ||| elements.
  24 | |||
  25 | ||| Two common instantiations of f are the identity functor I and the constant
  26 | ||| functor K. For I, the sum becomes a direct generalization of the Either
  27 | ||| type to arbitrarily many choices. For K a, the result is a homogeneous
  28 | ||| choice type, where the contents of the type-level list are ignored, but its
  29 | ||| length specifies the number of options.
  30 | |||
  31 | ||| In the context of the SOP approach to generic programming, an n-ary sum
  32 | ||| describes the top-level structure of a datatype, which is a choice between
  33 | ||| all of its constructors.
  34 | |||
  35 | ||| Examples:
  36 | |||
  37 | ||| ```idris example
  38 | ||| the (NS_ Type I [Char,Bool]) (Z 'x')
  39 | ||| the (NS_ Type I [Char,Bool]) (S $ Z False)
  40 | ||| ```
  41 | public export
  42 | data NS_ : (k : Type) -> (f : k -> Type) -> (ks : List k) -> Type where
  43 |   Z : (v : f t)  -> NS_ k f (t :: ks)
  44 |   S : NS_ k f ks -> NS_ k f (t :: ks)
  45 | 
  46 | ||| Type alias for `NS_` with type parameter `k` being
  47 | ||| implicit. This reflects the kind-polymorphic data type
  48 | ||| in Haskell.
  49 | public export
  50 | NS : {k : Type} -> (f : k -> Type) -> (ks : List k) -> Type
  51 | NS = NS_ k
  52 | 
  53 | ||| Changes an n-ary sum to the identity context `I`
  54 | ||| by adjusting the types of stored values accordingly.
  55 | public export
  56 | toI : NS_ k f ks -> NS I (map f ks)
  57 | toI (Z v) = Z v
  58 | toI (S x) = S $ toI x
  59 | 
  60 | --------------------------------------------------------------------------------
  61 | --          Specialized Interface Functions
  62 | --------------------------------------------------------------------------------
  63 | 
  64 | ||| Specialiced version of `hmap`
  65 | public export
  66 | mapNS : (fun : forall a . f a -> g a) -> NS f ks -> NS g ks
  67 | mapNS fun (Z v) = Z $ fun v
  68 | mapNS fun (S x) = S $ mapNS fun x
  69 | 
  70 | ||| Specialization of `hfoldl`
  71 | public export
  72 | foldlNS : (fun : acc -> el -> acc) -> acc -> NS (K el) ks -> acc
  73 | foldlNS fun acc (Z v) = fun acc v
  74 | foldlNS fun acc (S x) = foldlNS fun acc x
  75 | 
  76 | ||| Specialization of `hfoldr`
  77 | public export %inline
  78 | foldrNS : (fun : el -> Lazy acc -> acc) -> Lazy acc -> NS (K el) ks -> acc
  79 | foldrNS fun acc (Z v) = fun v acc
  80 | foldrNS fun acc (S x) = foldrNS fun acc x
  81 | 
  82 | ||| Specialization of `hsequence`
  83 | public export
  84 | sequenceNS : Applicative g => NS (\a => g (f a)) ks -> g (NS f ks)
  85 | sequenceNS (Z v) = map Z v
  86 | sequenceNS (S x) = S <$> sequenceNS x
  87 | 
  88 | ||| Specialization of `hap`
  89 | public export
  90 | hapNS : NP (\a => f a -> g a) ks -> NS f ks -> NS g ks
  91 | hapNS (fun :: _)    (Z v) = Z $ fun v
  92 | hapNS (_   :: funs) (S y) = S $ hapNS funs y
  93 | 
  94 | ||| Specialization of `hcollapse`
  95 | public export
  96 | collapseNS : NS (K a) ks -> a
  97 | collapseNS (Z v) = v
  98 | collapseNS (S x) = collapseNS x
  99 | 
 100 | --------------------------------------------------------------------------------
 101 | --          Injections
 102 | --------------------------------------------------------------------------------
 103 | 
 104 | ||| An injection into an n-ary sum takes a value of the correct
 105 | ||| type and wraps it in one of the sum's possible choices.
 106 | public export
 107 | 0 Injection : (f : k -> Type) -> (ks : List k) -> (v : k) -> Type
 108 | Injection f ks v = f v -> K (NS f ks) v
 109 | 
 110 | ||| The set of injections into an n-ary sum `NS f ks` can
 111 | ||| be wrapped in a corresponding n-ary product.
 112 | public export
 113 | injectionsNP : NP g ks -> NP (Injection f ks) ks
 114 | injectionsNP []       = []
 115 | injectionsNP (_ :: t) = Z :: mapNP (S .) (injectionsNP t)
 116 | 
 117 | ||| The set of injections into an n-ary sum `NS f ks` can
 118 | ||| be wrapped in a corresponding n-ary product.
 119 | public export
 120 | injections : {ks : _} -> NP (Injection f ks) ks
 121 | injections = injectionsNP (pureNP ())
 122 | 
 123 | ||| Applies all injections to an n-ary product of values.
 124 | |||
 125 | ||| This is not implemented in terms of injections for the
 126 | ||| following reason: Since we have access to the structure
 127 | ||| of the n-ary product and thus `ks`, we do not need a
 128 | ||| runtime reference of `ks`. Therefore, when applying
 129 | ||| injections to an n-ary product, prefer this function
 130 | ||| over a combination involving `injections`.
 131 | public export
 132 | apInjsNP_ : NP f ks -> NP (K $ NS f ks) ks
 133 | apInjsNP_ []        = []
 134 | apInjsNP_ (v :: vs) = Z v :: mapNP S (apInjsNP_ vs)
 135 | 
 136 | ||| Alias for `collapseNP . apInjsNP_`
 137 | public export
 138 | apInjsNP : NP f ks -> List (NS f ks)
 139 | apInjsNP = collapseNP . apInjsNP_
 140 | 
 141 | --------------------------------------------------------------------------------
 142 | --          Extracting and injecting values
 143 | --------------------------------------------------------------------------------
 144 | 
 145 | ||| Injects a value into an n-ary sum.
 146 | public export
 147 | inject : {0 t : k} -> (v : f t) -> {auto prf : Elem t ks} -> NS f ks
 148 | inject v {prf = Here}    = Z v
 149 | inject v {prf = There _} = S $ inject v
 150 | 
 151 | ||| Tries to extract a value of the given type from an n-ary sum.
 152 | public export
 153 | extract : (0 t : k) -> NS f ks -> {auto prf : Elem t ks} -> Maybe (f t)
 154 | extract _ (Z v) {prf = Here}    = Just v
 155 | extract _ (S _) {prf = Here}    = Nothing
 156 | extract _ (Z _) {prf = There y} = Nothing
 157 | extract t (S x) {prf = There y} = extract t x
 158 | 
 159 | ||| Converts an n-ary sum into the corresponding n-ary product
 160 | ||| of alternatives.
 161 | public export
 162 | toNP : {ks : _} -> Alternative g => NS f ks -> NP (g . f) ks
 163 | toNP {ks = _ :: _} (Z v) = pure v :: hpure empty
 164 | toNP {ks = _ :: _} (S x) = empty  :: toNP x
 165 | 
 166 | --------------------------------------------------------------------------------
 167 | --          Expanding sums
 168 | --------------------------------------------------------------------------------
 169 | 
 170 | ||| Injects an n-ary sum into a larger n-ary sum.
 171 | public export
 172 | expand : NS f ks -> {auto prf: Sublist ks ks'} -> NS f ks'
 173 | expand (Z v) {prf = SLSame y} = Z v
 174 | expand (S x) {prf = SLSame y} = S $ expand x
 175 | expand v     {prf = SLDiff y} = S $ expand v
 176 | expand _     {prf = SLNil} impossible
 177 | 
 178 | ||| Tries to narrow down an n-ary sum to a subset of
 179 | ||| choices. `ks'` must be a sublist (values in the same order) of `ks`.
 180 | public export
 181 | narrow : NS f ks -> {auto prf: Sublist ks' ks} -> Maybe (NS f ks')
 182 | narrow _     {prf = SLNil}    = Nothing
 183 | narrow (Z v) {prf = SLSame x} = Just $ Z v
 184 | narrow (Z v) {prf = SLDiff x} = Nothing
 185 | narrow (S x) {prf = SLSame y} = S <$> narrow x
 186 | narrow (S x) {prf = SLDiff y} = narrow x
 187 | 
 188 | --------------------------------------------------------------------------------
 189 | --          Implementations
 190 | --------------------------------------------------------------------------------
 191 | 
 192 | public export %inline
 193 | HFunctor k (List k) (NS_ k) where hmap = mapNS
 194 | 
 195 | public export %inline
 196 | HAp k (List k) (NP_ k) (NS_ k) where hap = hapNS
 197 | 
 198 | public export %inline
 199 | HFold k (List k) (NS_ k) where
 200 |   hfoldl = foldlNS
 201 |   hfoldr = foldrNS
 202 | 
 203 | public export
 204 | HSequence k (List k) (NS_ k) where hsequence = sequenceNS
 205 | 
 206 | public export
 207 | HCollapse k (List k) (NS_ k) I where hcollapse = collapseNS
 208 | 
 209 | public export
 210 | (all : NP (Eq . f) ks) => Eq (NS_ k f ks) where
 211 |   (==) {all = _::_} (Z v) (Z w) = v == w
 212 |   (==) {all = _::_} (S x) (S y) = x == y
 213 |   (==) {all = _::_} _     _     = False
 214 | 
 215 | public export
 216 | (all : NP (Ord . f) ks) => Ord (NS_ k f ks) where
 217 |   compare {all = _::_} (Z v) (Z w) = compare v w
 218 |   compare {all = _::_} (S x) (S y) = compare x y
 219 |   compare {all = _::_} (Z _) (S _) = LT
 220 |   compare {all = _::_} (S _) (Z _) = GT
 221 | 
 222 | ||| Sums have instances of `Semigroup` and `Monoid`
 223 | ||| only when they consist of a single choice, which must itself be
 224 | ||| a `Semigroup` or `Monoid`.
 225 | public export
 226 | (all : NP (Semigroup . f) [k']) =>
 227 | Semigroup (NS_ k f [k']) where
 228 |   (<+>) {all = _ :: _} (Z l) (Z r) = Z $ l <+> r
 229 |   (<+>) {all = _ :: _} (S _) _    impossible
 230 |   (<+>) {all = _ :: _} _    (S _) impossible
 231 | 
 232 | public export
 233 | (all : NP (Show . f) ks) => Show (NS_ k f ks) where
 234 |   showPrec {all = _::_} p (Z v) = showCon p "Z" (showArg v)
 235 |   showPrec {all = _::_} p (S x) = showCon p "S" (showPrec App x)
 236 | 
 237 | ||| Sums have instances of `Semigroup` and `Monoid`
 238 | ||| only when they consist of a single choice, which must itself be
 239 | ||| a `Semigroup` or `Monoid`.
 240 | public export
 241 | (all : NP (Monoid . f) [k']) => Monoid (NS_ k f [k']) where
 242 |   neutral {all = _ :: _} = Z neutral
 243 | 
 244 | public export
 245 | Uninhabited (Data.SOP.NS.Z x = Data.SOP.NS.S y) where
 246 |   uninhabited Refl impossible
 247 | 
 248 | public export
 249 | Uninhabited (Data.SOP.NS.S x = Data.SOP.NS.Z y) where
 250 |   uninhabited Refl impossible
 251 | 
 252 | private
 253 | zInjective : Data.SOP.NS.Z x = Data.SOP.NS.Z y -> x = y
 254 | zInjective Refl = Refl
 255 | 
 256 | private
 257 | sInjective : Data.SOP.NS.S x = Data.SOP.NS.S y -> x = y
 258 | sInjective Refl = Refl
 259 | 
 260 | public export
 261 | (all : NP (DecEq . f) ks) => DecEq (NS_ k f ks) where
 262 |   decEq {all = _::_} (Z x) (Z y) with (decEq x y)
 263 |     decEq {all = _::_} (Z x) (Z x) | Yes Refl = Yes Refl
 264 |     decEq {all = _::_} (Z x) (Z y) | No contra = No (contra . zInjective)
 265 |   decEq {all = _::_} (Z x) (S y) = No absurd
 266 |   decEq {all = _::_} (S x) (Z y) = No absurd
 267 |   decEq {all = _::_} (S x) (S y) with (decEq x y)
 268 |     decEq {all = _::_} (S x) (S x) | Yes Refl = Yes Refl
 269 |     decEq {all = _::_} (S x) (S y) | No contra = No (contra . sInjective)
 270 | 
 271 | --------------------------------------------------------------------------------
 272 | --          Examples and Tests
 273 | --------------------------------------------------------------------------------
 274 | 
 275 | Ex1 : let T = NS I [Char,Bool] in (T,T)
 276 | Ex1 = (Z 'x', S $ Z False)
 277 |