Recently I’ve been working on a project where scoping is key to safety; the majority of functions in the library either require or provide a subscoping proof.
type role (~<) nominal nominal
data p ~< q = UnsafeSubscopeProof
The direct subscope relation is provided as a skeleton of proof elements, but in general the full reflexive transitive closure is required.
instance Category (~<) where
id = UnsafeSubscopeProof
!_ . !_ = UnsafeSubscopeProof
Collecting and composing these elements is a burden that need not be born by human hands, however—let’s offload this work onto GHC.
Constraint Implication
We open with a trick I incidentally mentioned in another post recently.
QuantifiedConstraints allows us to express constraint implication by using (=>) at Constraint -> Constraint -> Constraint. This relation is reflexive and transitive, and GHC knows it. As such, if we make our typeclass synonymous with such an implication, it will inherit these properties!
class SubscopeEndo s
class (SubscopeEndo p => SubscopeEndo q) => p <| q where
auto :: p ~< q
instance (SubscopeEndo p => SubscopeEndo q) => p <| q where
auto = UnsafeSubscopeProof
All that’s needed is to reflect each proof element. Sadly, the superclass constraint prevents the use of withDict, so we have to settle for unsafeCoerce.
reflect :: forall p q r. p ~< q -> (p <| q => r) -> r
reflect !_ r = case magic of
Dict -> r
where
magic :: Dict (p <| q)
magic = unsafeCoerce (Dict @(p <| p))
In addition to the main library, there are a few sublibraries doing dual service as usage examples and tests of the interface. In writing them, I found the inference provided by this approach to be excellent—never needing annotations or type applications when proving truths. The only flaw in the UX was that the type errors were somewhat cryptic when mistakenly asked to prove falsehoods.
There are deep flaws in the implementation, however. On top of the unsafe reflection, the key instance can only be written by abusing access to internals (or unsafeCoerce) to provide an evil all-proof: forall p q. p ~< q. It would also fail completely were the method to actually contain any data that could be distinguished at runtime.
The Direct Approach
I came face to face with the flaws above when I was refactoring to separate conveniences from the minimal complete public interface—proof tokens fell on one side while inference fell on the other.
Now, I could have just made an exception and shifted the declaration of ~< into an internal module, but it didn’t feel right to do so—I should be able to express my conveniences in terms of the public interface.
And what was wrong with the direct approach anyway? Perhaps we can write this safely. Let’s see.
class p <| q where
auto :: p ~< q
instance p <| p where
auto = id
instance (p <| q, q <| r) => p <| r where
auto = auto @q @r . auto @p @q
Rather than direct, the above is really the naïve approach. Firstly, those instances overlap, but that can be resolved. More problematic is that the linking q in the second instance is entirely ambiguous, and we really have no way to help GHC choose.
We need more structure to work with. Let’s start by distinguishing the direct subscoping proofs we reflect from the indirect ones we infer.
class Direct p q where
direct :: p ~< q
reflect :: p ~< q -> (Direct p q => r) -> r
reflect = withDict
Morally, this should have a p <| q superclass, but that won’t do reflect any favours so let’s not.
Intuitively, we now have our recursive structure: every auto is either id, or a direct composed with a “smaller” auto. But the matter of ambiguity remains.
We need either p or r to determine q in that second instance. This isn’t possible with <|, but direct subscope is functional! A scope may have many direct subscopes, but only one direct superscope.
Advising GHC of this fact by amending the declaration of class Direct with the functional dependency p -> q, we can finally write an instance that makes sense.
instance (Direct p q, q <| r) => p <| r where
auto = auto . direct
I expect that—with OVERLAPPING and OVERLAPPABLE pragmata in place—this approach would actually work out. For someone else, that is. I, on the other hand, am possessed of an unslakeable lust for RankNTypes.
You see, all the scopes in question are skolems introduced by polymorphic continuations. This complicates the resolution of overlap, because while GHC knows that the instance head p <| q matches, it cannot rule out the possibility that p <| p does too. The way to pull it out of this sticky situation and allow it to select p <| q is to slap INCOHERENT on instance p <| p.
… Or so I’d thought, anyway, but the behaviour of this direct approach is a little wild. At this point in time I don’t care to return for further meditations on the mysteries of Section 6.8.8.5, but it probably explains why I still can’t banish these overlap errors.
More interestingly, when not complaining about overlap, GHC instead throws this rare gem at me:
• Reduction stack overflow; size = 201
When simplifying the following type: q0 <| q1
• In the expression: auto
Oh dear. More mysteries I don’t wish to contemplate. In any case, I won’t fight this battle—let’s just run away.
Return to the Origin
Let’s start over; reduce the issue to our precise cards and goals—eliminating all else—then seek the way between.
Cards
We have, (we assume) some binary class C for which we can coherently implement:
refl :: forall x . Dict (C x x)
trans :: forall x y z. Dict (C x y) -> Dict (C y z) -> Dict (C x z)
Coherence means the dictionaries are singletons, so it follows trivially that refl is the identity to trans and that trans itself is associative—C is a reflected Category not just in my case, but more generally. Let’s call it >->. Without loss of generality:
class C x y where
reify :: x >-> y
There’s one last piece of structure that was hiding before the previous section unearthed it: functionality. The possibility exists that the constraint implication approach was always depending upon this additional structure while I was blissfully unaware.
But that’s not the case—the truth is worse. Upon further investigation, I found that the way GHC solves quantified constraints is painfully limited! It can solve c => e from (c => d, c => d', d => e), but not from (c => d, c' => d, d => e). In short: the implications in scope must be reverse functional.
That means my original approach was secretly broken, and should actually have used
class (SubscopeEndo q => SubscopeEndo p) => p <| q
but my testing either wasn’t extensive enough to uncover issues or my interface just happened to prevent them.
In any case, we don’t have a better approach to transitivity than constraint implication, so we must accept this restriction. Doing so gives us our last card: again w.l.o.g, class C x y | x -> y.
Goals
We want a class Transitive c x y such that Transitive C is indeed transitive (and reflexive), can be granted any instance that C has:
grant :: C x y => Dict (Transitive C x y)
and any generated instance can be retrieved in reified form:
retrieve :: Transitive C x y => x >-> y
The Way?
The best hint at a way forward is the type signature of trans, or equivalently, (.):
(.) :: forall x y z. y >-> z -> x >-> y -> x >-> z
With a little rearranging, that says we have mappings:
yoneda1 :: forall y z. y >-> z -> forall x. x >-> y -> x >-> z
yoneda1 yz = (yz .)
yoneda2 :: forall x y. x >-> y -> forall z. y >-> z -> x >-> z
yoneda2 xy = (. xy)
refl/id then provides the inverses, showing that these types are equivalent.
unYoneda1 :: forall y z. (forall x. x >-> y -> x >-> z) -> y >-> z
unYoneda1 f = f id
unYoneda2 :: forall x y. (forall z. y >-> z -> x >-> z) -> x >-> y
unYoneda2 f = f id
These Yoneda embeddings give us alternate representations for any Category, directly analogous to the Cayley transform on group-like structures (e.g. difference lists) and the Codensity of a Monad, down to the uniform re-association.
Translating the transformations onto C, we obtain excellent candidates for our implication constraint:
C y z ~= forall x. C x y => C x z
C x y ~= forall z. C y z => C x z
Of the two, only the latter is reverse functional, so that’s our best choice.
class (forall z. c y z => c x z) => Transitive c x y
instance (forall z. c y z => c x z) => Transitive c x y
Having achieved the first of our three goals, the third is easy.
retrieve :: forall x y. Transitive C x y => x >-> y
retrieve = case refl @y of Dict -> reify
The second isn’t. We can write one half:
ant :: C x y => forall z. Dict (C y z) -> Dict (C x z)
ant = trans Dict
The other half, on the other hand, doesn’t even seem to be possible!
gr :: (forall z. Dict (C y z) -> Dict (C x z)) -> Dict (Transitive C x y)
gr f = ???
In the particular case where (>->) carries no runtime-distinguishable data, gr can be “written” by ignoring the argument and cooking up a dictionary with unsafeCoerce, but that’s not exactly satisfactory.
Afterword
Having been taken on such a long ride only to face defeat at every turn, you must be very disappointed. I know I am. Perhaps somewhere out there, there’s a hero who can grant this tale the good ending it deserves.
