A Brief on Blame Calculus

This is a short overview of Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Programming Languages and Systems (Lecture Notes in Computer Science), Springer, Berlin, Heidelberg, 1–16.

1. What is Blame Calculus and what is it for?

Blame calculus is an extension of a mixed-typed lambda calculus (i.e. containing both typed terms and untyped terms working on the catch-all type Dyn).

The purpose is to create a language where:

Additions to mixed-typed calculus

It features the following extensions to the type system:

It features the following extensions to the expression list:

A blame on $p$ can either be

\[ (\left\langle S \rightarrow T \Leftarrow S' \rightarrow T'\right\rangle ^p f)(v : S) \longrightarrow \left\langle T \Leftarrow T'\right\rangle ^p\left(f \left(\left\langle S' \Leftarrow S\right\rangle ^{\overline{p}}v\right)\right) \]

(notice the flip from $p$ to $\overline p$ on the cast of $v$)

Subtyping in Blame Calculus

Instead of the standard subtyping relation, which is undecidable in Blame Calculus (due to refinement types), it opts to an equally powerful system called positive (safe casts without positive blames) (denoted as $S <:^+ T$), negative ($S <:^– T$) and naive ($S <:_n T$) (which means $S <:^+ T$ and $T <:^– S$).

Unlike standard subtyping which is contravariant on the argument and covariant on the return type, naive subtyping is covariant on both sides.


Two additional syntax extensions are made in order to mix typed and untyped expressions:

2. Remarks

The central result of the paper, the Blame Theorem, states that:

Let $t$ be a well-typed term with a subterm $\left\langle T \Leftarrow S\right\rangle ^p s$ containing the only occurrences of $p$ in $t$. Then: – If $S <:^+ T$ then $t \not\longrightarrow^* \Uparrow p$. – If $S <:^– T$ then $t \not\longrightarrow^* \Uparrow \overline p$. – If $S <: T$ then $t$ will not blame on either $p$ nor $\overline p$.

In other words, from the decidable positive/negative subtyping relations, we can safely deduce which casts will not create a positive or negative blame.

This solidifies the intuition of upcasting/downcasting in the simple OOP sense, and allows us to extend this blame calculus with more structures, as long as the subtyping relations are still decidable.

3. Semantics

Please refer to the paper.