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 <dimit...@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:c...@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 <simo...@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.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 > > _______________________________________________ > ghc-devs mailing list > 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