1. 45
  1. 9

    Idris looks really well designed, and I think these improvements are actually quite significant. Strictness by default is a game-changer for me; apparently the records and monads are more convenient to use (and there are effects, too? Not sure how experimental they are). If Idris was self-hosted, produced good static binaries with performance comparable to OCaml, and had a package manager I would definitely give it a serious try.

    1. 6

      Idris also has a quite buggy implementation at the moment, but like everything else you mentioned, it is a solvable problem. I think it’s a contender for a widely used industrial language in the future. Though at the moment it’s mainly used by people with pretty sophisticated FP knowledge, I think its dependent types and effect system may ultimately become something that’s easier for newcomers to understand than a lot of Haskell is.

      1. 7

        They are pretty unapologetic about 1.0 not being industry-grade, and it is not quite the goal of the language:

        Will version 1.0 be “Production Ready”?

        Idris remains primarily a research tool, with the goals of exploring the possibilities of software development with dependent types, and particularly aiming to make theorem proving and verification techniques accessible to software developers in general. We’re not an Apple or a Google or [insert large software company here] so we can’t commit to supporting the language in the long term, or make any guarantees about the quality of the implementation. There’s certainly still plenty of things we’d like to do to make it better.

        All that said, if you’re willing to get your hands dirty, or have any resources which you think can help us, please do get in touch!

        They do give guarantees for 1.0:

        Mostly, what we mean by calling a release “1.0” is that there are large parts of the language and libraries that we now consider stable, and we promise not to change them without also changing the version number appropriately. In particular, if you have a program which compiles with Idris 1.0 and its Prelude and Base libraries, you should also expect it to compile with any version 1.x. (Assuming you aren’t relying on the behaviour of a bug, at least :))

        Don’t get me wrong, I believe Idris is a great language precisely because of that: they want to be primarily a research language, but provide a solid base for research happening on top of their core. They have a small team and use those resources well for one aspect of the language usage. I would highly recommend having a look at it and working with it, this is just something to be aware of.

        from https://www.idris-lang.org/towards-version-1-0/

        1. 5

          Haskell is great because it’s where a lot of these ideas were tested and figured out. But it also has the cruft of legacy mistakes. Haskell can’t get rid of them now, but other languages can certainly learn from them.

      2. 1

        Re. 1:

        “[Haskell] code gets obscured by successive by pack and unpack calls”

        “You can call pack and unpack strings to go back an forth to a List Char representation [in Idris].”

        So, they’re exactly the same? I’m not sure what the improvement is here. Just the fact that Idris uses the equivalent of Text by default?

        Some of these other things are very cool. I’m especially a fan of the Show instance of IO values.

        1. 6

          There are some functions that are directly : String -> String -> String, concat comes to mind. This makes them much more efficient.

          1. 4

            So, they’re exactly the same? I’m not sure what the improvement is here. Just the fact that Idris uses the equivalent of Text by default?

            Pretty much. It doesn’t care about the details around chars unless you specifically request them.

            1. 6

              Which is a big deal, if you ask me. Haskell strings are a horror story because the default implementation is not the sane one. This is also true for more base library objects, such as ListT that was re-implemented several times.

              Take a look at Python 3. Not many libraries re-implement base functionality. Perhaps because it keeps evolving to actually remain a practical base. Unicode mess was cleaned up, collections were added, asyncio will help unification across several frameworks and so on.

            2. 1

              So, they’re exactly the same? I’m not sure what the improvement is here. Just the fact that Idris uses the equivalent of Text by default?

              Being Text by default means one isn’t likely to call pack and unpack much: all the APIs are in terms of an efficient type so you won’t be converting for efficiency and then deconverting to show (or perform other operations).