Class Equalities

An interesting extension to the associated types are equality constraints in the superclass context of type classes, which can also mention ATs defined in that same class. An interesting feature of this extension is that it enables to translate any FD program (that obeys the weak coverage condition) into an AT program. For example,

class C a b c | a b -> c, a c -> b

becomes

class (F1 a b = c, F2 a c = b) => C a b c where
  type F1 a b = c
  type F2 a c = b

NB: We are also using ATs with only a subset of the parameters of the class - a feature mentioned in Section 4.4 of the POPL AT paper.

TODO:

• Given the various classes of FD definitions identified by Sulzmann et al. in the Understanding FDs by CHRs paper, what do these classes map to under our translation and what are properties of the translated FD definitions. Do they behave the same as their FD counterparts?

• Implement in PHRaC?

The Extension

A superclass context can have equality constraints of the form S a1 .. an = b, where the ai and b are variables. (Could we also allow non-variable arguments and right-hand sides?)

Typing rules

As usual, a class head of the form

class <c-ctxt> => C a_1 .. a_n

where <c-ctxt> === (\pi_1, .., \pi_m), puts

forall a_1 .. a_n. C a_1 .. a_n => \pi_j   , 1 <= j <= m    (*)

into \Theta.

Now, given an instance

instance <i-ctxt> => C t_1 .. t_n where
  type S_1 t_1 .. t_n = s_1
  ..
  type S_m t_1 .. t_m = s_m
  ..

If S_i b_1 .. b_n = c occurs in <c-ctxt>, then the usual superclass rules for instances imply that we must have

  [t_1/a_1, .., t_n/a_n] (S_i b_1 .. b_n = c)  ===  S_i t_1 .. t_n = s_i

In other words, the form of the type definitions is restricted to those consistent with the class equalities.

The crucial novelty is that the implications introduced by (*) can fire whenever we try to derive a matching entailment judegment \Theta ||- t1 = t2; the existing entailment rules are already sufficient to use these implications.

The use of default type definitions

Due to the superclass rules for instances, it is convenient to use default type definitions in conjunction with class equalities. For example, given

class (S a b = b) => C a b where
  type S a b

the definition for S in an instance with head

instance C t1 t2

is restricted to be S t1 t2 = t2. By using a default type definition, we can avoid writing all the pre-determined type definitions; thusly,

class (S a b = b) => C a b where
  type S a b = b
instance C t1 t2

Inference

Somewhat surprisingly, it seems as if the existing inference algorithm is already sufficient to deal with class equalities, except that we have to generalise constraint entailment (Figure 6 in the Associated Type Synonyms paper) a little: in addition to Rule (eq_E), we need a rule that checks whether \Theta entails the equality via a (*) implication. What will happen is that we come across a match Si t1 .. tn = s that we can't solve, it is put into \Theta, and hence, may end up in a signature context (or the toplevel type). During context simplification, the corresponding implication from (*) will be invoked during checking constraint entailment and it will eliminate the constraint from the context.

NB: It should also be correct to extend Rule (syn_R) from unification, but that might make unification rather costly.

Translating Functional Dependencies

We generally have that an FD of the form as -> b c is equivalent to as -> b, as -> c. Hence, WLOG, we can assume a class declaration with FDs to have the following form:

class <c-ctxt> => C a_1 .. a_n | as_t -> a_t, .., as_n -> a_n where
  f_1 :: sig_1
  ..
  f_r :: sig_r

where 1 <= t <= m <= n and the asi are sequences of non-empty subsets of a1 .. a_(m-1). The intuition is that we distinguish three types of class parameters: (1) in, (2) out, and (3) inout. In-parameters occur only on the left-hand side of an FD arrow, out-parameters occur only on the right-hand side, and inout-parameter occur on both. So, the variables a1 .. a_(t-1) are in-parameters, the at .. a_(m-1) are inout-parameters, and the a_m .. a_n are out-parameters.

We need an AT for every inout- and out-parameter, but only the in- and inout-parameter remain as class (and AT) parameter, thus

class (<c-ctxt>, S_t as_t = a_t, .., S_(m-1) as_(m-1) = a_(m-1)) => C a_1 .. a_(m-1) where
  type S_t     as_t     = a_t
  ..
  type S_(m-1) as_(m-1) = a_(m-1)
  type S_m     as_m
  ..
  type S_n     as_n
  f_1 :: Ctheta sig_1
  ..
  f_r :: Ctheta sig_r

where Ctheta = [(S_m as_m)/a_m, .., (S_n as_n)/a_n] is a class substitution that we need to rewrite signatures mentioning the class C, including the method signatures. In other words, (1) the out-parameters are dropped from the list of class parameters and turned into unconstrained associated types; (2) the in-parameters have no associated type definition, but are also unconstrained; and (3) the inout-parameters turn into ATs constrained by class equalities, and hence, fully determined by default definitions.

FIXME: We could also add the a_t .. a_(m-1) to the class substitution. Would that make any difference?

When we encounter an instance declaration

instance <i-ctxt> => C t_1 .. t_n where
  f_1 = e_1
  ..
  f_r = e_r

we rewrite it to

instance <i-ctxt> => C t_1 .. t_(m-1) where
  type S_m (theta at_m) = t_m
  ..
  type S_n (theta at_n) = t_n
  f_1 = e_1
  ..
  f_r = e_r

where theta = [t_1/a_n, .., t_(m-1)/a_(m-1)]. The instance declaration will be well-formed if the FD instance meets the weak coverage condition. Moreover, given two non-overlapping and non-conflicting FD instances, the corresponding AT instances will be non-overlapping.

Observations:

• FD type inference uses improvement in two ways (cf. Jones' ESOP paper, Section 6.2): (1) if the in-parameters of a functional dependency of a class C coincide in two predicates C t1 and C t2, then the out-parameter of the FD must be the same, too; and (2) if the in-parameters of an FD of class C match a C instance, then the out-parameter must match under the same substitution.

• The first kind of improvement is trivial with ATs, as we have S ts = S ts for any application of an associated type S. For the class parameters identified as inout during converting an FD class declaration to an AT class declaration, the class parameters are instantiated by applications of associated types due to the class equalities.

• The second kind of improvement corresponds to the reduction of AT applications by Rule (syn_R) in Figure 4 of the ICFP AT paper.

• If an FD class declaration does not have any inout-parameters, class equalities are not needed at all. This seems to be the case for the majority of FD class declarations in actual use.

Incomplete lists of AT parameters

Section 4.4 of the POPL AT paper mentions the option of not using all class parameters for associated type definitions. At the point of writing this paper, we didn't have any use for such declarations and hence omitted them. For an accurate translation of FDs, this feature seems however to be necessary.

When an AT declaration has less parameters than its class, the definition of this AT can be overlapping for two instances where the actuall class declaration is not overlapping. Hence, the test for overlapping instances needs to be refinded such that it explicitly checks that all corresponding AT definitions are non-overlapping. (This corresponds to a similar test for FD classes.)