Opened 14 months ago

Last modified 13 months ago

#15493 new feature request

Elide empty dictionaries

Reported by: mnoonan Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by mnoonan)

Suppose you define a type class C with no methods, and use it as a constraint on a function f :: C => Foo. GHC's generated Core for f currently passes an empty dictionary for C. With optimizations, it seems to be true that at use sites, calls to f will be replaced with calls to an inner function that skips the typeclass dictionary. But can I count on this optimization always working?

Would it possible to get a guarantee that the C => constraint will have no run-time overhead, by dropping it entirely from the generated Core? Or is there a subtlety that prevents this from being sound?

For context, I would like to implicitly pass compile-time evidence that various properties hold (e.g. such-and-such a list is non-empty), while retaining a guarantee that the evidence will have no run-time cost. Like this:

newtype Named a name = Named a

class Fact p

-- Ideally, we'd have a guarantee that the following function
--   compiles to exactly the same code as `Prelude.head`
head :: Fact (IsCons xs) => ([a] `Named` xs) -> a
head xs = Prelude.head (coerce xs)

Change History (4)

comment:1 Changed 14 months ago by mnoonan

Description: modified (diff)

comment:2 Changed 14 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 14 months ago by Iceland_jack

See discussion in goldfire's "Constrained Type Families", subsection 7.3 Runtime Efficiency

Constrained type families may also seem to have a non-trivial efficiency impact. For a simple example, suppose we have a type family F, and consider an existentially-packaged type family application:

data FPack a where
  FPack :: F a -> FPack a

We might expect an FPack a value to contain exactly a value of type F a. With constrained type families, however, the declaration above would be incorrect; we would need to add a predicate for its constraining class, say C:

data FPack1 a where
  FPack1 :: C a => F a -> FPack1 a

Now, a value of type FPack1 a does not just contain an F a value, but must also carry a C a dictionary, and uses of FPack1 will be responsible for constructing, packing, and unpacking these dictionaries. Over sufficiently many uses of FPack1, this additional cost could be noticeable.

This efficiency impact can be mitigated, however. This issue can crop up only when we have a value of type F a (or other type family application) without an instance of the associated class C a. But in order for the value of type F a to be useful, parametricity tells us that C a, or some other class with a similar structure to the equations for F a must be in scope. Barring this, it must be that F a is used as a phantom type. In this case, we would want a “phantom dictionary” for C a, closely paralleling existing work on proof irrelevance in the dependently-typed programming community (..): the C a dictionary essentially represents a proof that will never be examined. While we do not propose here a new solution to this problem, we believe that existing work will be applicable in our case as well.

comment:4 Changed 13 months ago by simonpj

In Core, an empty dictionary turns into a dead variable, which is optimised away (with -O anyway).

But it'll still take up a field in FPack1. Reason: it might be bottom.

I'd be surprised if you found any appreciable performance impact.

Note: See TracTickets for help on using tickets.