Tag Archives: type-level programming

Dependently typed programming and theorem proving in Haskell

Programming languages with dependent types allow us to specify powerful properties of values using the type system. By employing the Curry–Howard correspondence, we can also use these languages as proof languages for higher-order logics. In this blog post, I want to demonstrate that Haskell as supported by the Glasgow Haskell Compiler (GHC) can give us almost the same features. Continue reading


Natural numbers in Haskell

It is a bit surprising that Haskell has no type for natural numbers. The Haskell Report defines only Integer for, well, integers and Int for integers that are reasonably small. The base package then adds Word as the unsigned variant of Int as well as types for signed and unsigned integers with a fixed number of bits. An unsigned variant of Integer is missing. Continue reading