Andrew Gibiansky | 7 Jan 04:17 2014
Picon

Class Instance with ExistentialQuantification

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.

-- Andrew
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Roman Cheplyaka | 7 Jan 11:18 2014

Re: Class Instance with ExistentialQuantification

* 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
Andrew Gibiansky | 7 Jan 16:11 2014
Picon

Re: Class Instance with ExistentialQuantification

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 Breitner | 7 Jan 16:16 2014
Picon

Re: Class Instance with ExistentialQuantification

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
Roman Cheplyaka | 7 Jan 23:33 2014

Re: Class Instance with ExistentialQuantification

* Joachim Breitner <mail <at> joachim-breitner.de> [2014-01-07 15:16:15+0000]
> Hi,
> 
> is it not allowed simply because none has needed it yet, or is there a
> deeper theoretical problem with it?

FWIW, here's Simon's answer on a similar topic:
http://osdir.com/ml/glasgow-haskell-users <at> haskell.org/2013-03/msg00048.html

> 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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard Eisenberg | 8 Jan 20:40 2014

Re: Class Instance with ExistentialQuantification

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

Gmane