Why Judgmental Equality Fails Under Defunctionalization

Table Of Links

ABSTRACT

1 INTRODUCTION

2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING

3 CASE STUDY

4 DESIGN CONSTRAINTS AND SOLUTIONS

5 FORMALIZATION

6 DE/REFUNCTIONALIZATION

7 FUTURE WORK

8 RELATED WORK

9 CONCLUSION AND REFERENCES

DESIGN CONSTRAINTS AND SOLUTIONS

Specifying a consistent set of typing and computation rules for data and codata types is not difficult. In this section, we show the difficulties that arise if we also want the rules to be closed under defunctionalization and refunctionalization. That is every program that typechecks should continue to typecheck if we defunctionalize or refunctionalize any of the types that occur in it.

4.1 Judgmental Equality of Comatches

Problem. For most dependently typed languages, the term 𝜆𝑥.𝑥 is judgmentally equal to the term 𝜆𝑦.𝑦, and likewise 𝜆𝑥.2 + 2 and 𝜆𝑥.4 are considered equal. Equating such terms becomes a problem, however, if we want to defunctionalize the programs which contain them. Different lambda abstractions in a program are defunctionalized to different constructors, which are then no longer judgmentally equal. Let us illustrate the problem with an example.

Consider the following proof that 𝜆𝑦.𝑦 is the same function from natural numbers to natural numbers as 𝜆𝑧.𝑧. We prove this fact using a third lambda abstraction 𝜆𝑥.𝑥 as an argument to the reflexivity constructor.

codata Fun(a b: Type) { Fun(a, b).ap(a b: Type, x: a): b } Refl(Fun(Nat, Nat), \x. x) : Eq(Fun(Nat, Nat), \y. y, \z. z)

If we defunctionalize this program, then each of these three lambda abstractions becomes one constructor of the data type. However since different constructors are not judgmentally equal, the following defunctionalized program no longer typechecks.

data Fun(a b: Type) { F1: Fun(Nat, Nat), F2: Fun(Nat, Nat), F3: Fun(Nat, Nat) } def Fun(a, b).ap(a b: Type, x: a): b { F1 => x, F2 => x, F3 => x } Refl(Fun(Nat, Nat), F1) : Eq(Fun(Nat, Nat), F2, F3)

Here is the gist of the problem: Judgmental equality must be preserved by defunctionalization and refunctionalization. This means that if we don’t want to treat different constructors of a data type as judgmentally equal, then we cannot treat all 𝛼-𝛽-equivalent comatches as judgmentally equal either.

It is not impossible to devise a scheme which lifts judgmentally equal comatches to the same constructors. However, we decided against this as it leads to confusing behavior. First, de- and refunctionalization would no longer be inverse transformations at least under syntactic equality. Second, such an attempt would necessarily be a conservative approximation as program equivalence is undecidable in general. In practice, that would mean that some comatches would be collapsed to the same constructor during lifting, while others would not.

Solution. Note that the opposite approach—never equating any comatches—doesn’t work either, since typing would then no longer be closed under substitution. For example, if 𝑓 is a variable standing for a function from natural numbers to natural numbers, then the term Refl(Fun(Nat, Nat), 𝑓 ) is a proof of the proposition Eq(Fun(Nat, Nat), 𝑓 , 𝑓 ). But we could not substitute a comatch 𝜆𝑦.𝑦 for 𝑓 , since the result would no longer typecheck. We therefore have to find a solution between these two extremes.

Our solution consists of always considering local comatches together with a name5 . Only comatches which have the same name are judgmentally equal, and this equality is preserved by reduction since the comatch is duplicated together with its name. Where do the names for local comatches come from? We support user-annotated labels, which allow the programmer to give meaningful names to comatches. Manually naming comatches in this way is useful as these labels can also be used by defunctionalization to name the generated constructors.

We enforce that these user-annotated labels are globally unique. However, as we do not want to burden the user with naming every single comatch in the program, we also allow unannotated comatches, for which we automatically generate unique names. As a result, each comatch occurring textually in the program has a unique name, but these names possibly become duplicated during normalization and typechecking.

4.2 Eta Equality

Problem. For reasons very similar to the previous section, 𝜂-equality is not preserved under defunctionalization and refunctionalization. Let us again consider a simple example. In the following proof, we show that a function 𝑓 is equal to its 𝜂-expanded form 𝜆𝑥.𝑓 .ap(𝑥). In order to typecheck, the proof would need to use a judgmental 𝜂-equality for functions.

codata Fun { ap(x: Nat): Nat } let prop_eta(f: Fun): Eq(Fun, f, (\x. f.ap(x))) ⅟= Refl(Fun, f);

However, defunctionalization of this proof would result in the following program, where we have used an ellipsis to mark all the constructors that were generated for the other lambda abstractions in the program.

data Fun { Eta(f: Fun), … } def Fun.ap(x: Nat): Nat { Eta(f) => f.ap(x),… } let prop_eta(f: Fun): Eq(Fun, f, Eta(f)) ⅟= Refl(Fun, f);

Using prop_eta it would now be possible to show that any constructor f of Fun is equal to Eta(f). This would contradict the provable proposition that distinct constructors are not equal.

Solution. We do not support 𝜂-equality in our formalization and implementation. This means that we only normalize 𝛽-redexes but not 𝜂-redexes during typechecking. However, it would be possible to support judgmental 𝜂-equality on a case-by-case basis similar to the eta-equality and no-eta-equality keywords in Agda which enable or disable eta-equality for a specific record type6 . De- and refunctionalization is then only available for types without 𝜂-equality.