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.diatchki@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 mailto:simonpj@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@haskell.orgmailto:ghc-devs-bounces@haskell.org [mailto:ghc-devs-bounces@haskell.orgmailto:ghc-devs-bounces@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.orgmailto:ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Simon Peyton-Jones :

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

These kinds of issues are the reason that my conclusion at the time was (as Richard put it)

Or, are | there any that are restricted because someone needs to think hard before | lifting it, and no one has yet done that thinking?

At the time, there were also problems with what the type equality solver was supposed to do with foralls.

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.

The solver changed quite a bit since I rewrote Tom's original prototype. So, maybe it is easy now, but maybe it is more tricky than you think. The idea of rewriting complex terms into equalities at the point of each application of a type synonym family (aka type function) assumes that you can pull subterms out of a term into a separate equality, but how is this going to work if a forall is in the way? E.g., given type family F a :: * the equality Maybe (forall a. F [a]) ~ G b would need to be broken down to x ~ F [a], Maybe (forall a. x) ~ G b but you cannot do that, because you just moved 'a' out of its scope. Maybe you can move the forall out as well? Manuel

Gabriel Dos Reis :

On Wed, Apr 3, 2013 at 8:01 PM, Manuel M T Chakravarty wrote:

...

E.g., given

type family F a :: *

the equality

Maybe (forall a. F [a]) ~ G b

would need to be broken down to

x ~ F [a], Maybe (forall a. x) ~ G b

but you cannot do that, because you just moved 'a' out of its scope. Maybe you can move the forall out as well?

yes, why wouldn't you pull it out as well:

x ~ forall a. F [a], Maybe x ~ G b

where you systematically introduce fresh type variables for an quantified type expressions?

One universally quantified variable may appear as the argument to two type family applications (or more generally, have two occurrences, of which only one is under the type family). Moreover, the whole equality solution mechanism quite fundamentally depends on producing equalities of the form x ~ F b1 ... bn for type family applications. Sticking a forall in there may lead to trouble with the proof theory. In particular, it would compromise the analogy to CHRs (constraint handling rules) which inspired our solution. Manuel

Manuel has an excellent point. See the Note below in TcCanonical! I have no clue how to deal with this Simon Note [Flattening under a forall] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Under a forall, we (a) MUST apply the inert subsitution (b) MUST NOT flatten type family applications Hence FMSubstOnly. For (a) consider c ~ a, a ~ T (forall b. (b, [c]) If we don't apply the c~a substitution to the second constraint we won't see the occurs-check error. For (b) consider (a ~ forall b. F a b), we don't want to flatten to (a ~ forall b.fsk, F a b ~ fsk) because now the 'b' has escaped its scope. We'd have to flatten to (a ~ forall b. fsk b, forall b. F a b ~ fsk b) and we have not begun to think about how to make that work! From: Manuel M T Chakravarty [mailto:chak@cse.unsw.edu.au] Sent: 04 April 2013 02:01 To: Simon Peyton-Jones Cc: Iavor Diatchki; ghc-devs Subject: Re: Restrictions on polytypes with type families Simon Peyton-Jones mailto:simonpj@microsoft.com>: 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 These kinds of issues are the reason that my conclusion at the time was (as Richard put it) Or, are | there any that are restricted because someone needs to think hard before | lifting it, and no one has yet done that thinking? At the time, there were also problems with what the type equality solver was supposed to do with foralls. 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. The solver changed quite a bit since I rewrote Tom's original prototype. So, maybe it is easy now, but maybe it is more tricky than you think. The idea of rewriting complex terms into equalities at the point of each application of a type synonym family (aka type function) assumes that you can pull subterms out of a term into a separate equality, but how is this going to work if a forall is in the way? E.g., given type family F a :: * the equality Maybe (forall a. F [a]) ~ G b would need to be broken down to x ~ F [a], Maybe (forall a. x) ~ G b but you cannot do that, because you just moved 'a' out of its scope. Maybe you can move the forall out as well? Manuel

On Fri, Apr 5, 2013 at 6:32 AM, Dimitrios Vytiniotis wrote:

Hmm, no I don’t think that Flattening is a very serious problem:

Firstly, we can somehow get around that if we use implication constraints and higher-order flattening

variables. We have discussed that (but not implemented). For example.

forall a. F [a] ~ G Int

becomes:

forall a. fsk a ~ G Int

forall a. true => fsk a ~ F [a]

Secondly: flattening under a Forall is not terribly important, unless you have type families that dispatch on

polymorphic types, which is admittedly a rather rare case. We lose some completeness but that’s ok.

For me, a more serious problem are polymorphic RHS, which give rise to exactly the same problems for type

inference as impredicative polymorphism. For instance:

type instance F Int = forall a. a -> [a]

g :: F Int

g = undefined

main = g 3

Should this type check or not? And then all our discussions about impredicativity, explicit type applications etc become

relevant again.

I would expect a saturated type family application to be expanded right away so that g effectively has type forall a . a -> [a], as if in fact we had type FInt = forall a . -> [a]. As long as you stay away from inferring type constructors, I suspect you should be fine. -- Gaby

Has there been any other discussions/write-ups regarding the issues in this (stale) thread? In particular, I'm interested in polytypes on the RHS of type family instances. The rest of this email just explains my interest a bit and culiminates in a more domain-specific and more open-response question. I'd like to explore some generalizations of GHC.Generics, but I think I'll need polytypes on the RHS of a type family instances. For example, this type family is a step towards Hinze's "Polytypic Values Possess Polykinded Types". type family NatroN (t::k) (s::k) :: * type instance NatroN t s = t -> s type instance NatroN t s = forall x. NatroN (t x) -> (s x) However, I'm not sure how I'd write an *equally general* type class for creating/applying such a value. Perhaps these two combinators (which I think would type-check) would help. lift1 :: (forall x. NatroN (t x) (s x)) -> NatroN t s lift1 f = f drop1 :: forall x. NatroN t s -> NatroN (t x) (s x) drop1 f = f I'm hoping these definitions might enable me to unify stacks of classes, such as class Functor1_1 t where fmap1_1 :: (a -> b) -> t a -> t b class Functor1_2 t where fmap1_2 :: (a -> b) -> t a y -> t b y class Functor2_1 t where fmap2_1 :: (forall x. a x -> b x) -> t a -> t b class Functor2_2 t where fmap2_2 :: (forall x. a x -> b x) -> t a y -> t b y into a single class such as class FunctorPK t where fmapPK :: Proxy t -> Proxy a -> Natro a b -> Natro (t a) (t b) So, an additional question: am I barking up the wrong tree? In other words, is there an alternative to expressing these kinds of kind-polymorphic values that is currently more workable? Thank you for your time. ----- PS Here's an optimistic guess at what instances of FunctorPK might look like, omitting the proxies for now. newtype Example g h a = Example {unExample :: g (h a) a)}

instance FunctorPK (g (h Int)) => FunctorPK (Example g h) where fmapPK f = Example . fmapPK {- at g -} (fmapPK {- at h -} f) . . {- drop1 ? -} (fmapPK {- at g (h a) -} f)) . unExample

instance FunctorPK g => FunctorPK (Example g) where

fmapPK f (Example x) = Example $ fmapPK {- at g -} ({- drop1 ? -} f) x

instance FunctorPK Example where

fmapPK f (Example x) = Example (f x)

Thanks again. On Fri, Apr 5, 2013 at 1:32 PM, Dimitrios Vytiniotis

wrote:

Hmm, no I don’t think that Flattening is a very serious problem:

Firstly, we can somehow get around that if we use implication constraints and higher-order flattening

variables. We have discussed that (but not implemented). For example.

forall a. F [a] ~ G Int

becomes:

forall a. fsk a ~ G Int

forall a. true => fsk a ~ F [a]

Secondly: flattening under a Forall is not terribly important, unless you have type families that dispatch on

polymorphic types, which is admittedly a rather rare case. We lose some completeness but that’s ok.

For me, a more serious problem are polymorphic RHS, which give rise to exactly the same problems for type

inference as impredicative polymorphism. For instance:

type instance F Int = forall a. a -> [a]

g :: F Int

g = undefined

main = g 3

Should this type check or not? And then all our discussions about impredicativity, explicit type applications etc become

relevant again.

Thanks!

d-

If the problem with foralls on the RHS is that it devolves into ImpredicativeTypes, what about only allowing them when ImpredicativeTypes is on?

*From:* Simon Peyton-Jones *Sent:* Friday, April 05, 2013 8:24 AM *To:* Manuel M T Chakravarty *Cc:* Iavor Diatchki; ghc-devs; Dimitrios Vytiniotis *Subject:* RE: Restrictions on polytypes with type families

Manuel has an excellent point. See the Note below in TcCanonical! I have no clue how to deal with this

Simon

Note [Flattening under a forall]

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Under a forall, we

(a) MUST apply the inert subsitution

(b) MUST NOT flatten type family applications

Hence FMSubstOnly.

For (a) consider c ~ a, a ~ T (forall b. (b, [c])

If we don't apply the c~a substitution to the second constraint

we won't see the occurs-check error.

For (b) consider (a ~ forall b. F a b), we don't want to flatten

to (a ~ forall b.fsk, F a b ~ fsk)

because now the 'b' has escaped its scope. We'd have to flatten to

(a ~ forall b. fsk b, forall b. F a b ~ fsk b)

and we have not begun to think about how to make that work!

*From:* Manuel M T Chakravarty [mailto:chak@cse.unsw.edu.au]

*Sent:* 04 April 2013 02:01 *To:* Simon Peyton-Jones *Cc:* Iavor Diatchki; ghc-devs *Subject:* Re: Restrictions on polytypes with type families

Simon Peyton-Jones :

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

These kinds of issues are the reason that my conclusion at the time was (as Richard put it)

Or, are | there any that are restricted because someone needs to think hard before | lifting it, and no one has yet done that thinking?

At the time, there were also problems with what the type equality solver was supposed to do with foralls.

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.

The solver changed quite a bit since I rewrote Tom's original prototype. So, maybe it is easy now, but maybe it is more tricky than you think. The idea of rewriting complex terms into equalities at the point of each application of a type synonym family (aka type function) assumes that you can pull subterms out of a term into a separate equality, but how is this going to work if a forall is in the way? E.g., given

type family F a :: *

the equality

Maybe (forall a. F [a]) ~ G b

would need to be broken down to

x ~ F [a], Maybe (forall a. x) ~ G b

but you cannot do that, because you just moved 'a' out of its scope. Maybe you can move the forall out as well?

Manuel

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

-- Your ship was destroyed in a monadic eruption. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Me neither. Simon From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard Eisenberg Sent: 12 November 2013 16:15 To: Nicolas Frisby Cc: Manuel Chakravarty; ghc-devs@haskell.org Subject: Re: Restrictions on polytypes with type families I'm unaware of any progress on this front since the thread died out. I don't really think I have time to get too involved in an answer, but I'd be quite keen to hear of one! Richard On Nov 11, 2013, at 2:47 PM, Nicolas Frisby wrote: Has there been any other discussions/write-ups regarding the issues in this (stale) thread? In particular, I'm interested in polytypes on the RHS of type family instances. The rest of this email just explains my interest a bit and culiminates in a more domain-specific and more open-response question. I'd like to explore some generalizations of GHC.Generics, but I think I'll need polytypes on the RHS of a type family instances. For example, this type family is a step towards Hinze's "Polytypic Values Possess Polykinded Types". type family NatroN (t::k) (s::k) :: * type instance NatroN t s = t -> s type instance NatroN t s = forall x. NatroN (t x) -> (s x) However, I'm not sure how I'd write an *equally general* type class for creating/applying such a value. Perhaps these two combinators (which I think would type-check) would help. lift1 :: (forall x. NatroN (t x) (s x)) -> NatroN t s lift1 f = f drop1 :: forall x. NatroN t s -> NatroN (t x) (s x) drop1 f = f I'm hoping these definitions might enable me to unify stacks of classes, such as class Functor1_1 t where fmap1_1 :: (a -> b) -> t a -> t b class Functor1_2 t where fmap1_2 :: (a -> b) -> t a y -> t b y class Functor2_1 t where fmap2_1 :: (forall x. a x -> b x) -> t a -> t b class Functor2_2 t where fmap2_2 :: (forall x. a x -> b x) -> t a y -> t b y into a single class such as class FunctorPK t where fmapPK :: Proxy t -> Proxy a -> Natro a b -> Natro (t a) (t b) So, an additional question: am I barking up the wrong tree? In other words, is there an alternative to expressing these kinds of kind-polymorphic values that is currently more workable? Thank you for your time. ----- PS Here's an optimistic guess at what instances of FunctorPK might look like, omitting the proxies for now. newtype Example g h a = Example {unExample :: g (h a) a)} instance FunctorPK (g (h Int)) => FunctorPK (Example g h) where fmapPK f = Example . fmapPK {- at g -} (fmapPK {- at h -} f) . . {- drop1 ? -} (fmapPK {- at g (h a) -} f)) . unExample instance FunctorPK g => FunctorPK (Example g) where fmapPK f (Example x) = Example $ fmapPK {- at g -} ({- drop1 ? -} f) x instance FunctorPK Example where fmapPK f (Example x) = Example (f x) Thanks again. On Fri, Apr 5, 2013 at 1:32 PM, Dimitrios Vytiniotis mailto:dimitris@microsoft.com> wrote: Hmm, no I don't think that Flattening is a very serious problem: Firstly, we can somehow get around that if we use implication constraints and higher-order flattening variables. We have discussed that (but not implemented). For example. forall a. F [a] ~ G Int becomes: forall a. fsk a ~ G Int forall a. true => fsk a ~ F [a] Secondly: flattening under a Forall is not terribly important, unless you have type families that dispatch on polymorphic types, which is admittedly a rather rare case. We lose some completeness but that's ok. For me, a more serious problem are polymorphic RHS, which give rise to exactly the same problems for type inference as impredicative polymorphism. For instance: type instance F Int = forall a. a -> [a] g :: F Int g = undefined main = g 3 Should this type check or not? And then all our discussions about impredicativity, explicit type applications etc become relevant again. Thanks! d- If the problem with foralls on the RHS is that it devolves into ImpredicativeTypes, what about only allowing them when ImpredicativeTypes is on? From: Simon Peyton-Jones Sent: Friday, April 05, 2013 8:24 AM To: Manuel M T Chakravarty Cc: Iavor Diatchki; ghc-devs; Dimitrios Vytiniotis Subject: RE: Restrictions on polytypes with type families Manuel has an excellent point. See the Note below in TcCanonical! I have no clue how to deal with this Simon Note [Flattening under a forall] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Under a forall, we (a) MUST apply the inert subsitution (b) MUST NOT flatten type family applications Hence FMSubstOnly. For (a) consider c ~ a, a ~ T (forall b. (b, [c]) If we don't apply the c~a substitution to the second constraint we won't see the occurs-check error. For (b) consider (a ~ forall b. F a b), we don't want to flatten to (a ~ forall b.fsk, F a b ~ fsk) because now the 'b' has escaped its scope. We'd have to flatten to (a ~ forall b. fsk b, forall b. F a b ~ fsk b) and we have not begun to think about how to make that work! From: Manuel M T Chakravarty [mailto:chak@cse.unsw.edu.au] Sent: 04 April 2013 02:01 To: Simon Peyton-Jones Cc: Iavor Diatchki; ghc-devs Subject: Re: Restrictions on polytypes with type families Simon Peyton-Jones mailto:simonpj@microsoft.com>: 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 These kinds of issues are the reason that my conclusion at the time was (as Richard put it) Or, are | there any that are restricted because someone needs to think hard before | lifting it, and no one has yet done that thinking? At the time, there were also problems with what the type equality solver was supposed to do with foralls. 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. The solver changed quite a bit since I rewrote Tom's original prototype. So, maybe it is easy now, but maybe it is more tricky than you think. The idea of rewriting complex terms into equalities at the point of each application of a type synonym family (aka type function) assumes that you can pull subterms out of a term into a separate equality, but how is this going to work if a forall is in the way? E.g., given type family F a :: * the equality Maybe (forall a. F [a]) ~ G b would need to be broken down to x ~ F [a], Maybe (forall a. x) ~ G b but you cannot do that, because you just moved 'a' out of its scope. Maybe you can move the forall out as well? Manuel _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs -- Your ship was destroyed in a monadic eruption. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs