> On Dec 30, 2019, at 11:16 AM, Alexis King <[email protected]> wrote:
>
> I don’t know if there is a way to encode those using the constraint language
> available in source Haskell today.
I gave it a good try, but failed. The trick I was hoping to leverage was
*partial improvement*. Here is an example of partial improvement:
> class FD1 a b | a -> b
> class FD2 a b | a -> b
>
> instance FD1 a b => FD2 (Maybe a) (Maybe b)
>
> f :: FD2 a b => a -> b
> f = undefined
>
> x = f (Just True)
This program will require solving [W] FD2 (Maybe Bool) beta, where the [W]
indicates that we have a "wanted" constraint (a goal we are trying to satisfy)
and beta is a unification variable. GHC can figure out from the fundep on FD2
that the only FD2 instance that can apply is the one we see above. It thus
knows that beta must be Maybe beta2 (for some fresh beta2). This is the essence
of partial improvement, when we solve one unification variable with an
expression involving another (but is more informative somehow).
I thought that, maybe, we could use partial improvement to give you what you
want, by replacing the RHSs of the type family with expressions involving
classes with fundeps. (Injective type families work very analogously, but it's
not worthwhile showing the translation of this idea to that domain here.) I
couldn't quite get it to work out, though. Maybe you can, armed with this
description... but I doubt it. The problem is that partial improvement must
always be a shadow of some "total" improvement process. In the example above,
note that I haven't written down an instance of FD1. Clearly, we'll need to
satisfy the FD1 constraint in order to satisfy the FD2 constraint. The problem
is that, in your example, we really only want partial improvement... and I
don't think there's a way to state that. What's tantalizing is that GHC already
does all this partial improvement stuff -- it's just that we can't seem to
write the instance declarations the way we want to satisfy your use case.
I don't know if this really moves us forward at all, but maybe a description of
my failure can lead to someone's success. Or perhaps it will lead to a language
improvement that will allow us to express what you want.
Richard
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
