Restrictions on polytypes with type families

[Iavor Diatchki]

Hello,

isn't this moving directly into the territory of impredicative types?  Not
that there is anything wrong with that, but there seemed to be a number of
different ways to implement these sorts of things, and my impression was
that neither is particularly simple.  I am thinking of examples like this:

    type family F a

    type instance F Int = Int
    type instance F Char = forall a. a -> a

It is somewhat unclear in what contexts it is OK to use `F`.  For
example, `Maybe
(F Int)` is OK, but `Maybe (F Char)` is not (or rather, it is
"impredicative").

-Iavor












On Wed, Apr 3, 2013 at 10:30 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

> I don't think there's a fundamental reason.  At least, provided we stick
> to impredicative polymorphism, we can just treat forall as another type
> former. The unifier *already* deals properly with forall, yielding a
> suitable coercion, at least I think so.
>
> Dimitrios may think of some gotchas, but mostly I think it'd be a question
> of pushing through the details.
>
> Simon
>
>
>
> | -----Original Message-----
> | From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org]
> | On Behalf Of Richard Eisenberg
> | Sent: 03 April 2013 17:40
> | To: ghc-devs
> | Subject: Restrictions on polytypes with type families
> |
> | Hi all,
> |
> | GHC doesn't allow type families to be used with polytypes:
> | 1) The right-hand side of a type family instance cannot have a "forall".
> | 2) A type family cannot be applied to a type containing a "forall".
> | 3) A pattern in a type family instance is (oddly) allowed to contain
> | "forall", but this is silly because of (2).
> |
> | Do these restrictions have known reasons for their existence? Or, are
> | there any that are restricted because someone needs to think hard before
> | lifting it, and no one has yet done that thinking? I know, for example,
> | that the unify function in types/Unify.lhs will have to be completed to
> | work with foralls, but this doesn't seem hard.
> |
> | I've run into two separate cases where I've hit this restriction, so
> | this isn't just idle thought.
> |
> | Thanks,
> | Richard
> | _______________________________________________
> | ghc-devs mailing list
> | ghc-devs at haskell.org
> | http://www.haskell.org/mailman/listinfo/ghc-devs
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130403/51a96e9c/attachment.htm>