[Ace17]

I don't get it. Is it just about rediscovering std::array?

[dllthomas]

Can you append a std::array<int, x> and a std::array<int, y> to get a std::array<int, x+y> with x and y chosen at runtime?

[Ace17]

Of course not. In my understanding, the article was about static type checking, though.

[dllthomas]

It is! That's what is so cool about it! Idris lets you write an append that will work for any X and Y chosen at runtime, but will check that the result must have length X + Y at compile time.