Idris is Pretty Cool

I've been reading recently about a programming language called Idris. Its similar to Haskell, but with dependent types. It is intended to be a practical programming language rather then a theorem proving language or a proof of concept, and there are papers about applying it to systems programming. That is one of my interests in dependent types- increasing the safety of complex programs that involve things like communicating with hardware. I use C to do this professionally, and I find that it is difficult to get this kind of programming correct every time with all the complicating factors. There are often times that I could express more about the structure of data or the flow of the program with a better type system. Dependent types have a lot of potential, and I would love to see them make their way into the kind of work that I do.

I may have to post about dependent types in the future, as they are probably the biggest thing that I know about in the functional programming community right now. They represent a real change in the use of programming languages and how one thinks about programming, and I for one am in favor of this change.