A bidirectional type checker

Overview

Homemade Bidirectional Typing

(λ f. (λ g. (λ x. f (g x))))
=> ((a -> b) -> ((c -> a) -> (c -> b)))

A bidirectional type inference system loosely based on Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.

I read a bit about bidirectional type inference about a year ago but was fuzzy on many of the details, so I figured that it would be a fun exercise to try to implement a full type inference and checking algorithm without consulting any references. This is the result.

Exposition

At the core is a small lambda calculus,

data Expr =
    EUnit Loc
  | EIdent Loc Id
  | EAnno Loc Expr Type
  | ELam Loc Id Expr
  | EApp Loc Expr Expr

featuring a unit type which is simply a base type but without anything interesting that you can do with it. Loc here refers to a type which specifies source location of the expression. After all, two variables with the same name in different parts of the program are unique and need not have the same type.

A corresponding interpreter is included as well,

data Val =
    VUnit
  | VLam Env Id Expr

type Env = Map Id Val

interp :: Env -> Expr -> Maybe Val
interp _ (EUnit _) = Just VUnit
interp env (EIdent _ x) = Map.lookup x env
interp env (EAnno _ body _) = interp env body
interp env (ELam _ x body) = Just (VLam env x body)
interp env (EApp _ f a) = case ((interp env f), (interp env a)) of
  (Just (VLam fenv y body), Just xval) -> interp (Map.insert y xval fenv) body
  otherwise -> Nothing

run :: Expr -> Maybe Val
run = interp Map.empty

Moving along...

Type Inference

This is the fun part. Bidirectional typing is centered on two operations, hence the name.

  • Type checking, checking that an expression satisfies a given type under some context. For example, checking that (λ x. x) has type a -> a should succeed but checking it against the unit type should fail.
  • Type synthesis, given an expression and some program context synthesize a new type for the expression. We may not have enough information to determine the exact type that the expression must have, but we can make a guess and put in some placeholders where necessary. For example, we know (λ x. ) must have a function type a -> b, but we can't quite be sure about what a and b are without looking into the body of the lambda.

Since I was starting with very few pre-conceived notions about what a bidirectional type inference algorithm should look like I ended up diverging from the "Complete and Easy" algorithm in a few ways. In particular, instead of maintaining a so-called "ordered algorithmic context" I simply maintained type environment that mapped source expressions to TypeIds which are then mapped to types:

newtype TypeId = TypeId Integer

data Type =
    TUnit
  | TIdent TypeId
  | TLam Type Type

data TypeStatus =
    Exists
  | Forall
  | Typed Type

data TypeEnv = TypeEnv Integer (Map Expr TypeId) (Map TypeId TypeStatus)

Well, it's a little bit more complicated than that: a TypeId can also be marked as existential (Exists), meaning that we have not yet determined what it should be, or universal (Forall), meaning that it is a type variable in some polymorphic type. The added indirection here is necessary to model the fact that multiple source expressions may map to the same type. It also allows types to reference other types via TIdents. We also keep an Integer around so we know what the next unused TypeId should be.

Another distinction is that I managed to reduce the checking half of bidirectional typing to simply a synthesis, followed by a subtype operation:

check :: TypeEnv -> Expr -> Type -> Maybe TypeEnv
check tenv expr typ = do
  (typ', tenv') <- synth tenv expr
  tenv'' <- subtype tenv' typ' typ
  return tenv''

I'm not sure if this is a good or bad thing really. I view it as a simplification, personally. (This is equivalent to the Sub rule in "Complete and Easy.")

The rest of the implementation actually reflects the "Complete and Easy" algorithm fairly closely. I also ended up with subtype and synth, but happened to inline the instantiation rules.

synth :: TypeEnv -> Expr -> Maybe (Type, TypeEnv)

subtype :: TypeEnv -> Type -> Type -> Maybe TypeEnv

These implementations are fairly routine. Function applications are a little tricky, but with those figured out the rest falls into place. Function subtyping also requires a little bit of care, of course. A1 <: A2 and B1 <: B2 does not imply A1 -> B1 <: A2 -> B2!

All in all, I'm pretty happy with the way it turned out. In my (very partial) opinion, the implementation with an unordered mapping from expressions to types is more intuitive than thinking about an ordered context of solved and unsolved types. The implementation also doesn't require type markers or list splicing kung fu which is nice.

I went back to read the paper and noted the connections between the two in code comments so it should be fairly approachable to readers who prefer reading at LaTeX.

TODO

  • There are a number of things that could be made more monadic/clean. PRs welcome!
  • Record subtyping is next on my list. I spent a bit of time on this, but I've come to the conclusion that it requires using a constraint solver approach. Should be do-able though.
You might also like...
An implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types

Vinilla Lang Vanilla is a pure functional programming language based on System F, a classic but powerful type system. Merits Simple as it is, Vanilla

Implementation of "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism"

Implementation of "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" See arXiv:1306.6032 This implementation focusses on read

bspipe A Rust implementation of Bidirectional Secure Pipe

bspipe A Rust implementation of Bidirectional Secure Pipe

This library implements a type macro for a zero-sized type that is Serde deserializable only from one specific value.

Monostate This library implements a type macro for a zero-sized type that is Serde deserializable only from one specific value. [dependencies] monosta

Type erased vector. All elements have the same type.

Type erased vector. All elements have the same type. Designed to be type-erased as far as possible - most of the operations does not know about concre

Translate C++/Rust type into C type with the same memory layout

clayout, translate C++/Rust type into C type with the same memory layout. Generally, clayout is used together with bpftrace. clayout is developed on d

A crate that allows you to mostly-safely cast one type into another type.

A crate that allows you to mostly-safely cast one type into another type. This is mostly useful for generic functions, e.g. pub fn fooS(s: S) {

A model checker for implementing distributed systems.
A model checker for implementing distributed systems.

A model checker for implementing distributed systems.

Source code spell checker

eztd is meant to close the ergonomics gap between Rust and Python.

Rust TLS/SSL certificate expiration date from command-line checker

Rust TLS/SSL certificate expiration date from command-line checker

Avro schema compatibility checker

DeGauss Your friendly neighborhood Avro schema compatibility checker. Install cargo install degauss Example Check the compatibility of your schemas d

WriteForAll is a text file style checker, that compares text documents with editorial tips to make text better.

WriteForAll: tips to make text better WriteForAll is a text file style checker, that compares text documents with editorial tips to make text better.

Checks all your documentation for spelling and grammar mistakes with hunspell and a nlprule based checker for grammar

cargo-spellcheck Check your spelling with hunspell and/or nlprule. Use Cases Run cargo spellcheck --fix or cargo spellcheck fix to fix all your docume

coins20's graduation requirements checker

tanici 筑波大学の履修管理システム twins が出力するCSV(UTF-8)をもとに,coins20(情報科学類2020年度生)が卒業可能であるかを判定し不足を出力します.おまけとしてGPAの算出も行います. (免責事項:精度の保証はしません.あくまで参考程度に,責任は負いません.) Usa

A simple, single threaded and minimalistic port checker

A simple, single threaded and minimalistic port checker

Tools to feature more lenient Polonius-based borrow-checker patterns in stable Rust
Tools to feature more lenient Polonius-based borrow-checker patterns in stable Rust

Though this be madness, yet there is method in 't. More context Hamlet: For yourself, sir, shall grow old as I am – if, like a crab, you could go back

A simple url checker for finding fraud url(s) or nearest url

urlchecker A simple url checker for finding fraud url(s) or nearest url while being fast (threading) Eg:- use std::collections::HashMap; use urlchecke

A credit card checker written in Rust

💳 Credit Card Checker A credit card checker written in Rust Checks if a card number is valid with the help of the Luhn algorithm and checks also for

'apk-yara-checker' is a little CLI tool written in Rust to check Yara rules against a folder of APK files.
'apk-yara-checker' is a little CLI tool written in Rust to check Yara rules against a folder of APK files.

apk-yara-checker 'apk-yara-checker' is a little CLI tool written in Rust to check Yara rules against a folder of APK files. You have to pass the folde

Owner
Samuel Ainsworth
PhD student at UW working in ML and robotics. #blacklivesmatter
Samuel Ainsworth
A credit card checker written in Rust

?? Credit Card Checker A credit card checker written in Rust Checks if a card number is valid with the help of the Luhn algorithm and checks also for

Oliver Borner 3 Aug 9, 2022
This crate provides a convenient macro that allows you to generate type wrappers that promise to always uphold arbitrary invariants that you specified.

prae This crate provides a convenient macro that allows you to generate type wrappers that promise to always uphold arbitrary invariants that you spec

null 96 Dec 4, 2022
A Rust framework for building context-sensitive type conversion.

Xylem is a stateful type conversion framework for Rust.

Jonathan Chan Kwan Yin 4 May 11, 2022
A fusion of OTP lib/dialyzer + lib/compiler for regular Erlang with type inference

Typed ERLC The Problem I have a dream, that one day there will be an Erlang compiler, which will generate high quality type-correct code from deduced

Dmytro Lytovchenko 35 Sep 5, 2022
Use explicit container types with Scrypto! Leverage the Rust compiler's type checking to increase security and productivity when developing Radix blueprints.

Scrypto Static Types Use explicit container types with Scrypto! Leverage the Rust compiler's type checking to increase security and productivity when

null 7 Aug 5, 2022
The never type (the true one!) in stable Rust.

::never-say-never The ! type. In stable Rust. Since 1.14.0. Better than an enum Never {} definition would be, since an instance of type ! automagicall

Daniel Henry-Mantilla 17 Jan 3, 2023
sblade or switchblade it's a multitool in one capable of doing simple analysis with any type of data, attempting to speed up ethical hacking activities

sblade or switchblade it's a multitool in one capable of doing simple analysis with any type of data, attempting to speed up ethical hacking activities

Gabriel Correia 1 Dec 27, 2022
Simplistic complier~virtual-machine that transforms AST into a Rust function, with basic type checking

rast-jit-vm rast-jit-vm is a simplistic, proof-of-concept~ish compiler / virtual machine that transforms syntax tree into a Rust function, type-checki

Patryk Wychowaniec 4 Oct 23, 2022
A bidirectional type checker

A bidirectional type inference system loosely based on Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.

Samuel Ainsworth 35 Sep 22, 2022
Build database expression type checker and vectorized runtime executor in type-safe Rust

Typed Type Exercise in Rust Build database expression type checker and vectorized runtime executor in type-safe Rust. This project is highly inspired

Andy Lok 89 Dec 27, 2022