Earlier quoted context omitted.
>And if it's not just a change in a default option, but the removal of laziness, we lose something, which will make the choice less obvious. What would we exactly lose? >As far as I can see, Idris is too much like Haskell to take its place. Porting thousands of libraries to a new language is a huge effort, so a huge advantage is required, which I don't see Idris offering. That is true, though. Perhaps Rust is the saf…
> What would we exactly lose? We'd lose composability and clearer code. This[1] section of the Haskell Wiki contains a good example. In short, with something like this: any :: (a -> Bool) -> [a] -> Bool any f lst = or boolLst where boolLst = map f lst the compiler can produce reasonably optimal code, because it doesn't have to convert the entire [a] to a [Bool] , because of lazy evaluation -- when or encounters the f…
any : (a -> Bool) -> Lazy List a -> Bool
... which would make it as performant and clearer than Haskell's any, since the laziness is explicit.
Someone with actual Idris experience might tell if it actually would work like this :) I guess we'd have to make sure that the used or function is also lazy.