One motivation for Apple was demonstrating typed array programming. Shape types are rich; we can use types as witnesses as in QuickCheck, generating test cases that are shape-correct.
We can test that the dot product of a vector with itself is nonnegative, viz.
:qc \x. [(+)/(*)`x y] x x >= 0.0
x is inferred to have type Vec i float in this case, so the property test
will only provide vectors, i.e. arrays of rank 1. This avoids the need to
specify what the programmer has already written in the expression.
Contrary to perception, static typing is not burdensome; in fact it is languages such as Python which lack, requiring explicit specification in order to generate test cases.
