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 <[email protected]>
> 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:[email protected]]
> 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 <[email protected]>:
>
> 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
> [email protected]
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
>
>
> --
> Your ship was destroyed in a monadic eruption.
> _______________________________________________
> ghc-devs mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
> _______________________________________________
> ghc-devs mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
