[Haskell-cafe] Class Instance with ExistentialQuantification

Richard Eisenberg eir at cis.upenn.edu
Wed Jan 8 19:40:01 UTC 2014


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.dehttp://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



More information about the Haskell-Cafe mailing list