import Revision from "../components/revision.tsx" import {Helmet} from "react-helmet"; import {Box, ThemeProvider, BaseStyles} 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

• cor/lss: A demonstration of lambda-set specialization as implemented in Roc. Supports composable effects, as in compose_fx.

  • Playground