3 ms·

Somewhat tangential, but I became infatuated with Idris's Effect system as a more approachable alternative to using monads directly. Yes, it's still monads unde

Somewhat tangential, but I became infatuated with Idris's Effect system as a more approachable alternative to using monads directly. Yes, it's still monads under the hood IIRC, but the syntax is a lot easier to reason about IMO. https://www.idris-lang.org/documentation/effects/ https://www.idris-lang.org/documentation/effects/

tombert 9y ago
I feel like a recurring theme I find in Idris (though keep in mind it's just something I play with every now and then, not something I use with any kind of regularity) is that it has this "feels like Haskell, but less frustrating and cleaner" quality. I feel like I make less dumb mistakes while using it, and it gives me pretty much all the stuff I love about Haskell. You of course have the relatively simple effects system (as mentioned),, but you also have the ability to use `do` notation without being in the monad context, and eager evaluation, which I find makes my program simpler to reason about.
- Legogris 9y ago
  I agree. I like to think that Idris is to Haskell what C# is to Java, with the exception that it's still a non-production-ready academic open source language.
  - lmm 9y ago
    It's not that academic AIUI - it was designed for production use, right?
    - Legogris 9y ago
      From the release notes of 1.0[0] last year: > Idris is primarily a research tool, arising from research into software development with dependent types which aims to make theorem proving and software verification accessible and practical for software developers in general. In calling this “1.0”, we mean no more than that the core language and base libraries are stable, and that you can expect any code that compiles with version 1.0 to compile with any version 1.x. > Since Idris has less than one person working on it full time, we don’t promise “production readiness”, in that there is still a lot to do to make the compiler and run time efficient, and there may be libraries you need which are not available. And, there will certainly be bugs! [0] https://www.idris-lang.org/idris-1-0-released/ https://www.idris-lang.org/idris-1-0-released/

tombert 9y ago

I feel like a recurring theme I find in Idris (though keep in mind it's just something I play with every now and then, not something I use with any kind of regularity) is that it has this "feels like Haskell, but less frustrating and cleaner" quality. I feel like I make less dumb mistakes while using it, and it gives me pretty much all the stuff I love about Haskell. You of course have the relatively simple effects system (as mentioned),, but you also have the ability to use `do` notation without being in the monad context, and eager evaluation, which I find makes my program simpler to reason about.

Legogris 9y ago
I agree. I like to think that Idris is to Haskell what C# is to Java, with the exception that it's still a non-production-ready academic open source language.
- lmm 9y ago
  It's not that academic AIUI - it was designed for production use, right?
  - Legogris 9y ago
    From the release notes of 1.0[0] last year: > Idris is primarily a research tool, arising from research into software development with dependent types which aims to make theorem proving and software verification accessible and practical for software developers in general. In calling this “1.0”, we mean no more than that the core language and base libraries are stable, and that you can expect any code that compiles with version 1.0 to compile with any version 1.x. > Since Idris has less than one person working on it full time, we don’t promise “production readiness”, in that there is still a lot to do to make the compiler and run time efficient, and there may be libraries you need which are not available. And, there will certainly be bugs! [0] https://www.idris-lang.org/idris-1-0-released/ https://www.idris-lang.org/idris-1-0-released/