Re: Typeable meeting

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