Mon May 27 08:52:05 EDT 2019


I guess it's just hard, because it's not just falling out.
Maybe change the monadic form first to support references.

Trying this:

p a b = do
  [d] <- loop $ \i -> do
    loop $ \j -> do
      c <- op "mul" [a i j, b i j]
      d <- op "mul" [a i j, c i j]
      return [d]
  loop $ \i -> do
    loop $ \j -> do
      c <- op "mul" [d i j]
      d <- op "mul" [a i j, c i j]
      return [d]

Where references are always explicit, and definitions are always

Basically what this means:

- assignment here is (incremental) definition of a finite function

- since we know the dependency graph of computations leading from
  constants and local indices to array references, we should be able
  to create a proof that the references are valid.

Maybe the real challenge here is to define what the binding means?

c <- op _ $ d i j

There are two levels to look at this:

- element-wise: c(i,j) is made of tx of d(i,j) and we're simply not
  writing down the indices at the LHS.

- whole array: c is made of tx of d as a whole, and there are some
  restrictions on how i and j can be used.

EDIT: This looks ok, but how to express it such that type inference