Is it ever logical to have arrays without indexing (diag(A) seems to be such a case, logical conclusion of generic programming)?

Akatz · May 22, 2022, 11:31pm

Check out Dex. It’s early days, but the point is to hide indexing in type-safe type enumeration and have any remaining indexing throw errors at compile time (but doesn’t take the normal dependent typing approach, and allows controlled mutation) :

github.com

axch/dex-lang/blob/533ea9a71b9a1c2c5f3640b1dbefab0837d7b4b5/examples/levenshtein-distance.dx

'# Levenshtein Distance

'May 13, 2022

'The Levenshtein distance is the minimum edit distance between two
sequences, counting insertions, deletions, and substitutions each as 1.

'Let's see how well Dex handles the conventional dynamic program for
this: For each pair of prefixes of the input strings, the Levenshtein
distance between those prefixes is the minimum obtainable from the
prefixes one shorter by inserting, deleting, or substituting an
element.

'Here is the helper that builds the dynamic program table.  Dex's
flexible index sets let us encode the fact that the table is 1 larger
in each dimension than the inputs.  By capturing the relationship
statically we avoid both programmer off-by-one errors and runtime array
bounds checks.

def levenshtein_table

This file has been truncated. show original

By exploiting the connection between arrays and memoized typed functions, you can have type safety but still generate all possible values of an array on the fly. So with the right type, you can avoid all or some index arithmetic that would normally be required, and it works on the GPU with the right loop effect type.

It has array shape information at compile time (even with complex shapes), without the complexities of full dependent typing or massive compilation cost. These array types or “index sets” are expressive enough to represent named dims, array of arrays and more, with full type safe indexing and safe/predictable parallel loops.

The dynamic programming levenshtein-distance example exploits this abstraction but still ends up being very close to c++ in runtime (without future compiler optimizations). It is totally type safe and even enforces at compile time that the output table is 1 larger
in each dimension than the inputs.

Compare to a Julia’s implementation which has more branching and error prone index arithmetic.

It would be interesting to see how we might be able to match the concision/expressiveness with a https://github.com/JuliaFolds/FGenerators.jl version…but we’ll never get the same type safety unless we could somehow lift it into the type domain and use JET.jl. Also not sure about SIMD, loop rolling, parallelism, GPU and other optimizations that the index sets approach provides as well.

As of [#876] tables themselves can be used as index sets, letting us build index sets whose dimension is determined at runtime, but still tracked by the compiler. For instance, the type (Fin D)=>letter represents the set of all D-letter strings. And the table for i:((Fin D)=>letter). i instantiates all those strings. For another example, ((Fin D)=>(Fin s))=>Float is a table of Floats with s^D elements.