[<<][rtl][>>][..]
Wed May 8 07:30:29 EDT 2019

Map/Fold

It is important to look at this the right way.  Ideally, I would like
to have only one looping construct: the one that includes output
feedback.

This encodes a mapping between the multi-dimensional object, and a
sequential encoding of the dependencies.  Note that mathematically,
there might be many forms of evaluation.

So ideally I want to express only the dependencies.

But in practice, I will need a space filling curve, a sequence.

Does it make sense to express things in that higher abstraction?  Or
is it better to stick to the reality of the loop?

In general it is better to do the specific case first to at least have
an example of what to generalize.

What is an array?

a :: i -> v

With the caveat that i is contained in an interval, and for a fold,
the interval grows during the loop.

In this context, map looks like:


map ::  (a -> r) -> (i -> a) -> (i -> r)


In practice, we want access to the current index:

imap ::  (i -> a -> r) -> (i -> a) -> (i -> r)


The multivariate version has v,w be tuples.  This is no essential
difference, so let's ignore it for now.

The version where random access is possible:

irmap :: (i -> (i -> a) -> r) -> (i -> a) -> (i -> r)


Note that (i -> a) now can be factored out completely into a global
environment.  Maybe this is important?

(i -> a) -> (i -> r)

What does this actually mean?  That a constant input is just a
function that has no influence on the shape of things.


Let's move on to folds first.

A fold looks like:


ifold ::  (i -> s -> a -> s) -> s -> (i -> a) -> s


Generalizing the loop state to an array, and allowing access to the
previous results inside the loop gives:

iafold :: (i -> (i -> s) -> s) -> (i -> s) -> (i -> s)

This seems to be the essential component, because all of these i->s
are different things.  The induction step is to take

i -> s where i \in [0,n[ to
i -> s where i \in [0,n]

It is a transformation between types.  I don't think I can express
this in the current encoding.

To read iafold's type: take a function that grows an array by one
element, and use it to transform an array of size 0 into an array of
size N (concrete).  Separately, provide some context such that the
array growing function can also reference arrays that are not being
constructed.

So basically, I'm building a sequential array constructor language.

Even simplified: the input i->s is actually just () if it is an empty
array.  So the type can be even simpler:

iafold' :: i -> (i -> (i -> s) -> s) -> (i -> s)

Take the size of an array, a body that has access to the current size
and the array constructed in the last step, and produce a new array.
Actually, the body needs access to the total size as well, but this
can be hidden in the closurs because it is a constant.

So it appears that the idea of "environment" is very important. Also,
there is some need to turn this into a type family, where the
induction step can be expressed at the type level.

Starting from the main iteration,
- map fits in here by never using the input state
- fold filds by only using the last state (reusable state variable)
- more complex siso machines can use multiple delay elements

It seems that focusing on the one true abstraction makes sense,
because that will be the only one that needs to be implemented.  In a
second step, constraints can be added at the type level for more
constrained iterators, and these type annotations could then be
propagated to the intermediate language to be used in non-local
optimizations, i.e. optimizations that will need to fold over the
entire IR.



Summary:

- make indices explicit

- explicit indices allow constant arrays to be hidden in an
  environment

- the essential "step" is appending one element to an array, where the
  whole previous array can be used as input.

- todo: find some way of encoding the n->n+1 size extension induction
  in the type

- additional patterns could be expressed as constraints on the main
  pattern: map, fold, and combinations with more complex state.




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