Lambda the Ultimate

BitC has vectors if you prefer that route. The reason arrays are in there is that there are far too many use cases for them in the context of being compatible with pre-existing data structures that come from the C world.

Your point is well taken, but it isn't addressing the topic.

We can probably summarise this as "you can't just abstract over literals without still suffering most of Pascal's problems" and "if you go any further you just got yourself dependently-typed programming"?

"you can't just abstract over literals without still suffering most of Pascal's problems"

Is that really the case? Aren't these problems really caused by the fact that an indexer in Pascal is not a first-class value?

For instance, in the Lightweight Static Capabilities linked paper above, any integer values have to be validated before being used as indexers. If they pass validation, they can then be passed around like ordinary indexes. Certainly there are limitations to this, but this would seem to strictly generalize Pascal's semantics.

"you can't just abstract over literals without still suffering most of Pascal's problems"

Is that really the case? Aren't these problems really caused by the fact that an indexer in Pascal is not a first-class value?

Emphasis on the just - doesn't have to be first class, but you do have to be able to pass it about.

Which is not necessarily a bad thing.

An example (using boost::array which is essentially the same as the shown array, but compatible with the standard algorithms):

template<typename T, int n, int m>
boost::array<T, n + m> concat(boost::array<T, n> const & x, boost::array<T, m> const & y)
{
   boost::array<T, n + m> result;
   std::copy(x.begin(), x.end(), result.begin());
   std::copy(y.begin(), y.end(), result.begin() + n);
   return result;
}

Isn't the problem of Pascal's arrays only that you can't write something like template<int n> in C++?

How would it work when you doesn't know before the length of the returned array?

For example, a filter function f(array[n] of T, predicate(T)->bool) -> array[m] which returns an array composed of the element where the predicate function is true..
All you can know at compile time is that m will be inferior or equal to n..

You can't write such a filter function returning an array with the correct size in C++ as it's unknown at compile-time. You'd have to return a vector, linked list, deque or any other collection with a dynamic size as in other languages.

Off-topic, if you are curious what you'd normaly do in C++ (but it's not interesting from a type system point of view):
You normaly don't program algorithms for a particular collection but you work with pairs of iterators representing a subrange of a collection (actually not only of a collection, but perhaps a file or whatever).
In this case you'd use std::remove_if to filter the whole array (well it's the opposite of filter as it removes the elements for which the predicate is true).

newEnd = std::remove_if(array.begin(), array.end(), predicate)

std::remove_if reorders the collection (or whatever is behind the iterators) so that the elements for which the predicated returns false are in the range [begin, newEnd).

If you don't want to mutate the collection you can use std::remove_copy_if which additionally takes an iterator to the begin of another range in which the result should be placed. You have to make sure on your own that the target range is big enough to hold the entire result!

In particular, I'll be interested to see how you get sound and complete inference out in usable form.

Who said anything about "complete inference"? :)

... at least that's what 'incomplete' inference for dependent types brings to my mind.

DML (Dependent ML) for example was built for around this idea: avoiding array bounds checks using static information on sizes available in types. The technology of singleton types was also further studied by Frank Pfenning and Bob Harper in different settings, have a look at their pages.

Yes, we fell down this hole in Cyclone as well and ended up with a design similar to DML at first, and then found this too limiting due to the lack of flow-sensitivity in the constraints. So we moved to something more like dependent types to handle the constraints. (That's what spawned the work on Hoare Type Theory and now Ynot.)

You might also check out Iavor Diatchki's thesis for doing sized types in Haskell.

Both of those pointers are helpful.

We're aware of Iavor's excellent work. His work and ours occurred at the same time independently, and I believe that the more general version presented in his dissertation was influenced in part by our discussions. The end form in BitC is more flexible, but not significantly different in its underlying structure. What Iavor's work does not resolve is prescriptive unboxing, which (in practice) interacts closely with the bit-level representation issue.