[<<][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][>>][..]