4 ms·

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 11y ago
  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 11y ago
    Almost arbitrarily - they must be computable... ;)
    • kazagistar 11y ago
      From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.
      • kmicklas 11y ago
        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).