1. 17

  2. 2

    How usable is Idris today?

    1. 12

      I’ve been using Idris to solve some of the advent of code problems this year. I’ve picked it up and put it down about 5 times now, for previous projects too.

      My breakdown:

      • The repl is very powerful. It has a bunch of nice features and is generally very fleshed out
      • The codegen for other platforms is very easy to get started with. I’ve been compiling Idris to JS, and using from inside Elm - Elm for the UI, Idris for the logic. It’s been working out pretty nicely on the whole
      • Proving and preventing things is very powerful, e.g just by limiting vectors to a size, you gain a bunch of reasoning around your code
      • Named arguments in the type signature is amazing and I wish more languages had that, especially since point-free style can be so pretty
      • Implied arguments can make a lot of sense sometime, e.g cast {from=String} {to=Int}
      • A lot of really nice extensions from Haskell are included by default. Records are generally better too
      • The docs are pretty well hidden.
        • Generally you are recommended to use the repl to figure things out, but a repl does not replace a good reference
        • Links to the library docs are nowhere to be found. I’ve had to bookmark the page because otherwise I end up losing it all the time
        • The tutorial is not written for inexperienced people.
      • Compiler error messages are definitely not friendly
      • Compile times for anything involving complicated proofs are very long
      • There’s a big lack of libraries. Part of this might be down to the lack of a package manager
      • Some things like take don’t seem to be correctly resolvable by the compiler - it will frequently complain about being unable to figure out which one you want unless you use List.take

      Overall, I’m having a blast. I’m even considering using it to generate Native Elm code in a safer manner. We’ll see about that though.

      1. 5

        I think the documentation being the REPL is a great thing:

        Idris> :doc Nat
        Data type Prelude.Nat.Nat : Type
            Natural numbers: unbounded, unsigned integers which can be pattern
            Z : Nat
            S : Nat -> Nat
        Idris> :apropos zip
        Prelude.List.unzip : List (a, b) -> (List a, List b)
        Split a list of pairs into two lists
        Prelude.Stream.unzip : Stream (a, b) -> (Stream a, Stream b)
        Create a pair of streams from a stream of pairs
        Prelude.List.unzip3 : List (a, b, c) -> (List a, List b, List c)
        Split a list of triples into three lists

        No need to click around a browser and find the right section. Just search your code and get documentation for whatever you like.

        1. 6

          It’s not discoverable. You need to know the commands in order to get the docs - e.g :doc, :search, :apropos, :t and so on. It’s not the natural point of entry for many people. It’s also quite hard to know what Idris has named some things, making searching via name or type not so easy. That’s when the reference docs come in handy. Having a browser and being able to link people directly to the function they need is kinda vital to encouraging more people to pick something up, I feel. repls for docs are great when you know what you’re even meant to be typing - not so much if you don’t :)

          1. 3

            I think it’s a natural entry point for people to type in :help. Yes, people have to learn how to use the commands but it’s definitely nicer than a website.

            You also often don’t have to know what Idris names things:

            Idris> :search S n + m = n + S m
            = Prelude.Nat.plusSuccRightSucc : (left : Nat) ->
                                              (right : Nat) -> S (left + right) = left + S right
            1. 1

              Until you’ve done something with Nat, you don’t even know what S or Z means. I think the repl is nice, but I also don’t think it can replace a website.

              1. 2

                My original example of :doc Nat shows what S and Z are - but I don’t think a REPL or a website are the appropriate tools for learning concepts such as Nat.

        2. 5

          Thanks for the constructive comments!

          We definitely need to improve documentation, or at least make it easier to find. There are links on http://www.idris-lang.org/documentation/ but it could still use some better organisation. When I wrote the tutorial it was pretty much entirely as a kind of bootstrap process to get some experienced people up to speed. I think it still serves a useful purpose in doing that, but some more introductory materials would be good. I keep hoping that someone will write an alternative tutorial with a different target audience, but alas “hoping” is not a very good strategy for getting things done…

          All of the other things you mention are things we’d like to improve. We don’t have many resources to throw at the problems though, so it’ll take time, but I hope we’ll get there eventually!

          1. 1

            No problem! Not sure if you remember me, but I was one of the people who interviewed to do a PhD with you (FRP in Idris). So it’s been on my “let’s really play with this” list since then - which was about two years ago! This is my first real attempt of using Idris from production perspective - other things I’ve made with it have mainly been experiments, whereas right now I’m seriously investigating using it with Elm, at least for some things.

            Is the main site on Github/open to pull requests? I’d love to help out a bit.

            1. 3

              Ah yes, I think I know who you are now :). We’re certainly open to pull requests. In particular, it’s good to see that you’re having some success with the JS back end, especially since we haven’t really put much effort into it for ages, so if you have useful contributions there, that’d be great!

            2. 1

              Do you have a link to a recent write-up on doing a systems application or component in IDRIS showing the triumphs or difficulties? And that is not by one of its developers? I mean, your write-ups are great but I like seeing what average newcomer from functional and/or systems background can do too. These can be different. ;)

          2. 2

            Main limitations for practical use for most people (assuming they get over the learning hurdle which is all most folks talk about) will be runtime performance and lack of a concurrency story.

            1. 2

              https://github.com/idris-lang/Idris-dev/blob/master/libs/base/System/Concurrency/Channels.idr is at least erlangish style concurrency via multiple processes if you do message passing.

              Everything else you said is spot on, Idris has lots of rough edges but its still a research compiler so to be expected.