[Haskell-cafe] Existential type variables in constraints

[Edward Kmett]

There's a lot here. I'm just going to laser lock on the starting impossible
part that AntC also tried to address.

On Sat, Apr 3, 2021 at 12:26 AM CASANOVA Juan <Juan.Casanova at ed.ac.uk>
wrote:

>
> 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
>
> This doesn't say what you seem to think it says.

It says:

    When you go to look for an instance for Class1, every such instance is
formed as follows:

    * First go resolve an Ord instance for a. (So far so good).

    * Next you need to show that for every single pair of types in the
universe b and c, Ord b and Ord c hold independently. (Which makes the
comparatively narrow ask for an Ord for a seem pretty redundant!)

That is an impassable bar. Full stop.

It is equivalent to

instance (forall x. Ord x) => Class1 a

The existence of any type anywhere without an Ord instance that can be
uniformly constructed without caring at all about any structure on 'a'
stops you cold.

That forall isn't denoting existential there, it really is denoting a
universal quantifier.

If you want 'b' and 'c' to be some function of a, you can use a type family
for each to pick them out or a multi-parameter typeclass that includes them
in the signature, but that is simply not what you wrote down.

-Edward

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.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210404/1a67ac6a/attachment.html>