GitLab

#20897 wonders about representing all dictionaries as data types.

Motivated by thoughts about -fdicts-strict, I want to go a step further and wonder: Can we represent all dictionaries as unlifted data types? That is, are there useful Haskell programs in which construction of a class dictionary may diverge? I suppose there is -XUndecidableInstances, but due to the global nature of dictionaries I think that if a dictionary diverges at definition site (where it would be forced if unlifted) it also has to diverge at use sites (where it needs to be forced even in the lifted scenario).

Note that I'm not advocating for representing the methods of dictionaries in some unlifted way, because that indeed would change runtime semantics.

Of course, it's not as simple. Here's a list of challenges:

1. Today, we have type Constraint = Type. For this ticket, we'd need type Constraint = UnliftedType. But then equality constraints would be unlifted, too and suddenly with GADTs we live in a very different language. I think this is already a nail in the coffin of this idea... Still, an interesting thought experiment.

   Alternatively, for a more complicated design without the GADT weakness, we could make equality constraints and dictionaries live in different kinds and provide levity polymorphic constraint tuple constructors. No idea if that is even feasible.

   The issue of levity in Constraint is a bit frustrating, because embedding an unlifted dictionary into a lifted field of a constraint tuple is a no-op as far dynamic semantics is concerned. We could even freely coerce from unlifted to lifted rep, so technically a lifted Constraint can simply embed an unlifted dictionary.

2. We'd need top-level unlifted bindings, #17521.