undefined | Better HN

0 pointsAce1710y ago0 comments

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

0 comments

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.

j / k navigate · click thread line to collapse

0 pointsAce1710y ago0 comments

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

0 comments

dllthomas10y ago

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.

j / k navigate · click thread line to collapse