PaperlayerView exact revision on arXiv

Source-linked AI summary

Unifying Function- and Argument-First Bidirectional Type Systems

Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi

arXiv:2609.02005v1cs.PL

TL;DR

Existing bidirectional type systems fix either function-first or argument-first typing, producing incompatible typeabilities. The paper introduces λBH, which unifies both styles through application guides and flexible type representations, and develops a worklist-based algorithm whose metatheory is mechanically verified.

  • Problem

    Existing bidirectional type systems fix the typing order for function applications, making function-first and argument-first typeabilities incompatible.

  • Method

    The paper introduces λBH with application guides, boxy types, and a worklist-based typing algorithm to support higher-rank polymorphism and either typing style.

  • Results

    λBH is sound and complete with respect to representative function-first and argument-first systems, while its typing algorithm is sound for λBH and complete for both representative systems.

  • Takeaways & Limitations

    λBH lets language designers choose function-first or argument-first typing per application while retaining a unified declarative system and algorithm.

  • Takeaways & Limitations

    The system does not yet support product types, let-polymorphism, or impredicativity, and its algorithm is not complete with respect to λBH itself.

Abstract

from arXiv · show

Bidirectional typing mixes type synthesis and type checking into a single process. Existing bidirectional type systems can be classified into two styles based on whether, given a function application, a bidirectional typing algorithm synthesizes the function's type first and typechecks the argument against the synthesized argument type, or it synthesizes the arguments' types first and typechecks the function against the synthesized arguments' types. We call the former _function-first_ and the latter _argument-first_. Not only do the two styles significantly differ in how the type systems and typing algorithms are formalized, but also they lead to incompatible typeabilities, forcing a language designer to select one style and to give up the other's typeabilities. In this paper, we unify the two styles and develop \lang with a new bidirectional type system for higher-rank polymorphism. Key ideas of the unification are twofold. Each function application is annotated with a bit of information to represent whether function- or argument-first typing is used, to allow a language designer (or even a programmer) to switch between the two styles at their discretion. We reformulate the function- and argument-first type systems by using ideas from colored types and boxy types, which can specify which part of a type should be synthesized or used for checking in a flexible manner. We also develop a typing algorithm based on the worklist approach by Zhao et al. The (declarative) type system of $λ^{BH}$ is shown to be sound and to subsume two representative function- and argument-first systems. Our typing algorithm is shown to be sound with respect to the type system of $λ^{BH}$ and complete with respect to representative function- and argument-first systems. We mechanically prove the metatheorems using the Abella theorem prover.

1 Introduction

Existing bidirectional systems fix either function-first or argument-first typing, making their typeabilities incompatible, while higher-rank polymorphism further distinguishes their formalizations. The paper introduces λBH, which unifies both styles through per-application guides and flexible type information, with soundness, completeness, and mechanical metatheoretic results.

  • Motivation: Function-first systems synthesize the function type before checking arguments, whereas argument-first systems synthesize argument types before checking the function.These styles differ in when polymorphic types are instantiated for higher-rank polymorphism.
  • Motivation: Fixed typing orders make existing function-first and argument-first systems typeability-incompatible, forcing language designers to choose one style.The incompatibility is especially relevant when typing function applications and supporting higher-rank polymorphism.
  • Unified design: λBH attaches a guide to each function application, allowing function-first or argument-first typing to be selected independently at each application.Fixing all guides to one style recovers the corresponding existing system, while guides can also follow language-specific heuristics.
  • Unified design: Boxy types represent partially known type information, addressing cases where different arguments require a mixture of synthesis and checking.Colored types and boxy types provide related mechanisms for specifying which type components are synthesized and which are used for checking.
  • Metatheory and implementation: The work provides a worklist-based typing algorithm that is sound for λBH and complete for representative function-first and argument-first systems.The declarative system is sound and complete with respect to representative systems, while the algorithm is not complete for λBH itself.
  • Metatheory and implementation: The declarative and algorithmic metatheory, including algorithm termination, is mechanically proved using the Abella theorem prover.A prototype implementation in OCaml provides heuristic elaboration of an ML-like language to λBH.

2 Overview

Bidirectional typing has function-first and argument-first styles with different formalizations and incompatible typeabilities. λBH unifies them using application guides and boxy types, supporting flexible switching and higher-rank polymorphism.

  • Bidirectional typing: Bidirectional typing combines synthesis, which produces a type, with checking, which verifies an expression against a supplied type.The two modes are represented by synthesis and checking judgments.
  • Two typing styles: Function-first typing synthesizes the function type before checking the argument, whereas argument-first typing synthesizes the argument before checking the function.The DK system represents the function-first style, while the XO system represents the argument-first style.
  • Two typing styles: The two styles have incompatible typeabilities for higher-rank polymorphism because each system can type examples the other rejects.One example is well-typed only under DK, while another is well-typed only under XO.
  • Unification challenge: Mixing the styles requires representing partially known type information when different arguments demand different synthesis and checking directions.Neither DK nor XO handles a function whose first argument type must be synthesized while its second argument type is checked.
  • Unification approach: λBH uses boxy types to encode which type components are synthesized and which are supplied for checking, without an application context.Boxy types adapt the original function-first idea to argument-first typing and support mixed applications.
  • Unification approach: Application guides let each function application select function-first or argument-first typing, enabling language-specific schemes and intermediate-language use.A language designer may, for example, choose argument-first typing only when an argument is a variable.

3 λBH and Its Type System

λBH presents a declarative type system using boxy types to unify synthesis and checking, together with subtyping and typing rules for guided applications. Its metatheory establishes soundness and completeness connections to System Fpι, DK, and XO.

  • Syntax: λBH expressions include unit, variables, annotated and unannotated lambdas, and two guided application forms, ↬ and ↫.Type annotations introduce variables with higher-rank polymorphic types.
  • Types and boxy types: Boxy types place synthesizable information inside boxes while requiring type information inside universal types to be fully given.This restriction ensures that synthesis results remain uniquely determined under the system’s guessing discipline.
  • Subtyping: λBH has two subtyping judgments that synthesize information inside a boxy supertype or subtype, respectively.The judgments differ according to which side contains boxes and use corresponding SL and SR rule families.
  • Typing: A single typing judgment unifies synthesis and checking: ordinary types represent synthesis, while boxy types represent checking with partial synthesis.The judgment’s inputs are the context, expression, and information outside boxes; its output fills information inside boxes.
  • Typing: The T_AppR rule implements function-first applications, while T_AppL implements argument-first applications.T_AppR first synthesizes the function’s argument type; T_AppL first synthesizes the argument type and checks the function against it.
  • Metatheory: The type system is sound with respect to System Fpι and complete with respect to both the DK and XO systems.The soundness result relates translated λBH terms to System Fpι terms, while the completeness theorems establish correspondence with DK and XO derivations.
  • Metatheory: Completeness with respect to XO translates applications using ↫ and embeds XO’s application context into a boxy type via FoldCurry.The theorem states that an XO derivation yields a corresponding λBH judgment using FoldCurry(Ξ, A).

4 Algorithmic Typing

The algorithm uses worklists extended with existential variables and typing judgments to process bidirectional typing incrementally. It is sound for λBH, complete for DK and XO, and decidable under stated well-formedness restrictions.

  • Worklist approach: A worklist extends the typing context with existential variables and subtyping or typing judgments, processing the rightmost judgment by reduction.Existential variables are solved only to monotypes well-formed in their preceding context, enforcing scope conditions.
  • Boxy types: Polymorphic existential variables propagate types filling boxes across work items, supporting boxy types with multiple output channels.Each box receives a polymorphic existential variable that can carry a polymorphic type to subsequent work items.
  • Metatheory: The algorithm is decidable, but it is not complete for the unrestricted declarative λBH system.The weaker completeness result excludes boxes containing non-polymorphic-existential types or multiple occurrences of one polymorphic existential variable.
  • Declarative correspondence: The algorithm uses worklist instantiation and declarative worklists to relate reductions to λBH’s declarative typing judgments.A successful instantiated worklist provides well-formed solutions for existential variables that make the corresponding declarative typing hold.
  • Metatheory: The algorithm is sound with respect to λBH’s declarative system.If a well-formed worklist reduces to the empty worklist, an instantiation exists that yields a corresponding declarative derivation.
  • Metatheory: The algorithm is complete with respect to both the DK and XO systems, including their synthesis and checking judgments.The corollary states reductions to the empty worklist for well-typed DK and XO programs after inserting appropriate polymorphic existential variables.

5 Related Work

Related systems differ in polymorphism, typing order, and switching flexibility. λBH uses boxy types to subsume representative function-first and argument-first systems while retaining a broader switching design space.

  • Predicative systems: Peyton Jones et al. use function-first typing for higher-rank polymorphism but restrict synthesized types by instantiating higher-rank types.That restriction can reject expressions whose synthesized type has a top-level quantifier.
  • Predicative systems: Dunfield and Krishnaswami add an application judgment that extracts an argument type from a polymorphic function type.λBH uses boxy types to subsume this function-first system.
  • Predicative systems: Xie and Oliveira introduce argument-first typing with an application context, while supporting let-polymorphism and conservatively extending Hindley–Milner.λBH’s boxy types subsume the application-context notion, but λBH does not share that full polymorphism scope.
  • Predicative systems: Annotation-free first-class-polymorphism systems do not accept every program accepted by argument-first typing.Their unannotated inference can reject a program requiring an argument type to check an abstraction body.
  • Impredicativity: Quick Look combines bidirectional typing with constraint-based inference for impredicativity but lacks some typeability of XO.The paper identifies it as a possible guide for extending λBH with impredicative polymorphism.
  • Generalizing bidirectional typing: Contextual typing and Contextual System F switch typing direction more flexibly than fixed-order systems but impose ordering or polymorphism restrictions relative to λBH.Contextual System F processes arguments left-to-right and can reject programs accepted by DK or XO.

6 Conclusion and Future Work

λBH unifies function-first and argument-first typing for higher-rank polymorphism, with a worklist algorithm whose metatheory is mechanically verified. Future work targets broader type features and practical evaluation.

  • Conclusion: λBH is a unified intermediate language that lets designers choose function-first or argument-first typing at each application.Its declarative system uses boxy types and subsumes both styles while supporting higher-rank polymorphism.
  • Conclusion: The typing algorithm is independent of the designer’s style-selection heuristics, sound for λBH, and complete for DK and XO.The algorithm is not complete for the full λBH declarative system.
  • Future work: Future declarative extensions include product types, let-polymorphism, impredicativity, and explicit type applications.Supporting let-polymorphism would allow λBH to subsume the original XO system completely.
  • Future work: Future algorithmic work includes level-based inference, typeability benchmarks, and evaluating typing stability under program transformations.The paper connects level-based inference to practical implementations and calls for benchmarks of practical usefulness.
  • Algorithm: The worklist approach represents typing contexts with existential variables and judgments processed through reductions.Scope-managed existential variables avoid accidentally solving variables outside the declarative system’s permitted scope.
  • Algorithm: Polymorphic existential variables propagate box-filled types across work items, including the synthesized argument type in function-first application rules.They act as placeholders that can be solved to polymorphic types, unlike variables restricted to guessed monotypes.

A.2.2 Scope Delimiters

Scope delimiters control where polymorphic existential variables are inserted, enabling the algorithm to solve them in the required worklist order.

  • Scope-delimiter mechanism: Inserting existential variables at the worklist's rightmost position can fail when polymorphic existential variables precede them.The existential variable γ cannot solve α and β when it appears after them in the worklist.
  • Scope-delimiter mechanism: The algorithm instead inserts γ before polymorphic existential variables α and β, allowing those variables to be solved to γ.The revised reduction is Γ, α, β ⇝ Γ, γ, α, β rather than placing γ after α and β.
  • Scope-delimiter mechanism: Scope delimiters ▷{⃗α} mark positions where polymorphic existential variables are inserted in the worklist.The algorithm introduces a delimiter alongside a type variable and inserts an existential variable immediately before the rightmost delimiter.
  • Scope-delimiter mechanism: Because type variables and scope delimiters are introduced together, the type variable can solve existential variables inserted before the delimiter.This mechanism explains why insertion occurs before the rightmost scope delimiter.
  • Algorithmic-system syntax: The algorithmic system extends worklists with existential variables, polymorphic existential variables, scope delimiters, subtyping work items, and typing work items.Successful typing is represented by a reduction sequence Γ ⇝* ∅.

B.1.2 Algorithmic Typing

Algorithmic typing reduces worklists by processing subtyping and typing judgments, solving existential variables while handling polymorphic applications and lambda abstractions.

  • Worklist reduction: Algorithmic typing is defined as worklist reduction, and Γ ⇝* ∅ represents successful completion.Each reduction processes a work item in one step, with newly introduced variables required to be fresh.
  • Algorithmic subtyping: Subtyping rules decompose function types, instantiate quantified variables, and solve existential variables subject to scope and well-formedness conditions.Box-solving requires the free type and existential variables of the solution to be bound in the appropriate scope.
  • Existential-variable solving: Existential-variable rules instantiate variables from the opposite side or decompose them into argument and result variables, with occurrence order controlling solvability.Function decomposition uses an occurs check to prevent invalid self-reference.
  • Application examples: Application examples show both application directions eventually checking unit against an existential variable that is solved to unit.The two examples correspond to function-first and argument-first application forms.

B.2.2 Soundness

The algorithm is sound with respect to λBH's declarative system, but it is not complete for all λBH derivations because a scope-ordering case can make reduction get stuck.

  • Soundness: If a well-formed worklist reduces successfully to the empty worklist, soundness yields a corresponding declarative derivation.The theorem applies to the algorithmic system of λBH.
  • Soundness: Soundness also holds for completed subtyping and typing work items after existential-variable instantiation and worklist translation.The resulting translated judgments are derivable under the corresponding declarative context.
  • Completeness boundary: Algorithmic completeness with respect to the full λBH declarative system does not hold.The paper explicitly introduces a counterexample where the required reduction sequence becomes stuck.
  • Completeness boundary: The counterexample gets stuck because existential variable γ occurs after polymorphic existential variables α and β, preventing the ASL_Box rule from solving them.The paper contrasts this issue with existing boxy-type approaches that omit the corresponding subtyping forms.

B.2.4 Completeness with respect to the DK and XO systems

Under a restriction excluding the problematic scope configuration, the algorithm is complete with respect to the Dunfield–Krishnaswami and Xie–Oliveira systems.

  • Input restriction: The restriction excludes the problematic worklist configuration and requires scope delimiters before work items.A second judgment constrains polymorphic existential-variable occurrences and their ordering in the worklist.
  • Input restriction: The restriction is not so strict that it rejects well-typed programs from the DK or XO systems.The paper states this directly before presenting the completeness corollary.
  • Completeness result: The algorithm is complete with respect to both the DK and XO systems.The corollary gives reductions to the empty worklist for synthesized and checked DK programs and for synthesized XO programs.
  • Completeness result: These reductions show that the algorithm successfully types programs accepted by DK or XO while inserting polymorphic existential variables appropriately.The result applies to the corresponding translations of programs and contexts.

B.2.5 Decidability

The typing algorithm is decidable: every well-formed worklist either reduces to the empty worklist or reaches a non-reducible non-empty worklist.

  • The typing algorithm is decidable.
  • Every well-formed worklist reduces to the empty worklist or to a non-empty worklist with no further reduction.
  • The proof strategy follows Zhao et al.'s approach to showing decidability.

C Application Guide Insertion

Application guides let λBH choose function-first or argument-first typing per application, while marking estimates guessing and supports guide insertion. The section also outlines extensions for let polymorphism and explicit type applications, including unresolved limitations.

  • C Application Guide Insertion: Application guides ↬ and ↫ select function-first and argument-first typing rules, respectively.
  • C Application Guide Insertion: Language designers can insert guides according to their preferred strategy, including choosing argument-first only when an argument is a variable.
  • C Application Guide Insertion: Guess values ? and ! estimate whether type synthesis may require guessing or has fully known information.
  • C Application Guide Insertion: The marking judgment assigns marks and guess values, then inserts application guides into expressions.
  • C Application Guide Insertion: The marking system accepts (f1 f2) f3 by producing (f1 ↬ f2) ↫ f3, although empirical evaluation remains future work.
  • D.1 Let Polymorphism: Let polymorphism would improve compatibility with Hindley–Milner and subsume the original XO system, but its traditional generalization rule conflicts with λBH's context-based type-variable management.
  • D.1 Let Polymorphism: A proposed let rule uses a separate type-variable-only context Σ to permit fresh type variables when synthesizing let-bound expressions.

D.2 Explicit Type Application

Explicit type applications extend λBH with known type arguments, supporting impredicative instantiation and improved typeability. Their interaction with polymorphic subtyping can violate subsumption, motivating alternative restrictions or revised rules.

  • D.2 Explicit Type Application: Explicit type applications can realize impredicative instantiation and improve typeability.
  • D.2 Explicit Type Application: XO's application context records supplied type arguments, allowing expressions such as (Λa.λx : a.x + 1) @ int to typecheck.
  • D.2 Explicit Type Application: λBH adds the boxy type @A → A□, whose rules substitute or use a known type argument when typing type abstractions and applications.
  • D.2 Explicit Type Application: Combining explicit type applications with polymorphic subtyping can break the subsumption lemma because type-application results depend on quantified-variable order.
  • D.2 Explicit Type Application: Two proposed directions are updating polymorphic subtyping rules or forbidding subtyping over an argument type.
  • D.2 Explicit Type Application: The formalization includes expressions, coercions, worklists, subtyping judgments, coercion composition, erasure, and translations for DK and XO systems.
Loading 2609.02005v1…