Thanks for summarizing this, Simon! Richard Eisenberg writes:

...

On Oct 6, 2016, at 11:57 AM, Simon Peyton Jones wrote:

1. Currently saturated (->) is treated differently to unsaturated (->), as witnessed by the special kinding rule for FunTy. The shortest path for TypeRep is to do the same: add TrFunTy.

Will this be changed after Ben's work to generalize the kind of (->)?

I suspect not; I think we'll want TrFunTy regardless of the kind of (->). If nothing else it makes common TypeReps a bit more compact.

...

1. Moreover we probably need FunCo for coercions; at the moment it's done with TyConAppCo, but that doesn't work with (->) :: * -> * -> *. Having FunCo would be (a) more efficient for a very common case, (b) deal with the kinding issue.

I've wondered why we haven't had this. But also: will this become unnecessary for use case (b) after Ben's work to generalize the kind of (->)?

There

...

2. splitAppTy_maybe currently will split a FunTy even when it is not used at kind *. This is probably wrong. Maybe it should return Nothing in the non-* case. Ben is trying this out.

Seems reasonable.

Indeed, but as I mentioned on Phabricator it looks like this won't be entirely trivial. I've put this aside for a bit to get the branch building.

...

3. Orthogonally, one could imagine generalising the kind of prefix (->) to (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type LiftedPtrRep Then FunTy would become an abbreviation/optimisation, to avoid a plethora of runtime-rep args. And splitAppTy_maybe could succeed all the time on FunTy. Ben is trying this.

Right. I like this direction of travel.

But it just struck me that

(->) :: forall r1. TYPE r1 -> forall r2. TYPE r2 -> TYPE LiftedPtrRep

might be a touch better, because it's more general. (We don't have deep skolemization at the type level. Yet.)

Seems reasonable.

...

4. Under (3) at what kinds is ((->) ?? LiftedPtrRep (Ord Int) Char) called? If we continue to distinguish * from Constraint, we'd need to instantiate ?? with ConstraintRep, and define type Constraint = TYPE ConstraintRep Orthogonally, one might wonder about combining * and Constraint, but we don't yet know how to do that well.

Urgh. This gives me the willies. The whole point of representation polymorphism is to common up things with the same representation. And here we're specifically taking two things with the same rep -- Type and Constraint -- and separating them. What's wrong with ((->) LiftedPtrRep LiftedPtrRep (Ord Int) Char)? Recall that `eqType Constraint Type` says `True`. It's only `tcEqType` that distinguishes between Constraint and Type.

Indeed this seems to be one of the possible conclusions of #11715. However, I think the point of the approach Simon describes is that we want to handle the Constraint ~ Type issue separately from Typeable (and the variety of other issues that it has dragged in). Introducing another RuntimeRep is merely a way of maintaining the status quo (where Constraint /~ Type) until we want to consider unifying the two. Also, Simon didn't mention another conclusion from our meeting: 5. TrTyCon should somehow carry the TyCon's kind variable instantiations, not the final kind of the type. That is, currently we have, TrTyCon :: TyCon -> TypeRep k -> TypeRep (a :: k) What we want, however, is something closer to, TrTyCon :: TyCon -> [SomeTypeRep] -> TypeRep (a :: k) This carries a complication, however, since typeRepKind needs to somehow reconstruct the kind `k` from the information carried by the TrTyCon. TyCon must carry additional information to make this feasible. The naive approach would be, data TyCon = TyCon { tyConName :: String , tyConKind :: [SomeTypeRep] -> SomeTypeRep } This, however, suffers from the fact that it can no longer be serialized. Consequently we'll need to use something like, type KindBinder = Int data TyConKindRep = TyConKindVar KindBinder | TyConKindApp TyCon [TyConKindRep] data TyCon = TyCon { tyConName :: String , tyConKindRep :: TyConKindRep } tyConKind :: TyCon -> [SomeTypeRep] -> SomeTypeRep Note that for simplicity I kept TyCon un-indexed, meaning that all of the kind-reconstruction logic is in the TCB. However, I suspect this is okay especially since we really need to keep an eye on the effort required by the compiler when generating TyCons. Keep in mind that we generate a TyCon for every datatype we compile; the existing Typeable implementation takes pains to generate efficient, already-optimized TyCon bindings. Moreover, serializing TyCon's will clearly carry a non-trivial cost, which we'll need to advertise to users. Serious users like Cloud Haskell will likely want to maintain some sort of interning table for TypeReps. Cheers, - Ben

On Oct 6, 2016, at 1:15 PM, Ben Gamari wrote:

...

...

1. Currently saturated (->) is treated differently to unsaturated (->), as witnessed by the special kinding rule for FunTy. The shortest path for TypeRep is to do the same: add TrFunTy.

Will this be changed after Ben's work to generalize the kind of (->)?

I suspect not; I think we'll want TrFunTy regardless of the kind of (->). If nothing else it makes common TypeReps a bit more compact.

So this will just be an optimization, then? May be worth thinking about how to measure whether this is actually an improvement. I was also under the impression that TypeReps would carry fingerprints for efficiency.... perhaps this will make TypeReps smaller in memory, but I don't foresee gobs and gobs of TypeReps filling up a lot of memory, so I'm not convinced this compression will be worth its weight. I do agree that we need TrFunTy now (because of the weird kind of (->)), but I'm unconvinced that we need it in the future.

...

...

4. Under (3) at what kinds is ((->) ?? LiftedPtrRep (Ord Int) Char) called? If we continue to distinguish * from Constraint, we'd need to instantiate ?? with ConstraintRep, and define type Constraint = TYPE ConstraintRep Orthogonally, one might wonder about combining * and Constraint, but we don't yet know how to do that well.

Urgh. This gives me the willies. The whole point of representation polymorphism is to common up things with the same representation. And here we're specifically taking two things with the same rep -- Type and Constraint -- and separating them. What's wrong with ((->) LiftedPtrRep LiftedPtrRep (Ord Int) Char)? Recall that `eqType Constraint Type` says `True`. It's only `tcEqType` that distinguishes between Constraint and Type.

Indeed this seems to be one of the possible conclusions of #11715.

However, I think the point of the approach Simon describes is that we want to handle the Constraint ~ Type issue separately from Typeable (and the variety of other issues that it has dragged in). Introducing another RuntimeRep is merely a way of maintaining the status quo (where Constraint /~ Type) until we want to consider unifying the two.

I believe that **right now**, if you say (eqType Constraint Type), you get True. So they're already unified! A problem is that this equality is not universally respected. If you try to splitAppTy Type, you get TYPE and LiftedPtrRep. If you try to splitAppTy Constraint, you fail. Perhaps the short-term thing is just to fix, e.g., splitAppTy.... much like we already special-case FunTy to be splittable, we can special-case Constraint to be splittable. I'm sure that the problem extends past just splitAppTy, but a scan through Type.hs, Kind.hs, and TcType.hs should hopefully show up all the problem sites.

Also, Simon didn't mention another conclusion from our meeting:

5. TrTyCon should somehow carry the TyCon's kind variable instantiations, not the final kind of the type.

Why? Will we want to decompose this? (I suppose we will. But do we have a use-case?) Why not carry both the kind instantiations and the final kind? That seems much simpler than the scheme below.

That is, currently we have,

TrTyCon :: TyCon -> TypeRep k -> TypeRep (a :: k)

What we want, however, is something closer to,

TrTyCon :: TyCon -> [SomeTypeRep] -> TypeRep (a :: k)

To be concrete, I'm proposing TrTyCon :: TyCon -> [SomeTypeRep] -> TypeRep k -> TypeRep (a :: k)

This carries a complication, however, since typeRepKind needs to somehow reconstruct the kind `k` from the information carried by the TrTyCon. TyCon must carry additional information to make this feasible. The naive approach would be,

data TyCon = TyCon { tyConName :: String , tyConKind :: [SomeTypeRep] -> SomeTypeRep }

This, however, suffers from the fact that it can no longer be serialized. Consequently we'll need to use something like,

type KindBinder = Int

data TyConKindRep = TyConKindVar KindBinder | TyConKindApp TyCon [TyConKindRep]

data TyCon = TyCon { tyConName :: String , tyConKindRep :: TyConKindRep }

tyConKind :: TyCon -> [SomeTypeRep] -> SomeTypeRep

I'm afraid this isn't quite sophisticated enough, because kind quantification isn't necessarily prenex anymore. For example: data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type Your TyConKindRep doesn't have any spot for kind quantification, so I'm assuming your plan is just to quantify everything up front... but that won't quite work, I think. Argh. Richard

On Oct 6, 2016, at 5:36 PM, Ben Gamari wrote:

The motivation here isn't that we want to decompose this. It's that carrying the kind variable instantiations will shrink the size of your typical (non-kind-polymorphic) TypeRep and may actually simplify a few things in the implementation. Namely, I suspect that the trouble we currently experience due to recursive kind relationships will vanish.

Ah. This is great motivation.

...

Why not carry both the kind instantiations and the final kind? That seems much simpler than the scheme below.

Admittedly there is a bit of complexity here. I haven't yet tried implementing it but I suspect it's manageable.

On further thought, my idea doesn't simplify any of the TyConKindRep stuff, so I retract my idea.

Oh dear. This will require some thought.

Indeed. It's never easy. :) Richard