Elementwise ("zippy") traversals ability

zippy.u

-- Ability to range over all the elements of a list
ability Each where
  each : [a] -> a

-- Implementation detail - standard early termination ability
ability Abort where abort : x

-- Here's a first usage. `each` lets us traverse multiple lists 
-- elementwise, matching up values at corresponding indices.
> handle 
    a = each [1,2,3]
    b = each ["a","b","c","d"]
    (a,b)
  with
    zippy -- implementation below

-- => [(1,"a"), (2,"b"), (3,"c")]

-- You don't need to name the intermediate expressions.
-- Here's a shockingly simple implementation of `zip`

zip2 : [a] -> [b] -> [(a,b)]
zip2 a b = handle (each a, each b) with zippy

> zip2 [1,2,3] [4,5,6,7]

-- [(1,4),(2,5),(3,6)]

-- Here's a dot product implementation
Nat.dot : [Nat] -> [Nat] -> Nat
Nat.dot a b = Nat.sum (handle each a * each b with zippy)

> dot [1,2,3,4] [4,3,2,1]  -- 1*4 + 2*3 + 3*2 + 4*1 = 4 + 6 + 6 + 4 = 20

-- => 20

-- here's the implementation of zippy

zippy : Request {Each} a -> [a]
zippy req = 

  -- Evaluate the request, treating all `each` requests
  -- as requests for the index `i`.
  go : Nat -> Request {Each} a ->{Abort} a
  go i = cases
    { a } -> a 
    { Each.each as -> k } -> 
      match List.at i as with
        None -> abort
        Some a -> handle k a with go i 

  -- Generate the output list by calling `go` with
  -- 0, 1, 2 ... until hitting `abort`
  go2 : [a] -> [a]
  go2 acc = 
    handle go (List.size acc) req with cases
      { Abort.abort -> k } -> acc
      { a }                -> go2 (acc :+ a)

  go2 []

-- Ideas for extension:
-- Combine zippy and cartesian product in a single ability 
-- Folds and scans
-- Generalize to things other than lists