David Roundy wrote:

data Arr a n = ... -- n is a type-level variable describing the dimension -- a is the data type stored withArrayFromList :: [a] -> (Nat n => Arr a n -> b) -> b ... But what I'm dreaming of is that the type system would enforce those run-time checks when necesary. e.g.

catArray :: Add n1 n2 n3 => Arr a n1 -> Arr a n2 -> Arr a n3

I imagine this is harder, but it's needed if these type-level binaries will be useful for the sorts of programs I tend to write--which have run-time sizes.

I believe the lightweight static capabilities approach will be more appropriate here. It already provides the function withArrayFromList, which is called `brand'. For example, KMP-deptype.hs includes

-- brand the packed string brandPS:: PackedString -> (forall r. (BPackedString r, BIndexP1 r) -> w) -> w -> w

which is quite like `withArrayFromList' only using `r' rather that 'n' and with an extra argument which is returned when the source packed string turns out empty. The approach almost fulfills your dream: only, instead of the `system' inserting run-time checks, it is the programmer who inserts the checks, to please the typechecker. In the catArray example, one would write something like that

-- kernel data Arr a = ... newtype BArr n a = BArr{unBArr:: Arr a} -- BArr data ctor not exported brand :: Arr a -> (forall n. (BArr n a, BIx n) -> w) -> w -- User code catArray :: BArr n1 a -> BArr n2 a -> Arr a catArray a1 a2 = concatArr (unBArr a1) (unBArr a2) test a1 a2 = brand (catArray a1 a2) (\newarray itsbound -> ...)

The user can easily write catArray to create an unbranded array. One needs branding however to be able to index into the array: thus one has to invoke brand (the `smart' constructor of the BArr type), which will do the run-time check. The kernel may provide other constructors of BArr from arguments of some particular types, which let us avoid the run-time check. Alas, the style of writing is a bit like CPS -- OTH, we write monadic code, which is CPS in thin disguise, with no complaints... One can use existentials to make the code look more direct-style, however. The programming becomes a bit like theorem proving: the indexing operation needs BArr, so we have to consider all the ways we can get a value of that type. The kernel provides a few constructors; one of which, brand, always applies, but it involves a run-time check. There may be other constructors; but they require arguments of particular types. We should see if we can produce the values of those types from already available values, etc. This is back-chaining theorem proving.