GHC syntax proposal: Guarded Instances

In GHC ticket #5590, I proposed some new syntactic sugar with an elaborative semantics. The objective is to make it easier to use type families for instance selection.

SPJ commented:

I’m afraid I do not understand the proposal in this ticket, yet anyway; an example or two doesn’t tell me its syntax, static semantics, internal language, or dynamic semantics.

I’m writing this post to emphasize that my proposal is technically just a new syntax with an elaboration semantics. I’ll still start with another example, but it’s a better one than I used in the ticket description. I’ll close with a more formal take on the proposed syntax and its elaboration semantics.

There are plenty of simpler examples of this technique, but I’m sharing an example here that

  1. uses rather familiar notions,
  2. I find compelling, and
  3. demonstrates the idea both for a class and for a type family.

In combination with total type families (possibly implemented via NewAxioms), this sugar could succinctly supplant much of the functionality of OverlappingInstances — stare deep into the Oleg.

Motivating Example

(Full code on hpaste.)

Consider writing a Functor instance for the * -> * composition type, :.:.

newtype (:.:) (f :: * -> *) (g :: * -> *) = Comp {unComp :: f (g a)}

The wrinkle with writing a Functor instance for :.: is that there are two equally valid implementations, but they are syntactically ambiguous. Because they have identical instance heads, GHC won’t allow both of them. Conal Elliott laments this problem in the type-compose package.

class Contra f where contramap :: (a -> b) -> f b -> f a

instance (Functor f, Functor g) => Functor (f :.: g) where
  fmap f = Comp . fmap (fmap f) . unComp

instance (Contra f, Contra g) => Functor (f :.: g) where
  fmap f = Comp . contramap (contramap f) . unComp

Solution with current GHC syntax

Here’s a solution to this wrinkle that I consider to be the most direct. My basic proposal in #5590 merely eliminates the syntactic overhead of this workaround — it involves no new semantics or expressivity.

The two Functor instances are distinguished semantically based on the variance of f (or of g — it seems to be a stylistic choice). This semantic information is not present in the instance head, so GHC cannot distinguish the instances. The distinction is present in the constraints, but GHC ignores those during instance selection.

The idea of using the instance contexts to differentiate instances raises even more issues, because of the various extensions to instances like Overlapping or Incoherent. Type families, on the other hand, do not raise such issues because their instances are more restricted than are class instances. So we turn to type families.

We encode variance, the property we wish to use to distinguish our two Functor instances, as a type family. We’ll keep it simple for now and consider only co- and contra-variant parametric data types.

{-# LANGUAGE DataKinds, PolyKinds #-} -- etc.

data V = CoV | ContraV -- datakind for variance; see footnote [1]

data PROXY a = PROXY -- polykinded proxy, for passing types explicitly

-- polykinded variance w.r.t. the next argument of t
type family Variance (t :: kD -> kR) :: V

type instance Variance [] = CoV
type instance Variance Maybe = CoV
type instance Variance (->) = ContraV
type instance Variance ((->) a) = CoV -- etc.

We’ll need an example contravariant type of kind * -> *.

newtype IntSink a = IntSink (a -> Int)

type instance Variance IntSink = ContraV
instance Contra IntSink where
  contramap f (IntSink x) = IntSink (x . f)

This is the type for which we need that second Functor instance, the one that uses Contra. For example, our goal is to make the test function below well-typed.

ex :: (IntSink :.: IntSink) String
ex = Comp $ IntSink $ \(IntSink sink) -> sink "payload"

test :: (IntSink :.: IntSink) Int
test = fmap length ex

The well-typedness of test requires the instance Functor (IntSink :.: IntSink).

All of the code up to this point is motivation for the example; we’re just now getting into the bits relevant to #5590.

Using the Variance type family, we declare an auxiliary class that accommodates our two instances with distinct instance heads.

class Functor_V f (v :: V) where
  fmap_V :: PROXY v -> (a -> b) -> f a -> f b

instance (Functor f, Functor g) => Functor_V (f :.: g) CoV where
  fmap_V _ f = Comp . fmap (fmap f) . unComp

instance (Contra f, Contra g) => Functor_V (f :.: g) ContraV where
  fmap_V _ f = Comp . contramap (contramap f) . unComp

Note that Functor_V is totally determined by Functor and our choice to branch based on Variance. The method bodies are thus just transliterations of our intended Functor instances. We include the additional PROXY argument so that the method’s type determines all of the class parameters.

Finally, we declare the instance of Functor for :.: by delegating to the auxiliary class Functor_V.

{-# LANGUAGE ScopedTypeVariables #-}

instance (fvar ~ Variance f, Functor_V f g fvar) =>
  Functor (f :.: g) where
  fmap = fmap_V (PROXY :: PROXY fvar)

Problem solved; our objective function test now type-checks as-is.

Not just for classes

Left-nestings of :.: will require an instance of Variance for :.:. We can use the same approach for the instance of Variance for :.: that we used for its Functor instance: use an auxiliary family indexed by V.

type instance Variance (f :.: g) = Variance_V (f :.: g) (Variance f)

type family Variance_V (a :: kD -> kR) (v :: V) :: V
type instance Variance_V (f :.: g) CoV = Variance g
type instance Variance_V (f :.: g) ContraV = NegateV (Variance g)

type family NegateV (v :: V) :: V
type instance NegateV CoV = ContraV
type instance NegateV ContraV = CoV

Both Variance_V and Functor_V just get an additional parameter. And both Variance (f :.: g) and Functor (f :.: g) instances just delegate to the *_V counterpart by passing in the appropriate V argument. These are two instantiations of the general technique:

Delegate to an auxiliary class/family that dispatches based on the result of a relevant type family.

My proposal in #5590 is syntactic sugar for that technique.

Solution with the proposed syntax

In the new syntax, we would write the following instead of the Functor_V class, its instances, and the delegating Functor instance for :.:.

guarded instance Functor (f :.: g) with (Variance f)

instance (Functor f, Functor g) => Functor (f :.: g) with CoV where
  fmap f = Comp . fmap (fmap f) . unComp

instance (Contra f, Contra g) => Functor (f :.: g) with ContraV where
  fmap f = Comp . contramap (contramap f) . unComp

It’s much the same for type instances; the following replaces the Variance_V class and its instances as well as the Variance instance for :.:.

type guarded instance Variance (f :.: g) with (Variance f)

type instance Variance (f :.: g) with CoV = Variance g
type instance Variance (f :.: g) with ContraV = NegateV (Variance g)

There are three major benefits of this syntax.

  1. The user isn’t required to invent names for the auxiliary class/family and duplicate the methods’ signatures.
  2. Instance selection is still straight-forward: a guarded instance just forces a bit of type computation and then proceeds with an extra type parameter.
  3. Everything remains open. In our example, the kind of the with parameter is closed since it’s a datakind. If it instead involved *, new with-instances could be declared as usual.

The New Syntax

My proposal enriches the notion of instance head (involving the new keyword with) and adds a new declaration form (involving the new keyword guarded).

In this rest of this post, I only discuss guarded instances of classes. Guarded instance of families are always simpler.

The definition of instance head is enriched to allow zero or more with-clauses on the end. A with-clause is the keyword with follow by one or more type expressions, which are separated syntactically in the same way as the parameters of a multi-parameter type class. These type expressions are called with arguments. Each occurrence of with in an instance head associates to the left; the left argument of a with-clause is called its source. For example, (a, b) with E1 with E2 is a with-clause E2 and its source (a, b) with E1. As a result of enriching instance heads, all instance declarations can now include zero or more with-clauses at the end of their head.

Each guarded instance has the syntactic form
guarded instance Θ => H with T0 T1 … Tn.

n must be positive. Θ is an instance context, H is the head of the guarded instance (and possibly includes further with-clauses), and each Ti is a type expression. All type variables occurring in those Tis must be bound by H or Θ.

Well-formedness

Any instance (guarded or vanilla) with a with-clause in its head has a head of the shape H with Ω. For this instance head to be well-formed, there must be a guarded instance in scope of the shape Hg with Ωg where H is an instance of Hg with the substitution σ and Ω is of the same kind as the application of σ to Ωg.

Elaboration semantics

Every guarded instance guarded instance Θ => H with Ω elaborates to two conventional declarations. Let C be H's class. The first generated declaration is an auxiliary class C' that is a fresh copy of C with a new parameter for each type in Ω (added after the existing parameters) and a new PROXY argument in every method for each new class parameter. The second generated declaration is an instance of C with context (Θ, H[C'/C] Ω) that defines each method by applying the corresponding method of C' to the appropriately typed proxy arguments.

Every instance with a head that includes with-clauses Θ => H with Ω elaborates to a single conventional instance (Θ, Θg') => H[C'/C] Ω, where C' and Θg are determined by the corresponding guarded instance for H.

Using polykinds, the elaborator could more efficiently re-use class copies that require the same number of additional parameters.

Conclusion

I’m confident this discussion is better than my original ticket, but it still seems to make it overly complicated. I’m only proposing a little sugar for the underlying technique that uses type families to encode richer instance selection. On the other hand, that technique isn’t even well-known or particularly simple. What can I say? It has worked pretty well for me, and I’d like to be able to use it with less syntactic overhead. YMMV.

Thanks for reading along! Please let me know what you think.


[1] — While I’ve kept the definition of V minimal for this example, it should in general be at least a complete lattice with four elements, co-, contra-, in-, and non-variance. Invariance is both co- and contra-, like a -> a; non-variance is neither co- nor contra-. NB even this lattice is insufficient for some higher-order data types, like data X a f = X (f a), where the variance w.r.t. one parameter depends on the variance of a later parameter. I’m not sure how Variance interacts with non-parametric types (= indexed? or >= indexed?).

About these ads

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s