ayazhafiz / plts

A collection of programming languages and type systems.

import Revision from "../components/revision.tsx" import {Helmet} from "react-helmet"; import {Box, ThemeProvider} from "@primer/react";

export default function Layout({children}) { return (<> <title>plts</title> <Box m={[4, 4, 10]}>{children} </>); }

plts

Implementations of type systems and programming languages I find interesting.

Repository: gh:ayazhafiz/plts.

• Introductory
• Flow Typing
• Gradual Typing
• Typed Assembly
• Subtyping
• Dependent Types
• Effects and Coroutines
• Roc

Introductory

• Emulating the Lambda Calculus in TypeScript's Type System: Evaluating the lambda calculus entirely using the TypeScript type system.

• TAPL: Selected implementations of languages formalized in Types and Programming Languages (Pierce 2002).

• Tiger: A compiler for the Tiger Language of Appel's 1998 Modern Compiler Implementation.

Flow Typing

• lang_narrow: A language with unions, records, and flow typing. A checker, interpreter, and C code generator is implemented.

  • Playground
  • Blog post

• FT: The FT (flow typing) calculus from David Pearce's 2012 paper Sound and Complete Flow Typing with Unions, Intersections, and Negations. Like lang_narrow, but smaller and proven sound and complete. Includes a self-designed type inferer guaranteed to infer principal types.

  • Playground
  • Pearce, 2012
  • Blog post: type inference for the calculus

Gradual Typing

• gtlc: A compiler for the gradually-typed lambda calculus, employing the type consistency relation of Siek and Taha (2006). The GTLC allows a developer to omit type annotations during development at the expense of run-time type casts. While the ahead-of-time typechecker will catch any non-sensical type errors, the runtime system will catch any cast errors.

  The compiler is multi-phase, optimizing, includes an interpretive mode and a type inferer, and provides code generators to C and TypeScript.

  • Playground
  • Siek and Taha, 2006
  • Type Inference for Gradual Typing (Siek and Vachharajani, 2008)

Typed Assembly

• TAL: A compiler from a System F-like language to the Typed Assembly Language of Morrisett, et.al. 1998. Also includes a compiler to x86 assembly using Linear Scan Register Allocation (Poletto & Sarkar 1999).
  • Playground

Subtyping

• HO21: An implementation of the algorithmic duotyping calculus invented by Huang and Oliveira in Distributing Intersection and Union Types with Splits and Duality (2021). The calculus includes union, intersection, and arrow types in the presence of non-trivial distributivity rules. The authors' duotyping algorithm is somewhat novel in that it computes subtyping relationship entirely on surface types of the language, without normalizing to a form like DNF. This implementation includes a type-derivation tree generator.

  • Playground
  • Huang and Oliveira, 2021

• simple_sub: A type system that supports type inference in the presence of subtyping and polymorphism, as described by Parreaux's The Simple Essence of Algebraic Subtyping (2020). Parreaux's work distills Dolan's 2017 thesis on Algebraic Subtyping into a simpler core.

Dependent Types

• deptypes: A dependent type theory as described in Chapter 2 of Pierce's Advanced Topics in Types and Programming Languages.

• more deptypes: Additional, alternate implementations of the basic dependently-typed lambda calculus.

Effects and Coroutines

• fx_cap: implements effect handlers via monadic translation of the capability-passing style.

• co_lc: a lambda calculus with stackful coroutines and defunctionalized calls. Targets a bytecode stack machine.

  • Playground

Roc

cor is a minimalization of Roc used for experimenting on the language and its compiler.

• cor/uls: A language with "unspecialized lambda sets", a novel extension of the Hindley-Milner type system that supports efficient resolution of ad-hoc polymorphic usages (a-la typeclasses) during unification.

  • Documentation
  • Playground

• cor/refine: An experimental extension of Roc with refinement of types bound in branch patterns. Provides a flow-typing-like ergonomics for a unification-based HM system.

  Includes an compiler of pattern matching to decision trees, and various other optimizations.

  • Playground

• cor/easy_tags: An experimental extension of Roc with polymorphic variants' type variables elided in output positions.

  • Playground

• cor/compose_fx: A demonstration of composable effects as designed in Roc.

  • Playground

plts's Issues

[gtlc] Optimize: remove unused parameters/variables

Finding unused variables is trivial, but removing them safely is trickier. If we remove an unused parameter, we need to update all places a value for that parameter is passed, which is non-trivial to figure out (consider using a graph representation of types here to make this easier; we only need to update the type once and then look at all values elaborated with that type).

The other issue to be careful of is the interaction with references. This is best illustrated by an example; consider the program

let a = ref (\x: _. 0) in
a := (\x: nat. x);
!a 1

applying the optimization naively would yield

let a = ref (\: 0) in
a := (\x: nat. x);
!a ()

but the problem is that a now has the type ref ([] -> nat), but then assigned a value of type [nat] -> nat, and the optimized-away call at the end is now unsound.

Nevertheless there are ways to handle this; as an initial pass, we could simply avoid modifying functions later used inside references.

[gtlc] Support references

Polymorphic variants for asti

Full CPS conversion for fx-cap

[gtlc] Garbage Collection and unboxing per data flow proofs

Closure conversion and defunctionalization for co_lc

Symbol table for co_lc

[gtlc] Better UX for inferred types

• Mark inferred types as `T, not just when being inferred
• Autofix/hover provider to show inferred type in playground
• Make program expression printing prettier