This page is a work in progress. Here be dragons.

Position tracking allows for a compiler to be aware of how dataflow must happen in a program.

Consider a word that takes two integers and returns two integers:

define foo [Int Int -> Int Int]:
  {- something -}

This type can be satisfied by swap, the identity function, nip dup, and any other arrangement that satisfies the effect ( a a -- a a ) or ( int int -- int int ). The type checker tracks what types are on the stack, but not which input ended up in which output position.

Position tracking makes this visible. With position annotations, these are all distinct:

swap    : 0 1 -- 1 0
id      : 0 1 -- 0 1
nip dup : 0 1 -- 1 1 

Imagine you meant to use nip dup. We can now annotate the function like so:

define foo [Int Int -> Int Int] {0 1 -> 1 1}:
  nip dup

What happens if you make a mistake, and type dup nip instead? The position tracker infers the position effect of dup nip to be 0 1 -- 0 1, and flags an error since it does not match the wanted effect. We have now prevented a bug during compile time!

Combinators

The examples above have static position effects, the shuffle is fully known at definition time. What about words like dip, which applies a caller-supplied quotation underneath a preserved element?

dip :: [..r a [..r -> ..s] -> ..s a]

The type signature tells us the quotation transforms the deeper part of the stack and the top element is preserved, but it says nothing about which values within ..r end up where in ..s.

We need a way to say: “the position effect of this combinator is parameterised by the position effect of its quotation argument.”

In this case, we introduce a shuffle pattern P, bound by the quotation’s contract:

dip :: {0..n σ:[0..n-1 -> P] -> P n}

Read this as: dip takes a stack of depth n, plus a quotation σ whose position effect maps the bottom n-1 elements to some output P. The result is P, which is whatever the quotation produced, with the element n of the stack appended.

When the quotation σ is statically known, the checker can instantiate this effect by substituting the quotation’s concrete contract for P.