Restrictions on polytypes with type families
Nicolas Frisby
nicolas.frisby at gmail.com
Mon Nov 11 19:47:12 UTC 2013
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 <dimitris at 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 at cse.unsw.edu.au<chak at 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 <simonpj at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
--
Your ship was destroyed in a monadic eruption.
_______________________________________________
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/20131111/4db54f78/attachment-0001.html>
More information about the ghc-devs
mailing list