[kmicklas]

Not quite. Types can depend on runtime values. This can in effect _force_ the programmer to perform the required validation when accepting foreign data.

[lambdasquirrel]

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.

[dllthomas]

Almost arbitrarily - they must be computable... ;)

[kazagistar]

From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.

[kmicklas]

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).