Restrictions on polytypes with type families
Gabriel Dos Reis
gdr at integrable-solutions.net
Wed Apr 3 21:04:10 CEST 2013
On Wed, Apr 3, 2013 at 12:53 PM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> isn't this moving directly into the territory of impredicative types?
>
>
>
> Ahem, maybe you are right. Impredicativity means that you can
>
> instantiate a type variable with a polytype
>
>
>
> So if we allow, say (Eq (forall a.a->a)) then we’ve instantiated Eq’s type
> variable with a polytype. Ditto Maybe (forall a. a->a).
>
>
>
> But this is only bad from an inference point of view, especially for
> implicit instantiation. Eg if we had
>
> class C a where
>
> op :: Int -> a
>
>
>
> then if we have
>
> f :: C (forall a. a->a) =>...
>
> f = ...op...
>
>
>
> do we expect op to be polymorphic??
>
>
>
> For type families maybe things are easier because there is no implicit
> instantiation.
>
>
>
> But I’m not sure
>
>
>
> Simon
I wouldn't expect any (technical) problem to arise.
I suspect the new formulation [1, 2] of MLF is doing
something like this already. Implementation wise, well,
it might be like moving to GADT :-)
Also, if you are doing it for type families, do it for data families too :-)
[1] http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski:xmlf@tcs2011.pdf
[2] http://www.sciencedirect.com/science/article/pii/S0890540109000145
-- Gaby
More information about the ghc-devs
mailing list