Skip to content

ayazhafiz/plts

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

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

Typed Assembly

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.

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

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.

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

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