Re: Typeable meeting

Richard Eisenberg writes:

...

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.

Perhaps; I seem to recall examining the effect of the reintroduction of FunTy in GHC to find that I was rather disappointed in the difference.

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.

Indeed we'll need to measure.

...

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.

The situation currently seems to be quite messy. I brought up all of this because this (in the context of coercions, as I discussed in one of our emails, Richard) was the most significant barrier I ran into while looking that the (->) generalization.

...

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?)

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. Relatedly, the fact that you no longer need to worry about recursive kind relationships simplifies serialization, as well as makes the serialized representation more compact. You would lose this benefit if you carried the result kind (either exclusively or in conjunction with the instantiations).

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.

...

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)

Right. Understood. This means that consumers that deeply traverse TypeReps (e.g. serializers) still need to worry about no traversing the kinds of certain types (e.g. Type).

...

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.

Oh dear. This will require some thought. Thanks! Cheers, - Ben