[Haskell-cafe] What are the problems with instances for polymorphic types?
glaebhoerl at gmail.com
Wed Jun 18 17:06:00 UTC 2014
On Tue, Jun 17, 2014 at 9:43 PM, Adam Gundry <adam at well-typed.com> wrote:
> On 16/06/14 11:14, Niklas Haas wrote:
> > On Sun, 15 Jun 2014 21:47:52 +0200, Gábor Lehel <glaebhoerl at gmail.com>
> >> 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
> >> me to an existing explanation, a previous discussion, or something of
> >> 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. 
> 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,
>  https://ghc.haskell.org/trac/ghc/wiki/TypeApplication
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe