ConstraintKinds explained on a super simple example

constraint-kinds, ghc, haskell, type-kinds

Solution

Well, I'll mention two practical things it allows you to do:

- Parametrize a type by a type class constraint

- Write type classes that allow their instances to specify constraints that they need.

Maybe it's best to illustrate this with an example. One of the classic Haskell warts is that you cannot make a `Functor` instance for types that impose a class constraint on their type parameter; for example, the `Set` class in the `containers` library, which requires an `Ord` constraint on its elements. The reason is that in "vanilla" Haskell, you'd have to have the constraint on the class itself:

class OrdFunctor f where
    fmap :: Ord b => (a -> b) -> f a -> f b

...but then this class only works for types that require specifically an `Ord` constraint. Not a general solution!

So what if we could take that class definition and abstract away the `Ord` constraint, allowing individual instances to say what constraint they require? Well, `ConstraintKinds` plus `TypeFamilies` allow that:

{-# LANGUAGE ConstraintKinds, TypeFamilies, FlexibleInstances #-}

import Prelude hiding (Functor(..))
import GHC.Exts (Constraint)
import Data.Set (Set)
import qualified Data.Set as Set

-- | A 'Functor' over types that satisfy some constraint.
class Functor f where
   -- | The constraint on the allowed element types.  Each
   -- instance gets to choose for itself what this is.
   type Allowed f :: * -> Constraint

   fmap :: Allowed f b => (a -> b) -> f a -> f b

instance Functor Set where
    -- | 'Set' gets to pick 'Ord' as the constraint.
    type Allowed Set = Ord
    fmap = Set.map

instance Functor [] where
    -- | And `[]` can pick a different constraint than `Set` does.
    type Allowed [] = NoConstraint
    fmap = map

-- | A dummy class that means "no constraint."
class NoConstraint a where

-- | All types are trivially instances of 'NoConstraint'.
instance NoConstraint a where

(Note that this isn't the only obstacle to making a `Functor` instance to `Set`; see this discussion. Also, credit to this answer for the `NoConstraint` trick.)

This sort of solution hasn't been generally adopted just yet, though, because `ConstraintKinds` are still more or less a new feature.

Another use of `ConstraintKinds` is to parametrize a type by a class constraint or class. I'll reproduce this Haskell "Shape Example" code that I wrote:

{-# LANGUAGE GADTs, ConstraintKinds, KindSignatures, DeriveDataTypeable #-}
{-# LANGUAGE TypeOperators, ScopedTypeVariables, FlexibleInstances #-}

module Shape where

import Control.Applicative ((<$>), (<|>))
import Data.Maybe (mapMaybe)
import Data.Typeable
import GHC.Exts (Constraint)

-- | Generic, reflective, heterogeneous container for instances
-- of a type class.
data Object (constraint :: * -> Constraint) where
    Obj :: (Typeable a, constraint a) => a -> Object constraint
           deriving Typeable

-- | Downcast an 'Object' to any type that satisfies the relevant
-- constraints.
downcast :: forall a constraint. (Typeable a, constraint a) =>
            Object constraint -> Maybe a
downcast (Obj (value :: b)) = 
  case eqT :: Maybe (a :~: b) of
    Just Refl -> Just value
    Nothing -> Nothing

Here the parameter of the `Object` type is a type class (kind `* -> Constraint`), so you can have types like `Object Shape` where `Shape` is a class:

class Shape shape where
  getArea :: shape -> Double

-- Note how the 'Object' type is parametrized by 'Shape', a class 
-- constraint.  That's the sort of thing ConstraintKinds enables.
instance Shape (Object Shape) where
    getArea (Obj o) = getArea o

What the `Object` type does is a combination of two features:

- An existential type (enabled here by `GADTs`), which allows us to store values of heterogeneous types inside the same `Object` type.

- `ConstraintKinds`, which allows us to, instead of hardcoding `Object` to some specific set of class constraints, have the users of the `Object` type specify the constraint they want as a parameter to the `Object` type.

And now with that we can not only make a heterogeneous list of `Shape` instances:

data Circle = Circle { radius :: Double }
            deriving Typeable

instance Shape Circle where
  getArea (Circle radius) = pi * radius^2


data Rectangle = Rectangle { height :: Double, width :: Double }
               deriving Typeable

instance Shape Rectangle where
  getArea (Rectangle height width) = height * width

exampleData :: [Object Shape]
exampleData = [Obj (Circle 1.5), Obj (Rectangle 2 3)]

...but thanks to the `Typeable` constraint in `Object` we can downcast: if we correctly guess the type contained inside an `Object`, we can recover that original type:

-- | For each 'Shape' in the list, try to cast it to a Circle.  If we
-- succeed, then pass the result to a monomorphic function that 
-- demands a 'Circle'.  Evaluates to:
--
-- >>> example
-- ["A Circle of radius 1.5","A Shape with area 6.0"]
example :: [String]
example = mapMaybe step exampleData
  where step shape = describeCircle <$> (downcast shape)
                 <|> Just (describeShape shape)

describeCircle :: Circle -> String
describeCircle (Circle radius) = "A Circle of radius " ++ show radius

describeShape :: Shape a => a -> String
describeShape shape = "A Shape with area " ++ show (getArea shape)

Problem

Original source

Related problems

• Can I parameterise the empty constraint type?