Didactic implementation of the type checker described in "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" written in OCaml

Overview

bidi-higher-rank-poly

Didactic implementation of the type checker described in "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" written in OCaml.

Notable detours from the paper

Added the empty program and type explicitly in order to have a better handle on them during random program generation for testing. The reason is there are many different terms that represent the empty type in System F (e.g. ∀a.a), however in general it is undecidable whether a type term is inhabited or not. Therefore generating random polymorphic type terms is not very useful for testing, since some of them will represent the empty type and there is no way to tell. The chosen strategy for testing therefore became; generate random monomorphic type terms (these are always inhabited), generalise these type terms by randomly substituting their subterms with existential variables (the results are still inhabited, and should sometimes implicitly create polymorphic type terms); from these type terms generate random typed programs.

Testing strategy

This project uses Property Based Testing through the QCheck module for OCaml. Code has been written that allows for the random generation of typed programs, and as well as type directed shrinking of said generated programs. This made it very easy to hone in on bugs in e.g. the type checker, type synthesis and interpreter.

Language feature additions

Computing only with abstractions and units is a little inconvenient, as such additional language features will be added over time to this language playground.

Added features so far:

  • Empty types and programs
  • Statements

Frontend syntax

// Types - t
nothing           (Empty type)
unit              (Singleton type)
x                 (Type variable)
s -> t            (Arrow type)
x => t            (Universally quantified type)

// Statements - s
x : t. s          (Variable declaration followed by statement)
x = e. s          (Variable definition followed by statement)
e                 (Statement terminal)

// Expressions - e
undefined         (Empty program)
unit              (Singleton value)
x                 (Variables)
x => s            (Abstractions)
f x               (Applications)
(e : t)           (Type annotation)

Building

cd bidi-higher-rank-poly/
dune build repl/bin   (Build the REPL)
dune build util/test  (Build the util tests)
dune build back/test  (Build the backend tests)
dune build front/test (Build the frontend tests)

Or build all artefacts at once with

dune build

Testing

_build/default/util/test/Tests.exe   (Run the util tests)
_build/default/back/test/Tests.exe   (Run the backend tests)
_build/default/front/test/Tests.exe  (Run the frontend tests)

Or run all tests at once with

dune runtest

Using the REPL

rlwrap ./_build/default/repl/bin/Main.exe
> exit;;          (Exit the REPL)
> context;;       (Print the current context)
> x => x;;        (Evaluate an input term and print its result)
You might also like...
Safe OCaml-Rust Foreign Function Interface

ocaml-rust This repo contains code for a proof of concept for a safe OCaml-Rust interop inspired by cxx. This is mostly optimized for calling Rust cod

Sets of libraries and tools to write applications and libraries mixing OCaml and Rust

Sets of libraries and tools to write applications and libraries mixing OCaml and Rust. These libraries will help keeping your types and data structures synchronized, and enable seamless exchange between OCaml and Rust

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 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

Alternative Mizar proof checker written in Rust

Mizar proof checker This is a (still experimental) proof checker for the Mizar language. To compile the project, get Rust 1.67 or later (https://rustu

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

Owner
Søren Nørbæk
Søren Nørbæk
An implementation of WICG Import Maps specification

import_map A Rust implementation of WICG Import Maps specification. This crates is used in Deno project. The implementation is tested against WPT test

Deno Land 20 Nov 21, 2022
A fast R-tree for Rust. Ported from an implementation that's designed for Tile38.

rtree.rs A fast R-tree for Rust. Ported from an implementation that's designed for Tile38. Features Optimized for fast inserts and updates. Ideal for

Josh Baker 102 Dec 30, 2022
Computational Geometry library written in Rust

RGeometry Computational Geometry in Rust! What is RGeometry? RGeometry is a collection of data types such as points, polygons, lines, and segments, an

null 101 Dec 6, 2022
A single-binary, GPU-accelerated LLM server (HTTP and WebSocket API) written in Rust

Poly Poly is a versatile LLM serving back-end. What it offers: High-performance, efficient and reliable serving of multiple local LLM models Optional

Tommy van der Vorst 13 Nov 5, 2023
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

Jakob Demler 95 Dec 20, 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
An Rust implementation of the Modified Merkle Patricia Tree described by ETH Yellow Paper

Merkle Patricia Tree的Rust实现 博客文章:https://dere.press/2022/01/24/eth-trie/ 本实现参考下列项目: https://ethereum.github.io/yellowpaper/paper.pdf https://github.co

M4tsuri 3 Dec 13, 2022
An implementation of the append-only log described in the Certificate Transparency specification (RFC 6962)

CT Merkle This is an implementation of the append-only log described in the Certificate Transparency specification (RFC 6962). The log is a Merkle tre

Michael Rosenberg 30 Dec 2, 2022
Collection of immutable and persistent data structures written in Rust, inspired by the standard libraries found in Haskell, Closure and OCaml

PRust: (P)ersistent & Immutable Data Structures in (Rust) This library houses a collection of immutable and persistent data structures, inspired by th

Victor Colombo 13 Aug 13, 2023
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