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

[John Meacham]

On Thu, Mar 08, 2007 at 08:24:57AM -0800, David Roundy wrote:
> This looks pretty nice, but I'm curious as to whether it can be extended to
> verify run-time checks?  i.e. I'd like to be able to use a natural number
> determined at run-time to create arrays that are statically
> bounds-checked.
> 
> i.e. I'm imagining something like this:
> 
> 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

I think the ST trick can be done here safely if you change the type to

> withArrayFromList :: [a] -> (forall n . Nat n => Arr a n -> b) -> b

notice the rank-2 type,

this ensures the argument is a function that can work on arrays of any
size, without specifying any size in particular at compile time.


run time checks would be needed only if you wanted to refine the type:

> assertSize4 :: Arr a n -> Maybe Arr a N4

but what is cool is you just need to perform this run-time check once
then all your code can work on 'Arr a N4' knowing that it has exactly 4
elements. the type system takes care of propegating the fact you already
did the appropriate run-time check for you. quite nice.

> which would allow me to initialize an array with static bounds checking,
> and use it in a function.  Of course, to support this we'd also need
> run-time comparison, add, etc.  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 think this sort of thing will 'just work' unless I am misunderstanding
what you want. 

This all seems very interesting, I would like it if there were a
standardish type level arithmetic library in base. though, I find it a
little aethetically jarring without user defined kinds like in omega.

        John

-- 
John Meacham - ⑆repetae.net⑆john⑈