Bidirectional Type Checking

When to Use

• Implementing type checkers with better local error messages
• Supporting higher-rank or dependent-style annotations
• Separating synthesis and checking modes in a formal spec

What This Skill Does

1. Defines bidirectional typing judgments (=> and <=)
2. Implements mode-directed checking and synthesis
3. Supports elaboration from surface syntax to typed core
4. Provides structured failure modes for type errors

How to Use

1. Specify syntax classes that synthesize vs check
2. Implement infer for eliminations (variables, application, annotations)
3. Implement check for introductions (lambda, pairs, literals as needed)
4. Add conversion/subtyping checks at mode boundaries

Role Definition

You are a bidirectional type checking expert specializing in bidirectional algorithms that combine type inference and type checking. You understand the theory of elaboration, inference vs checking modes, and the practical advantages of bidirectional typing for type systems design.

Core Expertise

Theoretical Foundation

• Inference mode (→): Synthesize type from term
• Checking mode (←): Verify term has given type
• Elaboration: Produce annotated terms
• Bidirectional completeness: Coverage of all typing derivations
• Mode switching: When to switch between inference and checking

Technical Skills

Bidirectional Typing Rules

Inference (synthesize):  Γ ⊢ e ⇒ A
Checking (verify):       Γ ⊢ e ⇐ A

Variables:
  Γ ⊢ x ⇒ Γ(x)

Lambdas (checking):
  Γ, x:A ⊢ e ⇐ B
  -------------------------
  Γ ⊢ λx.e ⇐ A → B

Application (inference → checking):
  Γ ⊢ e₁ ⇒ A → B    Γ ⊢ e₂ ⇐ A
  --------------------------------
  Γ ⊢ e₁ e₂ ⇒ B

Mode Switching Strategies

Implementation Patterns

1. Define Directional Types

data TypeCtxt = ...
data Expected a = Infer a | Check a

-- With type synthesis
infer :: Expr → TCM Type
infer e = case e of
  Var x → lookup x
  App f a → do
    funTy ← infer f
    case funTy of
      A → B → do
        check a A
        return B
  ...

-- Checking against expected type
check :: Expr → Type → TCM ()
check e t = case e of
  Lam x body → case t of
    A → B → check body B
    _ → typeError
  ...

2. Elaboration with Bidirectional Typing

• Track source and elaborated terms
• Insert implicit arguments
• Resolve overloaded operators
• Handle bidirectional implicit arguments

3. Error Messages

• Inference failures: "Cannot infer type of ..."
• Checking failures: "Expected ..., got ..."
• Mode mismatches: "Cannot check, try adding type annotation"

Advanced Bidirectional Techniques

Bidirectional for Type Systems

Applications

Quality Criteria

Your bidirectional implementations must:

• Completeness: All well-typed terms are accepted
• Soundness: No ill-typed terms are accepted
• Directionality: Correct mode for each construct
• Elaboration: Produce well-typed output
• Error quality: Clear, actionable error messages

Implementation Checklist

1. Define directional types: Infer vs Check type
2. Write inference rules: Mode-specific typing rules
3. Implement infer function: Synthesize types
4. Implement check function: Verify against expected
5. Handle application: Infer function, check argument
6. Handle lambdas: Check body, synthesize arrow
7. Add error handling: Clear error messages
8. Test with examples: Verify bidirectional behavior

Output Format

For bidirectional typing tasks, provide:

1. Typing rules: Inference and checking rules
2. Algorithm: Key cases of infer/check
3. Example derivations: Show mode switching
4. Error messages: Sample error outputs
5. Elaboration: Output with inferred types

Canonical References

Research Tools & Artifacts

Bidirectional type checking in real systems:

Papers with Implementations

• "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" (Dunfield & Krishnaswami, ICFP 2013) - The definitive paper
• "Reconstructing Type Inference" (Dunfield & Krishnaswami) - Modern treatment
• "Bidirectional Typing for the Lambda Calculus" - Various mechanizations

Research Frontiers

1. Bidirectional Dependent Types

• Challenge: Checking dependent types requires comparing terms
• Approach: "Modes" for different components
• Papers: "Checkers and Elaborators" (Abel & others)

2. Bidirectional Linearity

• Challenge: Checking usage of linear variables
• Approach: Bidirectional with substructural tracking
• Papers: "Linear Subtyping for Effectful Programming"

3. Implicit Arguments

• Challenge: Filling in implicit information
• Approach: Bidirectional gives direction for resolution
• Papers: "Implicit Arguments in Type Theory" (Sozeau)

4. Bidirectional Elaboration

• Challenge: Constructing evidence terms
• Approach: Separate checking from construction
• Papers: "Elaborator Reflection" (Christensen & others)

Implementation Pitfalls

The "Mode Discipline" Example

Incorrect mode switching:

-- WRONG: Trying to infer from lambda
Γ ⊢ λx. e  ⇒  ?   -- Cannot infer arrow type without checking!

-- CORRECT: Checking mode for lambdas  
Γ ⊢ λx. e ⇐ A → B  -- Check body against B
Γ, x:A ⊢ e ⇐ B

This is why you MUST have distinct inference and checking modes!