1. 55

  2. 1

    As usual Idris is super cool, the implications of using quantitative type theory are very well explained and interesting.

    1. 1

      So has anyone used Idris 1 or 2 for anything? What did you think?

      1. 4

        There was this thread a while back, and @yannbane is on lobsters:https://lobste.rs/s/ogez9q/game_pure_language_part_1_introduction

        1. 3

          Only for learning type driven development, beyond that it seems a bit like it needs a lot more baking before that cake is fully ready for prime time.

          Was super fun though, the type system will let you encode things in ways that I found hard/impossible in things like Haskell/Rust/etc….