Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Implementation

Two Syntactic Categories

The AST mirrors the type system’s value-computation split. Every term is either a value or a computation, and the two are represented by distinct enums that recursively refer to each other only at the modality boundaries.

#![allow(unused)]
fn main() {
use crate::errors::Span;
#[derive(Debug, Clone)]
pub enum Term {
    Val(Box<Value>),
    Comp(Box<Comp>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Comp {
    Return(Box<Value>, Span),
    Force(Box<Value>, Span),
    Abs(String, ValType, Box<Comp>, Span),
    App(Box<Comp>, Box<Value>, Span),
    To(Box<Comp>, String, Box<Comp>, Span),
    Let(String, Box<Value>, Box<Comp>, Span),
    If(Box<Value>, Box<Comp>, Box<Comp>, Span),
    Prim(PrimOp, Box<Value>, Box<Value>, Span),
}
#[derive(Debug, Clone, PartialEq, Copy)]
pub enum PrimOp {
    Add,
    Sub,
    Mul,
    Eq,
    Lt,
}
#[derive(Debug, Clone, PartialEq)]
pub enum ValType {
    Int,
    Bool,
    Unit,
    Pair(Box<ValType>, Box<ValType>),
    U(Box<CompType>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum CompType {
    F(Box<ValType>),
    Arrow(Box<ValType>, Box<CompType>),
}
impl PrimOp {
    pub fn name(self) -> &'static str {
        match self {
            PrimOp::Add => "add",
            PrimOp::Sub => "sub",
            PrimOp::Mul => "mul",
            PrimOp::Eq => "eq",
            PrimOp::Lt => "lt",
        }
    }

    pub fn result(self) -> ValType {
        match self {
            PrimOp::Add | PrimOp::Sub | PrimOp::Mul => ValType::Int,
            PrimOp::Eq | PrimOp::Lt => ValType::Bool,
        }
    }
}
impl Value {
    pub fn span(&self) -> Span {
        match self {
            Value::Var(_, s)
            | Value::Int(_, s)
            | Value::Bool(_, s)
            | Value::Unit(s)
            | Value::Pair(_, _, s)
            | Value::Thunk(_, s) => s.clone(),
        }
    }
}
impl Comp {
    pub fn span(&self) -> Span {
        match self {
            Comp::Return(_, s)
            | Comp::Force(_, s)
            | Comp::Abs(_, _, _, s)
            | Comp::App(_, _, s)
            | Comp::To(_, _, _, s)
            | Comp::Let(_, _, _, s)
            | Comp::If(_, _, _, s)
            | Comp::Prim(_, _, _, s) => s.clone(),
        }
    }
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Value::Var(n, _) => write!(f, "{}", n),
            Value::Int(n, _) => write!(f, "{}", n),
            Value::Bool(b, _) => write!(f, "{}", b),
            Value::Unit(_) => write!(f, "()"),
            Value::Pair(a, b, _) => write!(f, "({}, {})", a, b),
            Value::Thunk(c, _) => write!(f, "thunk ({})", c),
        }
    }
}
impl std::fmt::Display for Comp {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Comp::Return(v, _) => write!(f, "return {}", v),
            Comp::Force(v, _) => write!(f, "force {}", v),
            Comp::Abs(x, t, m, _) => write!(f, "\\{} : {}. {}", x, t, m),
            Comp::App(m, v, _) => write!(f, "{} {}", m, v),
            Comp::To(m, x, n, _) => write!(f, "{} to {}. {}", m, x, n),
            Comp::Let(x, v, m, _) => write!(f, "let {} = {} in {}", x, v, m),
            Comp::If(v, m, n, _) => write!(f, "if {} then {} else {}", v, m, n),
            Comp::Prim(op, a, b, _) => write!(f, "{} {} {}", op.name(), a, b),
        }
    }
}
impl std::fmt::Display for ValType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ValType::Int => write!(f, "Int"),
            ValType::Bool => write!(f, "Bool"),
            ValType::Unit => write!(f, "Unit"),
            ValType::Pair(a, b) => {
                write_val_factor(f, a)?;
                write!(f, " * ")?;
                write_val_factor(f, b)
            }
            ValType::U(c) => write!(f, "U ({})", c),
        }
    }
}
fn write_val_factor(f: &mut std::fmt::Formatter<'_>, t: &ValType) -> std::fmt::Result {
    match t {
        ValType::Pair(_, _) => write!(f, "({})", t),
        _ => write!(f, "{}", t),
    }
}
impl std::fmt::Display for CompType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            CompType::F(a) => match a.as_ref() {
                ValType::Pair(_, _) => write!(f, "F ({})", a),
                _ => write!(f, "F {}", a),
            },
            CompType::Arrow(a, c) => {
                write_val_factor(f, a)?;
                write!(f, " -> {}", c)
            }
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Value {
    Var(String, Span),
    Int(i64, Span),
    Bool(bool, Span),
    Unit(Span),
    Pair(Box<Value>, Box<Value>, Span),
    Thunk(Box<Comp>, Span),
}
}

The Var(name, span) constructor wraps a variable reference, with the span used for error reporting. The Int(n, span) and Bool(b, span) constructors wrap integer and boolean literals. The Unit(span) constructor is the singleton inhabitant of the unit type. The Pair(a, b, span) constructor is the product introduction form, with each component itself a value. The Thunk(c, span) constructor is the only place where a value embeds a computation: it wraps a Comp and the resulting value has type U C where C is the type of the wrapped computation. The boxed payload on Pair and Thunk keeps the enum size bounded despite the mutual recursion between Value and Comp.

#![allow(unused)]
fn main() {
use crate::errors::Span;
#[derive(Debug, Clone)]
pub enum Term {
    Val(Box<Value>),
    Comp(Box<Comp>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Value {
    Var(String, Span),
    Int(i64, Span),
    Bool(bool, Span),
    Unit(Span),
    Pair(Box<Value>, Box<Value>, Span),
    Thunk(Box<Comp>, Span),
}
#[derive(Debug, Clone, PartialEq, Copy)]
pub enum PrimOp {
    Add,
    Sub,
    Mul,
    Eq,
    Lt,
}
#[derive(Debug, Clone, PartialEq)]
pub enum ValType {
    Int,
    Bool,
    Unit,
    Pair(Box<ValType>, Box<ValType>),
    U(Box<CompType>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum CompType {
    F(Box<ValType>),
    Arrow(Box<ValType>, Box<CompType>),
}
impl PrimOp {
    pub fn name(self) -> &'static str {
        match self {
            PrimOp::Add => "add",
            PrimOp::Sub => "sub",
            PrimOp::Mul => "mul",
            PrimOp::Eq => "eq",
            PrimOp::Lt => "lt",
        }
    }

    pub fn result(self) -> ValType {
        match self {
            PrimOp::Add | PrimOp::Sub | PrimOp::Mul => ValType::Int,
            PrimOp::Eq | PrimOp::Lt => ValType::Bool,
        }
    }
}
impl Value {
    pub fn span(&self) -> Span {
        match self {
            Value::Var(_, s)
            | Value::Int(_, s)
            | Value::Bool(_, s)
            | Value::Unit(s)
            | Value::Pair(_, _, s)
            | Value::Thunk(_, s) => s.clone(),
        }
    }
}
impl Comp {
    pub fn span(&self) -> Span {
        match self {
            Comp::Return(_, s)
            | Comp::Force(_, s)
            | Comp::Abs(_, _, _, s)
            | Comp::App(_, _, s)
            | Comp::To(_, _, _, s)
            | Comp::Let(_, _, _, s)
            | Comp::If(_, _, _, s)
            | Comp::Prim(_, _, _, s) => s.clone(),
        }
    }
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Value::Var(n, _) => write!(f, "{}", n),
            Value::Int(n, _) => write!(f, "{}", n),
            Value::Bool(b, _) => write!(f, "{}", b),
            Value::Unit(_) => write!(f, "()"),
            Value::Pair(a, b, _) => write!(f, "({}, {})", a, b),
            Value::Thunk(c, _) => write!(f, "thunk ({})", c),
        }
    }
}
impl std::fmt::Display for Comp {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Comp::Return(v, _) => write!(f, "return {}", v),
            Comp::Force(v, _) => write!(f, "force {}", v),
            Comp::Abs(x, t, m, _) => write!(f, "\\{} : {}. {}", x, t, m),
            Comp::App(m, v, _) => write!(f, "{} {}", m, v),
            Comp::To(m, x, n, _) => write!(f, "{} to {}. {}", m, x, n),
            Comp::Let(x, v, m, _) => write!(f, "let {} = {} in {}", x, v, m),
            Comp::If(v, m, n, _) => write!(f, "if {} then {} else {}", v, m, n),
            Comp::Prim(op, a, b, _) => write!(f, "{} {} {}", op.name(), a, b),
        }
    }
}
impl std::fmt::Display for ValType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ValType::Int => write!(f, "Int"),
            ValType::Bool => write!(f, "Bool"),
            ValType::Unit => write!(f, "Unit"),
            ValType::Pair(a, b) => {
                write_val_factor(f, a)?;
                write!(f, " * ")?;
                write_val_factor(f, b)
            }
            ValType::U(c) => write!(f, "U ({})", c),
        }
    }
}
fn write_val_factor(f: &mut std::fmt::Formatter<'_>, t: &ValType) -> std::fmt::Result {
    match t {
        ValType::Pair(_, _) => write!(f, "({})", t),
        _ => write!(f, "{}", t),
    }
}
impl std::fmt::Display for CompType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            CompType::F(a) => match a.as_ref() {
                ValType::Pair(_, _) => write!(f, "F ({})", a),
                _ => write!(f, "F {}", a),
            },
            CompType::Arrow(a, c) => {
                write_val_factor(f, a)?;
                write!(f, " -> {}", c)
            }
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Comp {
    Return(Box<Value>, Span),
    Force(Box<Value>, Span),
    Abs(String, ValType, Box<Comp>, Span),
    App(Box<Comp>, Box<Value>, Span),
    To(Box<Comp>, String, Box<Comp>, Span),
    Let(String, Box<Value>, Box<Comp>, Span),
    If(Box<Value>, Box<Comp>, Box<Comp>, Span),
    Prim(PrimOp, Box<Value>, Box<Value>, Span),
}
}

The Return(v, span) constructor packages a value as the trivial computation that produces it, with type F A where A is the type of v. The Force(v, span) constructor crosses the boundary in the opposite direction: it requires v to have a thunk type U C and produces the wrapped computation of type C. The Abs(x, t, body, span) constructor is the lambda form, with x the binder name, t the binder’s annotated value type, and body the computation it abstracts over. The App(m, v, span) constructor applies the computation m to the value v; note that the argument position holds a Value rather than a Comp, which is how the calculus rules out passing computations directly. The To(m, x, n, span) constructor is the bind operator for the F modality: m to x. n runs m, binds its produced value to x, and continues with n. The Let(x, v, m, span) constructor is the value-level analogue, threading a value v through to a computation body without any monadic structure. The If(v, m, n, span) constructor is the conditional, with the scrutinee a value because conditions are pure. The Prim(op, a, b, span) constructor is a saturated primitive application, with both operands required to be values.

The type language is similarly split.

#![allow(unused)]
fn main() {
use crate::errors::Span;
#[derive(Debug, Clone)]
pub enum Term {
    Val(Box<Value>),
    Comp(Box<Comp>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Value {
    Var(String, Span),
    Int(i64, Span),
    Bool(bool, Span),
    Unit(Span),
    Pair(Box<Value>, Box<Value>, Span),
    Thunk(Box<Comp>, Span),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Comp {
    Return(Box<Value>, Span),
    Force(Box<Value>, Span),
    Abs(String, ValType, Box<Comp>, Span),
    App(Box<Comp>, Box<Value>, Span),
    To(Box<Comp>, String, Box<Comp>, Span),
    Let(String, Box<Value>, Box<Comp>, Span),
    If(Box<Value>, Box<Comp>, Box<Comp>, Span),
    Prim(PrimOp, Box<Value>, Box<Value>, Span),
}
#[derive(Debug, Clone, PartialEq, Copy)]
pub enum PrimOp {
    Add,
    Sub,
    Mul,
    Eq,
    Lt,
}
#[derive(Debug, Clone, PartialEq)]
pub enum CompType {
    F(Box<ValType>),
    Arrow(Box<ValType>, Box<CompType>),
}
impl PrimOp {
    pub fn name(self) -> &'static str {
        match self {
            PrimOp::Add => "add",
            PrimOp::Sub => "sub",
            PrimOp::Mul => "mul",
            PrimOp::Eq => "eq",
            PrimOp::Lt => "lt",
        }
    }

    pub fn result(self) -> ValType {
        match self {
            PrimOp::Add | PrimOp::Sub | PrimOp::Mul => ValType::Int,
            PrimOp::Eq | PrimOp::Lt => ValType::Bool,
        }
    }
}
impl Value {
    pub fn span(&self) -> Span {
        match self {
            Value::Var(_, s)
            | Value::Int(_, s)
            | Value::Bool(_, s)
            | Value::Unit(s)
            | Value::Pair(_, _, s)
            | Value::Thunk(_, s) => s.clone(),
        }
    }
}
impl Comp {
    pub fn span(&self) -> Span {
        match self {
            Comp::Return(_, s)
            | Comp::Force(_, s)
            | Comp::Abs(_, _, _, s)
            | Comp::App(_, _, s)
            | Comp::To(_, _, _, s)
            | Comp::Let(_, _, _, s)
            | Comp::If(_, _, _, s)
            | Comp::Prim(_, _, _, s) => s.clone(),
        }
    }
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Value::Var(n, _) => write!(f, "{}", n),
            Value::Int(n, _) => write!(f, "{}", n),
            Value::Bool(b, _) => write!(f, "{}", b),
            Value::Unit(_) => write!(f, "()"),
            Value::Pair(a, b, _) => write!(f, "({}, {})", a, b),
            Value::Thunk(c, _) => write!(f, "thunk ({})", c),
        }
    }
}
impl std::fmt::Display for Comp {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Comp::Return(v, _) => write!(f, "return {}", v),
            Comp::Force(v, _) => write!(f, "force {}", v),
            Comp::Abs(x, t, m, _) => write!(f, "\\{} : {}. {}", x, t, m),
            Comp::App(m, v, _) => write!(f, "{} {}", m, v),
            Comp::To(m, x, n, _) => write!(f, "{} to {}. {}", m, x, n),
            Comp::Let(x, v, m, _) => write!(f, "let {} = {} in {}", x, v, m),
            Comp::If(v, m, n, _) => write!(f, "if {} then {} else {}", v, m, n),
            Comp::Prim(op, a, b, _) => write!(f, "{} {} {}", op.name(), a, b),
        }
    }
}
impl std::fmt::Display for ValType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ValType::Int => write!(f, "Int"),
            ValType::Bool => write!(f, "Bool"),
            ValType::Unit => write!(f, "Unit"),
            ValType::Pair(a, b) => {
                write_val_factor(f, a)?;
                write!(f, " * ")?;
                write_val_factor(f, b)
            }
            ValType::U(c) => write!(f, "U ({})", c),
        }
    }
}
fn write_val_factor(f: &mut std::fmt::Formatter<'_>, t: &ValType) -> std::fmt::Result {
    match t {
        ValType::Pair(_, _) => write!(f, "({})", t),
        _ => write!(f, "{}", t),
    }
}
impl std::fmt::Display for CompType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            CompType::F(a) => match a.as_ref() {
                ValType::Pair(_, _) => write!(f, "F ({})", a),
                _ => write!(f, "F {}", a),
            },
            CompType::Arrow(a, c) => {
                write_val_factor(f, a)?;
                write!(f, " -> {}", c)
            }
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum ValType {
    Int,
    Bool,
    Unit,
    Pair(Box<ValType>, Box<ValType>),
    U(Box<CompType>),
}
}

The Int, Bool, and Unit constructors are the ground value types. The Pair(a, b) constructor is the product, with each component itself a value type. The U(c) constructor is the thunk modality, wrapping a CompType into a value type and pronouncing as “U of C”.

#![allow(unused)]
fn main() {
use crate::errors::Span;
#[derive(Debug, Clone)]
pub enum Term {
    Val(Box<Value>),
    Comp(Box<Comp>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Value {
    Var(String, Span),
    Int(i64, Span),
    Bool(bool, Span),
    Unit(Span),
    Pair(Box<Value>, Box<Value>, Span),
    Thunk(Box<Comp>, Span),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Comp {
    Return(Box<Value>, Span),
    Force(Box<Value>, Span),
    Abs(String, ValType, Box<Comp>, Span),
    App(Box<Comp>, Box<Value>, Span),
    To(Box<Comp>, String, Box<Comp>, Span),
    Let(String, Box<Value>, Box<Comp>, Span),
    If(Box<Value>, Box<Comp>, Box<Comp>, Span),
    Prim(PrimOp, Box<Value>, Box<Value>, Span),
}
#[derive(Debug, Clone, PartialEq, Copy)]
pub enum PrimOp {
    Add,
    Sub,
    Mul,
    Eq,
    Lt,
}
#[derive(Debug, Clone, PartialEq)]
pub enum ValType {
    Int,
    Bool,
    Unit,
    Pair(Box<ValType>, Box<ValType>),
    U(Box<CompType>),
}
impl PrimOp {
    pub fn name(self) -> &'static str {
        match self {
            PrimOp::Add => "add",
            PrimOp::Sub => "sub",
            PrimOp::Mul => "mul",
            PrimOp::Eq => "eq",
            PrimOp::Lt => "lt",
        }
    }

    pub fn result(self) -> ValType {
        match self {
            PrimOp::Add | PrimOp::Sub | PrimOp::Mul => ValType::Int,
            PrimOp::Eq | PrimOp::Lt => ValType::Bool,
        }
    }
}
impl Value {
    pub fn span(&self) -> Span {
        match self {
            Value::Var(_, s)
            | Value::Int(_, s)
            | Value::Bool(_, s)
            | Value::Unit(s)
            | Value::Pair(_, _, s)
            | Value::Thunk(_, s) => s.clone(),
        }
    }
}
impl Comp {
    pub fn span(&self) -> Span {
        match self {
            Comp::Return(_, s)
            | Comp::Force(_, s)
            | Comp::Abs(_, _, _, s)
            | Comp::App(_, _, s)
            | Comp::To(_, _, _, s)
            | Comp::Let(_, _, _, s)
            | Comp::If(_, _, _, s)
            | Comp::Prim(_, _, _, s) => s.clone(),
        }
    }
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Value::Var(n, _) => write!(f, "{}", n),
            Value::Int(n, _) => write!(f, "{}", n),
            Value::Bool(b, _) => write!(f, "{}", b),
            Value::Unit(_) => write!(f, "()"),
            Value::Pair(a, b, _) => write!(f, "({}, {})", a, b),
            Value::Thunk(c, _) => write!(f, "thunk ({})", c),
        }
    }
}
impl std::fmt::Display for Comp {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Comp::Return(v, _) => write!(f, "return {}", v),
            Comp::Force(v, _) => write!(f, "force {}", v),
            Comp::Abs(x, t, m, _) => write!(f, "\\{} : {}. {}", x, t, m),
            Comp::App(m, v, _) => write!(f, "{} {}", m, v),
            Comp::To(m, x, n, _) => write!(f, "{} to {}. {}", m, x, n),
            Comp::Let(x, v, m, _) => write!(f, "let {} = {} in {}", x, v, m),
            Comp::If(v, m, n, _) => write!(f, "if {} then {} else {}", v, m, n),
            Comp::Prim(op, a, b, _) => write!(f, "{} {} {}", op.name(), a, b),
        }
    }
}
impl std::fmt::Display for ValType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ValType::Int => write!(f, "Int"),
            ValType::Bool => write!(f, "Bool"),
            ValType::Unit => write!(f, "Unit"),
            ValType::Pair(a, b) => {
                write_val_factor(f, a)?;
                write!(f, " * ")?;
                write_val_factor(f, b)
            }
            ValType::U(c) => write!(f, "U ({})", c),
        }
    }
}
fn write_val_factor(f: &mut std::fmt::Formatter<'_>, t: &ValType) -> std::fmt::Result {
    match t {
        ValType::Pair(_, _) => write!(f, "({})", t),
        _ => write!(f, "{}", t),
    }
}
impl std::fmt::Display for CompType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            CompType::F(a) => match a.as_ref() {
                ValType::Pair(_, _) => write!(f, "F ({})", a),
                _ => write!(f, "F {}", a),
            },
            CompType::Arrow(a, c) => {
                write_val_factor(f, a)?;
                write!(f, " -> {}", c)
            }
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum CompType {
    F(Box<ValType>),
    Arrow(Box<ValType>, Box<CompType>),
}
}

The F(a) constructor is the returner modality, wrapping a value type into a computation type and pronouncing as “F of A”. The Arrow(a, c) constructor is the function arrow, with the argument a value type and the result a computation type. The arrow lives only in CompType, which is what makes CBPV functions reject computation-typed arguments. To pass a computation, the caller suspends it with thunk and passes the resulting U C value. The F and U constructors are the only places where the two type families touch each other, and they do so in opposite directions: U lifts a computation type to a value type, F lifts a value type to a computation type.

Primitive operations have fixed input and output types.

#![allow(unused)]
fn main() {
use crate::errors::Span;
#[derive(Debug, Clone)]
pub enum Term {
    Val(Box<Value>),
    Comp(Box<Comp>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Value {
    Var(String, Span),
    Int(i64, Span),
    Bool(bool, Span),
    Unit(Span),
    Pair(Box<Value>, Box<Value>, Span),
    Thunk(Box<Comp>, Span),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Comp {
    Return(Box<Value>, Span),
    Force(Box<Value>, Span),
    Abs(String, ValType, Box<Comp>, Span),
    App(Box<Comp>, Box<Value>, Span),
    To(Box<Comp>, String, Box<Comp>, Span),
    Let(String, Box<Value>, Box<Comp>, Span),
    If(Box<Value>, Box<Comp>, Box<Comp>, Span),
    Prim(PrimOp, Box<Value>, Box<Value>, Span),
}
#[derive(Debug, Clone, PartialEq)]
pub enum ValType {
    Int,
    Bool,
    Unit,
    Pair(Box<ValType>, Box<ValType>),
    U(Box<CompType>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum CompType {
    F(Box<ValType>),
    Arrow(Box<ValType>, Box<CompType>),
}
impl PrimOp {
    pub fn name(self) -> &'static str {
        match self {
            PrimOp::Add => "add",
            PrimOp::Sub => "sub",
            PrimOp::Mul => "mul",
            PrimOp::Eq => "eq",
            PrimOp::Lt => "lt",
        }
    }

    pub fn result(self) -> ValType {
        match self {
            PrimOp::Add | PrimOp::Sub | PrimOp::Mul => ValType::Int,
            PrimOp::Eq | PrimOp::Lt => ValType::Bool,
        }
    }
}
impl Value {
    pub fn span(&self) -> Span {
        match self {
            Value::Var(_, s)
            | Value::Int(_, s)
            | Value::Bool(_, s)
            | Value::Unit(s)
            | Value::Pair(_, _, s)
            | Value::Thunk(_, s) => s.clone(),
        }
    }
}
impl Comp {
    pub fn span(&self) -> Span {
        match self {
            Comp::Return(_, s)
            | Comp::Force(_, s)
            | Comp::Abs(_, _, _, s)
            | Comp::App(_, _, s)
            | Comp::To(_, _, _, s)
            | Comp::Let(_, _, _, s)
            | Comp::If(_, _, _, s)
            | Comp::Prim(_, _, _, s) => s.clone(),
        }
    }
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Value::Var(n, _) => write!(f, "{}", n),
            Value::Int(n, _) => write!(f, "{}", n),
            Value::Bool(b, _) => write!(f, "{}", b),
            Value::Unit(_) => write!(f, "()"),
            Value::Pair(a, b, _) => write!(f, "({}, {})", a, b),
            Value::Thunk(c, _) => write!(f, "thunk ({})", c),
        }
    }
}
impl std::fmt::Display for Comp {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Comp::Return(v, _) => write!(f, "return {}", v),
            Comp::Force(v, _) => write!(f, "force {}", v),
            Comp::Abs(x, t, m, _) => write!(f, "\\{} : {}. {}", x, t, m),
            Comp::App(m, v, _) => write!(f, "{} {}", m, v),
            Comp::To(m, x, n, _) => write!(f, "{} to {}. {}", m, x, n),
            Comp::Let(x, v, m, _) => write!(f, "let {} = {} in {}", x, v, m),
            Comp::If(v, m, n, _) => write!(f, "if {} then {} else {}", v, m, n),
            Comp::Prim(op, a, b, _) => write!(f, "{} {} {}", op.name(), a, b),
        }
    }
}
impl std::fmt::Display for ValType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ValType::Int => write!(f, "Int"),
            ValType::Bool => write!(f, "Bool"),
            ValType::Unit => write!(f, "Unit"),
            ValType::Pair(a, b) => {
                write_val_factor(f, a)?;
                write!(f, " * ")?;
                write_val_factor(f, b)
            }
            ValType::U(c) => write!(f, "U ({})", c),
        }
    }
}
fn write_val_factor(f: &mut std::fmt::Formatter<'_>, t: &ValType) -> std::fmt::Result {
    match t {
        ValType::Pair(_, _) => write!(f, "({})", t),
        _ => write!(f, "{}", t),
    }
}
impl std::fmt::Display for CompType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            CompType::F(a) => match a.as_ref() {
                ValType::Pair(_, _) => write!(f, "F ({})", a),
                _ => write!(f, "F {}", a),
            },
            CompType::Arrow(a, c) => {
                write_val_factor(f, a)?;
                write!(f, " -> {}", c)
            }
        }
    }
}
#[derive(Debug, Clone, PartialEq, Copy)]
pub enum PrimOp {
    Add,
    Sub,
    Mul,
    Eq,
    Lt,
}
}
#![allow(unused)]
fn main() {
use crate::errors::Span;
#[derive(Debug, Clone)]
pub enum Term {
    Val(Box<Value>),
    Comp(Box<Comp>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Value {
    Var(String, Span),
    Int(i64, Span),
    Bool(bool, Span),
    Unit(Span),
    Pair(Box<Value>, Box<Value>, Span),
    Thunk(Box<Comp>, Span),
}
#[derive(Debug, Clone, PartialEq)]
pub enum Comp {
    Return(Box<Value>, Span),
    Force(Box<Value>, Span),
    Abs(String, ValType, Box<Comp>, Span),
    App(Box<Comp>, Box<Value>, Span),
    To(Box<Comp>, String, Box<Comp>, Span),
    Let(String, Box<Value>, Box<Comp>, Span),
    If(Box<Value>, Box<Comp>, Box<Comp>, Span),
    Prim(PrimOp, Box<Value>, Box<Value>, Span),
}
#[derive(Debug, Clone, PartialEq, Copy)]
pub enum PrimOp {
    Add,
    Sub,
    Mul,
    Eq,
    Lt,
}
#[derive(Debug, Clone, PartialEq)]
pub enum ValType {
    Int,
    Bool,
    Unit,
    Pair(Box<ValType>, Box<ValType>),
    U(Box<CompType>),
}
#[derive(Debug, Clone, PartialEq)]
pub enum CompType {
    F(Box<ValType>),
    Arrow(Box<ValType>, Box<CompType>),
}
impl Value {
    pub fn span(&self) -> Span {
        match self {
            Value::Var(_, s)
            | Value::Int(_, s)
            | Value::Bool(_, s)
            | Value::Unit(s)
            | Value::Pair(_, _, s)
            | Value::Thunk(_, s) => s.clone(),
        }
    }
}
impl Comp {
    pub fn span(&self) -> Span {
        match self {
            Comp::Return(_, s)
            | Comp::Force(_, s)
            | Comp::Abs(_, _, _, s)
            | Comp::App(_, _, s)
            | Comp::To(_, _, _, s)
            | Comp::Let(_, _, _, s)
            | Comp::If(_, _, _, s)
            | Comp::Prim(_, _, _, s) => s.clone(),
        }
    }
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Value::Var(n, _) => write!(f, "{}", n),
            Value::Int(n, _) => write!(f, "{}", n),
            Value::Bool(b, _) => write!(f, "{}", b),
            Value::Unit(_) => write!(f, "()"),
            Value::Pair(a, b, _) => write!(f, "({}, {})", a, b),
            Value::Thunk(c, _) => write!(f, "thunk ({})", c),
        }
    }
}
impl std::fmt::Display for Comp {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Comp::Return(v, _) => write!(f, "return {}", v),
            Comp::Force(v, _) => write!(f, "force {}", v),
            Comp::Abs(x, t, m, _) => write!(f, "\\{} : {}. {}", x, t, m),
            Comp::App(m, v, _) => write!(f, "{} {}", m, v),
            Comp::To(m, x, n, _) => write!(f, "{} to {}. {}", m, x, n),
            Comp::Let(x, v, m, _) => write!(f, "let {} = {} in {}", x, v, m),
            Comp::If(v, m, n, _) => write!(f, "if {} then {} else {}", v, m, n),
            Comp::Prim(op, a, b, _) => write!(f, "{} {} {}", op.name(), a, b),
        }
    }
}
impl std::fmt::Display for ValType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ValType::Int => write!(f, "Int"),
            ValType::Bool => write!(f, "Bool"),
            ValType::Unit => write!(f, "Unit"),
            ValType::Pair(a, b) => {
                write_val_factor(f, a)?;
                write!(f, " * ")?;
                write_val_factor(f, b)
            }
            ValType::U(c) => write!(f, "U ({})", c),
        }
    }
}
fn write_val_factor(f: &mut std::fmt::Formatter<'_>, t: &ValType) -> std::fmt::Result {
    match t {
        ValType::Pair(_, _) => write!(f, "({})", t),
        _ => write!(f, "{}", t),
    }
}
impl std::fmt::Display for CompType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            CompType::F(a) => match a.as_ref() {
                ValType::Pair(_, _) => write!(f, "F ({})", a),
                _ => write!(f, "F {}", a),
            },
            CompType::Arrow(a, c) => {
                write_val_factor(f, a)?;
                write!(f, " -> {}", c)
            }
        }
    }
}
impl PrimOp {
    pub fn name(self) -> &'static str {
        match self {
            PrimOp::Add => "add",
            PrimOp::Sub => "sub",
            PrimOp::Mul => "mul",
            PrimOp::Eq => "eq",
            PrimOp::Lt => "lt",
        }
    }

    pub fn result(self) -> ValType {
        match self {
            PrimOp::Add | PrimOp::Sub | PrimOp::Mul => ValType::Int,
            PrimOp::Eq | PrimOp::Lt => ValType::Bool,
        }
    }
}
}

The arithmetic constructors Add, Sub, and Mul take two Int values and return an Int. The comparison constructors Eq and Lt take two Int values and return a Bool. The name method gives the surface-syntax keyword for pretty-printing and parsing, and the result method gives the value type that the primitive’s F-wrapped result delivers. Every primitive is a computation because it has an effect-like signature: its body is not a value, and its result must be sequenced into whatever needs it.

Bidirectional Checking

Type-checking is bidirectional with four entry points, one for each combination of value or computation against synthesis or checking.

#![allow(unused)]
fn main() {
pub fn synth_value(env: &Env, v: &Value) -> Result<ValType> {
    match v {
        Value::Int(_, _) => Ok(ValType::Int),
        Value::Bool(_, _) => Ok(ValType::Bool),
        Value::Unit(_) => Ok(ValType::Unit),
        Value::Var(n, s) => {
            env.get(n)
                .cloned()
                .ok_or_else(|| InferenceError::UnboundVariable {
                    name: n.clone(),
                    span: s.clone(),
                })
        }
        Value::Pair(a, b, _) => {
            let ta = Self::synth_value(env, a)?;
            let tb = Self::synth_value(env, b)?;
            Ok(ValType::Pair(Box::new(ta), Box::new(tb)))
        }
        Value::Thunk(c, _) => {
            let ct = Self::synth_comp(env, c)?;
            Ok(ValType::U(Box::new(ct)))
        }
    }
}
}

Values are simple enough to always synthesise. Literals produce their ground types. Variables look up in the environment. Pairs synthesise each component independently and assemble the product type. Thunks recursively synthesise their wrapped computation and wrap the result in U. There is no thunk-against-U checking shortcut, because synthesis is always cheap on the value side.

#![allow(unused)]
fn main() {
pub fn check_value(env: &Env, v: &Value, expected: &ValType) -> Result<()> {
    match (v, expected) {
        (Value::Thunk(c, _), ValType::U(ct)) => Self::check_comp(env, c, ct),
        (Value::Pair(a, b, _), ValType::Pair(ta, tb)) => {
            Self::check_value(env, a, ta)?;
            Self::check_value(env, b, tb)
        }
        _ => {
            let found = Self::synth_value(env, v)?;
            if &found == expected {
                Ok(())
            } else {
                Err(InferenceError::ValueMismatch {
                    expected: expected.clone(),
                    found,
                    span: v.span(),
                })
            }
        }
    }
}
}

The checker has only two structural rules: pair against pair, and thunk against U. Both push the expected type into the components. Every other value falls through to synthesis followed by an equality check. This matches the bidirectional idiom: structural rules where they help, synthesis otherwise.

The computation side is more interesting because the modalities have to be handled.

#![allow(unused)]
fn main() {
pub fn synth_comp(env: &Env, m: &Comp) -> Result<CompType> {
    match m {
        Comp::Return(v, _) => {
            let t = Self::synth_value(env, v)?;
            Ok(CompType::F(Box::new(t)))
        }
        Comp::Force(v, s) => {
            let t = Self::synth_value(env, v)?;
            match t {
                ValType::U(c) => Ok(*c),
                _ => Err(InferenceError::NotAThunk {
                    found: t,
                    span: s.clone(),
                }),
            }
        }
        Comp::App(f, arg, s) => {
            let ft = Self::synth_comp(env, f)?;
            match ft {
                CompType::Arrow(a, c) => {
                    Self::check_value(env, arg, &a)?;
                    Ok(*c)
                }
                _ => Err(InferenceError::NotAFunction {
                    found: ft,
                    span: s.clone(),
                }),
            }
        }
        Comp::Abs(x, t, body, _) => {
            let mut env1 = env.clone();
            env1.insert(x.clone(), t.clone());
            let c = Self::synth_comp(&env1, body)?;
            Ok(CompType::Arrow(Box::new(t.clone()), Box::new(c)))
        }
        Comp::To(m1, x, m2, _) => {
            let t1 = Self::synth_comp(env, m1)?;
            match t1 {
                CompType::F(a) => {
                    let mut env1 = env.clone();
                    env1.insert(x.clone(), *a);
                    Self::synth_comp(&env1, m2)
                }
                _ => Err(InferenceError::NotAProducer {
                    found: t1,
                    span: m1.span(),
                }),
            }
        }
        Comp::Let(x, v, m, _) => {
            let t = Self::synth_value(env, v)?;
            let mut env1 = env.clone();
            env1.insert(x.clone(), t);
            Self::synth_comp(&env1, m)
        }
        Comp::If(v, m1, m2, _) => {
            Self::check_value(env, v, &ValType::Bool)?;
            let c1 = Self::synth_comp(env, m1)?;
            let c2 = Self::synth_comp(env, m2)?;
            if c1 == c2 {
                Ok(c1)
            } else {
                Err(InferenceError::CompMismatch {
                    expected: c1,
                    found: c2,
                    span: m2.span(),
                })
            }
        }
        Comp::Prim(op, a, b, _) => {
            Self::check_value(env, a, &ValType::Int)?;
            Self::check_value(env, b, &ValType::Int)?;
            Ok(CompType::F(Box::new(op.result())))
        }
    }
}
}

Return v synthesises F (synth_value v), packaging the produced value’s type into the returner type. Force v synthesises synth_value v and inspects the result: it must be U C for some C, and the synthesised type is C. The App case synthesises the function’s type, requires it to be an Arrow(A, C), checks the argument against A, and returns C. The Abs case extends the environment with the binder at its annotated value type and recursively synthesises the body, producing an Arrow whose argument is the annotation and whose result is the synthesised computation type. The To case synthesises the producer, requires the result to be F A for some A, extends the environment with the bound variable at A, and synthesises the continuation. The Let case threads a value type through. The If case checks the scrutinee at Bool, synthesises both branches, and requires them to agree. The Prim case checks both arguments at Int and returns the primitive’s result type wrapped in F.

#![allow(unused)]
fn main() {
pub fn check_comp(env: &Env, m: &Comp, expected: &CompType) -> Result<()> {
    match (m, expected) {
        (Comp::Abs(x, t, body, span), CompType::Arrow(a, c)) => {
            if t != a.as_ref() {
                return Err(InferenceError::ValueMismatch {
                    expected: (**a).clone(),
                    found: t.clone(),
                    span: span.clone(),
                });
            }
            let mut env1 = env.clone();
            env1.insert(x.clone(), t.clone());
            Self::check_comp(&env1, body, c)
        }
        (Comp::Return(v, _), CompType::F(a)) => Self::check_value(env, v, a),
        (Comp::If(v, m1, m2, _), c) => {
            Self::check_value(env, v, &ValType::Bool)?;
            Self::check_comp(env, m1, c)?;
            Self::check_comp(env, m2, c)
        }
        (Comp::To(m1, x, m2, _), c) => {
            let t1 = Self::synth_comp(env, m1)?;
            match t1 {
                CompType::F(a) => {
                    let mut env1 = env.clone();
                    env1.insert(x.clone(), *a);
                    Self::check_comp(&env1, m2, c)
                }
                _ => Err(InferenceError::NotAProducer {
                    found: t1,
                    span: m1.span(),
                }),
            }
        }
        (Comp::Let(x, v, m, _), c) => {
            let t = Self::synth_value(env, v)?;
            let mut env1 = env.clone();
            env1.insert(x.clone(), t);
            Self::check_comp(&env1, m, c)
        }
        _ => {
            let found = Self::synth_comp(env, m)?;
            if &found == expected {
                Ok(())
            } else {
                Err(InferenceError::CompMismatch {
                    expected: expected.clone(),
                    found,
                    span: m.span(),
                })
            }
        }
    }
}
}

The checker has structural rules for lambda against arrow, return against F, if-then-else against any computation type, and the sequencing forms against any computation type. Lambda checking compares the annotated argument type against the expected argument type and pushes the expected result type into the body. Return checking pushes the expected value type into the returned value. If checking pushes the expected type into both branches. Sequencing pushes the expected continuation type into the body of the To or Let. The fall-through is the usual synthesis-then-equality check.

Driver

The top-level entry point classifies the term as either a value or a computation and dispatches to the appropriate synthesiser.

#![allow(unused)]
fn main() {
use std::collections::BTreeMap;
use crate::ast::{Comp, CompType, Term, ValType, Value};
use crate::errors::{InferenceError, Result};
pub type Env = BTreeMap<String, ValType>;
pub struct Checker;
impl Checker {
    // Synthesize the type of a value.
    pub fn synth_value(env: &Env, v: &Value) -> Result<ValType> {
        match v {
            Value::Int(_, _) => Ok(ValType::Int),
            Value::Bool(_, _) => Ok(ValType::Bool),
            Value::Unit(_) => Ok(ValType::Unit),
            Value::Var(n, s) => {
                env.get(n)
                    .cloned()
                    .ok_or_else(|| InferenceError::UnboundVariable {
                        name: n.clone(),
                        span: s.clone(),
                    })
            }
            Value::Pair(a, b, _) => {
                let ta = Self::synth_value(env, a)?;
                let tb = Self::synth_value(env, b)?;
                Ok(ValType::Pair(Box::new(ta), Box::new(tb)))
            }
            Value::Thunk(c, _) => {
                let ct = Self::synth_comp(env, c)?;
                Ok(ValType::U(Box::new(ct)))
            }
        }
    }

    // Check a value against an expected type.
    pub fn check_value(env: &Env, v: &Value, expected: &ValType) -> Result<()> {
        match (v, expected) {
            (Value::Thunk(c, _), ValType::U(ct)) => Self::check_comp(env, c, ct),
            (Value::Pair(a, b, _), ValType::Pair(ta, tb)) => {
                Self::check_value(env, a, ta)?;
                Self::check_value(env, b, tb)
            }
            _ => {
                let found = Self::synth_value(env, v)?;
                if &found == expected {
                    Ok(())
                } else {
                    Err(InferenceError::ValueMismatch {
                        expected: expected.clone(),
                        found,
                        span: v.span(),
                    })
                }
            }
        }
    }

    // Synthesize the type of a computation when possible.
    pub fn synth_comp(env: &Env, m: &Comp) -> Result<CompType> {
        match m {
            Comp::Return(v, _) => {
                let t = Self::synth_value(env, v)?;
                Ok(CompType::F(Box::new(t)))
            }
            Comp::Force(v, s) => {
                let t = Self::synth_value(env, v)?;
                match t {
                    ValType::U(c) => Ok(*c),
                    _ => Err(InferenceError::NotAThunk {
                        found: t,
                        span: s.clone(),
                    }),
                }
            }
            Comp::App(f, arg, s) => {
                let ft = Self::synth_comp(env, f)?;
                match ft {
                    CompType::Arrow(a, c) => {
                        Self::check_value(env, arg, &a)?;
                        Ok(*c)
                    }
                    _ => Err(InferenceError::NotAFunction {
                        found: ft,
                        span: s.clone(),
                    }),
                }
            }
            Comp::Abs(x, t, body, _) => {
                let mut env1 = env.clone();
                env1.insert(x.clone(), t.clone());
                let c = Self::synth_comp(&env1, body)?;
                Ok(CompType::Arrow(Box::new(t.clone()), Box::new(c)))
            }
            Comp::To(m1, x, m2, _) => {
                let t1 = Self::synth_comp(env, m1)?;
                match t1 {
                    CompType::F(a) => {
                        let mut env1 = env.clone();
                        env1.insert(x.clone(), *a);
                        Self::synth_comp(&env1, m2)
                    }
                    _ => Err(InferenceError::NotAProducer {
                        found: t1,
                        span: m1.span(),
                    }),
                }
            }
            Comp::Let(x, v, m, _) => {
                let t = Self::synth_value(env, v)?;
                let mut env1 = env.clone();
                env1.insert(x.clone(), t);
                Self::synth_comp(&env1, m)
            }
            Comp::If(v, m1, m2, _) => {
                Self::check_value(env, v, &ValType::Bool)?;
                let c1 = Self::synth_comp(env, m1)?;
                let c2 = Self::synth_comp(env, m2)?;
                if c1 == c2 {
                    Ok(c1)
                } else {
                    Err(InferenceError::CompMismatch {
                        expected: c1,
                        found: c2,
                        span: m2.span(),
                    })
                }
            }
            Comp::Prim(op, a, b, _) => {
                Self::check_value(env, a, &ValType::Int)?;
                Self::check_value(env, b, &ValType::Int)?;
                Ok(CompType::F(Box::new(op.result())))
            }
        }
    }

    pub fn check_comp(env: &Env, m: &Comp, expected: &CompType) -> Result<()> {
        match (m, expected) {
            (Comp::Abs(x, t, body, span), CompType::Arrow(a, c)) => {
                if t != a.as_ref() {
                    return Err(InferenceError::ValueMismatch {
                        expected: (**a).clone(),
                        found: t.clone(),
                        span: span.clone(),
                    });
                }
                let mut env1 = env.clone();
                env1.insert(x.clone(), t.clone());
                Self::check_comp(&env1, body, c)
            }
            (Comp::Return(v, _), CompType::F(a)) => Self::check_value(env, v, a),
            (Comp::If(v, m1, m2, _), c) => {
                Self::check_value(env, v, &ValType::Bool)?;
                Self::check_comp(env, m1, c)?;
                Self::check_comp(env, m2, c)
            }
            (Comp::To(m1, x, m2, _), c) => {
                let t1 = Self::synth_comp(env, m1)?;
                match t1 {
                    CompType::F(a) => {
                        let mut env1 = env.clone();
                        env1.insert(x.clone(), *a);
                        Self::check_comp(&env1, m2, c)
                    }
                    _ => Err(InferenceError::NotAProducer {
                        found: t1,
                        span: m1.span(),
                    }),
                }
            }
            (Comp::Let(x, v, m, _), c) => {
                let t = Self::synth_value(env, v)?;
                let mut env1 = env.clone();
                env1.insert(x.clone(), t);
                Self::check_comp(&env1, m, c)
            }
            _ => {
                let found = Self::synth_comp(env, m)?;
                if &found == expected {
                    Ok(())
                } else {
                    Err(InferenceError::CompMismatch {
                        expected: expected.clone(),
                        found,
                        span: m.span(),
                    })
                }
            }
        }
    }
}
pub enum TypeResult {
    Val(ValType),
    Comp(CompType),
}
impl std::fmt::Display for TypeResult {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            TypeResult::Val(t) => write!(f, "{}", t),
            TypeResult::Comp(c) => write!(f, "{}", c),
        }
    }
}
pub fn infer_type(term: &Term) -> Result<TypeResult> {
    let env = Env::new();
    match term {
        Term::Val(v) => Checker::synth_value(&env, v).map(TypeResult::Val),
        Term::Comp(c) => Checker::synth_comp(&env, c).map(TypeResult::Comp),
    }
}
}

The TypeResult enum reflects the value-computation split at the result level. A user-facing program reports its result type as one of two judgments depending on whether the top-level term is a value or a computation, and the pretty printer for TypeResult keeps the two cases distinct. This is what makes the CBPV reading visible to the user: a thunk is printed as U (F Int) rather than as some hidden encoding, and a returner is printed as F Int rather than collapsed to Int. The discipline keeps the operational reading of every well-typed term unambiguous.