The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamicallytyped code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this paper we prove that the polymorphic blame calculus satisfies relational parametricity. The proof relies on a stepindexed Kripke logical relation. The stepindexing is required to make the logical relation welldefined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their concrete types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence. To demonstrate the utility of parametricity in the polymorphic blame calculus, we derive two free theorems.
We present a type checker and stepper for the Polymorphic Blame Calculus. Programs written in the code box below may be typechecked and, if they pass, loaded into the stepper. Programs in the stepper are split into redex and context and may be evaluated either one step at a time or 100 steps at a time. The global name store is also displayed. Additionally, our artifact includes a step backwards button that reverses the last step taken.
Note: there are some syntactic differences from the presentation in the paper, which nonetheless we expect will be the primary reference for the language. These changes were made to eliminate the necessity of Unicode, reduce ambiguity in the grammar, and make the type checking algorithm syntaxdirected. We summarize these changes at the bottom of this page.
Examples from paper:
Additional examples:  Simple call  Omega  Factorial
Examples with errors:
Paper  Artifact  Description 

∀, λ, Λ, π_{1}, π_{2} 
forall, lam, Lam, pi1, pi2 
Greek letters and quantifiers are replaced by English keywords. 
⭑ 
* 
The dynamic type is written with the ASCII asterisk. 
e : T_{1} ⇒^{p} T_{2} 
e : T_{1} => T_{2} 
Cast expressions use an ASCII arrow and do not include the blame label. 
(e_{1}, e_{2}) 
<e_{1}, e_{2}> 
Pairs are enclosed in < and > instead of parentheses. 
T_{1} × T_{2} 
<T_{1}, T_{2}> 
Pair types are written with < and > instead of ×. 
let x = e_{1} in e_{2} 
let x : T = e_{1} in e_{2} 
Let expressions require a type annotation. 
exists X. T 
Existential types are provided by encoding into universals  
pack T_{1}, e in X. T_{2}
 Create an existential package from the value of e ,
hiding type T_{1} as X
inside T_{2} .
Expression e should have type
T_{2}[T_{1}/X] .
The result type is exists X. T_{2} . 

unpack[T_{1},T_{2}] X,x = e_{1} in e_{2} 
Unpack an existential. The expression e_{1}
should have type exists X. T_{1}
and expression e_{2} should have
type T_{2} . The variable
x has type T_{1} and is
in scope for e_{2} .
