Typeable meeting

[Ben Gamari]

Thanks for summarizing this, Simon!


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

>> On Oct 6, 2016, at 11:57 AM, Simon Peyton Jones <simonpj at microsoft.com> 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
-------------- 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/a255a921/attachment.sig>