[Haskell-cafe] Existential type variables in constraints

Sat Apr 3 07:20:44 UTC 2021

Richard's answer sounds like pretty much what I thought on my follow-up message, and I guess I'll have to go the route of re-writing all the constraints that do not contain the type variable no longer there.

Anthony,

I won't argue with the discussion on which extensions are problematic. The reason I thought people saw UndecidableInstances as problematic is that, precisely because of the undecidability (semidecidability?), you can write incorrect programs that do not terminate to compile, and it can be hard to debug. I do know that whenever the program is correct then it works fine. But we don't always write correct programs, and debugging is an essential thing as well. That said, I have ran into the overlapping instances issues myself plenty of times so I'm not disagreeing, I just had this impression I think from reading people talk about UndecidableInstances.

On your discussion of my particular example, I think I did not make it clear enough why I want to do things like that. I did try to explain it, but it seems it did not click with you. Also, I think one of the statements you made is flat out incorrect, but maybe I'm mistaken. One thing at a time.

> instance (Ord a, forall b c. (Ord b, Ord c)) => Class1 a where
>   fun1 = (<)

Why does that even mention `b` or `c`? There's no FunDep from `a`, to get a FunDep there'd be a constraint `D a b c` or something. They seem totally redundant.

This example is just to corner the problem in one example. The reality of what I would do would be more like this:

> type CType b c = (Ord b, Ord c)
> instance (Ord a, forall b c. CType b c) => Class1 a where
>   fun1 = (<)

Why do I do this? Because, as I tried to explain, my CType in practice is much larger, and it includes many more type variables. I do it to avoid having 5-line constraints on every function I write. Maybe if I show you the actual example it'll click with you. Here's some of the examples:

type ESMGUConstraints t pd fn v sov = (Ord sov, SimpleTerm t, Eq fn, HasArity fn, HasArity sov, ChangeArity sov, Functor (t (SOTerm fn sov)), Functor (t fn), Bifunctor t, Traversable (t (GroundSOT fn)), Unifiable (t (SOTerm fn sov)), Variabilizable v, Variable v, Variabilizable sov, Variable sov, Ord v, Functor (t (GroundSOT fn)), Eq (t fn (Fix (t fn))), Show sov, Show fn, Show v, Show (t (SOTerm fn sov) (UTerm (t (SOTerm fn sov)) v)), Show (t (GroundSOT fn) (UTerm (t (GroundSOT fn)) v)), Ord fn, Ord (t (SOTerm fn sov) (UTerm (t (SOTerm fn sov)) v)))
type ESMGUConstraintsU t pd fn v sov uv = (ESMGUConstraints t pd fn v sov, Show uv, Ord uv, Variable uv, Variabilizable uv)
type ESMGUConstraintsPdPmv pd pmv = (Ord pd, Ord pmv, Eq pd, Eq pmv, Show pmv, Show pd, HasArity pd, HasArity pmv, Variable pmv, Variabilizable pmv, ChangeArity pmv)
type ESMGUConstraintsUPmv t pd fn v pmv fmv uv = (ESMGUConstraintsU t pd fn v fmv uv, ESMGUConstraintsPdPmv pd pmv)
type ESMGUConstraintsA a = (SimpleTerm a)
type ESMGUConstraintsAMpd a mpd = (ESMGUConstraintsA a, Functor (a mpd), Eq mpd, Ord mpd)
type ESMGUConstraintsSS ss = (Functor ss, Unifiable ss)
type ESMGUConstraintsAMpdSs a t ss mpd pd fn v pmv fmv = (ESMGUConstraints t pd fn v fmv, ESMGUConstraintsSS ss, ESMGUConstraintsAMpd a mpd, Eq (a mpd (ss (SOAtom pd fn pmv fmv))), Eq (a (SOAtom pd fn pmv fmv) (SOMetawrap t fn v fmv)), ESMGUConstraintsPdPmv pd pmv)
type ESMGUConstraintsALL a t ss mpd pd fn v pmv fmv uv = (ESMGUConstraintsU t pd fn v fmv uv, ESMGUConstraintsAMpdSs a t ss mpd pd fn v pmv fmv)

I think you can see why I would want to avoid having to write all of this on every function that I write. In fact you can see I already have it partially split, but not in all the ways I may want to use it. In particular,  there are others in other modules that build on these and add a few others, and I want those except I no longer have the "uv" type variable on one of the functions I have, but I internally use functions that use the constraints that include it, and functional dependencies should ensure that it is instantiated to one particular class.

But this leads to your second point, the one in which I think you said something incorrect, or maybe you didn't see how my example was simplified on purpose. You said:

No it isn't possible, even in principle: `(..., ...)` is a tuple constructor, not a class; therefore no FunDep could apply.

What about the following code then:

class Class1 a b | b -> a where
  fun1 :: b -> a

type CType a b = (Ord a, Class1 a b)

fun2 :: (forall b. CType a b) => a -> a -> Bool
fun2 = (>)

Now, fun2 in particular can be made to work because it only makes use of (Ord a) and not (Class1 a b), but the tuple constraint type (CType a b) does have a functional dependency from b to a, so I can see why a is not an entirely separable variable in the forall-quantified constraint, which is why I think ultimately GHC works the way Richard mentioned and why I can't do what I want, even if the specific (Ord a) constraint can be used.

Of course the issue, I see, is that this could produce (and does, in my case) chains of functional dependencies that, when existentially quantified, become difficult/problematic. For example:

class Class1 a b | b -> a where
  fun1 :: b -> a

type CType a b c = (Class1 a b, Class1 b c)

fun2 :: (forall c. CType a b c) => b -> a
fun2 = fun1

fun1 does not depend on c, but the type b does, through the functional dependency in (Class1 b c). I don't even know if it would make sense for this to work or not. You can separate (Class1 a b) like you could with (Ord a), but now it's not completely independent of the rest. of (CType a b c). In other words, I'm not sure if the semantics of (forall c. CType a b c) are the same as the semantics of (Class1 a b, forall c. Class1 b c).

Now, my actual situation in practice is more something like this:

class Class1 a b | b -> a where
  fun1 :: b -> a

type CType a b c = (Class1 a b, Class1 b c)

fun2 :: (forall b. CType a b c) => c -> a
fun2 c = fun1 (fun1 c)

This makes sense conceptually. fun2 does not specify which b we are talking about, but for every c, there should be only one b that works. That, of course, ultimately means that fun2 will not work for any a and c, but only for those for which there is a b linking them. It seems as if GHC does not have the ability to do this.

Actually at this point I'm not sure if I can do what I want without instantiating the type variables.

Juan.
________________________________
From: Haskell-Cafe <haskell-cafe-bounces at haskell.org> on behalf of Anthony Clayden <anthony_clayden at clear.net.nz>
Sent: 03 April 2021 02:18
To: The Haskell Cafe <haskell-cafe at haskell.org>
Subject: Re: [Haskell-cafe] Existential type variables in constraints

This email was sent to you by someone outside the University.
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.
> because UndecidableInstances is definitely required for this and I know it's a problematic one.

Hi Juan, I'll knock that on the head at once. `UndecidableInstances` is not "problematic" (or at least it's far less problematic than others you list). Although we're lacking a proof that it can't lead to incoherence/type unsafety, nobody's demonstrated unsafety due to `UndecidableInstances` alone -- that is, providing the program compiles (i.e. instance resolution terminates).

OTOH `FlexibleInstances` can give `OverlappingInstances` -- maybe overlapping with those in some other module, thus giving the dreaded Orphan instances problems. I'd be much more concerned about them.

> instance (Ord a, forall b c. (Ord b, Ord c)) => Class1 a where
>   fun1 = (<)

Why does that even mention `b` or `c`? There's no FunDep from `a`, to get a FunDep there'd be a constraint `D a b c` or something. They seem totally redundant.

> completely overlooked by the compiler

Yes. Quite. What do you expect the compiler to do? Even if the class decl gave a signature for `fun1` mentioning `b`, `c`, those would be _distinct_ tyvars, because they're not scoped in the class head.

> is there any way I can make this work?

Sorry, I don't know what you want to "work". Please at least show a class decl with a FunDep. From your second message:

> it is possible in principle that (Ord a, Ord b) produces a functional dependency between a and b

No it isn't possible, even in principle: `(..., ...)` is a tuple constructor, not a class; therefore no FunDep could apply.

AntC

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th' ann an Oilthigh Dh?n ?ideann, cl?raichte an Alba, ?ireamh cl?raidh SC005336.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210403/559ccb61/attachment.html>