# Typesafe Loops

## Kinds

We have three kinds. The most familiar is `Data`, which is your usual `*` for types that have a runtime representation.

``````Data     :: Kind
a        :: Data``````

Next, we have `Rate` kinds, which are a very coarse symbolic signifier of the length of an array or loop. In the absence of dependent types, performing arbitrary computations on rates would be prohibitively hard, if not impossible.

``````Rate     :: Kind
k        :: Rate``````

Instead, we only allow certain limited computations, and take a conservative view of equality: if two arrays have the same rate syntactically they are assured to be equal, but the converse is not necessarily true.

``````Append   :: Rate ~> Rate ~> Rate
Cross    :: Rate ~> Rate ~> Rate``````

Other rate computations that are too hard to capture exactly are approximated by introducing existential rates for the result. For example, the output rate of a filter is the number of elements that satisfy the predicate. Since we cannot evaluate this during type checking, we simply say that there exists some rate for the result, but we don’t know what it is. Essentially, this means that the result rate is not equal to any of the outer rates.

``````filter   :: [k : Rate]. [a z : Data]
-- Predicate
.  (a -> Bool)
-- Input vector of rate k
-> RateVec k a
-- Introduce existential for k'
-> ([k' : Rate]. RateVec k' a -> z)
-> z``````

Finally, `Proc` kinds are used to stop leaking loop computations out of the loop environment. For each loop, we introduce a new existential `Proc` and require that all loop combinators are annotated with the same process.

``````Proc     :: Kind
p        :: Proc``````

## Types

We have three different array representations. `Vector a`s are buffers of `a`s with no type-level rate information.

``Vector   ::                 Data ~> Data``

`RateVec k a`s have been converted from `Vector a` and anointed with a rate `k`.

``````RateVec  ::         Rate ~> Data ~> Data

ratify0  :: [z : Data]
.  Nat
-> ([k : Rate]. z)
-> z

ratifyN  :: [a0..aN z : Data]
.  Vector    a0 .. Vector   aN
-> ([k : Rate]. RateVec k a0 .. RateVec k aN -> z)
-> z``````

`Series p k a` exist inside a process `p`, and only exist in memory as a single element at a time, unless explicitly converted to or from a manifest buffer.

``````Series   :: Proc ~> Rate ~> Data ~> Data

series   :: [p : Proc]. [k : Rate]. [a : Data]
.  RateVec k a -> Series p k a``````

Selectors convert from one rate to others. Selectors rely on Series, so can only exist within the context of a specific process. Sel1 is so named because it only has one output rate.

``````Sel1     :: Proc ~> Rate ~> Rate ~> Data

mkSel1   :: [p : Proc]. [k1 kL : Rate]
.  Series p k1 Bool
-> ([k2 : Rate]. Sel1 p k1 k2 -> Process  p kL)
-> Process  p kL

pack     :: [p : Proc]. [k1 k2 : Rate]. [a : Data]
.  Sel1 p k1 k2
-> Series p k1 a
-> Series p k2 a``````

Segment descriptors represent nested arrays. The constructor here relies on a Series, but I imagine the same segment descriptor could be used by multiple processes. Indeed, a segment descriptor could even be used as an argument to a function, so I don’t think it should be restricted to a particular process.

``````Segd     ::         Rate ~> Rate ~> Data

mkSegd   :: [p : Proc]. [k1 kL : Rate]
.  Series  p k1 Nat
-> ([k2 : Rate]. Segd  k1 k2 -> Process  p kL)
-> Process  p kL``````

Processes are indexed by a proc and a rate describing the loop size. The proc is introduced as an existential by `runProc`, which ensures that different calls to runProc cannot share processes. Only processes of the same proc and loop size can be merged, or joined, together. Loop sizes can be changed in specific ways, for example a smaller loop can be injected into a larger one, and we end up with a constructive proof witness that all loops in the process can be converted to the same size.

``````Process  :: Proc ~> Rate         ~> Data

runProc  :: [k : Rate] [a : Data]
. ([p : Proc]. Unit -> Process p k)
-> Unit

pjoin    :: [p : Proc]. [k : Rate]
.  Process p k
-> Process p k
-> Process p k``````

## Combinators

``````rep      :: [p : Proc] [k : Rate] [a : Data]
.  a -> Series p k a

reps     :: [p : Proc]. [k1 k2 : Rate]. [a : Data]
.  Segd k1 k2 -> Series p k1 a -> Series p k2 a

indices  :: [p : Proc]. [k1 k2 : Rate].
.  Segd k1 k2 -> Series p k2 Nat

map      :: [p : Proc]. [k : Rate] [a b : Data]
.  (a -> b) -> Series p k a -> Series p k b

mapN     :: [p : Proc] [k : Rate] [a0..aN : Data]
.  (a0 -> .. aN) -> Series p k a0 -> .. Series p k aN

sappend  :: [p : Proc]. [k l : Rate]. [a : Data]
.  Series p         k    a
-> Series p           l  a
-> Series p (Append k l) a

scross   :: [p : Proc]. [kR kO : Rate]. [a b : Data]
.  Series p        kR      a
-> RateVec            kO     b
-> Series p (Cross kR kO) (a,b)

generate :: [p : Proc]. [k : Rate]. [a : Data]
.  (Nat  -> a) -> Series p k a

reduce   :: [p : Proc]. [k : Rate]. [a : Data]
.  Ref a -> (a -> a -> a) -> a -> Series p k a -> Process p k

folds    :: [p : Proc]. [k1 k2 : Rate]. [a : Data]
.  Segd  k1 k2 -> Series p k1 a -> Series k2 b

scatter  :: [p : Proc]. [k : Rate]. [a : Data]
.  Vector a -> Series p k Nat  -> Series p k a -> Process p k

gather   :: [p : Proc]. [k1 k2 : Rate]. [a : Data]
.  RateVec k1 a -> Series p k2 Nat  -> Series p k2 a

fill     :: [p : Proc]. [k : Rate]. [a : Data]
.  Series p k a
-> Process p k``````

## Changing rates

To merge processes together, they must have the same size. However, we can inject certain loops inside larger ones. The general rule seems to be to inject more specific, or smaller, loops inside more general, larger ones, but that’s not always right.

``````Inject   :: Rate ~> Rate ~> Data

iid      :: [k : Rate]
.  Inject k k

pinj     :: [p : Proc]. [k k' : Rate]
.  Inject    k k'
-> Process p k
-> Process p   k'``````

Injecting into appends is simple: given an append of two consecutive loops `k` and `l`, we could inject a `k` into the left, or an `l` into the right.

``````injAppL  :: [k k' l : Rate]
.  Inject k         k'
-> Inject k (Append k' l)

injAppR  :: [k l l' : Rate]
.  Inject l           l'
-> Inject l (Append k l')``````

We can also perform arbitrary injections over the contents of an append.

``````injApp   :: [k k' l l' : Rate]
.  Inject         k            k'
-> Inject           l             l'
-> Inject (Append k l) (Append k' l')``````

Given a filter, or Sel1, we can inject the known-smaller filter result into the original rate.

``````injSel1  :: [p : Proc]. [j k l : Rate]
.  Sel1  p   k l
-> Inject  j   l
-> Inject  j k``````

Here, it gets hairy. Given a `Segd k1 k2`, we could plausibly go in either direction. Since `mkSegd` introduces the new rate, k2, moving from k2 to k1 seems to make more sense: k1 is the more general rate that we were originally working over.

``````injSegd  :: [j k l : Rate]
.  Segd      k l
-> Inject  j   l
-> Inject  j k``````

A loop of size `k * l` can be converted to a nested loop, whose outer rate is `k` with an inner loop of `l` at each iteration. We only track the outer rates in the types.

``````injCross :: [j k l : Rate]
.  Inject j (Cross k l)
-> Inject j        k``````

## Examples

### Segmented

``````segs lens base things
= do   segd    = mkSegd    lens
bases   = reps      segd base
offsets = indices   segd
ixs     = map2 (+)  bases offsets
results = map  (things!) ixs
firsts  = map  (things!) base
firstsr = reps      segd firsts
(results, firstr)``````

becomes

``````segs    [p : Proc] [k1 kT : Rate]
(lens      : RateVec k1 Nat)
(base      : RateVec k1 Nat)
(things    : RateVec kT Float32)
(out1 out2 : Vector     Float32)
: Process p k1
= do   lens' = series lens                             -- Series k1 Nat
base' = series base                             -- Series k1 Nat
mkSegd [:p k1 k1:] lens'                        -- Process p k1
(/\(k2 : Rate). \(segd : Segd k1 k2).
do  bases   = reps    segd base'            -- Series k2 Nat
offsets = indices segd                  -- Series k2 Nat
ixs     = map2    add bases offsets     -- Series k2 Nat
results = gather  things ixs            -- Series k2 Float32
firsts  = gather  things base'          -- Series k1 Float32
firstsr = reps    segd firsts           -- Series k2 Float32

pout1   = fill    out1 results          -- Process p k2
pout2   = fill    out2 firstsr          -- Process p k2

pouts   = pjoin pout1 pout2             -- Process p k2

i       = injSegd segd iid              -- Inject k2 k1

pinj i pouts)                           -- Process p k1``````

### Partitioning

``````part ins
= filter (>5) ins ++ filter (<5) ins``````

becomes

``````part [p : Proc] [k : Rate]
(ins : RateVec k Int)
(out : Vector    Int)
: Process p (Append k k)
= do   ins' = series   ins                             -- Series  p k  Int
gts  = map (>5) ins'                            -- Series  p k  Bool
lts  = map (<5) ins'                            -- Series  p k  Bool
mkSel1 gts                                      -- Process p (Append k k)
(/\(kg : Rate). (\sg : Sel1 k kg).
mkSel1 lts                                      -- Process p (Append k k)
(/\(kl : Rate). (\sl : Sel1 k kl).
do  gs   = pack    sg  ins'                 -- Series  p kg Int
ls   = pack    sl  ins'                 -- Series  p kl Int

ap   = sappend gs  ls                   -- Series  p (Append kg kl) Int
pout = fill    out ap                   -- Process p (Append kg kl)

isg  = injSel1 sg  iid                  -- Inject  kg k
isl  = injSel1 sl  iid                  -- Inject  kl k

i    = injApp isg isl                   -- Inject (Append kg kl) (Append k k)

pinj pout))                             -- Process p (Append k k)``````

### Duplicating work

An append can duplicate work.

``````dupe ins
= do   exp = map expensive ins
exp ++ exp``````
``````dupe [p : Proc] [k : Rate]
(ins : RateVec k Int)
(out : Vector    Int)
: Process p (Append k k)
= do   ins' = series   ins                             -- Series  p k  Int
exp  = map expensive ins'                       -- Series  p k  Int
ap   = sappend exp exp                          -- Series  p (Append k k) Int
fill out ap                                     -- Process p (Append k k)``````

Will be translated into something imperative like this, with calls to expensive for both sides of the append:

``````int o = 0;
for (int i = 0; i != ins.length; ++i) {
out[o++] = expensive(ins[i]);
}
for (int i = 0; i != ins.length; ++i) {
out[o++] = expensive(ins[i]);
}``````

Is this a problem?

I think this could be outlawed with linear types, or by changing append to introduce two new process contexts:

``````append :: [p : Proc]. [k1 k2 : Rate]. [a : Data]
.  ([p' : Proc]. Series p' k1 a)
-> ([p' : Proc]. Series p' k2 a)
-> Series p (Append k1 k2) a``````

Here, each side of the append must be a series in a fresh existential context, which means it cannot refer to outside Series in process p. We could still write the above program, but the duplication would have to be explicit:

``````dupe [p : Proc] [k : Rate]
(ins : RateVec k Int)
(out : Vector    Int)
: Process p (Append k k)
= do   ap = sappend                                    -- Series  p  (Append k k) Int
(/\(p' : Proc).
do  ins' = series   ins                     -- Series  p' k  Int
exp  = map expensive ins'               -- Series  p' k  Int
exp)
(/\(p' : Proc).
do  ins' = series   ins                     -- Series  p' k  Int
exp  = map expensive ins'               -- Series  p' k  Int
exp)
fill out ap                                     -- Process p (Append k k)``````

However this doesn’t play nicely with filters or other existentials, so we would need to change its type to allow for that, which actually gets rather confusing. I think at this point, we’re screwed.

``````append :: [p : Proc]. [a z : Data]
.  ([p' p'' : Proc].
([k1 k2 : Rate]. Series p' k1 a -> Series p'' k2
-> (Series p (Append k1 k2) a -> z) -> z) -> z)
-> z

append
(/\(p1 p2 : Proc).
\(f : [k1 k2 : Rate]. Series p1 k1 -> Series p2 k2
-> (Series p (Append k1 k2) a -> z)
-> z).
f (_ : Series p1 k3 a) (_ : Series p2 k4 a)
(\(ap : Series p (Append k3 k4) a). return z))``````
November 9, 2014