I actually thought of a new solution proposal for this half a year ago, but didn't get around to posting it. I had a look at the GHC.Magic.Dict module and it feels like the WithDict
class is backed by some magic machinery that's very similar to what's needed here.
With WithDict
, we can do stuff like
import GHC.Magic.Dict
import GHC.TypeNats
withSNat :: forall n r. SNat n -> (KnownNat n => r) -> r
withSNat s x = withDict @(KnownNat n) @(SNat n) s x
A bit like Typeable
, I guess the WithDict
instance is created on the fly by the compiler. The first type parameter, the class constraint, basically dictates what the second type parameter is, namely the type of the class's only method. (You'd think there was as fundep relationship, but there's not.)
What I'm thinking about is adding a similar typeclass in the same module, like
class WithQuantifiedDict constraint term where
withQuantifiedDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). term -> (constraint => r) -> r
WithQuantifiedDict
is really just like WithDict
, even down to kind (maybe they can even be the same class). But what's different is that WithQuantifiedDict
isn't expecting the constraint
argument to be a single-method type class and term
to be a value of that method's type. Instead, it expects constraint
to be a constraint that consists of a combination of forall
s and implications with =>
. And then, term
is a translation of constraint
into a corresponding Type
-kinded type.
I'm thinking that implication constraints would translate into functions between dictionaries and forall
s come along largely the same as they were in constraint
. Dictionaries could be defined in various ways, but for example, let's say:
type role Dict representational
data Dict c where
Dict :: c => Dict c
For example, when constraint
is forall a. Foo a => Bar a
, then term
is forall a. Dict (Foo a) -> Dict (Bar a)
. Using the withQuantifiedDict
function, a user can then call a function that requires that implication constraint as context, as long as they can provide an implementation for a function of type forall a. Dict (Foo a) -> Dict (Bar a)
.
Then it should be possible to write all of the above reifyImplicationX
variations that @treeowl displayed above:
reifyImplication :: forall a b. (forall r. a => (b => r) -> r) -> (forall r. ((a => b) => r) -> r)
reifyImplication f expr =
withQuantifiedDict
@(a => b)
@(Dict a -> Dict b)
(\(Dict :: Dict a) -> f (Dict @b))
expr
reifyImplication1 :: forall a b. (forall r x. a x => (b x => r) -> r) -> (forall r. ((forall x. a x => b x) => r) -> r)
reifyImplication1 f expr =
withQuantifiedDict
@(forall x. a x => b x)
@(forall x. Dict (a x) -> Dict (b x))
(\(Dict :: Dict (a x)) -> f @_ @x (Dict @(b x)))
expr
reifyImplication2 :: forall a b. (forall r x y. a x y => (b x y => r) -> r) -> (forall r. ((forall x y. a x y => b x y) => r) -> r)
reifyImplication2 f expr =
withQuantifiedDict
@(forall x y. a x y => b x y)
@(forall x y. Dict (a x y) -> Dict (b x y))
(\(Dict :: Dict (a x y)) -> f @_ @x @y (Dict @(b x y)))
expr
reifyImplicationQ :: forall a b y. (forall r x. a x y => (b x y => r) -> r) -> (forall r. ((forall x. a x y => b x y) => r) -> r)
reifyImplicationQ f expr =
withQuantifiedDict
@(forall x. a x y => b x y)
@(forall x. Dict (a x y) -> Dict (b x y))
(\(Dict :: Dict (a x y)) -> f @_ @x (Dict @(b x y)))
expr
I can't claim that I know anything about what machinery could make this become possible. This is only a new idea for how the surface language could express this intent.