Some interesting features of Haskell’s type system

One of the most important ingredients of Haskell is its type system. Standard Haskell already provides a lot of useful mechanisms for having things checked at compile time, and the language extensions provided by the Glasgow Haskell Compiler (GHC) improve heavily on this.

In this article, I will present several of Haskell’s type system features. Some of them belong to the standard, others are only available as extensions. This is a write-up of a talk I gave on 31 January 2013 during the Theory Lunch of the Institute of Cybernetics. This talk provided the basics for another Theory Lunch talk, which was about the Constraint kind. Continue reading

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