3 ms·

The book is fantastic. If you think this model is interesting, please consider trying Idris and reading the Idris book: https://www.manning.com/books/type-driv

• etatoby 8y ago
  I learned a bit of Idris on the book you link, but I gave up after trying to implement Quicksort (the classical Haskell one-liner) in Idris vectors. You need to manually write a page of theorems for Idris to accept it. It's crazy.
  • KirinDave 8y ago
    So don't write quicksort in Idris. It's not going to work very well anyways. It's not at all well-suited, and isn't really even an especially important sorting algorithm in a world where linear time sorting and constant time indexed searches are a thing. But most of the work you'd be doing to write quicksort is writing the machinery for structurally recursive sorting, which a lot of tutorials write not because you have to, but because it's a very good exercise for learning how to write total functions that are recursive in a way DT systems can prove totality on. Most of these tools are in the contrib library (and the book mentions this). For example the preorder interface you need: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Decidable/Order.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/con...