Safe, polykinded universally quantified constraints (Part 1 of 3)

There are a few times in my Haskelling that I’ve wanted to use universal quantification to specify a constraint. Earlier this year, I went ahead and asked glasgow-haskell-users about it, and thus learned about the Data.Constraint.Forall module in Edward Kmett’s constraints package. He uses an interesting mechanism for extra robustness in there that took me a while to appreciate. Over the next few posts, I explain his mechanism and then demonstrate a path toward even more robustness that I’ve been discussing with him. It was initially inspired by SPJ’s idea for “Fixing Any and some discussions with my lab mate Neil Sculthorpe. My hopes for it were raised when Kmett noticed its resemblance to Hilbert’s ε operator.

My lab mate Neil also learned me some domain theory, which I’ll use to (hopefully correctly) discuss a subtlety of GHC’s type equality that derails one of our early attempts.

This draft post ended up quite long, so I split it in three. Find a break down and links at the bottom of this one.

Objective: Universally quantified constraints

Here’s the general form of quantification that I’m discussing in this post.

example :: (forall a. p a) => ... -- not valid in GHC 7.6.1

The constraint is a universally quantified constraint. In it, we have quantified over the predicate p, by saying for how many of its possible arguments it must be satisfiable: all of them.

The need for quantified constraints arises when you attempt to work with an existentially quantified type that is not constrained as much as you would like it to be. For example, somewhere within an expression, I open up a Box and want to act on its contents with some class method, say mappend.

data Box t = forall a. Box (t a)

-- ill-typed!
--   example (Box x) = Box (x `mappend` x)
-- No instance for (Monoid (t a)) arising from a use of `mappend'
-- Possible fix: add an instance declaration for (Monoid (t a))

This error is pointing out that we don’t know enough about the existential type variable (ie a) that is encapsulated by Box to gaurantee we get a monoid when you tuck that variable inside some t.

I know two ways to make this well-typed. One is to change the binding of the existential type variable. We would update the definition of Box.

data Box t = forall a. Monoid (t a) => Box (t a)

-- inferred: example :: Box t -> Box t
example (Box x) = Box (x `mappend` x)

But that’s a bit dissatisfying. Perhaps we use Box in other parts of our program in ways that are now ill-typed. Or maybe during development we learn that we need other properties of t a; we’ll have to glom them into the constraint inside Box too. Do note, though, that this is a simple fix, and might work well for you in the future. In particular, if your constraint actually depends directly on the existential type variable, it’s your only option. But future-you also might prefer to use a universally quantified constraint, if future-you can.

Here’s a little bit of prep work, pulling in Kmett’s constraints package and putting a thin wrapper on one of its combinators.

-- Kmett's constraints on Hackage
import Data.Constraint (Constraint, (:-), (\\))
import Data.Constraint.Forall (ForallF, instF)

-- thin wrapper around Data.Constraint.Forall (instF)
instF_ :: Predicate p -> Proxy (t a) -> ForallF p t :- p (t a)
instF_ _ _ = instF

data Predicate (a :: * -> Constraint) = Predicate

data Proxy (a :: *) = Proxy
proxy :: a -> Proxy a
proxy _ = Proxy

The instF function provides evidence (eg a type class dictionary) for the constraint p (t a), given evidence for the constraint ForallF p t. Notice how it is polymorphic in a; that’s the key. My wrapper just let’s me tidily specify some of the type arguments instF is expecting.

Here’s how to put instF to work in our example. Note that Box is back to its original definition.

data Box t = forall a. Box (t a) -- as originally

-- inferred, but tidied by hand:
--   example :: ForallF Monoid t => Box t -> Box t
example (Box x) = Box (x `mappend` x)
  \\ instF_ (Predicate :: Predicate Monoid) (proxy x)

Read the constraint ForallF Monoid t as forall a. Monoid (t a). The idea is that we don’t want the invocation of mappend to have anything to do with the existential type variable a. We want to instead require that the relevant Monoid instance for t is parametric in t’s argument: it works for all a.

Stepping back a bit, there might be some greater significance/usefulness to this quantifier. The general benefit is that we can now build constraints over higher-kinded parameters out of constraints over lower-kinded parameters. One place where this would be handy is in Oleg Kiselyov’s Haskell1 sublanguage. I had only the foggiest recollection of that article when writing this post, but Cale Gibbard, Jason Dagit, and Daniel Peebles helped me track it down in the #haskell IRC channel — thanks, guys! In that article Oleg makes a Monadish “class” that explicitly has the carrier as a class argument. Using a universal quantifier, we could recover the normal Monad constraint as a quantification of his.

-- a constraint synonym (via `XConstraintKinds`)
type Monad m = (forall a. C (RET m a), forall a b. C (BIND m a b))

OK. That’s the hook.

End of Part 1

Aww! Just before we get to the juicy parts: instF involves Unsafe.Coerce.unsafeCoerce! Kmett put some cleverness in Data.Constraint.Forall that guards rather well against the unsafeness; it is very practically safe.

In Part 2, I first explain the naïve direct approach to defining the Forall constraint synonym, and we see why it’s not as safe as Kmett’s mechanism. I also show how to subvert his mechanism, which motivates the most robust definition for Forall that I know of, given in Part 3. I then discuss some details of the GHC type system, focusing mostly on an elusive “a bottom type”. We end up discussing Hilbert’s ε operator a bit, thanks to Kmett’s eye for recognizing those important sort of things.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s