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

WIP Premises

Premises are conditions above the line in a typing rule, evaluated left-to-right to thread the typing context.

Premise Result

Evaluating a premise yields a three-valued result:

  • $\text{Ok}(\Gamma’)$: the premise holds. $\Gamma’$ is the modified context.
  • $\text{Fail}$: the premise is definitively violated.
  • $\text{Partial}$: the premise is undecided due to incomplete information.

This mirrors the tree status lattice. Typing constraints are deferred when information is missing.

Premise Types

Definition: Ascription (Inference)

$\Gamma \vdash e : \tau$ infers the type of $e$ in context $\Gamma$ and unifies with $\tau$.

  1. Resolve binding $e$ to a tree node.
  2. Recursively type-check the subtree.
  3. Unify the inferred type with $\tau$.
Definition: Check

$\Gamma \triangleright e$ asserts that $e$ is well-typed in $\Gamma$ without constraining its type.

  1. Resolve binding $e$.
  2. Type-check the subtree.
  3. Succeed if status is $\text{Valid}$ or $\text{Partial}$; fail if $\text{Invalid}$.
Definition: Membership

$x \in \Gamma$ asserts that $x$ is bound in context $\Gamma$.

  1. Resolve binding $x$ to its text value.
  2. Look up text in $\Gamma$.
  3. Succeed if found; fail if not; return $\text{Partial}$ if $x$ is incomplete.
Definition: Context Extension

$\Gamma[x:\tau]$ extends the context with binding $x:\tau$.

  1. Resolve $x$ and $\tau$.
  2. Call $\Gamma.\text{extend}(x, \tau)$.
  3. Succeed with $\Gamma’ = \Gamma[x:\tau]$; fail if $x$ exists in $\Gamma$.

Operation (Equality / Subtyping)

$\tau_1\ \text{op}\ \tau_2$ where $\text{op} \in \{=, \subseteq\}$.

  • $\tau_1 = \tau_2$: unify the two types.
  • $\tau_1 \subseteq \tau_2$: check the subtype relation.

Both use three-valued logic, returning $\text{Ok}$, $\text{Fail}$, or $\text{Partial}$.

Evaluation Order

Premises evaluate strictly left-to-right. The context from premise $i$ is input to $i+1$, unless in no-propagate mode. Premise ordering is semantically significant: reordering changes binding availability.