Not quite. Types can depend on runtime values. This can in effect _force_ the programmer to perform the required validation when accepting foreign data.
Not only that but you can arbitrarily encode constraints. Want to check something silly like whether there's an even number of elements in a list? Yea you can do that, and pass it along. I can do stuff like, okay, I know the max size of the files we're going to accept is 1mb.
Comments
Not quite. Types can depend on runtime values. This can in effect _force_ the programmer to perform the required validation when accepting foreign data.
Not only that but you can arbitrarily encode constraints. Want to check something silly like whether there's an even number of elements in a list? Yea you can do that, and pass it along. I can do stuff like, okay, I know the max size of the files we're going to accept is 1mb.
Almost arbitrarily - they must be computable... ;)
From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.
You're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).