implementation.md

Fundamental Constructs

Expressions

Expressions in Disp are programs and match the untyped lambda calculus. They are represented as follows:

enum Expr {
	Var,
	Lam { bind: Binding, expr: Expr },
	App { func: Expr, func: Expr },
}
enum Binding {
	None,
	End,
	Branch(Binding, Binding),
}

See how the Binding structure works here.

Judgements

struct Judgement {
	term: Expr,
	ty: Expr,
}

Judgements are considered valid if when the structure of term is encoded into the lambda calculus, and Expr::App(ty, encoding) beta-reduces to Expr::Var.

Contexts

struct Context {
	names: Map<String, Judgement>
}