Some Background:
- Gradual typing
-
Type systems that provide capability of controlling degree of static typing by annotating function parameters with types (or not) ([2])
- Contracts
-
Lightweight form of gradual typing, enforcing types dynamically using assertions
-
Advantageous because you can implement contracts for untyped and typed languages as a library
-
- Blame
-
- Positive blame
-
The subject (function) does not satisfy a contract
- Negative blame
-
The context (caller) does not respect a contract
Contracts
Example 1: First-Order Contract
f: int[> 9] -> int[0,99]
The contract compiler inserts code to check proper range of arguments and return values.
val rec f = λx. x + 100
If f’s result is not in the proper range, f is blamed itself (positive blame)
f 5
If x is not in the proper range on calling, f’s caller is blamed (negative blame).
Example 2: Higher-Order Functions
- Higher-order function
-
Functions that accept others as arguments or yield functions as results
g: (int[> 9] -> int[0,99]) -> int[0,99]
g accepts int → int functions and must apply them to ints larger than 9, which must return ints between 0 and 99.
g should accept functions without explicit contracts (g(λx.50)) and functions whose behavior depends on context.
Key point in [3] is that contract checker waits until the higher-order procedure is applied, providing a witness to the contract violation enabling proper assignment of blame.
In [3], they create a Contract Calculus to how types and contracts interact.
Blame
Intersection and Union Types
- Intersection types
-
-
if a value has type \(S\) and \(T\), it can be assigned the intersection type \(S \cap T\)
-
Useful for encoding overloaded functions (see below), mixins, multiple inheritance
-
- Union types
-
-
a term of type \(S\) or \(T\) may be viewed as having type \(S \cup T\)
-
Useful for encoding uncertain data from branching code
-
A context that wants to use a value of union type \(S \cup T\) must be prepared to deal with both \(S\) and \(T\) because no way to distinguish
-
Sidenote:
When we say "union types" here, we mean "non-disjoint union types", which are different from "disjoint union types."
Disjoint union types are: * sum type: set of values drawn from exactly two given types * variant type: labelled generalization of sums
An Example
function f(x) {
if (typeof x === 'boolean') {
if (x) return 'hello world'; else return !x;
}
return (x+10);
}Here, the function \(f\) has type \(\text{Bool} \rightarrow (\text{String} \cup \text{Bool}) \cap (\text{Int} \rightarrow \text{Int})\).
Why Intersection and Union Types make Blame Hard
Sub-contracts can be violated without implying that a top-level contract was violated (i.e. contract can fail without necessarily causing an error).
For example, caller of f can violate domain type in left branch of intersection if they satisfy domain type of right branch.
Their contributions
-
Extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, for the first time giving a uniform treatment to both.
-
Define blame allocation for intersection and union that supports uniform monitoring rules, stratifying blame allocation into two phases: blame assignment and blame resolution.
-
Providing a new definition of contract satisfaction in terms of blame behaviour.
Also Read:
[1] J. Williams, J. G. Morris, and P. Wadler, “The Root Cause of Blame: Contracts for Intersection and Union Types,” Proc. ACM Program. Lang., vol. 2, no. OOPSLA, pp. 134:1–134:29, Oct. 2018.
[2] J. G. Siek and W. Taha, “Gradual Typing for Functional Languages,” in In Scheme and Functional Programming Workshop, 2006, pp. 81–92.
[3] R. B. Findler and M. Felleisen, “Contracts for Higher-Order Functions,” in Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, 2002, pp. 48–59.
[4] P. Wadler and R. B. Findler, “Well-Typed Programs Can’t Be Blamed,” in Programming Languages and Systems, 2009, pp. 1–16.