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
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
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!
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!
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!
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.
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.
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
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!
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 any event, if you are interested in logic at pretty much any level, feel free to stop by the channel.
]]>