Typeable meeting

[Simon Peyton Jones]

Richard

Ben and I concluded

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.

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.

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.

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.

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.

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