I don't understand the issue... it is trivial and in fact extremely common-place in impure languages to fundamentally disallow modifications to something's type. C++, which is definitely not pure but yet essentially has dependent types, is easily able to express this exact thought without problem, as your ability to modify things at runtime is extremely limited.
(Of course, the place where C++ is limited is its inability to template over non-concrete values, but I see nothing about its model that fundamentally limits its ability to conceptualize such a thing. It is still technically a dependently typed language even without the ability to do this, of course.) [edit: matt-noonan has told me that I am wrong on that last comment :(... so not "of course".]
#include <stdlib.h>
template <size_t S, typename E>
class Vect {
private:
E data[S];
public:
const size_t size() const {
return S;
}
E &operator [](size_t i) {
return data[i];
}
const E &operator [](size_t i) const {
return data[i];
}
};
template <size_t N, size_t M, typename E>
Vect<N + M, E> append(const Vect<N, E> &l, const Vect<M, E> &r) {
Vect<N + M, E> v;
for (size_t i(0); i != N; ++i)
v[i] = l[i];
for (size_t i(0); i != M; ++i)
v[N+i] = r[i];
return v;
}
int main() {
Vect<4, int> a;
Vect<2, int> b;
Vect<6, int> c = append(a, b);
Vect<8, int> d = append(a, b);
return 0;
}
test.cpp:36:18: error: no viable conversion from 'Vect<4UL + 2UL aka 6, [...]>' to 'Vect<8, [...]>'
Vect<8, int> d = append(a, b);
^ ~~~~~~~~~~~~
test.cpp:4:7: note: candidate constructor (the implicit copy constructor) not viable: no known conversion from 'Vect<4UL + 2UL, int>' to
'const Vect<8, int> &' for 1st argument
class Vect {
^
1 error generated.