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
From: Iavor Diatchki [mailto:iavor.diatc...@gmail.com]
Sent: 03 April 2013 18:48
To: Simon Peyton-Jones
Cc: Richard Eisenberg; ghc-devs
Subject: Re: Restrictions on polytypes with type families
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
<simo...@microsoft.com<mailto:simo...@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-boun...@haskell.org<mailto:ghc-devs-boun...@haskell.org>
[mailto:ghc-devs-boun...@haskell.org<mailto:ghc-devs-boun...@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@haskell.org<mailto:ghc-devs@haskell.org>
| http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org<mailto:ghc-devs@haskell.org>
http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
