Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Relational Solver for Constraint-based Type Inference

Eridan Domoratskiy, Dmitry Boulytchev

TL;DR

A miniKanren-based type inferencer for an educational programming language with first-class functions, S-expressions, and pattern-matching with a number of tricks, optimizations, and extensions used.

Abstract

We present a miniKanren-based type inferencer for an educational programming language with first-class functions, S-expressions, and pattern-matching. The language itself is untyped which adds a certain specificity to the problem and requires the employment of techniques conventionally used in implicit/gradual typing settings. The presence of polymorphic and recursive types poses a certain challenge when implementing the inferencer in miniKanren and requires a number of tricks, optimizations, and extensions to be used; we report on those as well.

A Relational Solver for Constraint-based Type Inference

TL;DR

A miniKanren-based type inferencer for an educational programming language with first-class functions, S-expressions, and pattern-matching with a number of tricks, optimizations, and extensions used.

Abstract

We present a miniKanren-based type inferencer for an educational programming language with first-class functions, S-expressions, and pattern-matching. The language itself is untyped which adds a certain specificity to the problem and requires the employment of techniques conventionally used in implicit/gradual typing settings. The presence of polymorphic and recursive types poses a certain challenge when implementing the inferencer in miniKanren and requires a number of tricks, optimizations, and extensions to be used; we report on those as well.
Paper Structure (15 sections, 6 equations, 4 figures)

This paper contains 15 sections, 6 equations, 4 figures.

Table of Contents

  1. Introduction
  2. The $\lambda\hbox{$a$}\hbox{$\mathcal{M}$}\hbox{$a$}$ Programming Language
  3. Type system
  4. Constraint system
  5. Constraint solver
  6. Term shape check helpers
  7. Pruning the search space for function types
  8. Pruning the search space for S-expression types
  9. Partial support for recursive terms in OCanren
  10. Recursive types introduction and elimination
  11. Constraint solving order and runtime scheduling
  12. Invoking the solver
  13. Evaluation
  14. Examples
  15. Conclusion and future work

Figures (4)

  • Figure 1: Constraint entailment inference rules
  • Figure 2: Solutions tree for several different $Sexp$ constraints
  • Figure 3: Elapsed time for typecheck of tests
  • Figure 4: Elapsed time for typecheck of tests by number of $Sexp$ branches