Comment on Idris, a language that will change the way you think about programming (2015)Comments−Ace1710yI don't get it. Is it just about rediscovering std::array?−dllthomas10yCan 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?−Ace1710yOf course not. In my understanding, the article was about static type checking, though.−dllthomas10yIt 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.
Comments
I don't get it. Is it just about rediscovering std::array?
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?
Of course not. In my understanding, the article was about static type checking, though.
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.