Types and Effects

Type and Effect Systems

How can we reason about the effects of a program without using monads or uniqueness types?

An effect describes how an expression computes. Denoted by $\varphi$ annotation in the statics of the language.

Region-Based Memory Management

A region-inference judgment such as

$TE \vdash e ⇒ e' :(τ, ρ), \varphi$

where $TE$ is a type environment mapping variables with pairs $(\tau, \rho)$ of types and region variables (or place) and $\varphi$ is an effect (a finite set of region variables). It is read as:

in the type environment $TE$, the source expression $e$ is translated into a region-annotated expression $e'$, which has type $τ$, is placed in region $ρ$, and has effect $\varphi$.

$\varphi$ contains the superset of regions needed to evaluate $e$.

One of my misconceptions associated with regions was that they involve allocations only on the heap. But turns out the most common case is to have regions which only ever contain one value, called finite regions. A common optimization then is to allocate those on the stack.

(Partial) History

Partial history circa 2007. Credits: [François Pottier](http://pauillac.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf#page=5)
Partial history circa 2007. Credits: François Pottier



Edit this page

Graduate Student

Design and Verification of Programming Languages for realistic Quantum Computing