I wonder if Idris could some day take Haskell's place. It sports default eager evaluation. Seems like the tooling (package managers etc.) isn't quite there yet, though.
I think it's more likely that, if dependent types prove really useful, Haskell will adopt these, and people will adapt their code, rather than port everything to a new language.
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.
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 safer bet, even if it lacks many nice things. The sum is probably quite a lot better still.
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
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.
Out of curiosity, would you know whether there exists sufficient strictness pragmas in Haskell to translate your example Idris (pseudo) code into Haskell? I often hear about performance/memory usage pitfalls with Haskell laziness, so it'd be really nice if Haskell were able to emulate Idris in this regards, by enabling enough LANGUAGE pragmas to require explicitly annotating types if laziness is desired.
Indeed. Some people actually use Haskell, though. They even claim it's fun and productive, but having done so myself, I'm forced to be undecided on whether they're just suffering from Stockholm Syndrome.