We propose a language design where types can be enriched by tags corresponding to predicates written by the programmer. For instance, int&positive is a type, where positive is a user-defined boolean function on integers. Expressions of type int&positive are obtained by an explicit check construct, analogous to cast, e.g., (positive) 2. In this way, the fact that the value of an expression is guaranteed to succeed a runtime check is a static property which can be controlled by the type system. We formalize our proposal as an extension of the simply-typed lambda calculus, and prove, besides soundness, the fact that expressions of tagged types reduce to values which satisfy the corresponding predicates.
It is very common in programming that an application needs to handle only values which satisfy properties which can be checked through user-defined code. As a very simple example, integer numbers which are odd, or positive, or prime. In nominally typed languages, it is possible to declare specialized types which enforce/encode such invariants. This is obtained by performing runtime checks on the arguments of the constructor of the new type. There are two variations of this technique, the first is wrapping the original type, and the second is extending it. We describe them, by examples, using Java syntax.
The first solution is illustrated by the example of odd numbers: class Odd { public final int inner ; public Odd ( int inner ){ if ( inner %2==0){// not odd
throw new Error (...); } Copyright c by the paper’s authors. Copying permitted for private and academic purposes. this . inner = inner ; Here we encode by wrapping, in such a way that all instances of Odd will always contain an odd number. In particular, every method taking as input an Odd argument myOdd can rely on the (static) guarantee that myOdd.inner is an odd number.
The second solution is illustrated by an example of points with positive coordinates: class Point { int x; int y ;...} class PositivePoint extends Point { public PositivePoint ( int x , int y ){ super (x ,y );// checks parent invariant if (x <0 || y <0){// not positive
throw new Error (...); } Here we encode by extending the original type (class), calling the super constructor and then checking for more properties. Again, every method taking in input a PositivePoint may assume that the coordinates are positive numbers.
Both patterns could be verified by tools like Spec# [
– Anyway, both techniques require some amount of boilerplate code. We propose an alternative approach, whose goal is to synthesize the core concept behind these techniques: a user-defined predicate is checked on a value, and, in case of success, the value gets a more specific type, that keeps track of the success of the runtime test. For instance, we can declare two functions checking whether an integer is odd or positive, respectively: bool odd ( int i ){ return i %2!=0;} bool positive ( int i ){ return i >=0;} 4 Viper requires to encode the invariant as constructor postcondition, and to repeat it in the method precondition, while Spec# needs the assertion to be explicitly stated in the class contract, and allows strengthening of superclass invariants (as needed in PositivePoint).
Then, we can convert an integer to an odd, or to a positive, by a check construct, which has a cast-inspired syntax, and indeed can be seen as a generalization of cast:5 ( odd )35// ok ( positive ) -23 // runtime error ( positive )( odd )79 // checks chain
The expressions above have, respectively, tagged types: int&odd, int&positive, and int&odd&positive. Tagged types are nominal, since tags are predicate names, and behave as intuitively expected: tag sequences can be seen as sets (order and repetition are immaterial), and subtyping corresponds to set inclusion. They can be used, e.g., as types of local variables: int & positive & odd myInt =( positive )( odd )79 int & positive anotherInt = myInt // safe , thanks to subtyping or as types of function parameters/result: int & positive factorial ( int & positive n ){ if (n ==0){ return 1;} return n * factorial (( positive ) n -1); } Note that the function does not need to check whether the argument is positive (to avoid non termination), since this is ensured by the parameter type. However, we need the check to perform the recursive call.
The paper is organized as follows. We formalize our proposal and prove its expected properties in Sect.2. In Sect.3 we discuss related work, and present our conclusions and further work in Sect.4. 2
In this section we introduce syntax, operational semantics, and type system of our calculus. Moreover, we prove expected properties.
Syntax We formalize our proposal as an extension of the simply-typed (call-byvalue) lambda calculus. Syntax is given in Fig.1. We assume an infinite set of predicate names P.
Expressions include expressions of the lambda calculus (variable, abstraction and application) and those defined with operators of primitive types, e.g., the two boolean constants, and the infinite set of integer constants, ranged over by n. For simplicity we omit other standard additional constructs, such as conditional, let-in and recursion. In addition, there are two novel expressions: – (P)e is a check expression, corresponding to a runtime check that (the value of) expression e satisfies predicate P. If the runtime check succeeds, then the result of the check expression will be the value of e tagged by P. In case of failure, the result will be an error tagged by P. 5 That is, a standard cast expression (C)e can be seen as a particular case of check expression where the predicate is instanceof C. p :: = P=λx : T .e e :: = x | λx : T .e | e1 e2 | true | false | n | . . . | (P)e | v&P[e] predicate definition expression check expression checking expression v :: = base value true | false | n | . . . primitive value | v&P tagged value V :: = λx : T .e | v value E :: = [ ] | E e | V E
(P)E | v&P[E] t :: = bool | int | . . .
| t&P T :: = T 1 → T 2 | t Γ :: = x1:T 1 . . . xn:T n Δ :: = P1:T 1 . . . Pn:T n evaluation context base type primitive type tagged type type type context predicate type context
Values are abstractions, or values of primitive types, or tagged values as explained above. Note that we take a stratified approach, where only non-functional values can be tagged. Tagged values are identified modulo order and repetitions of tags, e.g., 1&positive&odd and 1&odd&positive are the same value. Operational Semantics The reduction relation e → e0 assumes a given predicate table PT = p1 . . . pn, which is a sequence of predicate definitions which associate to a predicate name a lambda expression (expected to be a predicate, that is, to return a boolean value). We assume, as usual, that order of definitions is immaterial, and there are no multiple definitions for the same predicate name. That is, the predicate table can be seen as a (partial) map from predicate names to predicates.
Reduction rules are given in Fig.2. (Ctx)
e → e0
E[e] → E[e0] (App) (λx : T .e) V → e[V/x]
(Ctx-Err) E[error P] → error P (Check) (P)v → v&P[(λx : T .e) v] vPTno(Pt)of=shλaxp:eTv.0e&P (No-Check) (P)v&P → v&P
The first two rules are standard contextual closure and error propagation rules. Evaluation contexts, given in Fig.1, are as expected. The third rule is (callby-value) application rule. We denote by e[e0/x] the standard capture-avoiding substitution of occurrences of x in e by e0.
The novel rule ( C h e c k ) models starting the runtime check that predicate named P holds on value v, by triggering the evaluation of the corresponding predicate application. This rule is applied when v is not tagged by P yet. Otherwise, this means that v is a value obtained through a previous check of predicate named P, hence it is useless to perform the check again, and the value is directly returned, as shown in rule ( N o - C h e c k ). Note that an implementation could keep the tags and follow the same strategy, avoiding useless checks, or be based on type erasure, but in this case checks should be repeated.
Type System Following the stratified approach mentioned above, there are two forms of types: – non-functional types, called base types, which are primitive types possibly tagged with a sequence of predicate names – functional types, which cannot be tagged.
As for tagged values, we assume that tagged types are identified modulo order and repetitions of tags, e.g., int&positive&odd and int&odd&positive are the same type.
The subtyping relation is given in Fig.3. Rule ( S u b - Tag ) expresses the expected property that adding tags we get more specific types, other rules are standard.
The typing judgment, Γ ` e : T , says that expression e has type T under the type context Γ , where type contexts, Γ , are sequences of assignments of types to (Sub-Tag) t&P ≤ t
T 01 ≤ T 1 T 2 ≤ T 02 (Sub-Fun) T 1 → T 2 ≤ T 01 → T 02 (Sub-Tr) T 1 ≤ T 2 T 2 ≤ T 3 (Sub-Refl) T ≤ T
T 1 ≤ T 3 variables, see Fig.1. In Fig.4 we give the rules for deriving the typing judgment. We assume a given predicate type context Δ, which is a sequence of assignments of types to predicate names, see Fig.1.
(T-Var) Γ ` x : T Γ (x) = T (T-Abs)
Γ, x:T ` e : T 0 Γ ` λx : T .e : T → T 0 (T-App) Γ ` e1 : T → T 0 Γ ` e2 : T 2 T 2 ≤ T
Γ ` e1 e2 : T 0 (T-Check)
Γ ` e : t Δ(P) = t0 → bool Γ ` (P)e : t&P t ≤ t0 (T-Checking) Γ ` v : t Γ ` e : bool Δ(P) = t0 → bool Γ ` v&P[e] : t&P t ≤ t0
Γ ` v : t Δ(P) = t0 → bool (T-Error) Γ ` v&P[false] : T t ≤ t0
The first three rules of Fig.4 are standard rules of the simply-typed lambda calculus. We omit obvious rules for boolean and integer constants.
In rule ( T - C h e c k ), a check expression has the type of the argument tagged by the predicate name. The argument type t must be a subtype of the parameter type of the predicate. Note that the explicit subtyping condition, rather than an implicit subsumption rule, is necessary to assign to the check expression type t&P, which is possibly more specific than t0&P. For instance, the predicate positive requires an int, the argument could be an int&odd, and we want to get an int&odd&positive.
Rule ( T - C h e c k i n g ) enforces the restriction that, in a checking expression of type t&P, the value v must have type t, and the expression e must be of type bool, so that, if it converges to a value, then the value is either true or false. As for rule ( T - C h e c k ), the type of the value must be a subtype of the parameter type of the predicate.
Finally, rule ( T - E r ro r ) states that an error has any type.6 Since we encode errors as checking expressions where the expression is false7, we also require for uniformity the same conditions on v of the two previous rules. Results To prove soundness, expressed as usual by subject reduction and progress theorems, we assume that the predicates in the predicate table be well-typed w.r.t. the predicate type context, that is, for all P ∈ dom(PT), ∅ ` PT(P) : Δ(P). The proof of subject reduction relies on the (standard) substitution and context lemmas, that follow.
Lemma 1 (Substitution). If Γ, x:T 0 ` e : T , and Γ ` e0 : T 0, then Γ ` e[e0/x] : T .
Lemma 2 (Context). Let Γ ` E[e] : T , then Γ ` e : T 0 for some T 0, and if Γ ` e0 : T 00, with T 00 ≤ T 0, then Γ ` E[e0] : T , for all e0.
Theorem 1 (Subject reduction). Let e be such that, for some Γ and T , we have that Γ ` e : T . If e → e0, then Γ ` e0 : T 0 for some T 0 such that T 0 ≤ T . Proof. By induction on the rule used for e → e0.
If the rule applied is ( C t x ), then we have the thesis by induction hypothesis, using Lemma 2.
If the rule applied is ( C t x - E r r ), since error P is abbreviation for v&P[false], from ( T - e r ro r ) of Fig.4 we have that Γ ` v&P[false] : T . This proves the thesis.
If the rule applied is ( A p p ), then e = (λx : T 1.e1) V, e0 = e1[V/x]. The proof is standard by using typing rules ( T - A p p ), ( T - A b s ), and Lemma 1.
If the rule applied is ( C h e c k ), then 1. e = (P)v, 2. e0 = v&P[(λx : t0.ep) v], where PT(P) = λx : t0.ep.
From Γ ` (P)v : T , and typing rule ( T - C h e c k ) for some t and t0 we have that: T = t&P, Γ ` v : t, Δ(P) = t0 → bool, and t ≤ t0. Moreover, we know that ∅ ` PT(P) : t0 → bool. Therefore, also Γ ` PT(P) : t0 → bool. Applying rule ( T - a p p ) of Fig.4, we get that Γ ` (λx : t0.ep) V : bool. Therefore, from Γ ` v : t, Γ ` (λx : t0.ep) V : bool, Δ(P) = t0 → bool, and t ≤ t0, applying rule ( T - c h e c k i n g ) of Fig.4, we derive Γ ` e0 : T .
If the rule applied is ( N o - C h e c k ), then 1. e = (P)v&P[true], and 2. e0 = v&P[true]. 6 Recall that this is a standard typing rule in calculi with dynamic errors, needed to ensure that error propagation, see rule ( C t x - E r r ), preserves type. 7 We could have, alternatively, one more reduction step into an additional error expression, but we prefer this more succinct formulation. From Γ ` e : T , and typing rule ( T - C h e c k ) for some t and t0 and we have that: T = t&P, Γ ` v&P[true] : t, Δ(P) = t0 → bool, and t ≤ t0. From Γ ` v&P[true] : t, and typing rule ( T - C h e c k i n g ) we have that t is already of shape t00&P, for some t00. Therefore, t = T , and Γ ` e0 : t. tu
The proof of progress relies on the canonical forms lemma, which characterizes the shape of values of specific types.
Lemma 3 (Canonical forms).
1. If ` V : T 1 → T 2, then V = λx : T 1.e. 2. If ` V : bool, then either V = false, or V = true. 3. If ` V : int, then V = n.
4. If ` V : t&P, then V = v&P, i.e., V = v&P[true].
Theorem 2 (Progress). Let e be such that, for some T , we have that ∅ ` e : T . Then, either e = V, for some V, or e = error P, or e → e0 for some e0. Proof. If e 6= V, for some V, and e 6= error P, then either e = e1 e2, or e = (P)e1, or e = v&P[e1]. We consider the last two cases.
If e = (P)e1, and e1 is not a value or error, then by induction hypothesis e1 → e2. Therefore, (P)e1 → (P)e2 with ( C t x ) and E = (P)[ ]. If e1 = error P, then e → error P with ( C t x - E r r ) and E = (P)[ ]. If e1 = V, for some V, from ∅ ` (P)V : T , and typing rule ( T - C h e c k ), we have that, for some t and t0: T = t&P, ∅ ` V : t, Δ(P) = t0 → bool, and t ≤ t0. There are two cases for type t: either t = t0&P for some t0, that is, the type is already tagged with P, or not.
If t = t0&P for some t0, then, from Lemma 3.4, V = v&P, and rule ( n o - c h e c k ) is applicable. So e → v&P.
Otherwise rule ( c h e c k ) is applicable, and e → V&P[(λx : t0.ep) V].
If e = v&P[e1], and e1 is not a value, as in the previous case we can apply either rule ( C t x ) or ( C t x - E r r ).
If e1 = V, for some V, then, from ∅ ` v&P[e1] : T , and typing rule ( T C h e c k i n g ), we have that ∅ ` e1 : bool. Therefore, from Lemma 3.2, e1 = true or e1 = false. If e1 = true, then e is the value v&P, and if e1 = false, then e = error P. tu
In addition to soundness, we expect the following key property to hold: if an expression of a tagged type t&P reduces to a value, then this value satisfies predicate P. This is implied by subject reduction, plus the fact that a value v of a tagged type t&P satisfies predicate P. The latter property is true “by construction” in our calculus, provided that we consider as values only the subset of syntactic values which can be actually obtained by reduction. (Recall that checking expressions cannot be written by the programmer.) This is formalized by the notion of admissible expression below.
Definition 1. The expression e is admissible if, for all subexpressions v&P[e0] of e, we have (λx : T .ep) v →? e0, where PT(P) = λx : T .ep. Note that expressions written by the programmer are always admissible since they do not have subexpressions which are checking expressions. Lemma 4. If e is admissible, and e → e0, then e0 is admissible. Proof. By induction on the reduction rules. The interesting case is: (Check) (P)v → v&P[(λx : T .e) v] PT(P) = λx : T .e In this case, the thesis holds since (λx : T .e) v reduces to itself in zero steps. Theorem 3. Let e be an admissible expression such that, for some Γ and T , we have that Γ ` e : T . If e →? v&P, then (λx : T .ep) v →? true, where PT(P) = λx : T .ep.
Proof. By subject reduction (Theorem 1) and Lemma 4. 3
tu
tu
Constrained types and type invariants The work most closely related to ours are
likely constrained types of X10 [
Whiley [
Another important difference is that, in both X10 and Whiley, interpretation
of predicates is structural, that is, the meaning of a predicate is its definition.
Our interpretation is nominal instead, that is, , the meaning of a predicate is its
name, and the current definition is just an implementation of such concept. Under
our lens, predicate subtyping must be defined explicitly by the programmer, if
needed, see Sect.4.
8 The user is able to escape the confines of static type-checking using dynamic casts,
as in our approach.
Pre/post conditions In the style of runtime verification, a method can have
preconditions on its arguments that are dynamically checked when the method
is invoked. If the preconditions do not hold, the caller is blamed. Then, before
producing the result, the postcondition is verified. If the postcondition does not
hold, the method implementation is blamed, see, e.g., [
In our approach, a method can encode preconditions as types of its parameters, guaranteeing that the check is performed at the client side.9 Then, the method may cast the result to a more specific type, as a way to check the postcondition. An advantage of encoding a precondition as a type is that in this way the information that a value satisfies the precondition can be propagated to internal calls with the same precondition, rather than be checked again.
Runtime certification Our work can be seen as a (circular) variation over runtime
certification as in Athena [
Refinement types and blame calculi Refinement types, introduced in [
The blame calculus, see [
We have proposed and formalized a lightweight approach for handling values which are required to satisfy a property.
Compared to works discussed in the previous section, which generally rely on separate assertion language, structural interpretation of predicates, and (some) static verification, our design is less powerful, but easier to integrate and implement in existing languages.
In particular, we adopt a meta-circular approach, where the property is implemented by the programmer in the language itself. Note that, in this way, checking that a value has a given property, say P, could lead to divergence. However, the fact that an expression is guaranteed to succeed the corresponding runtime check is a static property which can be controlled by the type system. More precisely, an expression of type t&P can either reduce to a value of the same type, which is guaranteed to succeed the check, or lead to a dynamic error, or not terminate, as it happens for any other type.
Note also that by the nominal interpretation of predicates we gain the wellknown advantages of the nominal approach for software evolution: the meaning of a predicate can change, and a system with structural approach would be fragile.
Our design is in principle language independent. To integrate and implement
check expressions on top of an existing language, they could be translated, by a
pre-processing step, into the application of the corresponding predicate, a function
written in the source language. In an imperative language, analogously to what
is required in other proposals, predicates should be pure functions, and an object
could be ensured to invariantly satisfy a property only under some conditions,
the simplest being that the object is deeply immutable, that is, all its fields
are (recursively) immutable. More permissive conditions could be allowed by
combining the type system with modifiers for aliasing and immutability control,
see, e.g., [
As future work, we also discuss two extensions.
Predicate subtyping Certain predicates may be stronger than others, for example we expect greaterThan5 to imply positive. Since these predicates are defined as code, there is no general way to discover such implications automatically. However, we could offer a language construct for subtyping relations declared by the programmer, as usual for nominal types, for example, using again a Java-like syntax: bool positive ( int x) { return x >=0;} bool greaterThan5 ( int x) { return x >5;}
implies positive This extension could be encoded in the original language by expanding occurrences of the stronger predicate name to a sequence, for instance: int & greaterThan5 x =( greaterThan5 )34 would be expanded to int & greaterThan5 & positive x =( greaterThan5 )( positive )34 Refinement for pre-existing operations One limitation of the proposed approach is that existing operations are unaware of newly introduced properties.
For example, assume to have a Sum operation encoding the sum of two numbers, with type int*int->int. If we add the concept of positive, we know that, in a context where a and b are positive, Sum(a,b) should be positive; but in the current system it is just an int. An extension of our approach could allow: SumPosPos refines Sum : int & positive * int & positive -> int & positive
This extension could be encoded in the original language by declaring an auxiliary function SumPosPos which just calls Sum and casts the result to int&positive. In the case of an overpermissive refinement, the error can be traced back to the declaration of SumPosPos.
Acknowledgments. We are grateful to the anonymous reviewers for their useful suggestions, which led to substantial improvements.