Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Flattening subtyping by eta expansion

Jana Dunfield

TL;DR

This work shows how eta-expansion can obviate deep subtyping by translating a language with deep subtyping into one with only shallow subtyping. It develops a concrete example system (STLC extended with numbers and products) to demonstrate deep versus shallow subtyping, and then defines explicit eta-expansion rules and a beta-eta framework to relate the two forms. The central contributions include a complete proof that the shallow system, after eta-expansion, is complete with respect to the deep system and a detailed historical/contextual discussion linking to Barendregt et al. (1983). The approach enables simpler type-system design and implementation by reducing the need to handle deep subtyping directly, while retaining the expressive power through eta-expansion in the source language and careful typing rules. The work also surveys bidirectional typing formulations and sketches concrete proofs, highlighting practical pathways for compiler design and type-system engineering.

Abstract

To design type systems that use subtyping, we have to make tradeoffs. Deep subtyping is more expressive than shallow subtyping, because deep subtyping compares the entire structure of types. However, shallow subtyping is easier to reason about. By eta-expanding source programs, we can get the effect of deep subtyping with less of its complexity. An early paper on filter models (Barendregt et al. 1983) examined two similar intersection type systems. The first included a subsumption rule that used a rich subtyping relation, including multiple rules for the top type and a distributivity rule. Their second type system dropped the subsumption rule, but added a rule that allowed a term to be eta-expanded before typing it. This rule in their second type system compensated for the lack of subsumption: where their first type system used subtyping to manipulate intersections deep inside types, their second type system used introduction and elimination rules directly on the subterms created by eta-expansion. Viewed as a computation, their proof of completeness for the second (shallow) system performs eta-expansion. Thus, we can regard their proof as inventing the application of eta-expansion to avoid deep subtyping. This paper serves as a tutorial on using eta-expansion to obviate deep subtyping, puts the invention of the technique by Barendregt et al. (1983) into context, gives a complete proof of the relevant lemma, and discusses how the technique can be used in type system design.

Flattening subtyping by eta expansion

TL;DR

This work shows how eta-expansion can obviate deep subtyping by translating a language with deep subtyping into one with only shallow subtyping. It develops a concrete example system (STLC extended with numbers and products) to demonstrate deep versus shallow subtyping, and then defines explicit eta-expansion rules and a beta-eta framework to relate the two forms. The central contributions include a complete proof that the shallow system, after eta-expansion, is complete with respect to the deep system and a detailed historical/contextual discussion linking to Barendregt et al. (1983). The approach enables simpler type-system design and implementation by reducing the need to handle deep subtyping directly, while retaining the expressive power through eta-expansion in the source language and careful typing rules. The work also surveys bidirectional typing formulations and sketches concrete proofs, highlighting practical pathways for compiler design and type-system engineering.

Abstract

To design type systems that use subtyping, we have to make tradeoffs. Deep subtyping is more expressive than shallow subtyping, because deep subtyping compares the entire structure of types. However, shallow subtyping is easier to reason about. By eta-expanding source programs, we can get the effect of deep subtyping with less of its complexity. An early paper on filter models (Barendregt et al. 1983) examined two similar intersection type systems. The first included a subsumption rule that used a rich subtyping relation, including multiple rules for the top type and a distributivity rule. Their second type system dropped the subsumption rule, but added a rule that allowed a term to be eta-expanded before typing it. This rule in their second type system compensated for the lack of subsumption: where their first type system used subtyping to manipulate intersections deep inside types, their second type system used introduction and elimination rules directly on the subterms created by eta-expansion. Viewed as a computation, their proof of completeness for the second (shallow) system performs eta-expansion. Thus, we can regard their proof as inventing the application of eta-expansion to avoid deep subtyping. This paper serves as a tutorial on using eta-expansion to obviate deep subtyping, puts the invention of the technique by Barendregt et al. (1983) into context, gives a complete proof of the relevant lemma, and discusses how the technique can be used in type system design.

Paper Structure

This paper contains 10 sections, 1 theorem, 8 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Example system
  3. Overview
  4. Grammar
  5. Typing rules
  6. Bidirectional version:
  7. Deep subtyping
  8. Shallow subtyping
  9. Eta expansion
  10. From deep to shallow

Key Result

Lemma 1

If $A :< B$ and $\Gamma |-_{\space:<:} e : A$ then there exists $e'$ such that $e' \twoheadrightarrow_{\eta} e$ and $\Gamma |-_{\space:<:} e' : B$.

Figures (5)

  • Figure 1: Simply typed lambda calculus plus integers, rationals, booleans and products
  • Figure 2: Rules for the system $|-$ using deep subtyping, and for $|-_{\space:<:}$ using shallow subtyping
  • Figure 3: Subtyping rules (deep; compare Figure \ref{['fig:subtyping-shallow']})
  • Figure 4: Subtyping rules (shallow; compare Figure \ref{['fig:subtyping-deep']})
  • Figure 5: Eta reduction (if reading right-to-left: eta expansion)

Theorems & Definitions (1)

  • Lemma 1: Shallow expansion