4 ms·

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,

by vesak 9y ago

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.

runeks 9y ago
Is a difference in a default option really enough for a language to take the place of another? 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. 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.
- firethief 9y ago
  A System F type system can't be replaced by a dependent type system without affecting existing code. There is no way to turn the libraries in Haskell into libraries in dependently-typed Haskell without "porting them to a new language" and all the work that entails.
  - taktoa 9y ago
    This is 100% false. The Calculus of Constructions is a superset of System F. You may be thinking of the fact that if you want your type system to be sound when interpreted as a logic, then termination must be guaranteed (which would break backwards compatibility). Dependent types and totality are often found together, but are in actuality orthogonal features.
- vesak 9y ago
  >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 safer bet, even if it lacks many nice things. The sum is probably quite a lot better still.
  - runeks 9y ago
    > 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 first True, the map f lst expression stops being evaluated because of lazy evaluation. [1] https://wiki.haskell.org/Non-strict_semantics#Why.3F https://wiki.haskell.org/Non-strict_semantics#Why.3F
    - vesak 9y ago
      I don't know Idris so this syntax is probably wrong, but by reading the docs for a short while, this would be 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.
      - runeks 9y ago
        I was commenting on what the effects would be from removing laziness. I'm not experienced enough in Haskell to know whether making strictness the default option would make sense, although I've seen a quote from Simon Peyton Jones saying he'd do that if he could start over. 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.
douche 9y ago
That place being the cool esoteric language that everybody fools around with on the weekends, but is almost never used seriously?
- vesak 9y ago
  > That place being the cool esoteric language that everybody fools around with on the weekends, but is almost never used seriously? 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.

by vesak 9y ago

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.

runeks 9y ago

Is a difference in a default option really enough for a language to take the place of another? 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. 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.

firethief 9y ago
A System F type system can't be replaced by a dependent type system without affecting existing code. There is no way to turn the libraries in Haskell into libraries in dependently-typed Haskell without "porting them to a new language" and all the work that entails.
- taktoa 9y ago
  This is 100% false. The Calculus of Constructions is a superset of System F. You may be thinking of the fact that if you want your type system to be sound when interpreted as a logic, then termination must be guaranteed (which would break backwards compatibility). Dependent types and totality are often found together, but are in actuality orthogonal features.
vesak 9y ago
>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 safer bet, even if it lacks many nice things. The sum is probably quite a lot better still.
- runeks 9y ago
  > 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 first True, the map f lst expression stops being evaluated because of lazy evaluation. [1] https://wiki.haskell.org/Non-strict_semantics#Why.3F https://wiki.haskell.org/Non-strict_semantics#Why.3F
  - vesak 9y ago
    I don't know Idris so this syntax is probably wrong, but by reading the docs for a short while, this would be 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.
    - runeks 9y ago
      I was commenting on what the effects would be from removing laziness. I'm not experienced enough in Haskell to know whether making strictness the default option would make sense, although I've seen a quote from Simon Peyton Jones saying he'd do that if he could start over. 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.

douche 9y ago

That place being the cool esoteric language that everybody fools around with on the weekends, but is almost never used seriously?

vesak 9y ago
> That place being the cool esoteric language that everybody fools around with on the weekends, but is almost never used seriously? 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.