[Haskell-cafe] Existential type variables in constraints

[CASANOVA Juan]

Edward,

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

Huh! You seem to be completely right. I think I had thought it would have an existential meaning like when you use constraints in data definitions, like:

data Foo = forall a. Ord a => Foo a

But I guess here the existential meaning comes from reading it as a universal quantifier on the co-variant argument: "For every a that is an Ord, we can build a Foo with the constructor Foo", which when used the other way around becomes: "If you have a foo, then you have some type with Ord".

This definitely does explain the entire problem with the behaviour I am expecting.

> 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.

Yes, this definitely seems to be the way to go (type families), though I still don't think what I'm trying to do is possible without type families, while keeping the genericity of the type parameters.

Thanks for confirming this, and for clarifying my fundamental misunderstanding with quantified constraints.

Juan.

________________________________
From: Edward Kmett <ekmett at gmail.com>
Sent: 04 April 2021 23:35
To: CASANOVA Juan <Juan.Casanova at ed.ac.uk>
Cc: 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.
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<mailto: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<mailto:haskell-cafe-bounces at haskell.org>> on behalf of Anthony Clayden <anthony_clayden at clear.net.nz<mailto:anthony_clayden at clear.net.nz>>
Sent: 03 April 2021 02:18
To: The Haskell Cafe <haskell-cafe at haskell.org<mailto: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/20210405/ccd53f59/attachment.html>