Type-Directed Synthesis

In type-directed synthesis, a program's type signature acts as a high-level, formal specification. The synthesizer's goal is to find a program term that inhabits a given type. For example, synthesizing a function of type (Int, Int) -> Int immediately constrains the search to functions that take two integers and return one. This is fundamentally different from synthesizing from input-output examples, as the type provides a logical contract about the program's behavior before any concrete execution. The process often involves proof search in a type theory, where constructing a term of a type is analogous to proving a theorem.

Refinement types augment standard types with logical predicates, enabling more precise specifications. A type like {v:Int | v > 0} (a positive integer) directly encodes a semantic constraint. A synthesizer tasked with generating a value of this type must not only produce an integer but also prove it satisfies v > 0. This allows synthesis of programs with guaranteed properties, such as:

• A function that returns a sorted list: List Int -> {l:List Int | sorted(l)}
• A divisor function that never divides by zero: (x:Int, {y:Int | y != 0}) -> Int Tools like LiquidHaskell use refinement types for verification and can guide synthesis.

Dependent types are types that depend on values, creating a unified language for programs and proofs. This allows specifications to express deep functional correctness. For instance, the type of a append function can guarantee the length of the output list: (xs:Vec A n, ys:Vec A m) -> Vec A (n + m). Type-directed synthesis with dependent types becomes a search for a proof term in a dependently typed calculus (like the Calculus of Constructions). While highly expressive, the search space is complex, requiring sophisticated proof assistants (like Coq or Agda) and tactics (auto, omega) to automate term construction.

The synthesis algorithm is typically an interactive proof search. The type goal is decomposed using the introduction and elimination rules of the type system.

• Forward Search (Bottom-Up): Enumerates well-typed terms, using types to prune invalid candidates.
• Backward Search (Top-Down): Starts with the goal type and applies typing rules in reverse, generating holes (or metavariables) for subterms. The synthesizer then incrementally fills these holes. This is closely related to programming with tactics in proof assistants, where the user guides the system to construct the required term. Higher-order unification is often used to solve for unknown function arguments.

Type-directed synthesis excels in domains requiring high assurance:

• Cryptographic Protocols: Synthesize implementations from formal specs (e.g., in *F` or Vale), ensuring adherence to security properties.
• Systems Programming: Generate safe, low-level code (e.g., device drivers, network parsers) with bounds-checking guarantees encoded in types.
• Library Development: Automatically create API-compliant functions or smart constructors that enforce invariants.
• Compiler Development: Generate optimization passes or parts of a compiler that are correct-by-construction, reducing the trusted code base.

Several research and industrial tools implement type-directed synthesis paradigms:

• Coq & Agda: Proof assistants where the Program command or tactic-based scripting (refine) performs synthesis.
• *F : A functional language that uses SMT-backed refinement types; its **F* extractor synthesizes OCaml, F#, C, or WASM code from high-level specs.
• LiquidHaskell: Adds refinement types to Haskell, enabling type-guided program construction and verification.
• Synquid (Synthesis with Qualitative and Quantitative Data): A synthesizer that uses refinement types and component-based search.
• Rosette: A solver-aided host language that, while not purely type-directed, uses symbolic types and constraints for synthesis.