Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Idris: A Language for Type-Driven Development. Parent comment
But the examples given missed the point imho.
All of the stated things don't need any type level machinery. You can just test things at runtime and be good.
If you want to prove things at compile time that's a very different story.
But than this needs to be explicitly stated in the examples.
There are no comments on this comment yet.
But the examples given missed the point imho.
All of the stated things don't need any type level machinery. You can just test things at runtime and be good.
If you want to prove things at compile time that's a very different story.
But than this needs to be explicitly stated in the examples.