What are the problems with instances for polymorphic types?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

What are the problems with instances for polymorphic types?

Gábor Lehel-2
In other words instances for forall-types, such as:

    instance Foo (forall a. [a]) where ...

It feels obvious to me that there *would* be problems with this, but I'm curious about what, exactly, they are.

Could someone familiar with the matter either elaborate on them, or refer me to an existing explanation, a previous discussion, or something of the sort?

I *don't* have any kind of use case in mind, I'm merely seeking a better understanding of the type-system issues involved.

(I attempted Google, but didn't have much success.)

Thanks in advance.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: What are the problems with instances for polymorphic types?

Ahn, Ki Yung
The only value that inhabits (forall a. [a]), except bottom, is the
empty list []. You can actually experiment this with ghci.


shell-prompt$ ghci -XRankNTypes
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.

Prelude> [] :: (forall a. [a])
[]

Prelude> [True] :: (forall a. [a])

<interactive>:7:2:
     Couldn't match expected type `a1' with actual type `Bool'
       `a1' is a rigid type variable bound by
            an expression type signature: [a1] at <interactive>:7:1
     In the expression: True
     In the expression: [True] :: forall a. [a]
     In an equation for `it': it = [True] :: forall a. [a]

Prelude> ['a'] :: (forall a. [a])

<interactive>:8:2:
     Couldn't match expected type `a1' with actual type `Char'
       `a1' is a rigid type variable bound by
            an expression type signature: [a1] at <interactive>:8:1
     In the expression: 'a'
     In the expression: ['a'] :: forall a. [a]
     In an equation for `it': it = ['a'] :: forall a. [a]

Prelude> [\x -> x] :: (forall a. [a])

<interactive>:9:2:
     Couldn't match expected type `a1' with actual type `t0 -> t0'
       `a1' is a rigid type variable bound by
            an expression type signature: [a1] at <interactive>:9:1
     The lambda expression `\ x -> x' has one argument,
     but its type `a1' has none
     In the expression: \ x -> x
     In the expression: [\ x -> x] :: forall a. [a]



2014년 06월 15일 12:47, Gábor Lehel 쓴 글:

> In other words instances for forall-types, such as:
>
>      instance Foo (forall a. [a]) where ...
>
> It feels obvious to me that there *would* be problems with this, but I'm
> curious about what, exactly, they are.
>
> Could someone familiar with the matter either elaborate on them, or
> refer me to an existing explanation, a previous discussion, or something
> of the sort?
>
> I *don't* have any kind of use case in mind, I'm merely seeking a better
> understanding of the type-system issues involved.
>
> (I attempted Google, but didn't have much success.)
>
> Thanks in advance.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: What are the problems with instances for polymorphic types?

Niklas Haas
In reply to this post by Gábor Lehel-2
On Sun, 15 Jun 2014 21:47:52 +0200, Gábor Lehel <[hidden email]> wrote:

> In other words instances for forall-types, such as:
>
>     instance Foo (forall a. [a]) where ...
>
> It feels obvious to me that there *would* be problems with this, but I'm
> curious about what, exactly, they are.
>
> Could someone familiar with the matter either elaborate on them, or refer
> me to an existing explanation, a previous discussion, or something of the
> sort?
>
> I *don't* have any kind of use case in mind, I'm merely seeking a better
> understanding of the type-system issues involved.
>
> (I attempted Google, but didn't have much success.)
>
> Thanks in advance.

It seems to me that it may be possible to get more information about
this by searching for issues related to ImpredicativeTypes, which seem
to be similar. (In fact, one could simulate instances like these by
implementing type classes using ImplicitParams + ImpredicativeTypes +
explicit instance records)
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: What are the problems with instances for polymorphic types?

Adam Gundry-2
On 16/06/14 11:14, Niklas Haas wrote:

> On Sun, 15 Jun 2014 21:47:52 +0200, Gábor Lehel <[hidden email]> wrote:
>> In other words instances for forall-types, such as:
>>
>>     instance Foo (forall a. [a]) where ...
>>
>> It feels obvious to me that there *would* be problems with this, but I'm
>> curious about what, exactly, they are.
>>
>> Could someone familiar with the matter either elaborate on them, or refer
>> me to an existing explanation, a previous discussion, or something of the
>> sort?
>>
>> I *don't* have any kind of use case in mind, I'm merely seeking a better
>> understanding of the type-system issues involved.
>>
>> (I attempted Google, but didn't have much success.)
>>
>> Thanks in advance.
>
> It seems to me that it may be possible to get more information about
> this by searching for issues related to ImpredicativeTypes, which seem
> to be similar. (In fact, one could simulate instances like these by
> implementing type classes using ImplicitParams + ImpredicativeTypes +
> explicit instance records)

I don't think there has been much research on type inference for these
kind of instances (though I'd be happy to be corrected). They are sort
of like ImpredicativeTypes but worse, in that it is very hard to tell
where the invisible type abstractions and applications go.

For example, suppose we have these declarations:

    class Foo t where
       useFoo :: t -> Int

    instance Foo (forall a. [a]) where
        useFoo x = length (x :: [()])

    f = useFoo []

The class and instance declarations make sense (the instance declaration
ends up checking `useFoo` with a higher-rank type, but that's okay). But
when inferring the type of `f`, we have

    useFoo :: forall t . Foo t => t -> Int

and the typechecker needs to magically guess that

    t ~ forall a . [a]

which is difficult.  If there was some way of explicitly writing the
type at which to instantiate `t`, for example

    f = useFoo @(forall a. [a]) []

then it might be possible to make progress. [1]

All this would, however, make perfect sense in System FC, once type
abstractions and applications have been made explicit, and typeclass
constraints have been replaced with visible dictionaries.

Hope this helps,

Adam

[1] https://ghc.haskell.org/trac/ghc/wiki/TypeApplication


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: What are the problems with instances for polymorphic types?

Gábor Lehel-2



On Tue, Jun 17, 2014 at 9:43 PM, Adam Gundry <[hidden email]> wrote:
On 16/06/14 11:14, Niklas Haas wrote:
> On Sun, 15 Jun 2014 21:47:52 +0200, Gábor Lehel <[hidden email]> wrote:
>> In other words instances for forall-types, such as:
>>
>>     instance Foo (forall a. [a]) where ...
>>
>> It feels obvious to me that there *would* be problems with this, but I'm
>> curious about what, exactly, they are.
>>
>> Could someone familiar with the matter either elaborate on them, or refer
>> me to an existing explanation, a previous discussion, or something of the
>> sort?
>>
>> I *don't* have any kind of use case in mind, I'm merely seeking a better
>> understanding of the type-system issues involved.
>>
>> (I attempted Google, but didn't have much success.)
>>
>> Thanks in advance.
>
> It seems to me that it may be possible to get more information about
> this by searching for issues related to ImpredicativeTypes, which seem
> to be similar. (In fact, one could simulate instances like these by
> implementing type classes using ImplicitParams + ImpredicativeTypes +
> explicit instance records)

I don't think there has been much research on type inference for these
kind of instances (though I'd be happy to be corrected). They are sort
of like ImpredicativeTypes but worse, in that it is very hard to tell
where the invisible type abstractions and applications go.

For example, suppose we have these declarations:

    class Foo t where
       useFoo :: t -> Int

    instance Foo (forall a. [a]) where
        useFoo x = length (x :: [()])

    f = useFoo []

The class and instance declarations make sense (the instance declaration
ends up checking `useFoo` with a higher-rank type, but that's okay). But
when inferring the type of `f`, we have

    useFoo :: forall t . Foo t => t -> Int

and the typechecker needs to magically guess that

    t ~ forall a . [a]

which is difficult.  If there was some way of explicitly writing the
type at which to instantiate `t`, for example

    f = useFoo @(forall a. [a]) []

then it might be possible to make progress. [1]

All this would, however, make perfect sense in System FC, once type
abstractions and applications have been made explicit, and typeclass
constraints have been replaced with visible dictionaries.

I see. Thanks a lot! So there wouldn't be any issues with coherence, or with typechecking itself: only with inference?

Would the foralls in instances essentially be treated as another type constructor under this scenario?
 

Hope this helps,

Adam

[1] https://ghc.haskell.org/trac/ghc/wiki/TypeApplication


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe