Re:Why is Idris 2 so much faster than Idris 1?
by icen on Tuesday May 26, 2020 @05:18AM
(#23308895)
It is more that you can have values like `payload : if byte[TYPE_OFFSET] == TYPE_INT then Int else String`.
You are required to disambiguate the type before anything useful can be done. What has happened is that you have types being passed around by functions and evaluations which reflect dynamic behaviour at runtime - but there is a type statically known at all times for each part of the program.
You are required to disambiguate the type before anything useful can be done. What has happened is that you have types being passed around by functions and evaluations which reflect dynamic behaviour at runtime - but there is a type statically known at all times for each part of the program.