Re:Why is Idris 2 so much faster than Idris 1?
by afiori on Tuesday May 26, 2020 @05:02AM
(#23308825)
The terminology is nearing its limit when talking about these kind of things.
I believe that static typing here means that there is no need for runtime dynamics type checks (outside of things like dynamic dispatch as with haskell typeclasses).
That is you can have a body of code where a variable can assume multiple incompatible types, but you always know that it will be the right one.
I would say it is a change in paradigm. Similarly to how rust' borrow checker and lifetimes change the paradigm of manual vs GC memory management
I believe that static typing here means that there is no need for runtime dynamics type checks (outside of things like dynamic dispatch as with haskell typeclasses).
That is you can have a body of code where a variable can assume multiple incompatible types, but you always know that it will be the right one.
I would say it is a change in paradigm. Similarly to how rust' borrow checker and lifetimes change the paradigm of manual vs GC memory management