Opened 3 years ago

Last modified 17 months ago

#13261 new task

Consider moving Typeable evidence generation wholly back to solver

Reported by: bgamari Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: Typeable Cc: oerjan, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #12276 Differential Rev(s):
Wiki Page:

Description

Since 91c6b1f54aea658b0056caec45655475897f1972 we have generated a set of bindings with each datatype definition which the compiler will refer to when constructing Typeable evidence. As described in the commit message, this came with a rather significant performance penalty, especially given that it is paid regardless of whether the code being compiled uses Typeable.

The type-indexed Typeable implementation (#11011) augments these bindings with additional information allowing the kind of a type of be reconstructing at runtime (#10343). Unfortunately, this further blows up the cost of associated with Typeable binding generation. Some of the testsuite regressions are hard to swallow to say the least.

While I'm still working out what can be done to reduce this cost, I do wonder whether the generating these bindings at the time of type definition is so wise. Relatively few users make use of Typeable and the cost is not negligible. Moreover, generating bindings for families of tycons (e.g. unboxed sums, which have thousands of type constructors and promoted data constructors) all at once produces a truly massive amount of code (albeit it only has to be done once).

On the other hand, I suppose if Richard's dependent types story comes to fruition then perhaps the weight imposed by generating Typeable bindings at type-definition time might pull its weight.

Anyways, just idle reflections.

Change History (10)

comment:1 Changed 3 years ago by simonpj

All we are doing is generating a bunch of records with strings in them. I wonder why that is so expensive?

One possibility is that we could inject them into Core right at the end, perhaps even after CoreTidy. Then they would get code generated but not be put in interface files etc. Runtime perf of typeable code would be a little less (no cross module inlining), but hey we are doing dynamic type tests.

Instead, we'd need distinctive names so that we knew that if we see Data.List.Maybe:tyconName in an interface file unfolding we aren't going to see it in the Data/List/Maybe.hi.

This is a bit like data constructor workers, I think.

Or we could inject them just before CoreTidy so they did appear in .hi files but didn't clog the optimisation pipeline.

comment:2 Changed 3 years ago by goldfire

For the record, I've never been totally convinced by the "generate Typeable stuff at declaration time" approach. As noted above, there is a shared cost. Do we have any program that shows a concrete speed boost by the new design? Yes, the new design seems like Typeable-heavy code would run faster, but it would be lovely to verify this fact and be able to quantify it.

Once there are dependent types, this issue does not really change. Yes, users could effectively use Typeable without writing the word Typeable in their programs, but they would still need to use runtime type tests to trigger any of this machinery. So I would consider this orthogonal.

comment:3 Changed 3 years ago by simonpj

I have no fixed objection to doing it on the fly. But then we'd probably want some way to avoid repeatedly generating the same stuff, some kind of on-the-fly CSE....

comment:4 Changed 3 years ago by nomeata

Can we do it like specializations: Create on the fly the first time we need them, but use an existing one if any dependency already created them? (Maybe this is what Simon means by on-the-fly CSE).

comment:5 Changed 3 years ago by bgamari

The unboxed sum problem is discussed in #13276.

comment:6 Changed 3 years ago by Ben Gamari <ben@…>

In 8fa4bf9a/ghc:

Type-indexed Typeable

This at long last realizes the ideas for type-indexed Typeable discussed in A
Reflection on Types (#11011). The general sketch of the project is described on
the Wiki (Typeable/BenGamari). The general idea is that we are adding a type
index to `TypeRep`,

    data TypeRep (a :: k)

This index allows the typechecker to reason about the type represented by the `TypeRep`.
This index representation mechanism is exposed as `Type.Reflection`, which also provides
a number of patterns for inspecting `TypeRep`s,

```lang=haskell
pattern TRFun :: forall k (fun :: k). ()
              => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                        (arg :: TYPE r1) (res :: TYPE r2).
                 (k ~ Type, fun ~~ (arg -> res))
              => TypeRep arg
              -> TypeRep res
              -> TypeRep fun

pattern TRApp :: forall k2 (t :: k2). ()
              => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
              => TypeRep a -> TypeRep b -> TypeRep t

-- | Pattern match on a type constructor.
pattern TRCon :: forall k (a :: k). TyCon -> TypeRep a

-- | Pattern match on a type constructor including its instantiated kind
-- variables.
pattern TRCon' :: forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
```

In addition, we give the user access to the kind of a `TypeRep` (#10343),

    typeRepKind :: TypeRep (a :: k) -> TypeRep k

Moreover, all of this plays nicely with 8.2's levity polymorphism, including the
newly levity polymorphic (->) type constructor.

Library changes
---------------

The primary change here is the introduction of a Type.Reflection module to base.
This module provides access to the new type-indexed TypeRep introduced in this
patch. We also continue to provide the unindexed Data.Typeable interface, which
is simply a type synonym for the existentially quantified SomeTypeRep,

    data SomeTypeRep where SomeTypeRep :: TypeRep a -> SomeTypeRep

Naturally, this change also touched Data.Dynamic, which can now export the
Dynamic data constructor. Moreover, I removed a blanket reexport of
Data.Typeable from Data.Dynamic (which itself doesn't even import Data.Typeable
now).

We also add a kind heterogeneous type equality type, (:~~:), to
Data.Type.Equality.

Implementation
--------------

The implementation strategy is described in Note [Grand plan for Typeable] in
TcTypeable. None of it was difficult, but it did exercise a number of parts of
the new levity polymorphism story which had not yet been exercised, which took
some sorting out.

The rough idea is that we augment the TyCon produced for each type constructor
with information about the constructor's kind (which we call a KindRep). This
allows us to reconstruct the monomorphic result kind of an particular
instantiation of a type constructor given its kind arguments.

Unfortunately all of this takes a fair amount of work to generate and send
through the compilation pipeline. In particular, the KindReps can unfortunately
get quite large. Moreover, the simplifier will float out various pieces of them,
resulting in numerous top-level bindings. Consequently we mark the KindRep
bindings as noinline, ensuring that the float-outs don't make it into the
interface file. This is important since there is generally little benefit to
inlining KindReps and they would otherwise strongly affect compiler performance.

Performance
-----------

Initially I was hoping to also clear up the remaining holes in Typeable's
coverage by adding support for both unboxed tuples (#12409) and unboxed sums
(#13276). While the former was fairly straightforward, the latter ended up being
quite difficult: while the implementation can support them easily, enabling this
support causes thousands of Typeable bindings to be emitted to the GHC.Types as
each arity-N sum tycon brings with it N promoted datacons, each of which has a
KindRep whose size which itself scales with N. Doing this was simply too
expensive to be practical; consequently I've disabled support for the time
being.

Even after disabling sums this change regresses compiler performance far more
than I would like. In particular there are several testcases in the testsuite
which consist mostly of types which regress by over 30% in compiler allocations.
These include (considering the "bytes allocated" metric),

 * T1969:  +10%
 * T10858: +23%
 * T3294:  +19%
 * T5631:  +41%
 * T6048:  +23%
 * T9675:  +20%
 * T9872a: +5.2%
 * T9872d: +12%
 * T9233:  +10%
 * T10370: +34%
 * T12425: +30%
 * T12234: +16%
 * 13035:  +17%
 * T4029:  +6.1%

I've spent quite some time chasing down the source of this regression and while
I was able to make som improvements, I think this approach of generating
Typeable bindings at time of type definition is doomed to give us unnecessarily
large compile-time overhead.

In the future I think we should consider moving some of all of the Typeable
binding generation logic back to the solver (where it was prior to
91c6b1f54aea658b0056caec45655475897f1972). I've opened #13261 documenting this
proposal.

comment:7 Changed 3 years ago by Ben Gamari <ben@…>

In 42ff5d97/ghc:

Disable Typeable binding generation for unboxed sums

These things are simply too expensive to generate at the moment. More
work is needed here; see #13276 and #13261.

comment:8 Changed 3 years ago by oerjan

Cc: oerjan added

comment:9 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:10 Changed 17 months ago by RyanGlScott

Keywords: Typeable added
Note: See TracTickets for help on using tickets.