> Gradual, dependently typed languages are the future
What's that?
Idris is dependently typed.
> Gradual typing is a type system that lies inbetween static typing and in dynamic typing. Some variables and expressions may be given types and the correctness of the typing is checked at compile time and some expressions may be left untyped and eventual type errors are reported at runtime.
That sounds miserable. I can't see how one would guarantee anything when types of other things aren't known. And I can't see how to connect that to dependent types either.
replies(4):