Typeable meeting

[Ben Gamari]

Richard Eisenberg <rae at cs.brynmawr.edu> writes:

>> On Oct 6, 2016, at 1:15 PM, Ben Gamari <ben at smart-cactus.org> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 454 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161006/07eb97d4/attachment.sig>