Typeable meeting

Thu Oct 6 16:15:36 UTC 2016

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

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

> 
> 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.

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

> 
> 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.

Richard

> 
> | -----Original Message-----
> | From: Richard Eisenberg [mailto:rae at cs.brynmawr.edu]
> | Sent: 06 October 2016 15:08
> | To: Ben Gamari <ben at smart-cactus.org>
> | Cc: Simon Peyton Jones <simonpj at microsoft.com>
> | Subject: Re: Typeable meeting
> | 
> | Just seeing this now. (Please use my new address: rae at cs.brynmawr.edu). I
> | wasn't available yesterday at that time, anyway.
> | 
> | Any conclusions reached?
> | 
> | > On Oct 4, 2016, at 5:39 PM, Ben Gamari <ben at smart-cactus.org> wrote:
> | >
> | > Simon Peyton Jones <simonpj at microsoft.com> writes:
> | >
> | >> Ben, and copying Richard who is far better equipped to respond than
> | me.
> | >>
> | >> I'm way behind the curve here.
> | >>
> | >> If "this is precisely what mkFunCo does" why not use mkFunCo? Why do
> | >> you want to "generalise the arrow operation"?
> | >>
> | > Perhaps I should have said "this is what mkFunCo is supposed to do".
> | > However, mkFunCo needs to be adjusted under the generalized (->)
> | > scheme, since the (->) tycon will gain two additional type arguments
> | > (corresponding to the RuntimeReps of the argument and result types).
> | > mkFunCo needs to fill these type arguments when constructing its
> | result.
> | >
> | >> I'm lost as to your goal and the reason why you need to wade through
> | this particular swamp.
> | >>
> | > There are a few reasons,
> | >
> | > * We want to provide a pattern to match against function types
> | >
> | >     pattern TrFun :: TypeRep arg -> TypeRep res -> TypeRep (arg ->
> | > res)
> | >
> | > * T11120 currently fails on my branch as it contains a TypeRep of a
> | >   promoted type containing an unboxed type. Namely,
> | >
> | >       import Data.Typeable
> | >       data CharHash = CharHash Char#
> | >       main = print $ typeRep (Proxy :: Proxy 'CharHash)
> | >
> | >   Note how 'CharHash has kind Char# -> Type. This kind occurs in one of
> | >   the terms in `typeRep` needed in the above program, which currently
> | >   results in core lint failures due to the restrictive kind of (->).
> | >   For this reason (->) needs to be polymorphic over runtime
> | >   representation.
> | >
> | >   This issue is mentioned in ticket:11714#comment:1.
> | >
> | > * I believe there were a few other testcases that failed in similar
> | >   ways to T11120.
> | >
> | > For what it's worth, the Type /~ Constraint issue that I'm currently
> | > fighting with in carrying out the (->) generalization is also the
> | > cause of another Typeable bug, #11715, so I think this is a worthwhile
> | > thing to sort out.
> | >
> | >> Also your text kind of stops... and then repeats itself.
> | >>
> | > Oh dear, I apologize for that. Clipboard malfunction. I've included a
> | > clean version below for reference.
> | >
> | >> We could talk at 2pm UK time tomorrow Weds.  Richard would you be
> | free?
> | >>
> | > That would work for me.
> | >
> | > Cheers,
> | >
> | > - Ben
> | >
> | >
> | >
> | >
> | > # Background
> | >
> | > Consider what happens when we have the coercions,
> | >
> | >    co1 :: (a ~ b)
> | >    co2 :: (x ~ y)
> | >
> | > where
> | >
> | >    a :: TYPE ra          b :: TYPE rb
> | >    x :: TYPE rx          y :: TYPE ry
> | >
> | > and we want to construct,
> | >
> | >    co :: (a -> x) ~ (b -> y)
> | >
> | > As I understand it this is precisely what Coercion.mkFunCo does.
> | > Specifically, co should be a TyConAppCo of (->) applied to co1, co2,
> | > and coercions showing the equalities ra~rx and rb~ry,
> | >
> | >    (->) (co_ax :: ra ~ rx) (co_by :: rb ~ ry) co1 co2
> | >
> | > Actually implementing mkFunCo to this specification seems to be not
> | > too difficult,
> | >
> | >    -- | Build a function 'Coercion' from two other 'Coercion's. That
> | is,
> | >    -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x)
> | > ~ (b -> y)@.
> | >    mkFunCo :: Role -> Coercion -> Coercion -> Coercion
> | >    mkFunCo r co1 co2 =
> | >        mkTyConAppCo r funTyCon
> | >        [ mkRuntimeRepCo r co1 -- ra ~ rx where a :: TYPE ra, x :: TYPE
> | > rx
> | >        , mkRuntimeRepCo r co2 -- rb ~ ry where b :: TYPE rb, y :: TYPE
> | > ry
> | >        , co1                  -- a ~ x
> | >        , co2                  -- b ~ y
> | >        ]
> | >
> | >    -- | For a constraint @co :: (a :: TYPE rep1) ~ (b :: TYPE rep2)@
> | > produce
> | >    -- @co' :: rep1 ~ rep2 at .
> | >    mkRuntimeRepCo :: Role -> Coercion -> Coercion
> | >    mkRuntimeRepCo r co = mkNthCoRole r 0 $ mkKindCo co
> | >      | Just (tycon, [co]) <- splitTyConAppCo_maybe $ mkKindCo co
> | >      = co
> | >      | otherwise
> | >      = pprPanic "mkRuntimeRepCo: Non-TYPE" (ppr co)
> | >
> | > So far, so good (hopefully).
> | >
> | > # The Problem
> | >
> | > Consider what happens when one of the types is, e.g., HasCallStack.
> | > For the sake of argument let's say
> | >
> | >    co1 = <HasCallStack>_R
> | >    co2 = <Int>_R
> | >
> | > Recall that HasCallStack is,
> | >
> | >    type HasCallStack = ((?callStack :: CallStack) :: Constraint)
> | >
> | > The problem arises when we attempt to evaluate
> | >
> | >    mkFunCo r co1 co2
> | >
> | > which will look at the kind coercion of co1,
> | >
> | >    mkKindCo co1  ===  <Constraint>_R
> | >
> | > and then attempt to splitTyConAppCo it, under the assumption that the
> | > kind coercion is an application of TYPE, from which we can extract the
> | > RuntimeRep coercion. Instead we find a nullary TyConAppCo of
> | > Constraint; things then blow up.
> | >
> | > This is the problem.
> | >
> | > Ultimately it seems all of this is due to the fact that we play it
> | > fast- and-loose with Type and Constraint in Core (#11715), especially
> | > with implicit parameters. I worry that resolving this is more than I
> | > have time to chew on before 8.2.
> 