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 →
Temporal logic and functional reactive programming are related via a Curry–Howard correspondence, as has recently be shown by Alan Jeffrey and by myself. Given this intriguing connection, it seems to be worthwhile to look for a common categorical semantics of temporal logic and FRP. This undertaking is a current research topic of mine. I will present some results on this at this year’s MFPS conference under the title Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. A preprint of the corresponding paper is now available online. Continue reading →