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