Generic programming is a powerful way to define a function that works in an analogous way for a class of types. In this article, I describe the latest approach to generic programming that is implemented in GHC. This approach goes back to the paper *A Generic Deriving Mechanism for Haskell* by José Pedro Magalhães, Atze Dijkstra, Johan Jeuring, and Andres Löh. Continue reading

# Tag Archives: literate programming

# Constrained monads

There are Haskell types that have an associated monad structure, but cannot be made instances of the `Monad`

class. The reason is typically that the *return* or the *bind* operation of such a type `m`

has a constraint on the type parameter of `m`

. As a result, all the nice library support for monads is unusable for such types. This problem is called the constrained-monad problem.

In my article *The Constraint kind*, I described a solution to this problem, which involved changing the

`Monad`

class. In this article, I present a solution that works with the standard `Monad`

class. This solution has been developed by Neil Sculthorpe, Jan Bracker, George Giorgidze, and Andy Gill. It is described in their paper *The Constrained-Monad Problem*and implemented in the

*constrained-normal*package. Continue reading

# MIU in Curry

More than two years ago, my colleague Denis Firsov and I gave a series of three Theory Lunch talks about the MIU string rewriting system from Douglas Hofstadter’s MU puzzle. The first talk was about a Haskell implementation of MIU, the second talk was an introduction to the functional logic programming language Curry, and the third talk was about a Curry implementation of MIU. The blog articles *MIU in Haskell* and *A taste of Curry* are write-ups of the first two talks. However, a write-up of the third talk has never seen the light of day so far. This is changed with this article. Continue reading

# A taste of Curry

Curry is a programming language that integrates functional and logic programming. Last week, Denis Firsov and I had a look at Curry, and Thursday, I gave an introductory talk about Curry in the Theory Lunch. This blog post is mostly a write-up of my talk. Continue reading

# MIU in Haskell

In the Theory Lunch of the last week, James Chapman talked about the MU puzzle from Douglas Hofstadter’s book *Gödel, Escher, Bach*. This puzzle is about a string rewriting system. James presented a Haskell program that computes derivations of strings. Inspired by this, I wrote my own implementation, with the goal of improving efficiency. This blog post presents this implementation. As usual, it is available as a literate Haskell file, which you can load into GHCi. Continue reading

# The Constraint kind

A recent language extension of the Glasgow Haskell Compiler (GHC) is the `Constraint`

kind. In this blog post, I will show some examples of how this new feature can be used. This is a write-up of my Theory Lunch talk from 7 February 2013. The source of this article is a literate Haskell file, which you can download and load into GHCi. Continue reading

# 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

# New release of the ucs LaTeX package

The *ucs* package provides advanced support for using UTF-8 as the input encoding of LaTeX files. It goes much beyond the standard UTF-8 support of LaTeX. In particular, it enables you to use non-ASCII characters in the LaTeX input of mathematical formulas. This feature is particularly important for Agda programmers that use lhs2TeX to typeset their code. The lhs2TeX preprocessor relies on *ucs* for typesetting all those mathematical symbols and greek letters that you typically find in Agda code.

The *ucs* package was originally developed by Dominique Unruh. Dominique had stopped working on *ucs* several years ago. In 2011, I took over the maintainer role. Now, I have made a new release – which is the first *ucs* release since 7.5 years. The current version is 2.0. At the time of writing, it is available on CTAN and in TeXLive. Continue reading