Improve projection detection to make Vector indexing O(1)

[ollef]

This was originally discovered in #104, and there's also a workaround there.

The ReturnDirection pass detects when it's safe for a function that returns something of unknown type to return it by (derived) pointer instead of by copying to an out parameter. For some reason this doesn't kick in for vector indexing. My hunch is that this is causing us to generate code that LLVM's optimiser doesn't easily see through, meaning that we don't get the constant-time goodness we would want.

This needs to be investigated and fixed if possible.

[bglgwyng]

Have you considred Vector indexed by Bin n rather than Nat? Here's a (surely invalid) sixten code for it.

-- Bin n represents n bits.
-- I (O (I H)) = 101(2)
type Bin: Nat -> Type where
  H: Bin 0
  I: Bin n -> Bin (Sunn c)
  O: Bin n -> Bin (Sunn c)

shift: n -> Bin m -> Bin (n + m)
shift Zero x = x
shift (Succ n) H = O (shift n H)
shift (Succ n) (I x) = I (shift n x)
shift (Succ n) (O x) = O (shift n x)

Vector : forall n. Bin n -> Type -> Type
Vector (H) _ = Unit
Vector (I H) a = a
Vector @n (I x) a = Pair (Pair (Vector y a) (Vector y a)) (Vector x a)
  where y = I (shift I (n - 1))
Vector (O x) a = Vector x a)

index : forall a. forall n. (len : Bin n) -> Vector len a -> Bin n -> Maybe a
index H MkUnit _ = Nothing
index (I H) x 0 = Just x
index (I y) (MkPair x _) (I z) = index y x z
index (I y) (MkPair _ x) (O z) = index y x z
index (O y) x (O z) = index y x z

With this definition, Vector n a is built like a binary trie and an index can be considered to be a path of trie . I think this definition represents the machine behavior more precisely. Random access is not O(1) but O(log n) where n is the length of address. Roughly speaking, memory access in 64bit address is 2 time slower than in 32 bit one.

I'm not sure LLVM can generate the optimized binary from this definition. But I think this definition gives sufficient information to do so. Because the pattern maching process within index skips elements in MkPairs whose summation of size is equal to given index i.

[ollef]

I haven't tried that, but it sounds like a fun idea to try!