### Re: Class Instance with ExistentialQuantification

Richard Eisenberg <eir <at> cis.upenn.edu>

2014-01-08 19:40:01 GMT

I think allowing polytype instances would lead to incoherence. This is, of course, OK with Coercible
(where incoherence is rife and completely appropriate). But, consider
> instance Foo (forall a. [a]) where ...
> instance Foo [Int] where ...
>
> bar :: Foo b => b -> ...
>
> quux = bar []
Which instance should be used in the call to `bar`? Perhaps those two instances would just be considered overlapping.
Another related issue is that making polytype instances useful seems to require impredicativity. Recall
that impredicativity means allowing type variables to take on polytype values. (Normally, type
variables are always instantiated to monotypes.) Type inference in the presence of impredicativity is
wonky at best.
A colleague (Hamidhasan Ahmed) is working on allowing explicit type applications, which would greatly
help with impredicative inference. When that's working, I think polytype instances may make more sense.
Though, in the end, I agree that this takes some Careful Thought.
Richard
On Jan 7, 2014, at 10:16 AM, Joachim Breitner <mail <at> joachim-breitner.de> wrote:
> Hi,
>
> is it not allowed simply because none has needed it yet, or is there a
> deeper theoretical problem with it?
>
> I’m asking because the implementation of Coercible behaves as if there
> is an instance
> instance forall a. (Coercible (t1 a) (t2 a)) => Coercible (forall a. t1 a) (forall a. t2 a)
> and if were theoretically dubious, I’d like to know about it
>
> Greetings,
> Joachim
>
> Am Dienstag, den 07.01.2014, 10:11 -0500 schrieb Andrew Gibiansky:
>> Ah, I see. I wasn't aware that constraints had to be over monotypes. I
>> figured that since you could write a function
>>
>>
>> f :: (forall a. a -> a) -> Bool
>>
>>
>> Then you could also do similar things with a class.
>>
>>
>> (The reason I was doing this was that I wanted a typeclass to match
>> something like "return 'a'" without using IncoherentInstances or other
>> sketchiness, and found that trying to have a typeclass with an
>> instance for 'forall m. Monad m => m Char` gave me this error.)
>>
>>
>> Thanks!
>> Andrew
>>
>>
>> On Tue, Jan 7, 2014 at 5:18 AM, Roman Cheplyaka <roma <at> ro-che.info>
>> wrote:
>> * Andrew Gibiansky <andrew.gibiansky <at> gmail.com> [2014-01-06
>> 22:17:21-0500]
>>> Why is the following not allowed?
>>>
>>> {-# LANGUAGE ExistentialQuantification, ExplicitForAll,
>> RankNTypes,
>>> FlexibleInstances #-}
>>>
>>> class Class a where
>>> test :: a -> Bool
>>>
>>> instance Class (forall m. m -> m) where
>>> test _ = True
>>>
>>> main = do
>>> putStrLn $ test id
>>>
>>> Is there a reason that this is forbidden? Just curious.
>>
>>
>> I believe the rule is that all constraints (including class
>> constraints)
>> range over monotypes.
>>
>> What are you trying to achieve?
>>
>> You can do this, for example:
>>
>> newtype Poly = Poly (forall a . a -> a)
>> instance Class Poly where test = const True
>>
>> main = print $ test $ Poly id
>>
>> BTW, this has nothing to do with ExistentialQuantification.
>>
>> Roman
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe <at> haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> --
> Joachim “nomeata” Breitner
> mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
> Jabber: nomeata <at> joachim-breitner.de • GPG-Key: 0x4743206C
> Debian Developer: nomeata <at> debian.org
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe