11institutetext:  Institut für Informatik, Kiel University, Germany
11email<EMAIL_ADDRESS>
# Inferring Non-Failure Conditions
for Declarative Programs

Michael Hanus

###### Abstract

Unintended failures during a computation are painful but frequent during
software development. Failures due to external reasons (e.g., missing files,
no permissions) can be caught by exception handlers. Programming failures,
such as calling a partially defined operation with unintended arguments, are
often not caught due to the assumption that the software is correct. This
paper presents an approach to verify such assumptions. For this purpose, non-
failure conditions for operations are inferred and then checked in all uses of
partially defined operations. In the positive case, the absence of such
failures is ensured. In the negative case, the programmer could adapt the
program to handle possibly failing situations and check the program again. Our
method is fully automatic and can be applied to larger declarative programs.
The results of an implementation for functional logic Curry programs are
presented.

##  1 Introduction

The occurrence of failures during a program execution is painful but still
frequent when developing software systems. The main reasons for such failures
are

  * •

external, i.e., outside the control of the program, like missing files or
access rights, unexpected formats of external data, etc.

  * •

internal, i.e., programming errors like calling a partially defined operation
with unintended arguments.

External failures can be caught by exception handlers to avoid a crash of the
entire software system. Internal failures are often not caught since they
should not occur in a correct software system. In practice, however, they
occur during software development and even in deployed systems which results
in expensive debugging tasks. For instance, a typical internal failure in
imperative programs is dereferencing a pointer variable whose current value is
the null pointer (due to this often occurring failure, Tony Hoare called the
introduction of null pointers his “billion dollar
mistake”111http://qconlondon.com/london-2009/speaker/Tony+Hoare).

Although null pointer failures cannot occur in declarative programs, such
programs might contain other typical programming errors, like failures due to
incomplete pattern matching. For instance, consider the following operations
(shown in Haskell syntax) which compute the first element and the tail of a
list:

⬇

head (x:xs) = x tail (x:xs) = xs

In a correct program, it must be ensured that head and tail are not evaluated
on empty lists. If we are not sure about the data provided at run time, we can
check the arguments of partial operations before the application. For
instance, the following code snippet defines an operation to read a command
together with some arguments from standard input (the operation words breaks a
string into a list of words separated by white spaces) and calls an operation
processCmd with the input data:

⬇

s <- getLine

let ws = words s

case null ws of True $\rightarrow{}\\!\\!\\!$ readCmd

False $\rightarrow{}\\!\\!\\!$ processCmd (head ws) (tail ws)

By using the predicate null to check the emptiness of a list, it is ensured
that head and tail are not applied to an empty list in the False branch of the
case expression.

In this paper we present a fully automatic tool which can verify the non-
failure of this program. Our technique is based on analyzing the types of
arguments and results of operations in order to ensure that partially defined
operations are called with arguments of appropriate types. The principle idea
to use type information for this purpose is not new. For instance, with
_dependent types_ , as in Agda [34], Coq [10], or Idris [11], or _refinement
types_ , as in LiquidHaskell [38, 39], one can express restrictions on
arguments of operations. Since one has to prove that these restrictions hold
during the construction of programs, the development of such programs becomes
harder [37]. Another alternative, proposed in [21], is to annotate operations
with _non-fail conditions_ and verify that these conditions hold at each call
site by an external tool, e.g., an SMT solver [16]. In this way, the
verification is fully automatic but requires user-defined annotations and, in
some cases, also the verification of post-conditions or contracts to state
properties about result values of operations [22].

The main idea of this work is to _infer_ non-fail conditions of operations.
Since the inference of precise conditions is undecidable in general, we
approximate them by _abstract types_ , e.g., finite representations of sets of
values. In particular, our contributions are as follows.

  1. 1.

We define a _call type_ for each operation. If the actual arguments belong to
the call type, the operation is reducible with some rule.

  2. 2.

For each operation, we define _in/out types_ to approximate its input/output
behavior.

  3. 3.

For each call to an operation $g$ occurring in a rule defining $f$, we check,
by considering the call structure and in/out types, whether the call type of
$g$ is satisfied. If this is not the case, the call type of $f$ is refined and
we repeat the checks with the refined call type.

At the end of this process, each operation has some correct call type which
ensures that it does not fail on arguments belonging to its call type. Note
that the call type might be empty on always failing operations. To avoid empty
call types, one can modify the program code so that a different branch is
taken in case of a failure.

In order to make our approach accessible to various declarative languages, we
formulate and implement it in the declarative multi-paradigm language Curry
[25]. Since Curry extends Haskell by logic programming features and there are
also methods to transform logic programs into Curry programs [23], our
approach can also be applied to purely functional or logic programs. A
consequence of using Curry is the fact that programs might compute with
failures, e.g., it is not an immediate programming error to apply head and
tail to possibly empty lists. However, subcomputations involving such possibly
failing calls must be encapsulated so that it can be checked whether such a
computation has no result (this corresponds to exception handling in
deterministic languages). If this is done, one can ensure that the overall
computation does not fail even in the presence of encapsulated logic (non-
deterministic) subcomputations.

The paper is structured as follows. After sketching the basics of Curry in the
next section, we introduce call types and their abstraction in Sect. 3.
Section 4 defines in/out types and methods to approximate them. The main
section 5 presents our method to infer and check call types for all operations
in a program. We evaluate our approach in Sect. 6 before we conclude with a
discussion of related work. The correctness results and their proofs are
contained in the appendix.

##  2 Functional Logic Programming and Curry

As mentioned above, we develop and implement our method in Curry so that it is
also available for purely functional or logic programs. Curry [25] amalgamates
features from functional programming (demand-driven evaluation, strong typing,
higher-order functions) and logic programming (computing with partial
information, unification, constraints), see [6, 20] for surveys. The syntax of
Curry is close to Haskell222Variables and function names usually start with
lowercase letters and the names of type and data constructors start with an
uppercase letter. The application of $f$ to $e$ is denoted by juxtaposition
(“$f~{}e$”). [35]. In addition to Haskell, Curry applies rules with
overlapping left-hand sides in a (don’t know) non-deterministic manner (where
Haskell always selects the first matching rule) and allows _free_ (_logic_)
_variables_ in conditions and right-hand sides of defining rules. The
operational semantics is based on an optimal evaluation strategy [4]—a
conservative extension of lazy functional programming and logic programming.

Curry is strongly typed so that a Curry program consists of data type
definitions (introducing _constructors_ for data types) and _functions_ or
_operations_ on these types. As an example, we show the definition of two
operations on lists: the well-known list concatenation “++” and an operation
dup which returns some list element having at least two occurrences:333Note
that Curry requires the explicit declaration of free variables, as x in the
rule of dup, to ensure checkable redundancy. Anonymous variables, denoted by
an underscore, need not be declared.

⬇

[] ++ ys = ys dup xs | xs == _ ++ [x] ++ _ ++ [x] ++ _

(x:xs) ++ ys = x : (xs ++ ys) = x where x free

Since dup might deliver more than one result for a given argument, e.g., dup
[1,2,2,1] yields 1 and 2, it is also called a _non-deterministic operation_.
Such operations, which are interpreted as mappings from values into sets of
values [19], are an important feature of contemporary functional logic
languages. To express failing computations, there is also a predefined
operation failed which has no value.

$\begin{array}[]{lcl@{\hspace{5ex}}l}P&::=&D_{1}\ldots D_{m}\hfil\hskip
21.52771pt&\mbox{(program)}\\\ D&::=&f(x_{1},\ldots,x_{n})=e\hfil\hskip
21.52771pt&\mbox{(function definition)}\\\ e&::=&x\hfil\hskip
21.52771pt&\mbox{(variable) }\\\ &|&c(x_{1},\ldots,x_{n})\hfil\hskip
21.52771pt&\mbox{(constructor application) }\\\
&|&f(x_{1},\ldots,x_{n})\hfil\hskip 21.52771pt&\mbox{(function call) }\\\
&|&e_{1}~{}\mathit{or}~{}e_{2}\hfil\hskip 21.52771pt&\mbox{(disjunction) }\\\
&|&\mathit{let}~{}x_{1},\ldots,x_{n}~{}\mathit{free~{}in}~{}e\hfil\hskip
21.52771pt&\mbox{(free variables) }\\\
&|&\mathit{let}~{}x=e~{}\mathit{in}~{}e^{\prime}\hfil\hskip
21.52771pt&\mbox{(let binding) }\\\
&|&\mathit{case}~{}x~{}\mathit{of}~{}\\{p_{1}\to e_{1};\ldots;p_{n}\to
e_{n}\\}\hfil\hskip 21.52771pt&\mbox{(case expression) }\\\
p&::=&c(x_{1},\ldots,x_{n})\hfil\hskip 21.52771pt&\mbox{(pattern)}\end{array}$
Figure 1: Syntax of the intermediate language FlatCurry

Curry has more features than described so far.444Conceptually, Curry is
intended as an extension of Haskell although not all extensions of Haskell are
actually supported. Due to these numerous features, language processing tools
for Curry (compilers, analyzers,…) often use an intermediate language where
the syntactic sugar of the source language has been eliminated and the pattern
matching strategy is explicit. This intermediate language, called FlatCurry,
has also been used, apart from compilers, to specify the operational semantics
of Curry programs [1] or to implement a modular framework for the analysis of
Curry programs [24]. Since we will use FlatCurry to describe and implement our
inference method, we sketch the structure of FlatCurry programs.

The abstract syntax of FlatCurry is summarized in Fig. 1. A FlatCurry program
consists of a sequence of function definitions (for the sake of simplicity,
data type definitions are omitted), where each function is defined by a single
rule. Patterns in source programs are compiled into case expressions,
overlapping rules are joined by explicit disjunctions, and arguments of
constructor and function calls are variables (introduced in left-hand sides,
let expressions, or patterns). We will write ${\cal{F}}$ for the set of
defined operations and ${\cal{C}}$ for the set of constructors of a program.
In order to provide a simple definition of our inference method, we assume
that FlatCurry programs satisfy the following properties:

  * •

All variables introduced in a rule (parameters, free variables, let bindings,
pattern variables) have unique identifiers.

  * •

For the sake of simplicity, let bindings are non-recursive, i.e., all
recursion is introduced by functions (although our implemented tool supports
recursive bindings).

  * •

The patterns in each case expression are non-overlapping and cover all data
constructors of the type of the discriminating variable. Hence, if this type
contains $n$ constructors, there are $n$ branches without overlapping
patterns. This can be ensured by adding missing branches with failure
expressions (failed).

Usually, the front end of a Curry compiler transforms source programs into
such a form for easier compilation [3, 7]. For instance, the operation head is
transformed into the following FlatCurry program:

##  3 Call Types and Abstract Types

We consider a computation as _non-failing_ if it does not stop due to a
pattern mismatch or a call to failed. In order to infer conditions on
arguments of operations so that the evaluation of an operation does not fail,
we will analyze the rules of each operation.555Note that we do not consider
external failures of operations, like file access errors, since they need to
be handled differently. For instance, the operation head is defined by the
single rule

Since there is no rule covering the empty list, the condition for a non-
failing evaluation of head is the non-emptiness of the argument list.
Sometimes the exact condition requires more advanced descriptions. For
instance, consider the operation lastTrue defined by

⬇

lastTrue (x:y:ys) = lastTrue (y:ys)

The evaluation of a call lastTrue$\;l$ does not fail if the argument list $l$
ends with True. Although such lists could be finitely described using regular
types [15], such a description is impossible for arbitrary operations. For
instance, if some branch in a condition of an operation causes a failure but
the condition of the branch contains a function call, the failure is only
relevant if the function call terminates. Due to the undecidability of the
halting problem, we cannot hope to infer exact non-failure conditions.

Due to this general problem, we _approximate_ non-failure conditions so that
the evaluation of a call where the arguments satisfy the non-failure
conditions is non-failing. However, there might be successfully evaluable
calls which do not satisfy the inferred non-failure condition.

In order to support different structures to approximate non-failure
conditions, we do not fix a language for call types but assume that there is a
domain ${\cal{A}}$ of _abstract types_. Elements of this domain describe sets
of concrete _data terms_ , i.e., terms consisting of data constructors only.
There are various options for such abstract types, like depth-$k$ abstractions
[36] or regular types [15]. The latter have been used to infer success types
to analyze logic programs [18], whereas depth-$k$ abstractions were used in
the abstract diagnosis of functional programs [2] or in the abstraction of
term rewriting systems [8, 9]. Since regular types are more complex and
computationally more expensive, we use depth-$k$ abstractions in our examples.
In this domain, denoted by $A_{k}$, subterms exceeding the given depth $k$ are
replaced by a specific constant ($\top$) that represents any term. Since the
size of this domain is quickly growing for $k>1$, we use $k=1$ in examples,
i.e., terms are approximated by their top-level constructors. As we will see,
this is often sufficient in practice to obtain reasonable results.
Nevertheless, our technique and implementation is parametric over the abstract
type domain (results w.r.t. different domains are shown in Appendix 0.A).

If ${\cal{C}}$ is the set of data constructors, _depth-1 types_ can be simply
described by the set

${\cal{A}}_{1}=\\{D\subseteq{\cal{C}}\mid\mbox{all constructors of $D$ belong
to the same type}\\}\cup\\{\top\\}$

Hence, each element of ${\cal{A}}_{1}$ is either a set of data constructors of
the same type or $\top$. The latter denotes the set of all data terms when no
type information is available.

Following the framework of abstract interpretation [14], the meaning of
abstract values is specified by a concretization function $\gamma$. For
${\cal{A}}_{1}$, $\gamma$ is defined by

$\begin{array}[]{r@{~~}c@{~~}l}\gamma(\top)~{}~{}&=\hfil~{}~{}&\\{t\mid
t\mbox{~{}is a data term}\\}\\\ \gamma(D)~{}~{}&=\hfil~{}~{}&\\{t\mid
t=c(t_{1},\ldots,t_{n})\mbox{~{}is a data term with }c\in D\\}\end{array}$

Thus, $\varnothing$ is the bottom element of this domain w.r.t. the standard
ordering defined by

$\begin{array}[]{r@{~\sqsubseteq~}l@{\quad}l}a~{}\sqsubseteq~{}&\top&\mbox{for
any }a\\\ a_{1}~{}\sqsubseteq~{}&a_{2}&\mbox{if }a_{1}\subseteq
a_{2}\end{array}$

In the following, we present a framework for the inference of call types which
is parametric over the abstract domain ${\cal{A}}$. Thus, we assume that
${\cal{A}}$ is a lattice with an ordering $\sqsubseteq$, greatest lower bound
($\sqcap$) and least upper bound ($\sqcup$) operations, a least or bottom
element $\bot$, and a greatest or top element $\top$. Furthermore, for each
$n$-ary data constructor $c$, there is an _abstract constructor application_
$c^{\alpha}$ which maps abstract values $a_{1},\ldots,a_{n}$ into an abstract
value $a$ such that $c(t_{1},\ldots,t_{n})\in\gamma(a)$ for all
$t_{1}\in\gamma(a_{1}),\ldots,t_{n}\in\gamma(a_{n})$. For the domain
${\cal{A}}_{1}$, which we use in the following in concrete examples, this can
be defined by $c^{\alpha}(x_{1},\ldots,x_{n})=\\{c\\}$ (it could also be
defined by $c^{\alpha}(x_{1},\ldots,x_{n})=\top$ but this yields less precise
approximations).

We use ${\cal{A}}$ to specify _call types_ or _non-failure conditions_ for
operations. Let $f$ be a unary operation (the extension to more than one
argument is straightforward). A call type $C\in{\cal{A}}$ is _correct_ for $f$
if the evaluation of $f(t)$ is non-failing for any $t\in\gamma(C)$. For
instance, the depth-1 type $\\{\mbox{\small{:}}\\}$ is correct for the
operations head or tail defined above.

In order to verify the correctness of call types for a program, we have to
check whether each call of an operation satisfies its call type. Since this
requires the analysis of conditions and other operations (see the operation
readCmd defined in Sect. 1), we will approximate the input/output behavior of
operations, as described in the following section.

##  4 In/Out Types

To provide a fully automatic inference method for call types, we need some
knowledge about the behavior of auxiliary operations. For instance, consider
the operation null defined by

⬇

null [] = True

null (x:xs) = False

This operation is used in the definition of readCmd (see Sect. 1) to ensure
that head and tail are applied to non-empty lists. In order to verify this
property, we have to infer that, if null ws evaluates to False, the argument
is a non-empty list.

For this purpose, we associate an in/out type to each operation. An _in/out
type_ $\mathit{io}$ for an $n$-ary operation $f$ is a set of elements
containing a sequence of $n+1$ abstract types, i.e.,

$\mathit{io}\subseteq\\{a_{1}\cdots a_{n}\hookrightarrow a\mid
a_{1},\ldots,a_{n},a\in{\cal{A}}\\}$

The first $n$ components of each element approximate input values (where we
write $\varepsilon$ if $n=0$) and the last component approximate output values
associated to the inputs. An in/out type $\mathit{io}$ is _correct_ for $f$
if, for each value $t^{\prime}$ of $f(t_{1},\ldots,t_{n})$, there is some
$a_{1}\cdots a_{n}\hookrightarrow a\in\mathit{io}$ such that
$t_{i}\in\gamma(a_{i})$ ($i=1,\ldots,n$) and $t^{\prime}\in\gamma(a)$.

Thus, in/out types are disjunctions of possible input/output behaviors of an
operation. For instance, a correct in/out type of null w.r.t. ${\cal{A}}_{1}$
is

Another trivial and less precise in/out type is
$\\{\top\hookrightarrow\top\\}$.

In/out types allow also to express non-terminating operations. For instance, a
correct in/out type for the operation loop defined by

is $\\{\varepsilon\hookrightarrow\varnothing\\}$. The empty type in the result
indicates that this operation does not yield any value.

Similarly to call types, we approximate in/out types since the inference of
precise in/out types is intractable in general. For this purpose, we analyze
the definition of each operation and associate patterns to result values.
Result values are based on general information about the abstract result types
of operations. Therefore, we assume that there is a mapping
$R:{\cal{F}}\to{\cal{A}}$ which associates to each defined function
$f\in{\cal{F}}$ an abstract type $R(f)\in{\cal{A}}$ approximating the possible
values to which $f$ (applied to some arguments) can be evaluated. For
instance, $R(\mbox{\small{loop}})=\varnothing$,
$R(\mbox{\small{null}})=\\{\mbox{\small{False}},\mbox{\small{True}}\\}$, and
$R(\mbox{\small{head}})=\top$ (w.r.t. the domain ${\cal{A}}_{1}$).
Approximations for $R$ can be computed in a straightforward way by a fixpoint
computation. Using the Curry analysis framework CASS [24], this program
analysis can be defined in 20 lines of code—basically a case distinction on
the structure of FlatCurry programs.666See module Analysis.Values of the Curry
package https://cpm.curry-lang.org/pkgs/cass-analysis.html

$\begin{array}[]{r@{\hspace{2ex}}cl}\mbox{\sf Var}\hskip
8.61108pt&\Gamma~{}\vdash x:\\{\Gamma\hookrightarrow\Gamma(x)\\}&\mbox{($x$
variable)}\\\\[4.30554pt] \mbox{\sf Cons}\hskip 8.61108pt&\Gamma~{}\vdash
c(x_{1},\ldots,x_{n}):\\{\Gamma\hookrightarrow
c^{\alpha}(\Gamma(x_{1}),\ldots,\Gamma(x_{n}))\\}&\mbox{($c$
constructor)}\\\\[4.30554pt] \mbox{\sf Func}\hskip 8.61108pt&\Gamma~{}\vdash
f(x_{1},\ldots,x_{n}):\\{\Gamma\hookrightarrow R(f)\\}&\mbox{($f$
operation)}\\\\[4.30554pt] \mbox{\sf Or}\hskip
8.61108pt&{\displaystyle\frac{\Gamma~{}\vdash e_{1}:io_{1}\quad\Gamma~{}\vdash
e_{2}:io_{2}}{\Gamma~{}\vdash e_{1}~{}or~{}e_{2}:io_{1}\cup
io_{2}}}&\\\\[12.91663pt] \mbox{\sf Free}\hskip
8.61108pt&{\displaystyle\frac{\Gamma[\overline{x_{n}\mapsto\top}]\vdash
e:io}{\Gamma\vdash\mathit{let}~{}x_{1},\ldots,x_{n}~{}\mathit{free~{}in}~{}e:io}}&\\\\[12.91663pt]
\mbox{\sf Let}\hskip 8.61108pt&{\displaystyle\frac{\Gamma[x\mapsto\top]\vdash
e^{\prime}:io}{\Gamma\vdash let~{}x=e~{}in~{}e^{\prime}:io}}&\\\\[12.91663pt]
\mbox{\sf Case}\hskip 8.61108pt&{\displaystyle\frac{\Gamma_{1}\vdash
e_{1}:io_{1}~{}~{}\ldots~{}~{}\Gamma_{n}\vdash
e_{n}:io_{n}}{\Gamma\vdash\mathit{case}~{}x~{}\mathit{of}~{}\\{p_{1}\to
e_{1};\ldots;p_{n}\to e_{n}\\}:io_{1}\cup\ldots\cup io_{n}}}\\\\[12.91663pt]
\hskip 8.61108pt&\mbox{ where }p_{i}=c_{i}(\overline{x_{n_{i}}})\mbox{ and
}\Gamma_{i}=\Gamma[x\mapsto
c_{i}^{\alpha}(\overline{\top}),\overline{x_{n_{i}}\mapsto\top}]\end{array}$
Figure 2: Approximation of in/out types

Our actual approximation of in/out types is defined by the rules in Fig. 2. A
sequence $o_{1},\ldots,o_{n}$ of objects is abbreviated by $\overline{o_{n}}$.
We use a _type environment_ $\Gamma$ which maps variables into abstract types.
We denote by $\Gamma[x\mapsto e]$ the environment $\Gamma^{\prime}$ with
$\Gamma^{\prime}(x)=e$ and $\Gamma^{\prime}(y)=\Gamma(y)$ for all $x\neq y$.
The judgement $\Gamma\vdash e:\\{\overline{\Gamma_{k}\hookrightarrow
a_{k}}\\}$ is interpreted as “the evaluation of the expression $e$ in the
context $\Gamma$ yields a new context $\Gamma_{i}$ and result value of
abstract type $a_{i}$, for some $i\in\\{1,\ldots,k\\}$.” To infer an in/out
type $io$ of an operation $f$ defined by $f(x_{1},\ldots,x_{n})=e$, we derive
the judgement $\\{\overline{x_{n}\mapsto\top}\\}\vdash
e:\\{\overline{\Gamma_{k}\hookrightarrow a_{k}}\\}$ and return the in/out type

Thus, we derive an in/out type without any restriction on the arguments.

Let us consider the inference rules in more detail. In the case of variables
or applications, the type environment is not changed and the approximated
result is returned, e.g., the abstract type of the variable (rule Var), the
abstract representation of the constructor (rule Cons), or the approximated
result value of the operation (rule Func). Rule Or combines the results of the
different branches. Rules Free and Let add the new variables to the type
environment with most general types. Although one could refine these types, we
try to keep the analysis simple since this seems to be sufficient in practice.

The most interesting rule is Case. The results from the different branches are
combined, but inside each branch, the type of the discriminating variable $x$
is refined to the constructor of the branch. For instance, consider the
operation

If we analyze the in/out type with our rules, we start with the type
environment $\Gamma_{0}=\\{\mbox{\small{zs}}\mapsto\top\\}$. Inside the
branch, $\Gamma_{0}$ is refined to
$\Gamma_{1}=\\{\mbox{\small{zs}}\mapsto\\{\mbox{\small{[]}}\\}\\}$ and
$\Gamma_{2}=\\{\mbox{\small{zs}}\mapsto\\{\mbox{\small{:}}\\},\mbox{\small{x}}\mapsto\top,\mbox{\small{xs}}\mapsto\top\\}$,
respectively, so that the in/out type (w.r.t. ${\cal{A}}_{1}$) derived for
null is
$\\{\\{\mbox{\small{[]}}\\}\hookrightarrow\\{\mbox{\small{True}}\\},\\{\mbox{\small{:}}\\}\hookrightarrow\\{\mbox{\small{False}}\\}\\}$.

In our implementation, we keep in/out types in a normalized form where
different pairs with identical in types are joined by the least upper bound of
their out types. Moreover, the in/out types of failed branches are omitted so
that we obtain

⬇

tail : $\\{\\{\mbox{\small{:}}\\}\hookrightarrow\top\\}$

##  5 Inference and Checking of Call Types

Based on the pieces introduced in the previous sections, we can present our
method to infer and verify call types for all operations in a given program.
Basically, our method performs the following steps:

  1. 1.

The in/out types for all operations are computed (see Sect. 4).

  2. 2.

Initial call types for all operations are computed by considering the left-
hand sides or case structure of their defining rules.

  3. 3.

These call types are abstracted w.r.t. the abstract type domain.

  4. 4.

For each call to an operation $g$ occurring in a rule defining operation $f$,
we check, by considering the call structure and in/out types, whether the call
type of $g$ is satisfied.

  5. 5.

If some operation cannot be verified due to unsatisfied call type
restrictions, its call type is refined by considering the additional call-type
constraints due to operations called in its right-hand side, and start again
with step 4.

This fixpoint computation terminates if the abstract type domain is finite
(which is the case for depth-$k$ types) or it is ensured that there are only
finitely many refinements for each call type in step 5 (which could be ensured
by widening steps in infinite abstract domains [14]). In the worst case, an
empty call type might be inferred for some operation. This does not mean that
this operation is not useful but one has to encapsulate its use with some
safeness check.

In the following, we describe these steps in more detail.

###  5.1 Initial Call Types

Concrete call types are easy to derive by considering the structure of case
expressions in the transformed FlatCurry program. If all constructors of some
data type are covered in non-failed branches of some case construct, there is
no call type restriction due to this pattern matching. Otherwise, the call
type restriction consists of those constructors occurring in non-failed
branches. For instance, the operation null has no call type restriction,
whereas the operations head and tail have failed branches for the empty list
so that the call type restriction could be expressed by the set of terms

$\\{t_{1}\mbox{\small{:}}t_{2}\mid t_{1},t_{2}\mbox{ are arbitrary terms}\\}$

As already discussed, we map such sets into a finite representation by using
abstract types. Hence, the _abstract call type_ of an $n$-ary operation is a
sequence of elements of ${\cal{A}}$ of length $n$. We say that such a type is
_trivial_ if all elements in this sequence are $\top$. In case of the abstract
type domain ${\cal{A}}_{1}$, the set above is abstracted to
$\\{\mbox{\small{:}}\\}$, thus, it is non-trivial. Since the derivation of
concrete call types and their abstraction is straightforward, we omit further
details here.

###  5.2 Call Type Checking

We assume that two kinds of information are given for a defined operation $f$:

  * •

An in/out type $\mathit{IO}(f)$ approximating the input/output behavior of
$f$.

  * •

An abstract call type $\mathit{CT}(f)$ specifying the requirements to evaluate
$f$ without failure.

$\mathit{IO}(f)$ can be computed as shown in Sect. 4. $\mathit{CT}(f)$ can be
approximated as discussed above, but we have to show that all calls to $f$
actually satisfy these requirements. This is the purpose of the inference
system shown in Fig. 3.

As discussed in Sect. 4, it is important to have information about the
input/output behavior of operations. Therefore, we introduced the notion of
in/out types. Now we use this information to approximate values of variables
occurring in program rules and pass this information through the rules during
checking time. For this purpose, we use _variable types_ which are triples of
the form $(z,\mathit{io},x_{1}\ldots x_{n})$ where $z,x_{1},\ldots,x_{n}$ are
program variables and $\mathit{io}$ is an in/out type for an $n$-ary
operation. This is interpreted as: $z$ might have some value of the result
type $a$ for some $a_{1}\ldots a_{n}\hookrightarrow a\in\mathit{io}$ and, in
this case, $x_{1},\ldots,x_{n}$ have values of type $a_{1},\ldots,a_{n}$,
respectively. For instance, the variable type

expresses that $z$ might have value True and $xs$ is an empty list, or $z$ has
value False and $xs$ is a non-empty list. Since we approximate values, we
abstract a set of variable environments with concrete values for variables to
a set of variable types. If such a set contains only one triple for some
variable and the $io$ component is a one-element set, we can use it for
definite reasoning. To have a more compact notation for the abstract type of a
program variable, we denote by $x::a$ the triple $(x,\\{\varepsilon\mapsto
a\\},\varepsilon)$.

Now we have a closer look at the rules of Fig. 3. This inference system
derives judgements of the form $\Delta,z=e\vdash\Delta^{\prime}$ containing
sets of variable types $\Delta,\Delta^{\prime}$, a variable $z$, and an
expression $e$. This is interpreted as “if $\Delta$ holds, then the expression
$e$ evaluates without a failure and, if $z$ is bound to the result of this
evaluation, $\Delta^{\prime}$ holds.” To check the call type $a_{1}\ldots
a_{n}$ of an operation $f$ defined by $f(x_{1},\ldots,x_{n})=e$, we try to
derive the judgement

$\\{x_{1}::a_{1},\ldots,x_{n}::a_{n}\\},z=e\vdash\Delta$

for some fresh variable $z$. Thus, we assign the call types as initial values
of the parameters and analyze the right-hand side of the operation.

$\begin{array}[]{r@{\hspace{2ex}}cl}\mbox{\sf Var${}_{\mathit{nf}}$}\hskip
8.61108pt&\Delta,z=x\vdash\\{(z,\\{\varepsilon\mapsto\Delta(x)\\},\varepsilon)\\}&\\\\[4.30554pt]
\mbox{\sf Cons${}_{\mathit{nf}}$}\hskip
8.61108pt&\Delta,z=c(x_{1},\ldots,x_{n})\vdash\\{(z,\\{\top^{n}\hookrightarrow
c^{\alpha}(\overline{\Delta(x_{n})})\\},x_{1}\ldots x_{n})\\}&\\\\[4.30554pt]
\mbox{\sf Func${}_{\mathit{nf}}$}\hskip
8.61108pt&{\displaystyle\frac{\mathit{CT}(f)=a_{1}\ldots
a_{n}\quad\Delta(x_{i})\sqsubseteq
a_{i}~{}(i=1,\ldots,n)}{\Delta,z=f(x_{1},\ldots,x_{n})\vdash\\{(z,\mathit{IO}(f),x_{1}\ldots
x_{n})\\}}}&\\\\[12.91663pt] \mbox{\sf Or${}_{\mathit{nf}}$}\hskip
8.61108pt&{\displaystyle\frac{\Delta,z=e_{1}\vdash\Delta_{1}\quad\Delta,z=e_{2}\vdash\Delta_{2}}{\Delta,z=e_{1}~{}or~{}e_{2}\vdash\Delta_{1}\cup\Delta_{2}}}&\\\\[12.91663pt]
\mbox{\sf Free${}_{\mathit{nf}}$}\hskip
8.61108pt&{\displaystyle\frac{\Delta\cup\\{x_{1}::\top,\ldots,x_{n}::\top\\},z=e\vdash\Delta^{\prime}}{\Delta,z=\mathit{let}~{}x_{1},\ldots,x_{n}~{}\mathit{free~{}in}~{}e\vdash\Delta^{\prime}}}&\\\\[12.91663pt]
\mbox{\sf Let${}_{\mathit{nf}}$}\hskip
8.61108pt&{\displaystyle\frac{\Delta,x=e\vdash\Delta^{\prime}\quad\Delta\cup\Delta^{\prime},z=e^{\prime}\vdash\Delta^{\prime\prime}}{\Delta,z=let~{}x=e~{}in~{}e^{\prime}\vdash\Delta^{\prime\prime}}}\\\\[12.91663pt]
\mbox{\sf Case${}_{\mathit{nf}}$}\hskip
8.61108pt&{\displaystyle\frac{\Delta_{r_{1}},z=e_{r_{1}}\vdash\Delta^{\prime}_{r_{1}}~{}~{}\ldots~{}~{}\Delta_{r_{k}},z=e_{r_{k}}\vdash\Delta^{\prime}_{r_{k}}}{\Delta,z=\mathit{case}~{}x~{}\mathit{of}~{}\\{p_{1}\to
e_{1};\ldots;p_{n}\to
e_{n}\\}\vdash\Delta^{\prime}_{r_{1}}\cup\ldots\cup\Delta^{\prime}_{r_{k}}}}\\\\[12.91663pt]
\hskip 8.61108pt&\mbox{ where
}p_{i}=c_{i}(\overline{x_{n_{i}}}),\Delta_{i}=(\Delta\wedge[x\mapsto
c_{i}])\cup\\{x_{1}::\top,\ldots,x_{n_{i}}::\top\\},\\\ \hskip
8.61108pt&\mbox{ and }r_{1},\ldots,r_{k}\mbox{ are the reachable branches
(i.e., $\Delta_{r_{j}}(x)\neq\bot$)}\\\ \end{array}$ Figure 3: Call type
checking

Keeping the interpretation of variable types in mind, the inference rules are
not difficult to understand. $\Delta(x)$ denotes the least upper bound of all
abstract type information about variable $x$ available in $\Delta$, which is
defined by

$\Delta(x)=\bigsqcup\;\\{a\mid(x,\\{\ldots,a_{1}\ldots a_{n}\hookrightarrow
a,\ldots\\},\ldots)\in\Delta\\}$

Rule Varnf is immediate since the evaluation of a value cannot fail so that we
set the result $z$ to the abstract type of $x$. Rule Consnf adds the simple
condition that $z$ is bound to the constructor $c$ after the evaluation
($\top^{n}=\top\ldots\top$ is a sequence of $n$ $\top$ elements). Rule Funcnf
is the first interesting rule. The condition states that the abstract
arguments of the function must be smaller than the required call type so that
the concrete values are in a subset relationship. If the requirements on call
types hold, the operation is evaluable and we connect the results and the
arguments with the in/out type of the operation. The rules for disjunctions
and free variable introduction are straightforward. In rule Letnf, the result
of analyzing the local binding is used to analyze the expression. We finally
discuss the most important rule for case selections.

In rule Casenf, $\Delta\wedge[x\mapsto c_{i}]$ denotes the set of variable
types $\Delta$ modified by the definite binding of $x$ to the constructor
$c_{i}$. This means that, if $\Delta$ contains a triple $(x,io,xs)$, all
result values in $io$ which are incompatible to $c_{i}$ are removed. After
this modification of $\Delta$, it may happen that $\Delta(x)$ is the empty
type, i.e., there is no concrete value which $x$ can have so that this branch
is _unreachable_. Therefore, the right-hand side of this branch need not be
analyzed so that rule Casenf does not consider them. For the remaining
reachable branches, the right-hand side is analyzed with the modified set of
variable types so that the value in the specific branch value is considered.

As an example, we check the simple operation

⬇

False $\rightarrow{}\\!\\!\\!$ head(x)

Recall that, for the abstract type domain ${\cal{A}}_{1}$, the in/out type of
null is

and the abstract call type of head is $\\{\mbox{\small{:}}\\}$. When we check
the right-hand side of the definition of f, we start the checking of the case
(after having checked the let binding) with the set of variable types

The check of the first case branch is immediate. For the second case branch,
we modify the previous set of variable types to
$\Delta_{2}=\Delta_{1}\wedge[\mbox{\small{y}}\mapsto\mbox{\small{False}}]$ so
that we have

The definite binding for y implies a definite binding for x so that
$\Delta_{2}$ is equivalent to

Hence, if we check the call “head(x)” w.r.t. $\Delta_{3}$, the abstract
argument type is $\Delta_{3}(\mbox{\small{x}})=\\{\mbox{\small{:}}\\}$ so that
the call type of head is satisfied.

As we have seen in this example, sets of variable types should be kept in a
simplified form in order to deduce most precise type information. For
instance, the definite bindings of variables, like
$(\mbox{\small{y}},\\{\\{\mbox{\small{:}}\\}\hookrightarrow\\{\mbox{\small{False}}\\}\\},\mbox{\small{x}})$,
should be propagated to get a definitive binding for x. Although this is not
explicitly stated in the inference rules, we assume that it is always done
whenever sets of variable types are modified.

###  5.3 Iterated Call Type Checking

Consider the operation

Applying the inference rules of Fig. 3 is not successful: the initial abstract
call type for hd is $\top$ so that the call type requirement for head is not
satisfied.

In order to compute call types for all operations, we try to refine the call
type of hd. For this purpose, we collect the requirements on variables for
unsatisfied call types during the check of an operation. If such a required
type is on some variable occurring in the left-hand side of an operation, the
call type of the operation is restricted and the operation is checked again.
In case of the operation hd, the failure in the call head(x) leads to the
requirement that x must have the abstract type $\\{\mbox{\small{:}}\\}$ so
that we check hd again but with this new call type—which is now successful.

There are also cases where such a refinement is not possible. For instance,
consider the slightly modified example

Since the type restriction $\\{\mbox{\small{:}}\\}$ on variable y can not be
obtained by restricting the call type of hdfree, we assume the most restricted
call type $\mathit{CT}(\mbox{\small{hdfree}})=\\{\\}$. This means that any
call to hdfree might fail so that one has to encapsulate calls to hdfree with
some safeness check.

This strategy leads to an iterated analysis of call types. In each iteration,
either all call types can be verified or the call type of some operation
becomes more restricted. This iteration always terminates if one can ensure
finitely many refinements of call types (which is the case for depth-$k$
types).

For an efficient computation of this fixpoint computation, it is reasonable to
use call dependencies of operations so that one has to re-check only the more
restricted operations and the operations that use them. We have implemented
this strategy in our tool and obtained a good improvement compared to the
initial naive fixpoint computation. For instance, the prelude of Curry (the
base module containing a lot of basic definitions for arithmetic, lists, type
classes, etc) contains 1262 operations (public and also auxiliary operations).
After the first iteration, the call types of 14 operations are refined so that
17 operations are reanalyzed in the next iteration. Altogether, the check of
the prelude requires five iterations.

###  5.4 Extensions

Up to now, we presented the analysis of a kernel language. Since application
programs use more features, we discuss in the following how to cover all
features occurring in Curry programs.

####  5.4.1 Literals

Programs might contain numbers or characters which are not introduced by
explicit data definitions. Although there are conceptually infinitely many
literals, their handling is straightforward. A literal can be treated as a
$0$-ary constructor. Since there are only finitely many literals in each
program, the abstract types for a given program are also finite. For instance,
consider the operation

⬇

k 1 = ’b’

The call type of k inferred w.r.t. domain ${\cal{A}}_{1}$ is
$\mathit{CT}(\mbox{\small{k}})=\\{\mbox{\small{0}},\mbox{\small{1}}\\}$.
Similarly, the in/out type of k is
$\mathit{IO}(\mbox{\small{k}})=\\{\\{\mbox{\small{0}}\\}\hookrightarrow\\{\mbox{\small{'a'}}\\},\\{\mbox{\small{1}}\\}\hookrightarrow\\{\mbox{\small{'b'}}\\}\\}$.

####  5.4.2 External operations

Usually, externally defined primitive operations do not fail so that they have
trivial call types. There are a few exceptions which are handled by explicitly
defined call types, like the always failing operation failed, or arithmetic
operations like division.

####  5.4.3 Higher-order operations

Since it is seldom that generic higher-order operations have functional
parameters with non-trivial call types, we take a simple approach to check
higher-order operations. We assume that higher-order arguments have trivial
call types and check this property for each call to a higher-order operation.
Thus, a call like “map head [[1,2],[3,4]]” is considered as potentially
failing. Our practical evaluation shows this assumption provides reasonable
results in practice.

####  5.4.4 Encapsulation

Failures might occur during run time, either due to operations with complex
non-failure conditions (e.g., arithmetic) or due to the use of logic
programming techniques with search and failures. In order to ensure an overall
non-failing application in the presence of possibly failing subcomputations,
the programmer has to encapsulate such subcomputations and then analyze its
outcome, e.g., branching on the result of the encapsulation. For this purpose,
one can use an exception handler (which represents a failing computation as an
error value) or some method to encapsulate non-deterministic search (e.g., [5,
12, 28, 29]). For instance, the primitive operation allValues returns all the
values of its argument expression in a list so that a failure corresponds to
an empty list. In order to include such a primitive in our framework, we
simply skip the analysis of its arguments. For instance, a source expression
like “allValues (head ys)” is not transformed it into “let x = head ys in
allValues x” (where x is fresh), but it is kept as it is. Furthermore, rule
Funcnf is specialized for allValues so that the condition on the arguments
w.r.t. the call type is omitted and the in/out type is trivial, i.e.,
$\mathit{IO}(\mbox{\small{allValues}})=\\{\top\hookrightarrow\top\\}$. In a
similar way, other methods to encapsulate possibly non-deterministic and
failing operations, like _set functions_ [5], can be handled.

####  5.4.5 Errors as Failures

The operation error is an external operation to emit an error message and
terminate the program (if it does not occur inside an exception handler).
Since we are mainly interested to avoid internal programming errors, error is
not considered as a failing operation in the default mode. Thus, if we change
the definition of head into (as in Haskell)

⬇

head [] = error "head: empty list"

head (x:xs) = x

the inferred call type is $\top$ so that the call “head []” is not considered
as failing. From some point of view, this is reasonable since the evaluation
does not fail but shows a result—the error message.

However, in safety-critical applications we want to be sure that all errors
are caught. In this case, we can still use our framework and define the call
type of error as $\bot$ so that any call to error is considered as failing.
Moreover, exception handlers can be treated similarly to encapsulated search
operators as described above. In order to be flexible with the interpretation
of error, our tool (see below) provides an option to set one of these two
views of error.

##  6 Evaluation

We have implemented the methods described above in a tool777Available as
package https://cpm.curry-lang.org/pkgs/verify-non-fail-1.0.0.html written in
Curry. In the following we evaluate it by discussing some examples and
applying it to various libraries.

First, we compare our approach to a previous tool to verify non-failing Curry
programs [21]. In that tool the programmer has to annotate partially defined
operations with _non-fail conditions_. Based on these conditions, the tool
extracts proof obligations from a program which are sent to an SMT solver. For
instance, consider the operation to compute the last element of a non-empty
list:

⬇

last (_:x:xs) = last (x:xs)

The condition to express the non-failure of this expression must be explicitly
defined as a predicate on the argument:

This predicate together with the definition of the involved operations are
translated to SMT formulas and then checked by an SMT solver, e.g., Z3 [16].
Using our approach, the abstract call type
$\mathit{CT}(\mbox{\small{last}})=\\{\mbox{\small{:}}\\}$ is automatically
inferred and the definition of last is successfully checked. Actually, we
tested our tool on various libraries and could deduce almost all manually
written non-fail conditions of [21]. Only in four prelude operations, our tool
could not infer these non-fail conditions since they contain arithmetic
conditions on integers. We leave it for future work to combine our approach
with an SMT solver to enable also successful checks in these cases.

Another interesting example is the operation split from the library Data.List.
This operation takes a predicate and a list as arguments and splits this list
into sublists at positions where the predicate holds. It is defined in Curry
as

⬇

split _ [] = [[]]

split p (x:xs) | p x = [] : split p xs

| otherwise = let (ys:yss) = split p xs

in (x:ys):yss

The interesting point in this example is the pattern matching in the right-
hand side “let (ys:yss) =$\;\cdots$”. In order to implement this pattern
matching in a lazy manner, specific selector operations are introduced when
this definition is transformed into a kernel language like FlatCurry, since
FlatCurry allows only variable bindings but not constructor patterns in let
expressions. Thus, the FlatCurry code generated for this definition introduces
two selector operations (named split_ys and split_yss below) to implement the
lazy pattern matching in the let expression. The standard front end of Curry
implementations translates the definition above into the following FlatCurry
code (which is bit more relaxed than required in Fig. 1):

⬇

split p zs = case zs of

[] $\rightarrow{}\\!\\!\\!$ [] : []

x : xs $\rightarrow{}\\!\\!\\!$ let px = apply p x

in case px of

True $\rightarrow{}\\!\\!\\!$ [] : (split p xs)

False $\rightarrow{}\\!\\!\\!$ let o = otherwise

in case o of

True $\rightarrow{}\\!\\!\\!$ let ts = split p xs

in let ys = split_ys ts

in let yss = split_yss ts

in (x : ys) : yss

False $\rightarrow{}\\!\\!\\!$ failed

split_ys :: [[a]] $\rightarrow{}\\!\\!\\!$ [a]

split_ys zs = case zs of x : xs $\rightarrow{}\\!\\!\\!$ x

split_yss :: [[a]] $\rightarrow{}\\!\\!\\!$ [[a]]

split_yss zs = case zs of x : xs $\rightarrow{}\\!\\!\\!$ xs

apply is a predefined primitive operation to implement higher-order
application. The predefined operation otherwise is equivalent to True so that
the occurrence of failed is not reachable.

Note that the selector operations split_ys and split_yss are partially defined
(they correspond to head and tail). Since they are generated during the
compilation process, a non-fail condition cannot be explicitly defined in the
source program so that the tool described in [21] could not verify this
definition of split. As mentioned in [21], it is necessary to include explicit
calls to head and tail instead of the pattern matching of let. Moreover, the
post-condition

had to be added and proved by a contract checker [22] so that this information
is used by the verifier to ensure that the recursive call to split always
returns a non-empty list.

With our method, such manual additions are not required since the call types
of the introduced selector operations are automatically inferred together with
the in/out type

Thanks to this in/out type, the abstract result of the recursive call to split
is $\\{\mbox{\small{:}}\\}$ which matches the call types required for the
selector operations. Thus, in contrast to [21], no manual annotations or code
modifications are necessary to check the non-failure of split.

If our tool is applied to a Curry module, it infers the in/out types and the
call types of all operations defined in this module and then checks all
branches and calls whether they might be failing. If this is the case, the
call types are refined and the problematic ones are reported to the user. Then
the user can decide to either accept the refined call types or modify the
program code to handle possible failures so that the call type does not need a
refinement.

Module | operations |  | in/out
---
types
| initial
---
call
types
| final
---
call
types
| final
---
failing
| itera-
---
tions
| verify
---
time
Prelude | 862/ | 1262 | 605/ | 857 | 24/ | 32 | 63/ | 71 | 45/ | 53 | 5 | 969
Data.Char | 9/ | 9 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 272
Data.Either | 7/ | 11 | 5/ | 9 | 2/ | 2 | 2/ | 2 | 0/ | 0 | 1 | 113
Data.List | 49/ | 87 | 39/ | 73 | 7/ | 15 | 8/ | 16 | 1/ | 1 | 2 | 290
Data.Maybe | 8/ | 9 | 7/ | 8 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 113
Numeric | 5/ | 7 | 0/ | 2 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 273
System.Console.GetOpt | 6/ | 47 | 5/ | 41 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 287
System.IO | 32/ | 51 | 10/ | 12 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 115
Text.Show | 4/ | 4 | 4/ | 4 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 110
Table 1: Inference of call types for some standard libraries

Table 1 contains the results of checking various Curry libraries with our
tool. The “operations” column contains the number of public (exported)
operations and the number of all operations defined in the module. Similarly,
the following three columns shows the information for public and all
operations. The “in/out types” column shows the numbers of non-trivial in/out
types. The initial and final call types are the number of non-trivial call
types computed at the beginning and obtained after some iterations (the number
of iterations is shown in the next to last column). The “final failing” column
contains the number of operations where an empty call type is inferred, i.e.,
there is no precise information about the required call types. The last column
shows the verification time in milliseconds.888We measured the verification
time on a Linux machine running Ubuntu 22.04 with an Intel Core i7-1165G7
(2.80GHz) processor with eight cores.

As one can see from this table, even quite complex modules, like the prelude,
have only a few operations with non-trivial call types that need to be
checked. Therefore, the effort to infer and check modules is limited. The
higher number of failing operations in the prelude are the various arithmetic
division operators and enumeration and parsing operations where a precise call
type cannot be inferred.

##  7 Related Work

The exclusion of run-time failures at compile time is a practically relevant
but also challenging issue. Therefore, there are many approaches targeting it
so that we can only discuss a few of them. We concentrate on approaches for
functional and logic programming, although there are also many in the
imperative world. As mentioned in the introduction, the exclusion of
dereferencing null pointers is quite relevant there. As an example from
object-oriented programming, the Eiffel compiler uses appropriate type
declarations and static analysis to ensure that pointer dereference failures
cannot occur in accepted programs [30].

In logic programming, there is no common definition of “non-failing” due to
different interpretations of non-determinism. Whereas we are interested to
exclude any failure in a top-level computation, other approaches, like [13,
17], consider a predicate in a logic program as non-failing if at least one
answer is produced. Similarly to our approach, type abstractions are used to
approximate non-failure properties, but the concrete methods are different.

Another notion of failing programs in a dynamically typed programming language
is based on success types, e.g., as used in Erlang [27]. Success types over-
approximate possible uses of an operation so that an empty success type
indicates an operation that never evaluates to some value. Thus, success types
can show definite failures, whether we are interested in definite non-
failures.

Strongly typed programming languages are a reasonable basis to check run-time
failures at compile time, since the type system already ensures that some kind
of failures cannot occur (“well-typed programs do not go wrong” [31]).
However, failures due to definitions with partial patterns are not covered by
a standard type system. Therefore, Mitchell and Runciman developed a checker
for Haskell to verify the absence of pattern-match errors due to incomplete
patterns [32, 33]. Their checker extracts and solves specific constraints from
pattern-based definitions. Although these constraints have similarities to the
abstract type domain ${\cal{A}}_{1}$, our approach is generic w.r.t. the
abstract type domain so that it can also deal with more powerful abstract
types.

An approach to handle failures caused by restrictions on number arguments is
described in [26]. It is based on generating (arithmetic) constraints which
are translated into an imperative program such that the constraints are
satisfiable iff the translated program is safe. This enables the inference of
complex conditions on numbers, but pattern matching with algebraic data types
and logic-oriented subcomputations are not supported.

Another approach to ensure the absence of failures is to make the type system
stronger or more expressive in order to encode non-failing conditions in the
types. For instance, operations in dependently typed programming languages,
such as Coq [10], Agda [34], or Idris [11], must be totally defined, i.e.,
terminating and non-failing. Such languages have termination checkers but non-
fail conditions need to be explicitly encoded in the types. For instance, the
definition of the operation head in Agda [34] requires, as an additional
argument, a proof that the argument list is not empty. Thus, head could have
the type signature

Therefore, each use of head must provide, as an additional argument, an
explicit proof for the non-emptiness of the argument list xs. Type-checked
Agda programs do not contain run-time failures but programming in a
dependently typed language is more challenging since the programmer has to
construct non-failure proofs.

Refinement types, as used in LiquidHaskell [38, 39], are another approach to
encode non-failing conditions or more general contracts on the type-level.
Refinement types extend standard types by a predicate that restricts the set
of allowed values. For instance, the applications of head to the empty list
can be excluded by the following refinement type [38]:

The correctness of refinement types is checked by an SMT solver so that they
are more expressive than our non-failure conditions. On the other hand,
refinement types must be explicitly added by the programmer whereas our goal
is to infer non-failure conditions from a given program without specific
annotations. This allows the use of potentially failing operations in
encapsulated subcomputations, which is relevant to use logic programming
techniques. This aspect is also the motivation for the non-failure checking
tool proposed in [21]. As already discussed in Sect. 6, the advantage of our
tool is the automatic inference of non-failing conditions which supports an
easier application to larger programs.

##  8 Conclusions

In this paper we proposed a new technique and a fully automatic tool to check
declarative programs for the absence of failing computations. In contrast to
other approaches, our approach does not require the explicit specification of
non-fail conditions but is able to infer them. In order to provide flexibility
with the structure of non-fail conditions, our approach is generic w.r.t. a
domain of abstract types to describe non-fail conditions. Since we developed
our approach for Curry, it is also applicable to purely functional or logic
programs. Due to the use of Curry, we do not need to abandon all potentially
failing operations. Partially defined operations and failing evaluations are
still allowed in logic-oriented subcomputations provided that they are
encapsulated in order to control possible failures.

Although the inference of non-fail conditions is based on a fixpoint iteration
and might yield, in the worst case, an empty (i.e., always failing) condition,
our practical evaluation showed that even larger programs contain only a few
operations with non-trivial non-fail conditions which are inferred after a
small number of iterations. When a non-trivial non-fail condition is inferred
for some operation, the programmer can either modify the definition of this
operation (e.g., by adding missing case branches) or control the invocation of
this operation by checking its outcome with some control operator.

For future work, we plan to extend our approach to built-in types, like
integers, and infer non-failure conditions on such types, like non-negative or
positive numbers, and check them using SMT solvers. Furthermore, it is
interesting to see whether other abstract domains, e.g., regular types, yield
more precise results in application programs. Our first experiments with
depth-$k$ domains (see Appendix 0.A) showed that a rather simple domain seems
sufficient in practical programs.

## References

  * [1] E. Albert, M. Hanus, F. Huch, J. Oliver, and G. Vidal.  Operational semantics for declarative multi-paradigm languages.  Journal of Symbolic Computation, 40(1):795–829, 2005.
  * [2] M. Alpuente, M. Comini, S. Escobar, M. Falaschi, and S. Lucas.  Abstract diagnosis of functional programs.  In Proc. of the 12th Int’l Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR 2002), pages 1–16. Springer LNCS 2664, 2002\.
  * [3] S. Antoy.  Constructor-based conditional narrowing.  In Proc. of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), pages 199–206. ACM Press, 2001.
  * [4] S. Antoy, R. Echahed, and M. Hanus.  A needed narrowing strategy.  Journal of the ACM, 47(4):776–822, 2000.
  * [5] S. Antoy and M. Hanus.  Set functions for functional logic programming.  In Proceedings of the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’09), pages 73–82. ACM Press, 2009.
  * [6] S. Antoy and M. Hanus.  Functional logic programming.  Communications of the ACM, 53(4):74–85, 2010.
  * [7] S. Antoy, M. Hanus, A. Jost, and S. Libby.  ICurry.  In Declarative Programming and Knowledge Management - Conference on Declarative Programming (DECLARE 2019), pages 286–307. Springer LNCS 12057, 2020.
  * [8] D. Bert and R. Echahed.  Abstraction of conditional term rewriting systems.  In Proc. of the 1995 International Logic Programming Symposium, pages 147–161. MIT Press, 1995.
  * [9] D. Bert, R. Echahed, and M. Østvold.  Abstract rewriting.  In Proc. Third International Workshop on Static Analysis, pages 178–192. Springer LNCS 724, 1993.
  * [10] Y. Bertot and P. Castéran.  Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004\.
  * [11] E. Brady.  Idris, a general-purpose dependently typed programming language: Design and implementation.  Journal of Functional Programming, 23(5):552–593, 2013.
  * [12] B. Braßel, M. Hanus, and F. Huch.  Encapsulating non-determinism in functional logic computations.  Journal of Functional and Logic Programming, 2004(6), 2004.
  * [13] F. Bueno, P. López-García, and M.V. Hermenegildo.  Multivariant non-failure analysis via standard abstract interpretation.  In 7th International Symposium on Functional and Logic Programming (FLOPS 2004), pages 100–116. Springer LNCS 2998, 2004.
  * [14] P. Cousot and R. Cousot.  Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints.  In Proc. of the 4th ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.
  * [15] P.W. Dart and J. Zobel.  A regular type language for logic programs.  In F. Pfenning, editor, Types in Logic Programming, pages 157–187. MIT Press, 1992.
  * [16] L. de Moura and N. Bjørner.  Z3: An efficient SMT solver.  In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), pages 337–340. Springer LNCS 4963, 2008.
  * [17] S. Debray, P. López-García, and M.V. Hermenegildo.  Non-failure analysis for logic programs.  In 14th International Conference on Logic Programming (ICLP’97), pages 48–62. MIT Press, 1997.
  * [18] J.P. Gallagher and K.S. Henriksen.  Abstract domains based on regular types.  In 20th International Conference on Logic Programming (ICLP 2004), pages 27–42. Springer LNCS 3132, 2004.
  * [19] J.C. González-Moreno, M.T. Hortalá-González, F.J. López-Fraguas, and M. Rodríguez-Artalejo.  An approach to declarative programming based on a rewriting logic.  Journal of Logic Programming, 40:47–87, 1999.
  * [20] M. Hanus.  Functional logic programming: From theory to Curry.  In Programming Logics - Essays in Memory of Harald Ganzinger, pages 123–168. Springer LNCS 7797, 2013.
  * [21] M. Hanus.  Verifying fail-free declarative programs.  In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming(PPDP 2018), pages 12:1–12:13. ACM Press, 2018.
  * [22] M. Hanus.  Combining static and dynamic contract checking for Curry.  Fundamenta Informaticae, 173(4):285–314, 2020.
  * [23] M. Hanus.  From logic to functional logic programs.  Theory and Practice of Logic Programming, 22(4):538–554, 2022.
  * [24] M. Hanus and F. Skrlac.  A modular and generic analysis server system for functional logic programs.  In Proc. of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM’14), pages 181–188. ACM Press, 2014.
  * [25] M. Hanus (ed.).  Curry: An integrated functional logic language (vers. 0.9.0).  Available at http://www.curry-lang.org, 2016.
  * [26] R. Jhala, R. Majumdar, and A. Rybalchenko.  HMC: verifying functional programs using abstract interpreters.  In 23rd International Conference on Computer Aided Verification (CAV 2011), pages 470–485. Springer LNCS 6806, 2011.
  * [27] T. Lindahl and K. Sagonas.  Practical type inference based on success typings.  In Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2006), pages 167–178. ACM Press, 2006.
  * [28] F.J. López-Fraguas and J. Sánchez-Hernández.  A proof theoretic approach to failure in functional logic programming.  Theory and Practice of Logic Programming, 4(1):41–74, 2004.
  * [29] W. Lux.  Implementing encapsulated search for a lazy functional logic language.  In Proc. 4th Fuji International Symposium on Functional and Logic Programming (FLOPS’99), pages 100–113. Springer LNCS 1722, 1999.
  * [30] B. Meyer.  Ending null pointer crashes.  Communications of the ACM, 60(5):8–9, 2017.
  * [31] R. Milner.  A theory of type polymorphism in programming.  Journal of Computer and System Sciences, 17:348–375, 1978.
  * [32] N. Mitchell and C. Runciman.  A static checker for safe pattern matching in Haskell.  In Trends in Functional Programming, volume 6, pages 15–30. Intellect, 2007.
  * [33] N. Mitchell and C. Runciman.  Not all patterns, but enough: an automatic verifier for partial but sufficient pattern matching.  In Proc. of the 1st ACM SIGPLAN Symposium on Haskell (Haskell 2008), pages 49–60. ACM, 2008.
  * [34] U. Norell.  Dependently typed programming in Agda.  In Proceedings of the 6th International School on Advanced Functional Programming (AFP’08), pages 230–266. Springer LNCS 5832, 2008.
  * [35] S. Peyton Jones, editor.  Haskell 98 Language and Libraries—The Revised Report.  Cambridge University Press, 2003.
  * [36] T. Sato and H. Tamaki.  Enumeration of success patterns in logic programs.  Theoretical Computer Science, 34:227–240, 1984.
  * [37] A. Stump.  Verified Functional Programming in Agda.  ACM and Morgan & Claypool, 2016.
  * [38] N. Vazou, E.L. Seidel, and R. Jhala.  LiquidHaskell: Experience with refinement types in the real world.  In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, pages 39–51. ACM Press, 2014.
  * [39] N. Vazou, E.L. Seidel, R. Jhala, D. Vytiniotis, and S. Peyton Jones.  Refinement types for Haskell.  In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 269–282. ACM Press, 2014\.

##  Appendix 0.A Inference of Call Types with Different Domains

Our inference of call types is parametric w.r.t. the domain of abstract types.
In the examples of the paper, a simple domain, where data terms are abstracted
to their top-level constructors, is used. The actual implementation supports
also depth-$k$ abstractions [36] with $k>1$. Although deeper abstractions
could provide more precision, we show by the analysis of standard libraries
that this is seldom in practical programs. The following tables show the
results for $k=1$ (which is identical to Table 1), $k=2$, and $k=5$. Apart
from the execution times, the results are identical.

##### Inference of call types with the depth-1 domain:

Module | operations |  | in/out
---
types
| initial
---
call
types
| final
---
call
types
| final
---
failing
| itera-
---
tions
| verify
---
time
Prelude | 862/ | 1262 | 605/ | 857 | 24/ | 32 | 63/ | 71 | 45/ | 53 | 5 | 969
Data.Char | 9/ | 9 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 272
Data.Either | 7/ | 11 | 5/ | 9 | 2/ | 2 | 2/ | 2 | 0/ | 0 | 1 | 113
Data.List | 49/ | 87 | 39/ | 73 | 7/ | 15 | 8/ | 16 | 1/ | 1 | 2 | 290
Data.Maybe | 8/ | 9 | 7/ | 8 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 113
Numeric | 5/ | 7 | 0/ | 2 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 273
System.Console.GetOpt | 6/ | 47 | 5/ | 41 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 287
System.IO | 32/ | 51 | 10/ | 12 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 115
Text.Show | 4/ | 4 | 4/ | 4 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 110

##### Inference of call types with the depth-2 domain:

Module | operations |  | in/out
---
types
| initial
---
call
types
| final
---
call
types
| final
---
failing
| itera-
---
tions
| verify
---
time
Prelude | 862/ | 1262 | 605/ | 857 | 24/ | 32 | 63/ | 71 | 45/ | 53 | 5 | 986
Data.Char | 9/ | 9 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 381
Data.Either | 7/ | 11 | 5/ | 9 | 2/ | 2 | 2/ | 2 | 0/ | 0 | 1 | 118
Data.List | 49/ | 87 | 39/ | 73 | 7/ | 15 | 8/ | 16 | 1/ | 1 | 2 | 405
Data.Maybe | 8/ | 9 | 7/ | 8 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 118
Numeric | 5/ | 7 | 0/ | 2 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 393
System.Console.GetOpt | 6/ | 47 | 5/ | 41 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 425
System.IO | 32/ | 51 | 10/ | 12 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 126
Text.Show | 4/ | 4 | 4/ | 4 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 117

##### Inference of call types with the depth-5 domain:

Module | operations |  | in/out
---
types
| initial
---
call
types
| final
---
call
types
| final
---
failing
| itera-
---
tions
| verify
---
time
Prelude | 862/ | 1262 | 605/ | 857 | 24/ | 32 | 63/ | 71 | 45/ | 53 | 5 | 987
Data.Char | 9/ | 9 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 431
Data.Either | 7/ | 11 | 5/ | 9 | 2/ | 2 | 2/ | 2 | 0/ | 0 | 1 | 120
Data.List | 49/ | 87 | 39/ | 73 | 7/ | 15 | 8/ | 16 | 1/ | 1 | 2 | 438
Data.Maybe | 8/ | 9 | 7/ | 8 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 119
Numeric | 5/ | 7 | 0/ | 2 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 424
System.Console.GetOpt | 6/ | 47 | 5/ | 41 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 462
System.IO | 32/ | 51 | 10/ | 12 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 127
Text.Show | 4/ | 4 | 4/ | 4 | 0/ | 0 | 0/ | 0 | 0/ | 0 | 1 | 117

##  Appendix 0.B Correctness

In the following, we show that inference systems defined in the paper
correctly approximate the evaluation of functional logic programs. Similarly
to the inference systems, we consider the evaluation of FlatCurry programs
(see Fig. 1). Function definitions are considered as rewrite rules and do not
contain unbound variables, i.e., all variables occurring in the right-hand
side are either parameters or introduced by $\mathit{let}$ bindings or
$\mathit{case}$ patterns. FlatCurry expressions are evaluated by term
rewriting with the following specific evaluation rules:

  * •

A disjunction $e_{1}~{}\mathit{or}~{}e_{2}$ is non-deterministically
evaluated, i.e., reduced to either $e_{1}$ or $e_{2}$. Thus, our reduction
relation is non-deterministic so that all possible evaluations are considered.

  * •

The evaluation of
$\mathit{let}~{}x_{1},\ldots,x_{n}~{}\mathit{free~{}in}~{}e^{\prime}$ guesses
values (data terms) $t_{1},\ldots,t_{n}$ for the free variables
$x_{1},\ldots,x_{n}$ so that it reduces to $\rho(e^{\prime})$ where
$\rho=\\{x_{1}\mapsto t_{1},\ldots,x_{n}\mapsto t_{n}\\}$. Actual
implementations defer this guessing to the point where a value of a variable
is needed, which is called narrowing. Since we do not consider a specific
operational semantics, we use this quite general (non-deterministic) guessing
step.

  * •

A let binding $\mathit{let}~{}x=e~{}\mathit{in}~{}e^{\prime}$ is evaluated by
evaluating $e$ to a data term $t$999 In order to model non-strict evaluation,
one could add partial terms, i.e., an undefined value, and the possibility to
reduce a term to an undefined value, as in the rewriting logic CRWL [19]. For
the sake of simplicity, we omit the introduction of partial terms.  and
evaluating $\rho(e^{\prime})$ where $\rho=\\{x\mapsto t\\}$.

  * •

A case expression $\mathit{case}~{}x~{}\mathit{of}~{}\\{p_{1}\to
e_{1};\ldots;p_{n}\to e_{n}\\}$ is evaluated by reducing it to $\rho(e_{i})$
where $x$ matches the pattern $p_{i}$ and $\rho$ binds the variables of
$p_{i}$. Note that the case expression covers all constructors of a type so
that such a reduction step is always possible.

In the following, we denote by $\mathit{Var}(e)$ the set of all unbound
variables of an expression $e$, i.e., all variables occurring in $e$ which are
not introduced in patterns or let expressions.

###  0.B.1 Correctness of In/Out Types

First we show that the inference rules in Fig. 2 correctly approximate the
input-output behavior of operations. For this purpose, we denote by
$\mathit{dom}(\Gamma)$ the domain of a type environment $\Gamma$ (a mapping
from variables into abstract types). We state the correctness of the inference
rules as follows.

###### Theorem 0.B.1

Let $\mathit{Var}(e)\subseteq\mathit{dom}(\Gamma)$, $\Gamma\vdash
e:\\{\overline{\Gamma_{k}\hookrightarrow a_{k}}\\}$ be derivable by the
inference rules in Fig. 2, and $\sigma$ be a substitution with
$\sigma(x)\in\gamma(\Gamma(x))$ for all $x\in\mathit{Var}(e)$. If $\sigma(e)$
is reducible to some data term $t$, then there is some $i\in\\{1,\ldots,k\\}$
with $t\in\gamma(a_{i})$ and $\sigma(x)\in\gamma(\Gamma_{i}(x))$ for all
$x\in\mathit{Var}(e)$.

###### Proof

By induction on the height of the proof tree to derive $\Gamma\vdash
e:\mathit{io}$. We assume that the theorem’s preconditions hold, i.e.,
$\mathit{Var}(e)\subseteq\mathit{dom}(\Gamma)$, $\Gamma\vdash e:\mathit{io}$
with $\mathit{io}=\\{\overline{\Gamma_{k}\hookrightarrow a_{k}}\\}$ is
derivable with an proof tree of height $h$, $\sigma$ is a substitution with
$\sigma(y)\in\gamma(\Gamma(y))$ for all $y\in\mathit{Var}(e)$, and $\sigma(e)$
is reducible to some data term $t$. We have to show that there is some
$i\in\\{1,\ldots,k\\}$ with

  * (1)

$t\in\gamma(a_{i})$ and

  * (2)

$\sigma(y)\in\gamma(\Gamma_{i}(y))$ for all $y\in\mathit{Var}(e)$.

Induction base $h=1$: We distinguish the different axioms, i.e., the rules
Var, Cons, and Func:

Rule Var is applied:

Then $e=x$, $k=1$, $\Gamma_{1}=\Gamma$, $a_{1}=\Gamma(x)$, and $t=\sigma(x)$
since $\sigma(x)$ is a data term. Since $\sigma(x)\in\gamma(\Gamma(x))$,
properties (1) and (2) hold.

Rule Cons is applied:

In this case we have $e=c(x_{1},\ldots,x_{n})$, $k=1$, $\Gamma_{1}=\Gamma$,
and $a_{1}=c^{\alpha}(\Gamma(x_{1}),\ldots,\Gamma(x_{n}))$.
$\sigma(x_{i})\in\gamma(\Gamma(x_{i}))=\gamma(\Gamma_{1}(x_{i}))$
($i=1,\ldots,n$) so that (2) holds. Since $\sigma(e)$ is a data term,
$t=\sigma(e)=c(\sigma(x_{1}),\ldots,\sigma(x_{n}))$. This implies property (1)
since $\sigma(x_{i})\in\gamma(\Gamma(x_{i}))$ ($i=1,\ldots,n$) and
$t=c(\sigma(x_{1}),\ldots,\sigma(x_{n}))\in\gamma(c^{\alpha}(\Gamma(x_{1}),\ldots,\Gamma(x_{n})))$
by definition of the abstract constructor application (see Sect. 3).

Rule Func is applied:

Then $e=f(x_{1},\ldots,x_{n})$, $k=1$, $\Gamma_{1}=\Gamma$, and $a_{1}=R(f)$.
Hence $\sigma(x_{i})\in\gamma(\Gamma(x_{i}))=\gamma(\Gamma_{1}(x_{i}))$
($i=1,\ldots,n$) so that (2) holds. Furthermore,
$\sigma(e)=f(t_{1},\ldots,t_{n})$ for some terms $t_{1},\ldots,t_{n}$. Since
$R(f)$ approximates all possible values of a call to $f$, $t\in\gamma(R(f))$.

Induction step, i.e., $h>1$: In this case, one of the rules Or, Free, Let, or
Case is applied:

Rule Or is applied:

Then $e=e_{1}~{}\mathit{or}~{}e_{2}$ so that either $\sigma(e_{1})$ or
$\sigma(e_{2})$ is reducible to $t$. Consider the case that $\sigma(e_{1})$ is
reducible to $t$ (the other case can be similarly proved). Since $\Gamma\vdash
e_{1}:\mathit{io}_{1}$ with
$\mathit{io}_{1}=\\{\overline{\Gamma^{\prime}_{k^{\prime}}\hookrightarrow
a^{\prime}_{k^{\prime}}}\\}$ is derivable and $\sigma(e_{1})$ is reducible to
$t$, by induction hypothesis, there is some $j\in\\{1,\ldots,k^{\prime}\\}$
with $\sigma(x)\in\gamma(\Gamma^{\prime}_{j}(x))$ for all
$x\in\mathit{Var}(e_{1})$ and $t\in\gamma(a^{\prime}_{j})$. If there is some
variable $y\in\mathit{Var}(e_{2})$ and $y\not\in\mathit{Var}(e_{1})$,
$\sigma(y)\in\gamma(\Gamma(y))=\gamma(\Gamma^{\prime}_{j}(y))$, since an
abstract value in a type environment is only changed if this variable occurs
in a case expression as a discriminator (see the rules in Fig. 2) which cannot
be the case for $y$ in expression $e_{1}$. Since
$\mathit{io}_{1}\subseteq\mathit{io}$, properties (1) and (2) hold.

Rule Free is applied:

A reduction of the expression
$e=\mathit{let}~{}x_{1},\ldots,x_{n}~{}\mathit{free~{}in}~{}e^{\prime}$
guesses values for the free variables $x_{1},\ldots,x_{n}$ in order to reduce
$e^{\prime}$. Since $\sigma(e)$ reduces to $t$, there must be a substitution
$\rho=\\{\overline{x_{n}\mapsto t_{n}}\\}$ for the free variables such that
$\sigma(e)$ is reduced to $\sigma(\rho(e^{\prime}))$ which is reducible to
$t$.
$\mathit{Var}(e^{\prime})\subseteq\mathit{dom}(\Gamma[\overline{x_{n}\mapsto\top}])$
since $\mathit{Var}(e)\subseteq\mathit{dom}(\Gamma)$. Hence, by the induction
hypothesis, there is some $i\in\\{1,\ldots,k\\}$ with
$\sigma(\rho(y))\in\gamma(\Gamma_{i}(y))$ for all
$y\in\mathit{Var}(e^{\prime})$ and $t\in\gamma(a_{i})$. Thus, property (1)
holds. Since $\rho$ is the identity on variables different from
$x_{1},\ldots,x_{n}$, $\sigma(y)\in\gamma(\Gamma_{i}(y))$ for all
$y\in\mathit{Var}(e)$ so that property (2) also holds.

Rule Let is applied:

This is similar to rule Free since this rule introduces the bound variable
without any restriction on its value so that we can ignore the evaluation of
the bound expression.

Rule Case is applied:

Then $e=\mathit{case}~{}x~{}\mathit{of}~{}\\{p_{1}\to e_{1};\ldots;p_{n}\to
e_{n}\\}$. Since $\sigma(e)$ is reducible to $t$, there is some branch
$i\in\\{1\ldots,n\\}$ such that $\sigma(\rho(e_{i}))$ is reducible to $t$,
where $\rho$ is a matching substitution on the variables of pattern
$p_{i}=c_{i}(\overline{x_{n_{i}}})$. Let $\Gamma_{i}=\Gamma[x\mapsto
c_{i}^{\alpha}(\overline{\top}),\overline{x_{n_{i}}\mapsto\top}]$. Then
$\mathit{Var}(e_{i})\subseteq\mathit{dom}(\Gamma_{i})$, $\Gamma_{i}\vdash
e_{i}:\mathit{io}_{i}$ is derivable where the height of the proof tree is
smaller than $h$, and
$\mathit{io}_{i}=\\{\overline{\Gamma^{\prime}_{k^{\prime}}\hookrightarrow
a^{\prime}_{k^{\prime}}}\\}\subseteq\mathit{io}$. By the induction hypothesis,
there is some $j\in\\{1,\ldots,k^{\prime}\\}$ with
$\sigma(y)\in\gamma(\Gamma^{\prime}_{j}(y))$ for all $y\in\mathit{Var}(e_{i})$
and $t\in\gamma(a^{\prime}_{j})$. This immediately implies property (1). To
show property (2), consider the discriminating variable $x$ of the case
expression, which might not occur in $\mathit{Var}(e_{i})$. In this case,
$\Gamma^{\prime}_{j}(x)=\Gamma_{i}(x)$ since the abstract type of $x$ is not
changed in the proof tree for $\Gamma_{i}\vdash e_{i}:\mathit{io}_{i}$
(compare proof of rule Or). Since branch $i$ has been selected for the
reduction of $\sigma(e)$, $\sigma(x)$ must match the pattern
$c_{i}(\overline{x_{n_{i}}})$ so that
$\sigma(x)\in\gamma(c_{i}^{\alpha}(\overline{\top}))=\gamma(\Gamma_{i}(x))$.
Finally, if there is some variable $y\in\mathit{Var}(e)$ with
$y\not\in\mathit{Var}(e_{i})$, then
$\sigma(y)\in\gamma(\Gamma(y))=\gamma(\Gamma^{\prime}_{j}(y))$ since the
abstract type of $y$ is not changed in the proof tree for $\Gamma_{i}\vdash
e_{i}:\mathit{io}_{i}$ (compare proof of rule Or). Therefore,
$\sigma(y)\in\gamma(\Gamma^{\prime}_{j}(y))$ holds for all
$y\in\mathit{Var}(e)$, which proves property (2). ∎

For an operation $f$ defined by $f(x_{1},\ldots,x_{n})=e$, we infer its in/out
type $\mathit{io}$ by deriving the judgement

$\\{\overline{x_{n}\mapsto\top}\\}\vdash
e:\\{\overline{\Gamma_{k}\hookrightarrow a_{k}}\\}$

and defining

$\mathit{io}=\\{\Gamma_{i}(x_{1})\cdots\Gamma_{i}(x_{n})\hookrightarrow
a_{i}\mid i=1,\ldots,k\\}$

Hence, Theorem 0.B.1 implies the following property of inferred in/out types.

######  Corollary 1 (Correctness of inferred in/out types)

If

$\\{a_{i1}\cdots a_{in}\hookrightarrow a_{i}\mid i=1,\ldots,k\\}$

is an inferred in/out type for an $n$-ary operation $f$ and
$t_{1},\ldots,t_{n},t$ are data terms such that $f(t_{1},\ldots,t_{n})$ is
reducible to $t$, then there is some $i\in\\{1,\ldots,k\\}$ with
$t_{j}\in\gamma(a_{ij})$ ($j=1,\ldots,n$) and $t\in\gamma(a_{i})$.

###  0.B.2 Correctness of Call Types

In the following we show that the inference rules in Fig. 3 correctly
approximate the non-failure property of operations.

As described in Sect. 5.2, if an operation $f$ is defined by
$f(x_{1},\ldots,x_{n})=e$, an assumed call type $\mathit{CT}(f)=a_{1}\ldots
a_{n}$ is checked by deriving the judgement

$\\{(x_{1},\\{\varepsilon\mapsto
a_{1}\\},\varepsilon),\ldots,(x_{n},\\{\varepsilon\mapsto
a_{n}\\},\varepsilon)\\},z=e\vdash\Delta$

for some fresh variable $z$. If this check is successful, i.e., the judgement
is derivable, we say that $\mathit{CT}(f)$ is _verified_. Furthermore, a
(variable-free) expression $e$ is _non-failing_ if all finite reductions of
$e$ end in a data term (i.e., containing only data constructors). In the
following we show that function calls are non-failing for arguments satisfying
$\mathit{CT}$ if the call types of all functions specified by $\mathit{CT}$
are verified.

Recall that we write $\Delta(x)$ for the least upper bound of all abstract
type information about variable $x$ available in the set of variable types
$\Delta$, which is defined by

$\Delta(x)=\bigsqcup\;\\{a\mid(x,\mathit{io},x_{1}\ldots
x_{n})\in\Delta,~{}a_{1}\ldots a_{n}\hookrightarrow a\in\mathit{io}\\}$

The inference rules derive sets of variable types $\Delta$ which should be
satisfied by substitutions occurring in concrete evaluation. For this purpose,
we define the _domain_ of a set of variable types $\Delta$ by

$\mathit{dom}(\Delta)=\\{x\mid(x,\mathit{io},x_{1}\ldots x_{n})\in\Delta\\}$

We say that a set of variable types $\Delta$ is _correct_ for a substitution
$\sigma$ if, for all variables $x\in\mathit{dom}(\Delta)$, there is some
$(x,\mathit{io},x_{1}\ldots x_{n})\in\Delta$ and some $a_{1}\ldots
a_{n}\hookrightarrow a\in\mathit{io}$ such that $\sigma(x)\in\gamma(a)$ and
$\sigma(x_{i})\in\gamma(a_{i})$ for $i=1,\ldots,n$.

Thus, a set of variables types is correct for a substitution if there is
_some_ in/out type conform to the substitution. This weakness is a consequence
of our approximation of non-deterministic computations. Nevertheless,
variables types can be helpful to deduce definite information if they contain
only a single element for some variable or all elements have the same result
type.

The following lemmas state simple consequences of this definition.

###### Lemma 1

If a set of variable types $\Delta$ is correct for a substitution $\sigma$,
then $\sigma(x)\in\gamma(\Delta(x))$ for all variables
$x\in\mathit{dom}(\Delta)$.

###### Proof

If $\Delta$ is correct for $\sigma$ and $x\in\mathit{dom}(\Delta)$, then there
is some $(x,\mathit{io},x_{1}\ldots x_{n})\in\Delta$ and some $a_{1}\ldots
a_{n}\hookrightarrow a\in\mathit{io}$ with $\sigma(x)\in\gamma(a)$. Hence, by
definition of $\Delta(x)$, $a\sqsubseteq\Delta(x)$ so that
$\sigma(x)\in\gamma(a)\subseteq\gamma(\Delta(x))$. ∎

###### Lemma 2

If $\Delta=\\{(x,\\{\varepsilon\mapsto a\\},\varepsilon)\\}$ and
$\sigma(x)\in\gamma(a)$, then $\Delta$ is correct for $\sigma$.

###### Proof

This is an immediate consequence of the definition above. ∎

Now we can state the correctness of the inference rules in Fig. 3 as follows.

###### Theorem 0.B.2

Assume that the call types of all functions specified by $\mathit{CT}$ are
verified. Let $\mathit{Var}(e)\subseteq\mathit{dom}(\Delta)$,
$z\not\in\mathit{Var}(e)$, $\Delta,z=e\vdash\Delta^{\prime}$ be derivable by
the inference rules in Fig. 3, and $\sigma$ be a substitution such that
$\Delta$ is correct for $\sigma$. Then all finite reductions of $\sigma(e)$
end in some data term $t$ with $t\in\gamma(\Delta^{\prime}(z))$ and
$\Delta^{\prime}$ is correct for $\sigma$.

###### Proof

We assume that the preconditions of the theorem hold, i.e.,
$\Delta,z=e\vdash\Delta^{\prime}$ is derivable with a proof tree of height $h$
and $\sigma$ is a substitution such that $\Delta$ is correct for $\sigma$. By
Lemma 1, $\sigma(x)\in\gamma(\Delta(x))$ for all $x\in\mathit{Var}(e)$.

We prove the claim by induction on the number of steps of finite derivations
of $\sigma(e)$ and a nested induction on the height of the proof tree. We
distinguish the kind of expression $e$:

Variable:

If $e=x$, where $x$ is a variable, then $\sigma(x)\in\gamma(\Delta(x))$ is a
data term so that the evaluation of $\sigma(e)$ ends in $\sigma(x)$ (base case
with $0$ derivation steps) and
$\sigma(x)\in\gamma(\Delta(x))=\gamma(\Delta^{\prime}(z))$ (by rule Varnf).
With Lemma 2, the claim holds.

Constructor:

If $e=c(x_{1},\ldots,x_{n})$, where $x$ is a variable, then
$\sigma(x_{i})\in\gamma(\Delta(x_{i}))$ are data terms ($i=1,\ldots,n$) so
that $\sigma(e)$ is also a data term. Hence, the evaluation of $\sigma(e)$
ends in the data term $t=\sigma(e)$ (base case with $0$ derivation steps).
Since $\Delta^{\prime}=\\{(z,\\{\top^{n}\hookrightarrow
c^{\alpha}(\overline{\Delta(x_{n})})\\},x_{1}\ldots x_{n})\\}$ (by rule
Consnf), $t=\sigma(e)\in\gamma(\Delta^{\prime}(z))$ so that the claim holds
with Lemma 2.

Function:

Let $e=f(x_{1},\ldots,x_{n})$, $f$ defined by
$f(y_{1},\ldots,y_{n})=e^{\prime}$, and $\mathit{CT}(f)=a_{1}\ldots a_{n}$.
Since Funcnf is applicable,
$\sigma(x_{i})\in\gamma(\Delta(x_{i}))\subseteq\gamma(a_{i})$
($i=1,\ldots,n$). Let
$\sigma^{\prime}=\\{\overline{y_{n}\mapsto\sigma(x_{n})}\\}$. Then $\sigma(e)$
is reducible to $\sigma^{\prime}(e^{\prime})$ and, for all finite derivations
of $\sigma(e)$, the same result can be derived from
$\sigma^{\prime}(e^{\prime})$ with a smaller number of derivations steps so
that we can apply the induction hypothesis to $\sigma^{\prime}(e^{\prime})$.
Let

$\Delta^{\prime\prime}=\\{(y_{1},\\{\varepsilon\mapsto
a_{1}\\},\varepsilon),\ldots,(y_{n},\\{\varepsilon\mapsto
a_{n}\\},\varepsilon)\\}$

Since $\sigma^{\prime}(y_{i})=\sigma(x_{i})\in\gamma(a_{i})$ for
$i=1,\ldots,n$, by Lemma 2, $\Delta^{\prime\prime}$ is correct for
$\sigma^{\prime}$. Since the call type of $f$ is verified,
$\Delta^{\prime\prime},z^{\prime}=e^{\prime}\vdash\Delta^{\prime\prime\prime}$
is derivable for some fresh variable $z^{\prime}$ and some set
$\Delta^{\prime\prime\prime}$ of variable types. By the induction hypothesis,
$\sigma^{\prime}(e^{\prime})$ is non-failing. Let $t$ be some value of a
derivation of $\sigma^{\prime}(e^{\prime})$. The claim holds by Corollary 1:
In particular, there is some $a_{1}\cdots a_{n}\hookrightarrow
a\in\mathit{IO}(f)$ with $t\in\gamma(a)$. Since
$a\sqsubseteq\Delta^{\prime}(z)$ (by rule Funcnf and definition of
$\Delta^{\prime}(z)$), $t\in\gamma(\Delta^{\prime}(z))$ so that the claim
holds.

Or expression:

If $e=e_{1}~{}\mathit{or}~{}e_{2}$, then the first step of a derivation of
$\sigma(e)$ reduces to $\sigma(e_{1})$ or $\sigma(e_{2})$. Assume the case
$\sigma(e_{1})$ (the other is symmetric). Since
$\Delta,z=e_{1}\vdash\Delta_{1}$ is derivable with a proof tree of height
smaller than $h$, the induction hypothesis implies that $\sigma(e_{1})$ is
non-failing, $\Delta_{1}$ is correct for $\sigma$, and if $t$ is some value of
$\sigma(e_{1})$, then $t\in\gamma(\Delta_{1}(z))$. Since
$\Delta\subseteq\Delta^{\prime}$, $\Delta_{1}(z)\sqsubseteq\Delta^{\prime}(z)$
and the claim holds (note that $\Delta_{2}$ is also correct for $\sigma$ by
the induction hypothesis applied to the proof tree of
$\Delta,z=e_{2}\vdash\Delta_{2}$).

Free variables:

If $e=\mathit{let}~{}x_{1},\ldots,x_{n}~{}\mathit{free~{}in}~{}e^{\prime}$,
then the first step of a derivation of $\sigma(e)$ reduces to
$\sigma(\rho(e^{\prime}))$ for some substitution
$\rho=\\{\overline{x_{n}\mapsto t_{n}}\\}$ for the free variables. By rule
Freenf,
$\Delta\cup\\{(x_{i},\\{\varepsilon\hookrightarrow\top\\},\varepsilon)\mid
i\in\\{1,\ldots,n\\}\\},z=e\vdash\Delta^{\prime}$ is derivable with a proof
tree of height smaller than $h$. By induction hypothesis (the extended set of
variable types is trivially correct for $\sigma\circ\rho$),
$\sigma(\rho(e^{\prime}))$ is non-failing, $\Delta^{\prime}$ is correct for
$\sigma\circ\rho$, and if $t$ is some value of $\sigma(\rho(e^{\prime}))$,
then $t\in\gamma(\Delta^{\prime}(z))$. This proves the claim.

Let binding:

Let $e=\mathit{let}~{}x=e^{\prime}~{}\mathit{in}~{}e^{\prime\prime}$. First,
consider the evaluation of the bound expression $\sigma(e^{\prime})$. By rule
Letnf, $\Delta,x=e^{\prime}\vdash\Delta^{\prime}$ is derivable with a proof
tree of height smaller than $h$. Thus, by the induction hypothesis,
$\sigma(e^{\prime})$ is non-failing and $\Delta^{\prime}$ is correct for
$\sigma$. Consider some value $t^{\prime}$ of $\sigma(e^{\prime})$ used to
evaluate $\sigma(e)$ to $t$. Then $t^{\prime}\in\gamma(\Delta^{\prime}(x))$ by
the induction hypothesis. Let $\sigma^{\prime}=\\{x\mapsto
t^{\prime}\\}\circ\sigma$. Since
$\Delta\cup\Delta^{\prime},z=e^{\prime\prime}\vdash\Delta^{\prime\prime}$ is
derivable with a proof tree of height smaller than $h$, by the induction
hypothesis (note that
$\sigma^{\prime}(y)\in\gamma((\Delta\cup\Delta^{\prime})(y)$ for all
$y\in\mathit{Var}(e^{\prime\prime})$), $\sigma^{\prime}(e^{\prime\prime})$ is
also non-failing, $\Delta^{\prime\prime}$ is correct for $\sigma^{\prime}$,
and, if $t^{\prime\prime}$ is some value of
$\sigma^{\prime}(e^{\prime\prime})$,
$t^{\prime\prime}\in\gamma(\Delta^{\prime\prime}(z))$. Thus, the claim holds.

Case expression:

If $e=\mathit{case}~{}x~{}\mathit{of}~{}\\{p_{1}\to e_{1};\ldots;p_{n}\to
e_{n}\\}$, $\sigma(e)$ is evaluated by selecting some matching branch (note
that the discriminating argument $\sigma(x)$ cannot be evaluated since
$\sigma(x)\in\gamma(\Delta(x))$). Such a selection step is possible since
$\sigma(x)=c_{i}(y_{1},\ldots,y_{m})$ for some $i\in\\{1,\ldots,n\\}$ (since
the case expression covers all constructors). By rule Casenf,
$\Delta_{i},z=e_{i}\vdash\Delta^{\prime}_{i}$ is derivable with a proof tree
of height smaller than $h$, where $p_{i}=c_{i}(x_{1},\ldots,x_{m})$ and
$\Delta_{i}=(\Delta\wedge[x\mapsto
c_{i}])\cup\\{x_{1}::\top,\ldots,x_{m}::\top\\}$. Since
$(\Delta\wedge[x\mapsto c_{i}])$ constrains the abstract value of $x$ to the
abstraction of the actual value $\sigma(x)$, $\Delta_{i}$ is correct for
$\sigma\circ\rho$. Thus, by the induction hypothesis, $\sigma(\rho(e_{i}))$ is
non-failing, where $\rho$ is the matching substitution on the variables of
pattern $p_{i}$, and $\Delta^{\prime}_{i}$ is correct for $\sigma\circ\rho$.
If $t$ is some value of $\sigma(\rho(e_{i}))$, then
$t\in\gamma(\Delta^{\prime}_{i}(z))$ so that the claim holds (since
$\Delta^{\prime}_{i}\subseteq\Delta^{\prime}$). ∎

The previous theorem implies the following property of successfully checked
call types.

######  Corollary 2 (Correctness of call type checking)

If, for all operations $f$ defined by $f(x_{1},\ldots,x_{n})=e$ and
$\mathit{CT}(f)=a_{1}\ldots a_{n}$, the judgement

$\\{(x_{1},\\{\varepsilon\mapsto
a_{1}\\},\varepsilon),\ldots,(x_{n},\\{\varepsilon\mapsto
a_{n}\\},\varepsilon)\\},z=e\vdash\Delta$

is derivable (for some fresh variable $z$), then $f(t_{1},\ldots,t_{n})$ is
non-failing if the arguments satisfy the call types, i.e.,
$t_{i}\in\gamma(a_{i})$ ($i=1,\ldots,n$).

###### Proof

Let

$\Delta_{0}=\\{(x_{1},\\{\varepsilon\mapsto
a_{1}\\},\varepsilon),\ldots,(x_{n},\\{\varepsilon\mapsto
a_{n}\\},\varepsilon)\\}$

and $\sigma=\\{x_{1}\mapsto t_{1},\ldots,x_{n}\mapsto t_{n}\\}$ where
$t_{i}\in\gamma(a_{i})$ ($i=1,\ldots,n$). By Lemma 2, $\Delta_{0}$ is correct
for $\sigma$. By Theorem 0.B.2, all finite reductions of $\sigma(e)$ end in
some data term so that $f(t_{1},\ldots,t_{n})$ is non-failing. ∎