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} </>); }
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
-
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.
-
lang_narrow: A language with unions, records, and flow typing. A checker, interpreter, and C code generator is implemented.
-
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
-
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.
- 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).
-
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.
-
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.
-
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.
-
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.
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.
-
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.
-
cor/easy_tags: An experimental extension of Roc with polymorphic variants' type variables elided in output positions.
-
cor/compose_fx: A demonstration of composable effects as designed in Roc.