News aggregator

I talked about the Constraint kind, a recent addition to Haskell. There is a write-up of my talk on my personal blog.

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.

The example code in this article needs support for the Constraint kind, of course. So we have to enable the appropriate language extension (which is surprisingly called ConstraintKinds instead of ConstraintKind). Furthermore, we want to make use of type families. All in all, this leads to the following LANGUAGE pragma:

We will define our own version of the Monad class. Therefore, we have to hide the Monad class from the Prelude:

We will need the module Data.Set from the containers package for some example code:

Last, but not least, we have to import the kind Constraint:

Originally, classes and contexts were not first-class citizens in Haskell. The introduction of the Constraint kind has changed this. Classes and contexts can now be used as parameters of types, for example. This is because they are now types themselves.

However, classes and contexts are still not types in the strict sense. There are still no values of type Eq or Eq Integer, for example. As I have explained in my previous post, Haskell’s notion of type is more general than the usual one. In particular, functions on types are types themselves. However, they are not types of kind *. The same holds for classes and contexts. They are not types of kind *, but they are types of some other kinds, so that they can generally be used in places where types can be used.

The new kind Constraint, which is exported by GHC.Exts, is the kind of all contexts. Classes and contexts are now handled as follows:

• Each class with parameters of kinds k_1 through k_n is a type of kind k_1 -> k_n -> Constraint.

• Each tuple type (t_1, ..., t_n) where t_1 through t_n are of kind Constraint is also of kind Constraint and denotes the conjunction of t_1 through t_n. As a corner case, the nullary tuple type () is also of type Constraint and denotes the constraint that is always true.

• A context can be any type of kind Constraint.

These rules guarantee that classes and contexts can be used as before. For example, (Read val, Show val) is still a context, because Read and Show are types of kind * -> Constraint, so Read val and Show val are types of kind Constraint, and therefore (Read val, Show val) is a type of kind Constraint.

However, classes and constraints can be used in new ways now. Here are some examples:

• Classes can be partially applied, and the results can be used like classes again.

• Classes, partially applied classes, and contexts can be parameters of types and instances of classes.

• Aliases of classes, partially applied classes, and contexts can be defined using type declarations.

• Families of classes, partially applied classes, and contexts can be defined using type synonym families.

In the remainder of this article, I will illustrate the last two of these points.

Sometimes, the same conjunction of several contexts appears in multiple types. In such cases, it can become cumbersome to always write these conjunctions explicitly. For example, there might be several functions in a library that deal with values that can be turned into strings and generated from strings. In this case, the types of these functions will typically have a context that contains constraints Show val and Read val. With the Constraint kind, we can define context aliases Text val as follows:

Instead of Show val, Read val, we can now simply write Text val in contexts.

A few years ago, there was an attempt to implement support for context aliases (often called class aliases) in GHC. With the Constraint kind, this is now obsolete, as context aliases are now just a special kind of type aliases.

We will illustrate the use of context families by defining a generalized version of the Monad class.

The actual definition of a monad from category theory says that a monad on a category