Until today I wasn’t aware it is possible to do dependently-typed programming in Haskell. It turns out it is possible! This is amazing news for writing code with even less bugs. I would argue that dependent typing takes software verification in software engineering to the next level. The key feature that enables it in Haskell is singleton, a type that has only one inhabitant, i.e., exactly one value. Justin Le has a nice blog post about this topic and I highly recommend it! It is part 1 of a series so I’m looking forward to the rest of the series.
As it turns out, writing dependently-typed programs in Haskell is a bit clumsy and requires boilerplate code, but the singletons library addresses these problems to some extent. Dependent typing is not as nice as in Idris because Idris has full support for dependent types. Furthermore, in Idris type- and level-programming share the same syntax. Nevertheless, I’m looking forward to using the singletons library for Haskell! Justin also says this in the post: “Real dependent types are coming to Haskell soon!” I’m not sure what exactly that entails and when it will happen, but this is a thrill for Haskell programmers!