
   0 | module Data.SOP.NP
   1 | 
   2 | import Data.List.Elem
   3 | import Data.SOP.Utils
   4 | import Data.SOP.Interfaces
   5 | 
   6 | import Decidable.Equality
   7 | 
   8 | %default total
   9 | 
  10 | ||| An n-ary product.
  11 | |||
  12 | ||| The product is parameterized by a type constructor f and indexed by a
  13 | ||| type-level list ks. The length of the list determines the number of
  14 | ||| elements in the product, and if the i-th element of the list is of type k,
  15 | ||| then the i-th element of the product is of type f k.
  16 | |||
  17 | ||| Two common instantiations of f are the identity functor I and the constant
  18 | ||| functor K. For I, the product becomes a heterogeneous list, where the
  19 | ||| type-level list describes the types of its components.  For K a, the product
  20 | ||| becomes a homogeneous list, where the contents of the type-level list are
  21 | ||| ignored, but its length still specifies the number of elements.
  22 | |||
  23 | ||| In the context of the SOP approach to generic programming, an n-ary product
  24 | ||| describes the structure of the arguments of a single data constructor.
  25 | |||
  26 | ||| Note: `NP_` takes an additional type parameter `k` to simulate
  27 | |||       Haskell's kind polymorphism. In theory, this could be left
  28 | |||       as an implicit argument. However, type-inference when calling
  29 | |||       interface functions like `hpure` was rather poor with `k`
  30 | |||       being implicit.
  31 | |||
  32 | |||       We therefore made `k` explicit and added a type alias `NP`
  33 | |||       to be used in those occasions when `k` can be inferred.
  34 | |||
  35 | ||| Examples:
  36 | |||
  37 | ||| ```idris example
  38 | ||| ex1 : NP I [Char,Bool]
  39 | ||| ex1 = ['c',False]
  40 | |||
  41 | ||| ex2 : NP (K String) [Char,Bool,Int]
  42 | ||| ex2 = ["Hello","World","!"]
  43 | |||
  44 | ||| ex3 : NP Maybe [Char,Bool,Int]
  45 | ||| ex3 = [Just 'x', Nothing, Just 1]
  46 | ||| ```
  47 | public export
  48 | data NP_ : (k : Type) -> (f : k -> Type) -> (ks : List k) -> Type where
  49 |   Nil  : NP_ k f []
  50 |   (::) : (v : f t) -> (vs : NP_ k f ks) -> NP_ k f (t :: ks)
  51 | 
  52 | ||| Type alias for `NP_` with type parameter `k` being
  53 | ||| implicit. This reflects the kind-polymorphic data type
  54 | ||| in Haskell.
  55 | public export
  56 | NP : {k : Type} -> (f : k -> Type) -> (ks : List k) -> Type
  57 | NP = NP_ k
  58 | 
  59 | ||| Changes an n-ary product to the identity context `I`
  60 | ||| by adjusting the types of stored values accordingly.
  61 | public export
  62 | toI : NP_ k f ks -> NP I (map f ks)
  63 | toI []       = []
  64 | toI (h :: t) = h :: toI t
  65 | 
  66 | --------------------------------------------------------------------------------
  67 | --          Specialized Interface Functions
  68 | --------------------------------------------------------------------------------
  69 | 
  70 | ||| Specialiced version of `hmap`
  71 | public export
  72 | mapNP : (fun : forall a . f a -> g a) -> NP f ks -> NP g ks
  73 | mapNP fun []        = []
  74 | mapNP fun (v :: vs) = fun v :: mapNP fun vs
  75 | 
  76 | ||| Specialization of `hpure`.
  77 | public export
  78 | pureNP : {ks : _} -> (forall a . f a) -> NP f ks
  79 | pureNP {ks = []}     _ = []
  80 | pureNP {ks = _ :: _} f = f :: pureNP f
  81 | 
  82 | ||| Specialization of `hap`.
  83 | public export
  84 | hapNP : NP (\a => f a -> g a) ks -> NP f ks -> NP g ks
  85 | hapNP []        []        = []
  86 | hapNP (f :: fs) (v :: vs) = f v :: hapNP fs vs
  87 | 
  88 | ||| Specialization of `hfoldl`
  89 | public export
  90 | foldlNP : (fun : acc -> el -> acc) -> acc -> NP (K el) ks -> acc
  91 | foldlNP _   acc []        = acc
  92 | foldlNP fun acc (v :: vs) = foldlNP fun (fun acc v) vs
  93 | 
  94 | ||| Specialization of `hfoldr`
  95 | public export
  96 | foldrNP : (fun : el -> Lazy acc -> acc) -> Lazy acc -> NP (K el) ks -> acc
  97 | foldrNP _   acc []        = acc
  98 | foldrNP fun acc (v :: vs) = fun v (foldrNP fun acc vs)
  99 | 
 100 | ||| Specialization of `hsequence`
 101 | public export
 102 | sequenceNP : Applicative g => NP (\a => g (f a)) ks -> g (NP f ks)
 103 | sequenceNP []        = pure []
 104 | sequenceNP (v :: vs) = [| v :: sequenceNP vs |]
 105 | 
 106 | ||| Specialization of `hcollapse`
 107 | public export
 108 | collapseNP : NP (K a) ks -> List a
 109 | collapseNP []        = []
 110 | collapseNP (v :: vs) = v :: collapseNP vs
 111 | 
 112 | --------------------------------------------------------------------------------
 113 | --          Core Functions
 114 | --------------------------------------------------------------------------------
 115 | 
 116 | ||| Returns the head of a non-empty n-ary product
 117 | public export
 118 | hd : NP f (k :: ks) -> f k
 119 | hd (v :: _) = v
 120 | 
 121 | ||| Returns the tail of a non-empty n-ary product
 122 | public export
 123 | tl : NP f (k :: ks) -> NP f ks
 124 | tl (_ :: vs) = vs
 125 | 
 126 | ||| Tries to creates a homogeneous n-ary product of the given
 127 | ||| shape from a list of values.
 128 | public export
 129 | fromListNP : NP f ks -> List a -> Maybe (NP (K a) ks)
 130 | fromListNP []       []        = Just []
 131 | fromListNP []       (_ :: _)  = Nothing
 132 | fromListNP (_ :: _) []        = Nothing
 133 | fromListNP (_ :: t) (x :: xs) = (x ::) <$> fromListNP t xs
 134 | 
 135 | ||| Like `fromListNP` but takes the shape from the implicit
 136 | ||| list of types.
 137 | public export
 138 | fromList : {ks : _} -> List a -> Maybe (NP (K a) ks)
 139 | fromList = fromListNP (pureNP ())
 140 | 
 141 | ||| Creates a homogeneous n-ary product of the given
 142 | ||| shape by repeatedly applying a function to a seed value.
 143 | public export
 144 | unfoldNP : NP f ks -> (s -> (s,a)) -> s -> NP (K a) ks
 145 | unfoldNP []       _ _ = []
 146 | unfoldNP (_ :: t) g s = let (s2,v) = g s
 147 |                          in v :: unfoldNP t g s2
 148 | 
 149 | ||| Like `unfoldNP` but takes the shape from the implicit
 150 | ||| list of types.
 151 | public export
 152 | unfold : {ks : _} -> (s -> (s,a)) -> s -> NP (K a) ks
 153 | unfold = unfoldNP (pureNP ())
 154 | 
 155 | ||| Creates a homogeneous n-ary product of the given
 156 | ||| shape using an initial value and a function for
 157 | ||| generating the next value.
 158 | public export
 159 | iterateNP : NP f ks -> (a -> a) -> a -> NP (K a) ks
 160 | iterateNP np f = unfoldNP np (\v => (f v, v))
 161 | 
 162 | ||| Like `iterate` but takes the shape from the implicit
 163 | ||| list of types.
 164 | public export
 165 | iterate : {ks : _} -> (a -> a) -> a -> NP (K a) ks
 166 | iterate = iterateNP (pureNP ())
 167 | 
 168 | ||| A projection of an n-ary product p extracts the
 169 | ||| value of p at a certain position.
 170 | public export
 171 | 0 Projection : (f : k -> Type) -> (ks : List k) -> (v : k) -> Type
 172 | Projection f ks v = NP f ks -> f v
 173 | 
 174 | ||| The set of projections of an n-ary product `NP f ks` can
 175 | ||| itself be wrapped in an n-ary product of the same shape.
 176 | public export
 177 | projections : {ks : _} -> NP (Projection f ks) ks
 178 | projections {ks = []}       = []
 179 | projections {ks = (_ :: _)} = hd :: mapNP (. tl) projections
 180 | 
 181 | --------------------------------------------------------------------------------
 182 | --          Accessing Values
 183 | --------------------------------------------------------------------------------
 184 | 
 185 | ||| Access the first element of the given type in
 186 | ||| an n-ary product
 187 | public export
 188 | get : (0 t : k) -> {auto prf : Elem t ks} -> NP_ k f ks -> f t
 189 | get t {prf = Here}    (v :: _) = v
 190 | get t {prf = There _} (_ :: vs) = get t vs
 191 | 
 192 | --------------------------------------------------------------------------------
 193 | --          Modifying Values
 194 | --------------------------------------------------------------------------------
 195 | 
 196 | ||| Modify a single element of the given type
 197 | ||| in an n-ary product, thereby possibly changing the
 198 | ||| types of stored values.
 199 | public export
 200 | modify :
 201 |      (fun : f t -> f t')
 202 |   -> {auto prf : UpdateOnce t t' ks ks'}
 203 |   -> NP_ k f ks
 204 |   -> NP_ k f ks'
 205 | modify fun {prf = UpdateHere}    (v :: vs) = fun v :: vs
 206 | modify fun {prf = UpdateThere _} (v :: vs) = v :: modify fun vs
 207 | 
 208 | ||| Modify a single element of the given type
 209 | ||| in an n-ary product by applying an effectful
 210 | ||| function.
 211 | |||
 212 | ||| This is the effectful version of `modify`.
 213 | public export
 214 | modifyF :
 215 |      {auto _ : Functor g}
 216 |   -> (fun : f t -> g (f t'))
 217 |   -> {auto prf : UpdateOnce t t' ks ks'}
 218 |   -> NP_ k f ks
 219 |   -> g (NP_ k f ks')
 220 | modifyF fun {prf = UpdateHere}    (v :: vs) = (:: vs) <$> fun v
 221 | modifyF fun {prf = UpdateThere _} (v :: vs) = (v ::)  <$> modifyF fun vs
 222 | 
 223 | ||| Modify several elements of the given type
 224 | ||| in an n-ary product, thereby possibly changing the
 225 | ||| types of stored values.
 226 | public export
 227 | modifyMany :
 228 |      (fun : f t -> f t')
 229 |   -> {auto prf : UpdateMany t t' ks ks'}
 230 |   -> NP_ k f ks
 231 |   -> NP_ k f ks'
 232 | modifyMany f {prf = UMNil}        []      = []
 233 | modifyMany f {prf = UMConsSame x} (v::vs) = f v :: modifyMany f vs
 234 | modifyMany f {prf = UMConsDiff x} (v::vs) = v   :: modifyMany f vs
 235 | 
 236 | ||| Modify several elements of the given type
 237 | ||| in an n-ary product by applying an effectful function.
 238 | |||
 239 | ||| This is the effectful version of `modifyMany`.
 240 | public export
 241 | modifyManyF :
 242 |      {auto _ : Applicative g}
 243 |   -> (fun : f t -> g (f t'))
 244 |   -> {auto prf : UpdateMany t t' ks ks'}
 245 |   -> NP_ k f ks
 246 |   -> g (NP_ k f ks')
 247 | modifyManyF f {prf = UMNil}        []      = pure []
 248 | modifyManyF f {prf = UMConsSame x} (v::vs) = [| f v :: modifyManyF f vs |]
 249 | modifyManyF f {prf = UMConsDiff x} (v::vs) = (v ::) <$> modifyManyF f vs
 250 | 
 251 | ||| Replaces the first element of the given type
 252 | ||| in an n-ary product, thereby possibly changing the
 253 | ||| types of stored values.
 254 | public export %inline
 255 | setAt :
 256 |      (0 t : k)
 257 |   -> (v' : f t')
 258 |   -> {auto prf : UpdateOnce t t' ks ks'}
 259 |   -> NP_ k f ks
 260 |   -> NP_ k f ks'
 261 | setAt t v' = modify {t = t} (const v')
 262 | 
 263 | ||| Replaces several elements of the given type
 264 | ||| in an n-ary product, thereby possibly changing the
 265 | ||| types of stored values.
 266 | public export %inline
 267 | setAtMany :
 268 |      (0 t : k)
 269 |   -> (v' : f t')
 270 |   -> {auto prf : UpdateMany t t' ks ks'}
 271 |   -> NP_ k f ks
 272 |   -> NP_ k f ks'
 273 | setAtMany t v' = modifyMany {t = t} (const v')
 274 | 
 275 | ||| Alias for `setAt` for those occasions when
 276 | ||| Idris cannot infer the type of the new value.
 277 | public export %inline
 278 | setAt' :
 279 |      (0 t  : k)
 280 |   -> (0 t' : k)
 281 |   -> (v' : f t')
 282 |   -> {auto prf : UpdateOnce t t' ks ks'}
 283 |   -> NP_ k f ks
 284 |   -> NP_ k f ks'
 285 | setAt' t _ v' np = setAt t v' np
 286 | 
 287 | ||| Alias for `setAtMany` for those occasions when
 288 | ||| Idris cannot infer the type of the new value.
 289 | public export %inline
 290 | setAtMany' :
 291 |      (0 t  : k)
 292 |   -> (0 t' : k)
 293 |   -> (v' : f t')
 294 |   -> {auto prf : UpdateMany t t' ks ks'}
 295 |   -> NP_ k f ks
 296 |   -> NP_ k f ks'
 297 | setAtMany' t _ v' np = setAtMany t v' np
 298 | 
 299 | --------------------------------------------------------------------------------
 300 | --          Narrowing and expanding products
 301 | --------------------------------------------------------------------------------
 302 | 
 303 | ||| Extracts a subset of values from an n-ary product.
 304 | ||| The values must appear in the same order in both lists.
 305 | public export
 306 | narrow : NP f ks -> {auto prf: Sublist ks' ks} -> NP f ks'
 307 | narrow x         {prf = SLNil}    = []
 308 | narrow (v :: vs) {prf = SLSame y} = v :: narrow vs
 309 | narrow (_ :: vs) {prf = SLDiff y} = narrow vs
 310 | 
 311 | ||| Appends two n-ary products.
 312 | public export
 313 | append : NP f ks -> NP f ks' -> NP f (ks ++ ks')
 314 | append []        y = y
 315 | append (v :: vs) y = v :: append vs y
 316 | 
 317 | ||| Expands an n-ary product by filling missing
 318 | ||| values with the given default-generating function.
 319 | public export
 320 | expand :
 321 |      {ks' : List k}
 322 |   -> (forall k . f k)
 323 |   -> NP f ks
 324 |   -> {auto prf : Sublist ks ks'}
 325 |   -> NP f ks'
 326 | expand f []                         = pureNP f
 327 | expand f (v :: vs) {prf = SLSame x} = v :: expand f vs
 328 | expand f vs        {prf = SLDiff x} = f :: expand f vs
 329 | 
 330 | ||| Expands an n-ary product by filling missing
 331 | ||| values with the given default-generating function.
 332 | |||
 333 | ||| This is the constrained version of `expand`.
 334 | public export
 335 | cexpand :
 336 |      (0 c : k -> Type)
 337 |   -> {auto cs  : NP c ks'}
 338 |   -> (forall k . c k => f k)
 339 |   -> {auto prf : Sublist ks ks'}
 340 |   -> NP_ k f ks
 341 |   -> NP_ k f ks'
 342 | cexpand c {cs = []}   f []                         = []
 343 | cexpand c {cs = _::_} f []                         = f :: cexpand c f []
 344 | cexpand c {cs = _::_} f (v :: vs) {prf = SLSame x} = v :: cexpand c f vs
 345 | cexpand c {cs = _::_} f vs        {prf = SLDiff x} = f :: cexpand c f vs
 346 | 
 347 | --------------------------------------------------------------------------------
 348 | --          Interface Conversions
 349 | --------------------------------------------------------------------------------
 350 | 
 351 | ||| This is needed to implement `Ord` below.
 352 | public export %hint
 353 | ordToEqNP : NP (Ord . f) ks -> NP (Eq . f) ks
 354 | ordToEqNP = mapNP (\_ => %search)
 355 | 
 356 | ||| This is needed to implement `Monoid` below.
 357 | public export %hint
 358 | monoidToSemigroupNP : NP (Monoid . f) ks -> NP (Semigroup . f) ks
 359 | monoidToSemigroupNP = mapNP (\_ => %search)
 360 | 
 361 | --------------------------------------------------------------------------------
 362 | --          Implementations
 363 | --------------------------------------------------------------------------------
 364 | 
 365 | public export %inline
 366 | HPure k (List k) (NP_ k) where hpure  = pureNP
 367 | 
 368 | public export %inline
 369 | HFunctor k (List k) (NP_ k) where hmap  = mapNP
 370 | 
 371 | public export %inline
 372 | HAp k (List k) (NP_ k) (NP_ k) where hap = hapNP
 373 | 
 374 | public export %inline
 375 | HFold k (List k) (NP_ k) where
 376 |   hfoldl = foldlNP
 377 |   hfoldr = foldrNP
 378 | 
 379 | public export %inline
 380 | HCollapse k (List k) (NP_ k) List where hcollapse = collapseNP
 381 | 
 382 | public export %inline
 383 | HSequence k (List k) (NP_ k) where hsequence = sequenceNP
 384 | 
 385 | public export
 386 | (all : NP (Eq . f) ks) => Eq (NP_ k f ks) where
 387 |   (==) {all = []}     [] []               = True
 388 |   (==) {all = _ :: _} (v :: vs) (w :: ws) = v == w && vs == ws
 389 | 
 390 | public export
 391 | (all : NP (Ord . f) ks) => Ord (NP_ k f ks) where
 392 |   compare {all = []}     [] []               = EQ
 393 |   compare {all = _ :: _} (v :: vs) (w :: ws) = compare v w <+> compare vs ws
 394 | 
 395 | public export
 396 | (all : NP (Semigroup . f) ks) => Semigroup (NP_ k f ks) where
 397 |   (<+>) {all = []}     [] []               = []
 398 |   (<+>) {all = _ :: _} (v :: vs) (w :: ws) = (v <+> w) :: (vs <+> ws)
 399 | 
 400 | public export
 401 | (all : NP (Monoid . f) ks) => Monoid (NP_ k f ks) where
 402 |   neutral {all = []}     = []
 403 |   neutral {all = _ :: _} = neutral :: neutral
 404 | 
 405 | public export
 406 | (all : NP (Show . f) ks) => Show (NP_ k f ks) where
 407 |   show =  dispStringList . hcollapse . hcmap (Show . f) show
 408 | 
 409 | private
 410 | consInjective : Data.SOP.NP.(::) a b = Data.SOP.NP.(::) c d -> (a = c, b = d)
 411 | consInjective Refl = (Refl, Refl)
 412 | 
 413 | public export
 414 | (all : NP (DecEq . f) ks) => DecEq (NP_ k f ks) where
 415 |   decEq {all = []}     []        []        = Yes Refl
 416 |   decEq {all = _::_} (v::vs) (w::ws) with (decEq v w)
 417 |     decEq {all = _::_} (v::vs) (w::ws) | (No contra) =
 418 |       No $ contra . fst . consInjective
 419 |     decEq {all = _::_} (v::vs) (v::ws) | (Yes Refl) with (decEq vs ws)
 420 |       decEq {all = _::_} (v::vs) (v::vs) | (Yes Refl) | (Yes Refl) = Yes Refl
 421 |       decEq {all = _::_} (v::vs) (v::ws) | (Yes Refl) | (No contra) =
 422 |         No $ contra . snd . consInjective
 423 | 
 424 | --------------------------------------------------------------------------------
 425 | --          Examples and Tests
 426 | --------------------------------------------------------------------------------
 427 | 
 428 | Ex1 : NP I [Char,Bool]
 429 | Ex1 = ['c',True]
 430 | 
 431 | Ex2 : NP Maybe [Int,Int,Int]
 432 | Ex2 = [Nothing,Nothing,Just 2]
 433 | 
 434 | Ex3 : NP (K String) [Char,Bool,Int]
 435 | Ex3 = ["Hello","World","!"]
 436 | 
 437 | EqTest1 : Ex1 == Ex1 = True
 438 | EqTest1 = Refl
 439 | 
 440 | EqTest2 : Ex1 == ['x',False] = False
 441 | EqTest2 = Refl
 442 | 
 443 | OrdTest1 : compare Ex1 Ex1 = EQ
 444 | OrdTest1 = Refl
 445 | 
 446 | OrdTest2 : compare Ex1 ['x',False] = LT
 447 | OrdTest2 = Refl
 448 | 
 449 | HdTest : hd Ex1 = 'c'
 450 | HdTest = Refl
 451 | 
 452 | TlTest : tl Ex1 = [True]
 453 | TlTest = Refl
 454 | 
 455 | SemiTest : the (NP I [String]) ["hello"] <+> ["world"] = ["helloworld"]
 456 | SemiTest = Refl
 457 | 
 458 | NeutralTest : the (NP I [String,List Int]) Prelude.neutral = ["",[]]
 459 | NeutralTest = Refl
 460 | 
 461 | HMapTest : hmap Just Ex1 = [Just 'c', Just True]
 462 | HMapTest = Refl
 463 | 
 464 | HCMapRes : NP (K String) [Char,Bool]
 465 | HCMapRes = hcmap Show show Ex1
 466 | 
 467 | HPureTest : NP Maybe [String,Int]
 468 | HPureTest = hpure Nothing
 469 | 
 470 | CPureNeutralTest : NP I [String,String]
 471 | CPureNeutralTest = hcpure Monoid neutral
 472 | 
 473 | Person : (f : Type -> Type) -> Type
 474 | Person f = NP f [String,Int]
 475 | 
 476 | toPersonMaybe : Person I -> Person Maybe
 477 | toPersonMaybe = hmap Just
 478 | 
 479 | personShowValues : Person I -> Person (K String)
 480 | personShowValues = hcmap Show show
 481 | 
 482 | emptyPerson : Person Maybe
 483 | emptyPerson = hpure Nothing
 484 | 
 485 | fooPerson : Person (K String)
 486 | fooPerson = hconst "foo"
 487 | 
 488 | Foo : (f : Type -> Type) -> Type
 489 | Foo f = NP f [String,String,List Int]
 490 | 
 491 | neutralFoo : Foo I
 492 | neutralFoo = hcpure Monoid neutral
 493 | 
 494 | update : forall a . Maybe a -> I a -> I a
 495 | update (Just a) _ = a
 496 | update Nothing  a = a
 497 | 
 498 | updatePerson : Person (\a => a -> a)
 499 | updatePerson = hmap update [Just "foo", Nothing]
 500 | 
 501 | updatedPerson : Person I
 502 | updatedPerson = hap updatePerson ["bar",12]
 503 | 
 504 | seqMaybe : NP Maybe [Int,String] -> Maybe (NP I [Int,String])
 505 | seqMaybe = hsequence
 506 | 
 507 | htraverseEx : NP (Either String) [Int,String] -> Maybe (NP I [Int,String])
 508 | htraverseEx = htraverse (either (const Nothing) Just)
 509 | 
 510 | interface Read a where
 511 |   read : String -> Maybe a
 512 | 
 513 | hctraverseEx : NP Read [Int,String] => NP (K String) [Int,String] -> Maybe (NP I [Int,String])
 514 | hctraverseEx = hctraverse Read read
 515 | 
 516 | subproductEx : NP I [Int,String,Bool,Maybe Bool] -> NP I [Int,Bool]
 517 | subproductEx np = narrow np
 518 |