[Haskell] Re: ANN: binary arithmetic type library over natural kinds

[oleg at pobox.com]

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.