A video of his talk is available over on his blog, and his presentation is remarkably clear, and would serve as a good preamble to the code I'm going to present below.

Andrej gave a related invited talk back at MSFP 2008 in Iceland, and afterwards over lunch I cornered him (with Dan Piponi) and explained how you could use parametricity to close over the side-effects of monads (or arrows, etc) but I think that trick was lost in the chaos of the weekend, so I've chosen to resurrect it here, and improve it to handle some of his more recent performance enhancements, and show that you don't need side-effects to speed up the search after all!

First, we'll need to import a few things:

 
{-# LANGUAGE RankNTypes #-}
 
import Data.Maybe (fromMaybe)
import Control.Applicative
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Control.Monad
import Control.Monad.Trans.Class
import Data.Functor.Identity
 

What are looking for is an implementation of Hilbert's epsilon.

This is a formal mechanism for eliminating existentials over some non-empty set X by defining a function

 
ε: (X -> Prop) -> X
 

such that if there exists an x in X such that p(X) holds then p(ε(p)) holds.

As noted by Andrej, we could reify this constructively as a function "epsilon :: (X -> Bool) -> X" for some X.

Now, for some sets, Hilbert's epsilon is really easy to define. If X is a finite set, you can just exhaustively enumerate all of the options returning a member of X such that the property holds if any of them do, otherwise since X is non-empty, just return one of the elements that you tested.

This would be a pretty boring article and I'd be back to eating Christmas dinner with my family if that was all there was to it. However, certain infinite spaces can also be searched.

Last year, Luke Palmer wrote a post on "Searchable Data Types" that might also serve as a good introduction. In that article he led off with the easiest infinite space to search, the lazy naturals, or the 'one point compactification of the naturals'. That is to say the natural numbers extended with infinity.

 
data LazyNat = Zero | Succ LazyNat
infinity :: LazyNat
infinity = Succ infinity
 

Now we can implement Palmer's epsilon (called lyingSearch in his article).

 
palmer :: (LazyNat -> Bool) -> LazyNat
palmer p
  | p Zero = Zero
  | otherwise = Succ $ palmer $ p . Succ
 

The trick to making this work is that we place a requirement that the predicate that you pass has to terminate in a bounded amount of time no matter what input you give it, and since we're working with the naturals extended with infinity, if no natural satisfies the predicate, we'll just keep returning a longer and longer chain of Succ's, effectively yielding infinity.

To check to see if the returned number satisfies the predicate you can always use p (palmer p). The predicate is required to terminate in finite time, even when given infinity, so this will yield a Bool and not bottom out unless the user supplied predicate takes an unbounded amount of time.

I posted a reply to Luke's article when it came up on reddit which included a Hinze-style generic implementation of his lyingSearch predicate, which you can see now is just Hilbert's epsilon for arbitrary recursive polynomial data types.

http://www.reddit.com/r/haskell/comments/e7nij/searchable_data_types/c15zs6l

Another space we can search is the Cantor space 2^N.

 
type Cantor = Integer -> Bool
 

With that we jump clear from countable infinity to uncountable infinity, but it can still be searched in finite time!

This is the space we'll be paying attention to for the rest of this article.

First we'll define how to "book a room in Hilbert's Hotel."

 
infixr 0 #
(#) :: Bool -> Cantor -> Cantor
(x # a) 0 = x
(x # a) i = a (i - 1)
 

Then this can be used to obtain the following implementation of Hilbert's epsilon for the Cantor space, attributed by Andrej to Ulrich Berger.

 
berger :: (Cantor -> Bool) -> Cantor
berger p =
  if ex $ \a -> p $ False # a
  then False # berger $ \a -> p $ False # a
  else True  # berger $ \a -> p $ True # a
  where ex q = q (berger q)
 

This version is particularly close in structure to the one for searching the LazyNats, but it is dreadfully slow!

It would be nice to be able to search the space faster and that is just what Martin Escardo's improved version does, through a more sophisticated divide and conquer technique.

 
escardo :: (Cantor -> Bool) -> Cantor
escardo p = go x l r where
  go x l r n =  case divMod n 2 of
    (0, 0) -> x
    (q, 1) -> l q
    (q, 0) -> r $ q-1
  x = ex $ \l -> ex $ \r -> p $ go True l r
  l = escardo $ \l -> ex $ \r -> p $ go x l r
  r = escardo $ \r -> p $ go x l r
  ex q = q (escardo q)
 

To proceed from here I'll need a State monad:

 
newtype S s a = S { runS :: s -> (a, s) }
 
instance Functor (S s) where
  fmap f (S m) = S $ \s -> case m s of
    (a, s') -> (f a, s')
 
instance Applicative (S s) where
  pure = return
  (< *>) = ap
 
instance Monad (S m) where
  return a = S $ \s -> (a, s)
  S m >>= k = S $ \s -> case m s of
    (a, s') -> runS (k a) s'
 

And now we've reached the point. From here, Andrej's pure code ends, and his side-effecting ocaml and custom programming language start. The first thing he does is compute the modulus of continuity by using a side-effect that writes to a reference cell which he very carefully ensures doesn't leak out of scope, so he doesn't have to concern himself with the proposition code editing the value of the reference.

 
let mu f a =
  let r = ref 0 in
  let b n = (r := max n ! r; a n) in
    ignore (f b);
    !r
 

To obtain the same effect we'll instead make a predicate using the state monad to model the single reference cell.

 
-- bad
modulus :: (Num b, Ord s) =>
  ((s -> S s a) -> S b c) -> (s -> a) -> b
 

We can mash b and s together, and try to make the ordering and number agree by claiming that it is instead Real and we'd get the slightly more reasonable looking type:

 
-- still bad
modulus :: Real a =>
  ((a -> S n b) -> S n c) -> (a -> b) -> a
 

In the imperative code, lexical scoping had ensured that no other code could edit the reference cell, but with this type we don't have that. The predicate is allowed to use arbitrary state actions to muck with the modulus of convergence even though the only thing that should be editing it is the wrapper beta that we placed around alpha.

But how can we ensure that the end user couldn't gain access to any of the additional functionality from the monad? Parametricity!

 
-- getting better
modulus :: Real a =>
  (forall f. Monad f => (a -> f b) -> f c) ->
  (a -> b) ->
  a
 

Here the only thing you are allowed to assume about f is that it forms a monad. This gives you access to return and >>=, but the predicate can't do anything interesting with them. All it can do is work with what is effectively the identity monad, since it knows no additional properties!

We can have mercy on the end user and give them a little bit more syntactic sugar, since it doesn't cost us anything to let them also have access to the Applicative instance.

 
-- good
modulus :: Real a =>
  (forall f. (Monad f, Applicative f) => (a -> f b) -> f c) ->
  (a -> b) ->
  a
 

With that we can show Andrej's version of the modulus of convergence calculation does not need side-effects!

>
> modulus (\a -> a 10 >>= a) (\n -> n * n)
100
 

Admittedly plumbing around the monadic values in our proposition is a bit inconvenient.

His next example was written in a custom ocaml-like programming language. For translating his effect type into Haskell using parametricity, we'll need a CPS'd state monad, so we can retry from the current continuation while we track a map of assigned values.

 
newtype K r s a = K { runK :: (a -> s -> r) -> s -> r }
 
instance Functor (K r s) where
  fmap = liftM
 
instance Applicative (K r s) where
  pure = return
  (< *>) = ap
 
instance Monad (K r s) where
  return a = K $ \k -> k a
  K m >>= f = K $ \k -> m $ \a -> runK (f a) k
 

For those of you who have been paying attention to my previous posts, K r s is just a Codensity monad!

 
neighborhood ::
  (forall f. (Applicative f, Monad f) => (Int -> f Bool) -> f Bool) ->
  IntMap Bool
neighborhood phi = snd $ runK (phi beta) (,) IntMap.empty where
  beta n = K $ \k s -> case IntMap.lookup n s of
    Just b -> k b s
    Nothing -> case k True (IntMap.insert n True s) of
      (False, _) -> k False (IntMap.insert n False s)
      r -> r
 

With that we can adapt the final version of Hilbert's epsilon for the Cantor space that Andrej provided to run in pure Haskell.

 
bauer ::
  (forall f. (Applicative f, Monad f) => (Int -> f Bool) -> f Bool) ->
  Cantor
bauer p = \n -> fromMaybe True $ IntMap.lookup n m where
  m = neighborhood p
 

With a little work you can implement a version of an exists and forAll predicate on top of that by running them through the identity monad.

 
exists ::
  (forall f. (Applicative f, Monad f) => (Int -> f Bool) -> f Bool) ->
  Bool
forAll ::
  (forall f. (Applicative f, Monad f) => (Int -> f Bool) -> f Bool) ->
  Bool
 

I've gone further in playing with this idea, using monad homomorphisms rather than simply relying on the canonical homomorphism from the identity monad. You can get the gist of it here:

https://gist.github.com/1518767

This permits the predicates themselves to embed some limited monadic side-effects, but then you get more extensional vs. intensional issues.

An obvious direction from here is to fiddle with a version of Martin Escardo's search monad that takes advantage of these techniques, but I'll leave the exploration of these ideas to the reader for now and go enjoy Christmas dinner.

Happy Holidays,
Edward Kmett

Reflecting Classes and Instances

Most of the implications we use on a day to day basis come from our class and instance declarations, but last time we only really dealt with constraint products.

For example given:

 
#if 0
class Eq a => Ord a
instance Eq a => Eq [a]
#endif
 

we could provide the following witnesses

 
ordEq :: Ord a :- Eq a
ordEq = Sub Dict
 
eqList :: Eq a :- Eq [a]
eqList = Sub Dict
 

But this would require a lot of names and become remarkably tedious.

So lets define classes to reflect the entailment provided by class definitions and instance declarations and then use them to reflect themselves.

 
class Class b h | h -> b where
  cls :: h :- b
 
infixr 9 :=>
class b :=> h | h -> b where
  ins :: b :- h
 
instance Class () (Class b a) where cls = Sub Dict
instance Class () (b :=> a) where cls = Sub Dict
 

Now we can reflect classes and instances as instances of Class and (:=>) respectively with:

 
-- class Eq a => Ord a where ...
instance Class (Eq a) (Ord a) where cls = Sub Dict
-- instance Eq a => Eq [a] where ...
instance Eq a :=> Eq [a] where ins = Sub Dict
 

That said, instances of Class and Instance should never require a context themselves, because the modules that the class and instance declarations live in can't taken one, so we can define the following instances which bootstrap the instances of (:=>) for Class and (:=>) once and for all.

 
#ifdef UNDECIDABLE
instance Class b a => () :=> Class b a where ins = Sub Dict
instance (b :=> a) => () :=> b :=> a where ins = Sub Dict
#endif
 

These two instances are both decidable, and following a recent bug fix, the current version of GHC HEAD supports them, but my local version isn't that recent, hence the #ifdef.

We can also give admissable-if-not-ever-stated instances of Class and (:=>) for () as well.

 
instance Class () () where cls = Sub Dict
instance () :=> () where ins = Sub Dict
 

Reflecting the Prelude

So now that we've written a handful of instances, lets take the plunge and just reflect the entire Prelude, and (most of) the instances for the other modules we've loaded.

 
instance Class () (Eq a) where cls = Sub Dict
instance () :=> Eq () where ins = Sub Dict
instance () :=> Eq Int where ins = Sub Dict
instance () :=> Eq Bool where ins = Sub Dict
instance () :=> Eq Integer where ins = Sub Dict
instance () :=> Eq Float where ins = Sub Dict
instance () :=> Eq Double where ins = Sub Dict
instance Eq a :=> Eq [a] where ins = Sub Dict
instance Eq a :=> Eq (Maybe a) where ins = Sub Dict
instance Eq a :=> Eq (Complex a) where ins = Sub Dict
instance Eq a :=> Eq (Ratio a) where ins = Sub Dict
instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict
instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict
instance () :=> Eq (Dict a) where ins = Sub Dict
instance () :=> Eq (a :- b) where ins = Sub Dict
 

 
instance Class (Eq a) (Ord a) where cls = Sub Dict
instance () :=> Ord () where ins = Sub Dict
instance () :=> Ord Bool where ins = Sub Dict
instance () :=> Ord Int where ins = Sub Dict
instance ():=> Ord Integer where ins = Sub Dict
instance () :=> Ord Float where ins = Sub Dict
instance ():=> Ord Double where ins = Sub Dict
instance () :=> Ord Char where ins = Sub Dict
instance Ord a :=> Ord (Maybe a) where ins = Sub Dict
instance Ord a :=> Ord [a] where ins = Sub Dict
instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict
instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict
instance Integral a :=> Ord (Ratio a) where ins = Sub Dict
instance () :=> Ord (Dict a) where ins = Sub Dict
instance () :=> Ord (a :- b) where ins = Sub Dict
 

 
instance Class () (Show a) where cls = Sub Dict
instance () :=> Show () where ins = Sub Dict
instance () :=> Show Bool where ins = Sub Dict
instance () :=> Show Ordering where ins = Sub Dict
instance () :=> Show Char where ins = Sub Dict
instance Show a :=> Show (Complex a) where ins = Sub Dict
instance Show a :=> Show [a] where ins = Sub Dict
instance Show a :=> Show (Maybe a) where ins = Sub Dict
instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict
instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict
instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict
instance () :=> Show (Dict a) where ins = Sub Dict
instance () :=> Show (a :- b) where ins = Sub Dict
 

 
instance Class () (Read a) where cls = Sub Dict
instance () :=> Read () where ins = Sub Dict
instance () :=> Read Bool where ins = Sub Dict
instance () :=> Read Ordering where ins = Sub Dict
instance () :=> Read Char where ins = Sub Dict
instance Read a :=> Read (Complex a) where ins = Sub Dict
instance Read a :=> Read [a] where ins = Sub Dict
instance Read a :=> Read (Maybe a) where ins = Sub Dict
instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict
instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict
instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict
 

 
instance Class () (Enum a) where cls = Sub Dict
instance () :=> Enum () where ins = Sub Dict
instance () :=> Enum Bool where ins = Sub Dict
instance () :=> Enum Ordering where ins = Sub Dict
instance () :=> Enum Char where ins = Sub Dict
instance () :=> Enum Int where ins = Sub Dict
instance () :=> Enum Integer where ins = Sub Dict
instance () :=> Enum Float where ins = Sub Dict
instance () :=> Enum Double where ins = Sub Dict
instance Integral a :=> Enum (Ratio a) where ins = Sub Dict
 

 
instance Class () (Bounded a) where cls = Sub Dict
instance () :=> Bounded () where ins = Sub Dict
instance () :=> Bounded Ordering where ins = Sub Dict
instance () :=> Bounded Bool where ins = Sub Dict
instance () :=> Bounded Int where ins = Sub Dict
instance () :=> Bounded Char where ins = Sub Dict
instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict
 

 
instance Class () (Num a) where cls = Sub Dict
instance () :=> Num Int where ins = Sub Dict
instance () :=> Num Integer where ins = Sub Dict
instance () :=> Num Float where ins = Sub Dict
instance () :=> Num Double where ins = Sub Dict
instance RealFloat a :=> Num (Complex a) where ins = Sub Dict
instance Integral a :=> Num (Ratio a) where ins = Sub Dict
 

 
instance Class (Num a, Ord a) (Real a) where cls = Sub Dict
instance () :=> Real Int where ins = Sub Dict
instance () :=> Real Integer where ins = Sub Dict
instance () :=> Real Float where ins = Sub Dict
instance () :=> Real Double where ins = Sub Dict
instance Integral a :=> Real (Ratio a) where ins = Sub Dict
 

 
instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict
instance () :=> Integral Int where ins = Sub Dict
instance () :=> Integral Integer where ins = Sub Dict
 

 
instance Class (Num a) (Fractional a) where cls = Sub Dict
instance () :=> Fractional Float where ins = Sub Dict
instance () :=> Fractional Double where ins = Sub Dict
instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict
instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict
 

 
instance Class (Fractional a) (Floating a) where cls = Sub Dict
instance () :=> Floating Float where ins = Sub Dict
instance () :=> Floating Double where ins = Sub Dict
instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict
 

 
instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict
instance () :=> RealFrac Float where ins = Sub Dict
instance () :=> RealFrac Double where ins = Sub Dict
instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict
 

 
instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict
instance () :=> RealFloat Float where ins = Sub Dict
instance () :=> RealFloat Double where ins = Sub Dict
 

 
instance Class () (Monoid a) where cls = Sub Dict
instance () :=> Monoid () where ins = Sub Dict
instance () :=> Monoid Ordering where ins = Sub Dict
instance () :=> Monoid [a] where ins = Sub Dict
instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict
instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict
 

 
instance Class () (Functor f) where cls = Sub Dict
instance () :=> Functor [] where ins = Sub Dict
instance () :=> Functor Maybe where ins = Sub Dict
instance () :=> Functor (Either a) where ins = Sub Dict
instance () :=> Functor ((->) a) where ins = Sub Dict
instance () :=> Functor ((,) a) where ins = Sub Dict
instance () :=> Functor IO where ins = Sub Dict
 

 
instance Class (Functor f) (Applicative f) where cls = Sub Dict
instance () :=> Applicative [] where ins = Sub Dict
instance () :=> Applicative Maybe where ins = Sub Dict
instance () :=> Applicative (Either a) where ins = Sub Dict
instance () :=> Applicative ((->)a) where ins = Sub Dict
instance () :=> Applicative IO where ins = Sub Dict
instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict
 

 
instance Class (Applicative f) (Alternative f) where cls = Sub Dict
instance () :=> Alternative [] where ins = Sub Dict
instance () :=> Alternative Maybe where ins = Sub Dict
 

 
instance Class () (Monad f) where cls = Sub Dict
instance () :=> Monad [] where ins = Sub Dict
instance () :=> Monad ((->) a) where ins = Sub Dict
instance () :=> Monad (Either a) where ins = Sub Dict
instance () :=> Monad IO where ins = Sub Dict
 

 
instance Class (Monad f) (MonadPlus f) where cls = Sub Dict
instance () :=> MonadPlus [] where ins = Sub Dict
instance () :=> MonadPlus Maybe where ins = Sub Dict
 

Of course, the structure of these definitions is extremely formulaic, so when template-haskell builds against HEAD again, they should be able to be generated automatically using splicing and reify, which would reduce this from a wall of text to a handful of lines with better coverage!

An alternative using Default Signatures and Type Families

Many of the above definitions could have been streamlined by using default definitions. However, MPTCs do not currently support default signatures. We can however, define Class and (:=>) using type families rather than functional dependencies. This enables us to use defaulting, whenever the superclass or context was ().

 
#if 0
class Class h where
  type Sup h :: Constraint
  type Sup h = ()
  cls :: h :- Sup h
  default cls :: h :- ()
  cls = Sub Dict
 
class Instance h where
  type Ctx h :: Constraint
  type Ctx h = ()
  ins :: Ctx h :- h
  default ins :: h => Ctx h :- h
  ins = Sub Dict
 
instance Class (Class a)
instance Class (Instance a)
 
#ifdef UNDECIDABLE
instance Class a => Instance (Class a)
instance Instance a => Instance (Instance a)
#endif
 
instance Class ()
instance Instance ()
#endif
 

This seems at first to be a promising approach. Many instances are quite small:

 
#if 0
instance Class (Eq a)
instance Instance (Eq ())
instance Instance (Eq Int)
instance Instance (Eq Bool)
instance Instance (Eq Integer)
instance Instance (Eq Float)
instance Instance (Eq Double)
#endif
 

But those that aren't are considerably more verbose and are much harder to read off than the definitions using the MPTC based Class and (:=>).

 
#if 0
instance Instance (Eq [a]) where
  type Ctx (Eq [a]) = Eq a
  ins = Sub Dict
instance Instance (Eq (Maybe a)) where
  type Ctx (Eq (Maybe a)) = Eq a
  ins = Sub Dict
instance Instance (Eq (Complex a)) where
  type Ctx (Eq (Complex a)) = Eq a
  ins = Sub Dict
instance Instance (Eq (Ratio a)) where
  type Ctx (Eq (Ratio a)) = Eq a
  ins = Sub Dict
instance Instance (Eq (a, b)) where
  type Ctx (Eq (a,b)) = (Eq a, Eq b)
  ins = Sub Dict
instance Instance (Eq (Either a b)) where
  type Ctx (Eq (Either a b)) = (Eq a, Eq b)
  ins = Sub Dict
#endif
 

Having tested both approaches, the type family approach led to a ~10% larger file size, and was harder to read, so I remained with MPTCs even though it meant repeating "where ins = Sub Dict" over and over.

In a perfect world, we'd gain the ability to use default signatures with multiparameter type classes, and the result would be considerably shorter and easier to read!

Fake Superclasses

Now, that we have all this machinery, it'd be nice to get something useful out of it. Even if we could derive it by other means, it'd let us know we weren't completely wasting our time.

Let's define a rather horrid helper, which we'll only use where a and b are the same constraint being applied to a newtype wrapper of the same type, so we can rely on the fact that the dictionaries have the same representation.

 
evil :: a :- b
evil = unsafeCoerce refl
 

We often bemoan the fact that we can't use Applicative sugar given just a Monad, since Applicative wasn't made a superclass of Monad due to the inability of the Haskell 98 report to foresee the future invention of Applicative.

There are rather verbose options to get Applicative sugar for your Monad, or to pass it to something that expects an Applicative. For instance you can use WrappedMonad from Applicative. We reflect the relevant instance here.

 
instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict
 

Using that instance and the combinators defined previously, we can obtain the following

 
applicative :: forall m a. Monad m => (Applicative m => m a) -> m a
applicative m =
  m \\ trans (evil :: Applicative (WrappedMonad m) :- Applicative m) ins
 

Here ins is instantiated to the instance of (:=>) above, so we use trans to compose ins :: Monad m :- Applicative (WrappedMonad m) with evil :: Applicative (WrappedMonad m) :- Applicative m to obtain an entailment of type Monad m :- Applicative m in local scope, and then apply that transformation to discharge the Applicative obligation on m.

Now, we can use this to write definitions. [Note: Frustratingly, my blog software inserts spaces after <'s in code]

 
(< &>) :: Monad m => m a -> m b -> m (a, b)
m < &> n = applicative $ (,) < $> m < *> n
 

Which compares rather favorably to the more correct

 
(< &>) :: Monad m => m a -> m b -> m (a, b)
m < &> n = unwrapMonad $ (,) < $> WrapMonad m < *> WrapMonad n
 

especially considering you still have access to any other instances on m you might want to bring into scope without having to use deriving to lift them onto the newtype!

Similarly you can borrow < |> and empty locally for use by your MonadPlus with:

 
instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict
 
alternative :: forall m a. MonadPlus m => (Alternative m => m a) -> m a
alternative m =
  m \\ trans (evil :: Alternative (WrappedMonad m) :- Alternative m) ins
 

The correctness of this of course relies upon the convention that any Applicative and Alternative your Monad may have should agree with its Monad instance, so even if you use Alternative or Applicative in a context where the actual Applicative or Alternative instance for your particular type m is in scope, it shouldn't matter beyond a little bit of efficiency which instance the compiler picks to discharge the Applicative or Alternative obligation.

Note: It isn't that the Constraint kind is invalid, but rather that using unsafeCoerce judiciously we can bring into scope instances that don't exist for a given type by substituting those from a different type which have the right representation.

[Source]

Constraint Kinds adds a new kind Constraint, such that Eq :: * -> Constraint, Monad :: (* -> *) -> Constraint, but since it is a kind, we can make type families for constraints, and even parameterize constraints on constraints.

So, let's play with them and see what we can come up with!

A Few Extensions

First, we'll need a few language features:

 
{-# LANGUAGE
  CPP,
  ScopedTypeVariables,
  FlexibleInstances,
  FlexibleContexts,
  ConstraintKinds,
  KindSignatures,
  TypeOperators,
  FunctionalDependencies,
  Rank2Types,
  StandaloneDeriving,
  GADTs
  #-}
 

Because of the particular version of GHC I'm using I'll also need

 
{-# LANGUAGE UndecidableInstances #-}
#define UNDECIDABLE
 

but this bug has been fixed in the current version of GHC Head. I'll be explicit about any instances that need UndecidableInstances by surrounding them in an #ifdef UNDECIDABLE block.

Explicit Dictionaries

So with that out of the way, let's import some definitions

 
import Control.Monad
import Control.Monad.Instances
import Control.Applicative
import Data.Monoid
import Data.Complex
import Data.Ratio
import Unsafe.Coerce
 

and make one of our own that shows what we get out of making Constraints into a kind we can manipulate like any other.

 
data Dict a where
  Dict :: a => Dict a
 

Previously, we coud make a Dict like data type for any one particular class constraint that we wanted to capture, but now we can write this type once and for all. The act of pattern matching on the Dict constructor will bring the constraint 'a' into scope.

Of course, in the absence of incoherent and overlapping instances there is at most one dictionary of a given type, so we could make instances, like we can for any other data type, but standalone deriving is smart enough to figure these out for me. (Thanks copumpkin!)

 
deriving instance Eq (Dict a)
deriving instance Ord (Dict a)
deriving instance Show (Dict a)
 

If we're willing to turn on UndecidableInstances to enable the polymorphic constraint we can even add:

 
#ifdef UNDECIDABLE
deriving instance a => Read (Dict a)
instance a => Monoid (Dict a) where
  mappend Dict Dict = Dict
  mempty = Dict
#endif
 

and similar polymorphically constrained instances for Enum, Bounded, etc.

Entailment

For that we'll need a notion of entailment.

 
infixr 9 :-
newtype a :- b = Sub (a => Dict b)
 
instance Eq (a :- b) where
  _ == _ = True
 
instance Ord (a :- b) where
  compare _ _ = EQ
 
instance Show (a :- b) where
  showsPrec d _ = showParen (d > 10) $
    showString "Sub Dict"
 

Here we're saying that Sub takes one argument, which is a computation that when implicitly given a constraint of type a, can give me back a dictionary for the type b. Moreover, as a newtype it adds no overhead that isn't aleady present in manipulating terms of type (a => Dict b) directly.

The simplest thing we can define with this is that entailment is reflexive.

 
refl :: a :- a
refl = Sub Dict
 

Max has already written up a nice restricted monad example using these, but what I want to play with today is the category of substitutability of constraints, but there are a few observations I need to make, first.

ConstraintKinds overloads () and (a,b) to represent the trivial constraint and the product of two constraints respectively.

The latter is done with a bit of a hack, which we'll talk about in a minute, but we can use the former as a terminal object for our category of entailments.

 
weaken1 :: (a, b) :- a
weaken1 = Sub Dict
 
weaken2 :: (a, b) :- b
weaken2 = Sub Dict
 

Constraints are idempotent, so we can duplicate one, perhaps as a prelude to transforming one of them into something else.

 
contract :: a :- (a, a)
contract = Sub Dict
 

But to do much more complicated, we're going to need a notion of substitution, letting us use our entailment relation to satisfy obligations.

 
infixl 1 \\ -- required comment
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
 

The type says that given that a constraint a can be satisfied, a computation that needs a constraint of type b to be satisfied in order to obtain a result, and the fact that a entails b, we can compute the result.

The constraint a is satisfied by the type signature, and the fact that we get quietly passed whatever dictionary is needed. Pattern matching on Sub brings into scope a computation of type (a => Dict b), and we are able to discharge the a obligation, using the dictionary we were passed, Pattern matching on Dict forces that computation to happen and brings b into scope, allowing us to meet the obligation of the computation of r. All of this happens for us behind the scenes just by pattern matching.

So what can we do with this?

We can use \\ to compose constraints.

 
trans :: (b :- c) -> (a :- b) -> a :- c
trans f g = Sub $ Dict \\ f \\ g
 

In fact, the way the dictionaries get plumbed around inside the argument to Sub is rather nice, because we can give that same definition different type signatures, letting us make (,) more product-like, giving us the canonical product morphism to go with the weakenings/projections we defined above.

 
(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)
f &&& g = Sub $ Dict \\ f \\ g
 

And since we're using it as a product, we can make it act like a bifunctor also using the same definition.

 
(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)
f *** g = Sub $ Dict \\ f \\ g
 

Limited Sub-Superkinding?

Ideally we'd be able to capture something like that bifunctoriality using a type like

 
#if 0
class BifunctorS (p :: Constraint -> Constraint -> Constraint) where
  bimapS :: (a :- b) -> (c :- d) -> p a c :- p b d
#endif
 

In an even more ideal world, it would be enriched using something like

 
#ifdef POLYMORPHIC_KINDS
class Category (k :: x -> x -> *) where
  id :: k a a
  (.) :: k b c -> k a b -> k a c
instance Category (:-) where
  id = refl
  (.) = trans
#endif
 

where x is a kind variable, then we could obtain a more baroque and admittedly far less thought-out bifunctor class like:

 
#if 0
class Bifunctor (p :: x -> y -> z) where
  type Left p :: x -> x -> *
  type Left p = (->)
  type Right p :: y -> y -> *
  type Right p = (->)
  type Cod p :: z -> z -> *
  type Cod p = (->)
  bimap :: Left p a b -> Right p c d -> Cod p (p a c) (p b d)
#endif
 

Or even more more ideally, you could use the fact that we can directly define product categories!

Since they are talking about kind-indexing for classes and type families, we could have separate bifunctors for (,) for both kinds * and Constraint.

The current constraint kind code uses a hack to let (a,b) be used as a type inhabiting * and as the syntax for constraints. This hack is limited however. It only works when the type (,) is fully applied to its arguments. Otherwise you'd wind up with the fact that the type (,) needs to have both of these kinds:

 
-- (,) :: Constraint -> Constraint -> Constraint and
-- (,) :: * -> * -> *
 

What is currently done is that the kind magically switches for () and (,) in certain circumstances. GHC already had some support for this because it parses (Foo a, Bar b) as a type in (Foo a, Bar b) => Baz a b before transforming it into a bunch of constraints.

Since we already have a notion of sub-kinding at the kind level, we could solve this for () by making up a new kind, say, ??? which is the subkind of both * and Constraint, but this would break the nice join lattice properties of the current system.

[Edit: in the initial draft, I had said superkind]

 
--    ?
--   / \
-- (#)  ??
--     /  \
--    #    *  Constraint
--          \ /
--          ???
 

But this doesn't address the kind of (,) above. With the new polymorphic kinds that Brent Yorgey and company have been working on and a limited notion of sub-superkinding, this could be resolved by making a new super-kind @ that is the super-kind of both * and Constraint, and which is a sub-superkind of the usual unnamed Box superkind.

 
-- Box
--  |
--  @
 

Then we can have:

 
-- (,) :: forall (k :: @). k -> k -> k
-- () :: forall (k :: @). k
 

and kind checking/inference will do the right thing about keeping the kind ambiguous for types like (,) () :: forall (k :: @). k

This would get rid of the hack and let me make a proper bifunctor for (,) in the category of entailments.

The version of GHC head I'm working with right now doesn't support polymorphic kinds, so I've only been playing with these in a toy type checker, but I'm really looking forward to being able to have product categories!

Stay Tuned

Next, we'll go over how to reflect the class and instance declarations so we can derive entailment of a superclass for a class, and the entailment of instances.

[Source]

In particular, I want to talk about a novel encoding of linear functionals, polynomials and linear maps in Haskell, but first we're going to have to build up some common terminology.

Having obtained the blessing of Wolfgang Jeltsch, I replaced the algebra package on hackage with something... bigger, although still very much a work in progress.

(Infinite) Modules over Semirings

Recall that a vector space V over a field F is given by an additive Abelian group on V, and a scalar multiplication operator
(.*) :: F -> V -> V subject to distributivity laws

 
s .* (u + v) = s .* u + s .* v
(s + t) .* v = s .* v + t .* v
 

and associativity laws

 
   (s * t) .* v = s .* (t .* v)
 

and respect of the unit of the field.

 
   1 .* v = v
 

Since multiplication on a field is commutative, we can also add

 
  (*.) :: V -> F -> V
  v *. f = f .* v
 

with analogous rules.

But when F is only a Ring, we call the analogous structure a module, and in a ring, we can't rely on the commutativity of multiplication, so we may have to deal left-modules and right-modules, where only one of those products is available.

We can weaken the structure still further. If we lose the negation in our Ring we and go to a Rig (often called a Semiring), now our module is an additive moniod.

If we get rid of the additive and multiplicative unit on our Rig we get down to what some authors call a Ringoid, but which we'll call a Semiring here, because it makes the connection between semiring and semigroup clearer, and the -oid suffix is dangerously overloaded due to category theory.

First we'll define additive semigroups, because I'm going to need both additive and multiplicative monoids over the same types, and Data.Monoid has simultaneously too much and too little structure.

 
-- (a + b) + c = a + (b + c)
class Additive m where
  (+) :: m -> m -> m
  replicate1p :: Whole n => n -> m -> m -- (ignore this for now)
  -- ...
 

their Abelian cousins

 
-- a + b = b + a
class Additive m => Abelian m
 

and Multiplicative semigroups

 
-- (a * b) * c = a * (b * c)
class Multiplicative m where
  (*) :: m -> m -> m
  pow1p :: Whole n => m -> n -> m
  -- ...
 

Then we can define a semirings

 
-- a*(b + c) = a*b + a*c
-- (a + b)*c = a*c + b*c
class (Additive m, Abelian m, Multiplicative m) => Semiring
 

With that we can define modules over a semiring:

 
-- r .* (x + y) = r .* x + r .* y
-- (r + s) .* x = r .* x + s .* x
-- (r * s) .* x = r .* (s .* x)
class (Semiring r, Additive m) => LeftModule r m
   (.*) :: r -> m -> m
 

and analogously:

 
class (Semiring r, Additive m) => RightModule r m
   (*.) :: m -> r -> m
 

For instance every additive semigroup forms a semiring module over the positive natural numbers (1,2..) using replicate1p.

If we know that our addition forms a monoid, then we can form a module over the naturals as well

 
-- | zero + a = a = a + zero
class
    (LeftModule Natural m,
    RightModule Natural m
    ) => AdditiveMonoid m where
   zero :: m
   replicate :: Whole n => n -> m -> m
 

and if our addition forms a group, then we can form a module over the integers

 
-- | a + negate a = zero = negate a + a
class
    (LeftModule Integer m
    , RightModule Integer m
    ) => AdditiveGroup m where
  negate :: m -> m
  times :: Integral n => n -> m -> m
  -- ...
 

Free Modules over Semirings

A free module on a set E, is a module where the basis vectors are elements of E. Basically it is |E| copies of some (semi)ring.

In Haskell we can represent the free module of a ring directly by defining the action of the (semi)group pointwise.

 
instance Additive m => Additive (e -> m) where
   f + g = \x -> f x + g x
 
instance Abelian m => Abelian (e -> m)
 
instance AdditiveMonoid m => AdditiveMonoid (e -> m) where
   zero = const zero
 
instance AdditiveGroup m => AdditveGroup (e -> m) where
   f - g = \x -> f x - g x
 

We could define the following

 
instance Semiring r => LeftModule r (e -> m) where
   r .* f = \x -> r * f x
 

but then we'd have trouble dealing with the Natural and Integer constraints above, so instead we lift modules

 
instance LeftModule r m => LeftModule r (e -> m) where
   (.*) m f e = m .* f e
 
instance RightModule r m => RightModule r (e -> m) where
   (*.) f m e = f e *. m
 

We could go one step further and define multiplication pointwise, but while the direct product of |e| copies of a ring _does_ define a ring, and this ring is the one provided by the Conal Elliot's vector-space package, it isn't the most general ring we could construct. But we'll need to take a detour first.

Linear Functionals

A Linear functional f on a module M is a linear function from a M to its scalars R.

That is to say that, f : M -> R such that

 
f (a .* x + y) = a * f x + f y
 

Consequently linear functionals also form a module over R. We call this module the dual module M*.

Dan Piponi has blogged about these dual vectors (or covectors) in the context of trace diagrams.

If we limit our discussion to free modules, then M = E -> R, so a linear functional on M looks like (E -> R) -> R
subject to additional linearity constraints on the result arrow.

The main thing we're not allowed to do in our function is apply our function from E -> R to two different E's and then multiply the results together. Our pointwise definitions above satisfy those linearity constraints, but for example:

 
bad f = f 0 * f 0
 

does not.

We could capture this invariant in the type by saying that instead we want

 
newtype LinearM r e =
  LinearM {
    runLinearM :: forall r. LeftModule r m => (e -> m) -> m
  }
 

we'd have to make a new such type every time we subclassed Semiring. I'll leave further exploration of this more exotic type to another time. (Using some technically illegal module instances we can recover more structure that you'd expect.)

Now we can package up the type of covectors/linear functionals:

 
infixr 0 $*
newtype Linear r a = Linear { ($*) :: (a -> r) -> r }
 

The sufficiently observant may have already noticed that this type is the same as the Cont monad (subject to the linearity restriction on the result arrow).

In fact the Functor, Monad, Applicative instances for Cont all carry over, and preserve linearity.

(We lose callCC, but that is at least partially due to the fact that callCC has a less than ideal type signature.)

In addition we get a number of additional instances for Alternative, MonadPlus, by exploiting the knowledge that r is ring-like:

 
instance AdditiveMonoid r => Alternative (Linear r a) where
  Linear f < |> Linear g = Linear (f + g)
  empty = Linear zero
 

Note that the (+) and zero there are the ones defined on functions from our earlier free module construction!

Linear Maps

Since Linear r is a monad, Kleisli (Linear r) forms an Arrow:

 
b -> ((a -> r) ~> r)
 

where the ~> denotes the arrow that is constrained to be linear.

If we swap the order of the arguments so that

 
(a -> r) ~> (b -> r)
 

this arrow has a very nice meaning! (See Numeric.Map.Linear)

 
infixr 0 $#
newtype Map r b a = Map { ($#) :: (a -> r) -> (b -> r) }
 

Map r b a represents the type of linear maps from a -> b. Unfortunately due to contravariance the arguments wind up in the "wrong" order.

 
instance Category (Map r) where
  Map f . Map g = Map (g . f)
  id = Map id
 

So we can see that a linear map from a module A with basis a to a vector space with basis b effectively consists of |b| linear functionals on A.

Map r b a provides a lot of structure. It is a valid instance of an insanely large number of classes.

Vectors and Covectors

In physics, we sometimes call linear functionals covectors or covariant vectors, and if we're feeling particularly loquacious, we'll refer to vectors as contravariant vectors.

This has to do with the fact that when you change basis, you change map the change over covariant vectors covariantly, and map the change over vectors contravariantly. (This distinction is beautifully captured by Einstein's summation notation.)

We also have a notion of covariance and contravariance in computer science!

Functions vary covariantly in their result, and contravariant in their argument. E -> R is contravariant in E. But we chose this representation for our free modules, so the vectors in our free vector space (or module) are contravariant in E.

 
class Contravariant f where
  contramap :: (a -> b) -> f a -> f b
 
-- | Dual function arrows.
newtype Op a b = Op { getOp :: b -> a } 
 
instance Contravariant (Op a) where
  contramap f g = Op (getOp g . f)
 

On the other hand (E -> R) ~> R varies covariantly with the change of E.

as witnessed by the fact that it is a Functor.

 
instance Functor (Linear r) where
  fmap f m = Linear $ \k -> m $* k . f
 

We have lots of classes for manipulating covariant structures, and most of them apply to both (Linear r) and (Map r b).

Other Representations and Design Trade-offs

One common representation of vectors in a free vector space is as some kind of normalized list of scalars and basis vectors. In particular, David Amos's wonderful HaskellForMaths uses

 
newtype Vect r a = Vect { runVect :: [(r,a)] }
 

for free vector spaces, only considering them up to linearity, paying for normalization as it goes.

Given the insight above we can see that Vect isn't a representation of vectors in the free vector space, but instead represents the covectors of that space, quite simply because Vect r a varies covariantly with change of basis!

Now the price of using the Monad on Vect r is that the monad denormalizes the representation. In particular, you can have multiple copies of the same basis vector., so any function that uses Vect r a has to merge them together.

On the other hand with the directly encoded linear functionals we've described here, we've placed no obligations on the consumer of a linear functional. They can feed the directly encoded linear functional any vector they want!

In fact, it'll even be quite a bit more efficient to compute,

To see this, just consider:

 
instance MultiplicativeMonoid r => Monad (Vect r) where
   return a = Vect [(1,a)]
   Vect as >>= f = Vect
       [ (p*q, b) | (p,a) < - as, (q,b) <- runVect (f b) ]
 

Every >>= must pay for multiplication. Every return will multiply the element by one. On the other hand, the price of return and bind in Linear r is function application.

 
instance Monad (Linear r) where
  return a = Linear $ \k -> k a
  m >>= f = Linear $ \k -> m $* \a -> f a $* k
 

A Digression on Free Linear Functionals

To wax categorical for a moment, we can construct a forgetful functor U : Vect_F -> Set that takes a vector space over F to just its set of covectors.

 
F E = (E -> F, F,\f g x -> f x + g x ,\r f x -> r * f x)
 

using the pointwise constructions we built earlier.

Then in a classical setting, you can show that F is left adjoint to U.

In particular the witnesses of this adjunction provide the linear map from (E -> F) to V and the function E -> (V ~> F) giving a linear functional on V for each element of E.

In a classical setting you can go a lot farther, and show that all vector spaces (but not all modules) are free.

But in a constructive setting, such as Haskell, we need a fair bit to go back and forth, in particular we wind up need E to be finitely enumerable to go one way, and for it to have decidable equality to go in the other. The latter is fairly easy to see, because even going from E -> (E -> F) requires that we can define and partially apply something like Kronecker's delta:

 
delta :: (Rig r, Eq a) => e -> e -> r
delta i j | i == j = one
             | otherwise = zero
 

The Price of Power

The price we pay is that, given a Rig, we can go from Vect r a to Linear r a but going back requires a to be be finitely enumerable (or for our functional to satisfy other exotic side-conditions).

 
vectMap :: Rig r => Vect r a -> Linear r a
vectMap (Vect as) = Map $ \k -> sum [ r * k a | (r, a) < - as ]
 

You can still probe Linear r a for individual coefficients, or pass it a vector for polynomial evaluation very easily, but for instance determining a degree of a polynomial efficiently requires attaching more structure to your semiring, because the only value you can get out of Linear r a is an r.

Optimizing Linear Functionals

In both the Vect r and Linear r cases, excessive use of (>>=) without somehow normalizing or tabulating your data will cause a lot of repeated work.

This is perhaps easiest to see from the fact that Vect r never used the addition of r, so it distributed everything into a kind of disjunctive normal form. Linear r does the same thing.

If you look at the Kleisli arrows of Vect r or Linear r as linear mappings, then you can see that Kleisli composition is going to explode the number of terms.

So how can we collapse back down?

In the Kleisli (Vect r) case we usually build up a map as we walk through the list then spit the list back out in order having added up like terms.

In the Map r case, we can do better. My representable-tries package provides a readily instantiable HasTrie class, and the method:

 
memo :: HasTrie a => (a -> r) -> a -> r
 

which is responsible for providing a memoized version of the function from a -> r in a purely functional way. This is obviously a linear map!

 
memoMap :: HasTrie a => Map r a a
memoMap = Map memo
 

We can also flip memo around and memoize linear functionals.

 
memoLinear :: HasTrie a => a -> Linear r a
memoLinear = Linear . flip memo
 

Next time, (co)associative (co)algebras and the myriad means of multiplying (co)vectors!

In particular I spent a lot of time focusing on how to derive the construction of Hinze and Paterson's 2-3 finger trees via an extended detour into a whole menagerie of tree types, and less on particular applications of the final resulting structure.

Overall, I think the talk went over quite well.

In other finger-tree-related news, Mark Chu-Carroll recently wrote a blog post on finger trees as well, which might serve as a faster introduction in case you don't want to wade through 50 slides before seeing something recognizable as a finger tree. The comments given in reply to his very timely article were very useful in fleshing out this presentation.

For those who are interested, while we have yet to establish a good way to record video, here are my slides.

• Finger Trees [PDF]

There are two parts of the talk that may be difficult to adequately reconstruct from the slides alone:

1. I talked through the notion of safe and dangerous digits in a Hinze and Paterson tree and explained how the extra slop in a Hinze and Paterson tree work.
2. The other part that was talked through largely via the blackboard was how one uses the monotonicity of the function passed to split.

Otherwise, you can probably reconstruct the narrative from the slides.

If you have any questions or spot any errors or grievous omissions, please feel free to contact me.

[Edit: Updated slide 54]

Now, you no longer need to use big scary undefineds throughout your code and can instead program with implicit configurations more naturally, using Applicative and Monad sugar.

 
*Data.Reflection> reify (+)
    (reflect < *> pure 1 < *> (reflect < *> pure 2 < *> pure 3))
> 6
 

The Monad in question just replaces the lambda with a phantom type parameter, enabling the compiler to more readily notice that no instance can actually even try to use the value of the type parameter.

An example from the old API can be seen on the Haskell cafe.

This example can be made appreciably less scary now!

 
{-# LANGUAGE
     MultiParamTypeClasses,
     FlexibleInstances, Rank2Types,
     FlexibleContexts, UndecidableInstances #-}
import Control.Applicative
import Data.Reflection
import Data.Monoid
import Data.Tagged
 
newtype M s a = M a
 
instance Reifies s (a,a → a → a) ⇒ Monoid (M s a) where
    mempty = tagMonoid $ fst < $> reflect
    a `mappend` b = tagMonoid $
        snd < $> reflect < *> monoidTag a < *> monoidTag b
 
monoidTag :: M s a → Tagged s a
monoidTag (M a) = Tagged a
 
tagMonoid :: Tagged s a → M s a
tagMonoid (Tagged a) = M a
 
withMonoid :: a → (a → a → a) →
    (∀s. Reifies s (a, a → a → a) ⇒ M s w) → w
withMonoid e op m = reify (e,op) (monoidTag m)
 

And with that we can cram a Monoid dictionary -- or any other -- with whatever methods we want and our safety is assured by parametricity due to the rank 2 type, just like with the ST monad.

 
*> withMonoid 0 (+) (M 5 `mappend` M 4 `mappend` mempty)
9
 

[Edit: factored Tagged out into Data.Tagged in a separate package, and modified reflection to use that instead, with an appropriate version bump to satisfy the package versioning policy]

O.K. it was more of a polite request, but I did update it.