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

# Tag Archives: type-level programming

# 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