Restrictions on polytypes with type families
Simon Peyton-Jones
simonpj at microsoft.com
Tue Nov 12 22:14:18 UTC 2013
Me neither.
Simon
From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Richard Eisenberg
Sent: 12 November 2013 16:15
To: Nicolas Frisby
Cc: Manuel Chakravarty; ghc-devs at 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 <dimitris at microsoft.com<mailto: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]
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<mailto: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<mailto: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<mailto:ghc-devs at haskell.org>
http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto: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/20131112/5e05520b/attachment-0001.html>
More information about the ghc-devs
mailing list