`[<<][rtl][>>][..]`
Mon May 27 08:52:05 EDT 2019

## References

```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
implicit.

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
works?

```
`[Reply][About]`
`[<<][rtl][>>][..]`