There are various reasons why Idris is slow, but it generally comes down to it being because the current system is the result of lots of experimentation about how to even implement a dependently typed language in the first place, and what it should look like. It needs quite a bit of re-engineering - I prioritised ease of playing with features over efficiency.
The good news is that I'm working on a new version, taking into account the many things I know now that I didn't when starting on version 1. Don't hold your breath though, it might take a while...
In the end, it's a research project, and our job isn't so much to make a good product as to get people excited about the ideas. Mostly we do this by trying to be obviously having lots of fun. But I'd still like a better implementation, because then we can have even more fun.
Tracking state (sort of like Typestate) is not part of the type system, but you can encode it in the type system. So far, I've found this much more usable in practice than linear types, but I expect future work on linear types will change this, especially now that they're coming to GHC.
The new States library is really a new implementation of Effects. It works in pretty much the same way, but emphasising the thing that the Effects library is best at and fixing some of its shortcomings.
There are two main differences at the moment:
- Everything has to be labelled
- There's no 'implicit' lifting of smaller sets of states
The first is annoying for things like Console IO, so I might change that. The second means that we have a much better chance of providing decent error messages, one day.
The good news is that I'm working on a new version, taking into account the many things I know now that I didn't when starting on version 1. Don't hold your breath though, it might take a while...
In the end, it's a research project, and our job isn't so much to make a good product as to get people excited about the ideas. Mostly we do this by trying to be obviously having lots of fun. But I'd still like a better implementation, because then we can have even more fun.