\documentclass [12pt] {article}
\usepackage[utf8]{inputenc}
\usepackage[russian]{babel}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\begin{document}

\sloppy
\begin{center}
{\it\Large The Logic of Demand in Haskell}\\
\end{center}

\renewcommand{\subsection}[1] {\par \textit{#1.}}
\renewcommand{\subsubsection}[1] {}

\section*{Preface}
This paper considers the usage of the pattern matching as a tool to control the logic of demand in a lazy
functional programming language Haskell.
Some theoretical results are given both with an automatic tools to proove P-logic rules for programm
validation.
\section{Introduction}
Haskell is a lazy functional language but by using pattern matching and irrefutable patterns 
fine control of computation flow may be achieved. The interaction between lazy
semantics and pattern matching is complicated and not well known.
Since pattern matching provides fine control on computation process it is impossible to specify the finite
set of rules for complete validation.
Application of P-logic to the Haskell pattern matching is introduced. It provides a formalization of mixed
evaluation and simplifies the validation of programms.

\section{A Haskell fragment and its informal semantics}
The section provides an overview of Haskell approach to data types and case expressions.
A formal semantics is also described.

\subsection{Data types}
The data type declarations are needed to describe data constructors, giving a set of signatures of type
constructors. Strictness of constructor argument is explicitly specified by the tag \texttt L or
\texttt S.
\subsection{Case expressions}
\label{case expressions}
Pattern matching is used in a simple case expressions, a left-hand part of definitions or in an explicit
abstractions. Since they all are similar only case expressions are focused.
\subsubsection{Evaluating case expressions}
A Haskell case expression is construction of the case descriminator and the list of the case branches.
The case expressions are evaluated by repeatedly matching patterns of a branches.
If no branch matches an unrecoverable error is raised and the computation flow is aborted.
\subsubsection{Pattern matching is a binding operation}
The pattern carry out two tasks: control of the branch to execute and a binding of the variables.
\subsubsection{Variables and wildcard patterns}
Using variable as a pattern matches every descriminator. Using wildcard, underscore (\textsf{\_}), is like
the variable pattern but no binding occurs.
\subsubsection{Constructor patterns: strict and lazy}
Data constructors in the patterns have to be applied exactly as described in the data type declaration.
Pattern is matched only if the descriminator has exact type and all of the sub-terms matches.
Lazy computation of \textit{i}-th argument in the cases other than irrefutable patterns described
below is implied by non-strict declaration in the data constructor.
\subsubsection{Irrefutable patterns defer matching}
By using operator \texttt{\~\,} the evaluation operation of the irrefutable branch pattern is deferred
till the pattern values are needed. Then it is fully evaluated. If it fails no alternative is tried
and an unrecoverable error is raised.
\subsubsection{Fine control of demand: An example}
\label{fine control}
The Haskell example using the Tree data construction highlights how the deferred computation is working
and some of the pitfalls are described.

\section{Background}
Section 3 describes the Haskell specific type-frame semantics and gives an overview of the adopted
simple model of ML polymorphism.

\subsection{Type-frame semantics}
Frame model provides <<objects>> and axioms of representability and functions from objects to objects in 
terms of an application operator. Also an environment model condition is described.

\subsection{A simple model of ML polymorphism}
An overview of different models of polymorphism is given. Since article focuses on a fine control of demand
in Haskell only ML polymorphism is considered. Othori's ML model is used due to it simplicity. Also it is
possible to give the predicate semantics to ML polymorphism.

\section{Formal semantics of a Haskell fragment}
Section 4 describes the formal semantics of Haskell, static and denotational. Since the article focuses 
the pattern
matching the type semantics is given for the patterns. It consists of a
pattern and a record type. Latter is introduced to capture variable bindings but not to extend
Haskell. The type frame notion is extended to describe the Haskell semantics. It is done in the context
of a domain theory and fits in it.
\subsection{The Haskell fragment}
The Haskell type system is provided with some details but also with special features ommited.
It is a convenient type system for implicit polymorphism. First, the formal rules for the patterns are given
using a record types in the type rules.

\subsection{Simple model of polymorphism for the Haskell fragment}
The subsection describes how the simple Othori's model of ground types is extended to the semantics of
polymorphic terms. Since the original model defines the meaning of polymorphic expressions in terms
of the ground instances and the type-indexed set of denotations it has to be adopted to reflect the
semantics of Haskell fragment.
\subsection{Haskell frames}
The subsection consists of the detailed description of the Haskell fragment frame.
\subsubsection{CPO structure}
The first part of the frame is complete partial order (cpo) semantics. 
Note that CPO semantics for typed $\lambda$-calculus is frame model.
\subsubsection{Pointedness in Haskell}
Every Haskell frame has a bottom element. The definitions of bottom of the compound frames are given in
a domain theory terms.
\subsubsection{Currying and Uncurrying}
Currying and uncurrying operators are defined and equations for them are given.
\subsubsection{Haskell data types}
Since data type constructors may be lazy recursive infinite types may be defined. Also strictness may be
specified explicitly. The saturation strict on \textit i-th argument property is defined to outline
the difference between meanings of the <<strictness>>.
\subsubsection{Type frames for data constructors}
Data type constructors are presented in the context of type frames. Also the article adduces the case of
curried constructors in the same context.
\subsubsection{Representing the Maybe monad in $\mathcal{D}$}
As pattern-matching is computed in Maybe monad, the monadic computation must be considered in the type 
frame semantics.
\subsubsection{Frame semantics of records}
Different aspects of record type are studied in the context of frame semantics.
A combination operator on the result of the monadic computation is defined.
\subsubsection{Control Operators: Diagrammatic Kleisli ($\diamond$) and Alternation ( $[]$ )}
The Definition of operators $\diamond$ and $[]$ for the simple types using Maybe monad are given.

\subsection{Typed semantics for the simply-typed Haskell fragment}
The denotation semantics is given in this section as a conservative extension of the semantic 
of ground terms.
\section{Logic for the Haskell fragment}
The denotation semantics only defines an abstract model, the verification logic is not considered.
P-logic is used to verify semantic properties of expressions.
This section provides the meaning to the formulas of P-logic by binding them with the formal semantics of the 
Haskell fragment. Some basic proof rules of P-logic are considered in the context of frame semantics.
Multi-place predicates are not considered since they are too complex and their formal definition
of the notion does not fit into the article.
The unary predicates and their usage are described both formal and informal. Both strict and lazy
P-logic predicates are defined in this section.

\subsection{Predicates in P-logic}
Two ways of the predicate combination in P-logic are described.
First, the implicit <<lifting>> of data type constructors to act as the predicate constructors in P-logic.
Second, the <<arrow>> predicate used to describe the compound predicate that is satisfied by the function-typed
expression.
Besides two of the atomic unary predicates, the abstract Haskell definition and the typing rules for predicates 
are provided.

\subsection{Judgement forms}
A judgement form in P-logic is a relation of typing environment and two lists of assertions:
the first whose conjunction is an assumption and the second whose disjunction constitutes the conclusion of judgement.
As the example property of the standard function map from Haskell prelude is given.

\subsection{Inference rules for properties of the Haskell fragment}
Two types of the inference rules in P-logic are defined: left, when property is on the left side of entailment
symbol, and the right one.

\subsubsection{Abstraction and function application}
Rules asserting an arrow property of the Haskell frame are defined. As the example the increment
function for the type Integer is considered and the formal validation rules are provided.
\subsubsection{Application}
Both right and left-introduction rules for the properties of the function application are defined
for the strong and weak arrow properties respectively.
\subsubsection{Constructor application}
Lifting data type constructor to the predicate constructor for further applying to the predicates is defined
and formal declaration in surface syntax is given. The paper defines the rule asserting difference of resulting predicate
constructors lifted from the different data types so the strict type validation may be achieved on
the preprocessing stage.

\subsection{Pattern matching}
The algorithms deriving predicates from the Haskell patterns are provided. Derived predicate describes both
the control aspect of a pattern and the subterms of matching term.
\subsubsection{Pattern predicates}
Since patterns may be nested, it is convenient to use the algorithmic calculation of patterns instead of
directl formulation of proof rules. Function \texttt{pi} implementing desired algorithms of
recursive pattern processing  and producing pattern 
predicates is defined and its Haskell code is given. Different examples of the irrefutable patterns
are considered, both with the explicit strictness modifiers and without them.
\subsubsection{The domain of a pattern}
The domain of a pattern is defined introducing predicate for a non-deferred match. Both irrefutable (or
wildcard) cases and strong matches are covered.
\subsubsection{Properties of case branches}
Two rules for the branch computation are defined --- one for the match successfull and another
for failure.
\subsubsection{Properties of case expressions}
Rules for the case computation are given using \texttt{Maybe} monad and the inductive monadic computation of
the set of branches.
\subsubsection{Example: deriving a property of a case expression}
The following examples are considered: one with the match that succeded and another with exception branch computation that
generates pattern match failure error (also known as <<Non-exhaustive pattern>> error).

\subsection{A semantic interpretation of P-logic}
P-logic extends a Haskell by providing the predicate constants and the predicate constructors.
The meaning of the simple type is intricated by the meaning of the predicates over underlying frame that interprets
the Haskell term type. The article gives the definition and description of the predicate environment.
\subsubsection{Strong predicates}
Also the interpretation of the characteristic predicates of sets in a type frame is defined.
\subsubsection{Universal predicates}
The paper gives the interpretation of the unversal predicates satisfied by any or only bottom element.
\subsubsection{Predicate variables}
The predicate variable is a result of applying the predicate environment map to the name of the variable.
\subsubsection{Data-induced congruence predicates}
The article provides the equation describing the meaning of a predicate formed with the data
constructor at a ground instance of the Haskell data type.
\subsubsection{Arrow predicates}
The function-typed term property characterizing a predicate is also described.
\subsubsection{Negated predicates}
\subsubsection{Polymorphic predicates}
The negated and polymorphic predicates are defined too.

\subsection{Satisfiability and validity of a sequent}
A formalization of a well-typed term to satisfy a compatibly typed predicate is given, stating it in the
setting of type frame semantics. A ground proposition and a bunch of sequent definitions are declared.
\subsubsection{Satisfiability of polymorphic predicates}
The lemma formalizing an assertion that the meaning of a polymorphic predicate cannont depend on the
structure of terms of underlaying type is suggested and proved.

\section{Soundness of P-logic}
Soundness of a logic means that all of its inference rules are coherent with its
semantics. An inference rule asserts a propositional implication of a consequent
judgement from zero or more antecedent judgement forms.

\subsection{Soundness of inference rules}
An inference rule is sound if the implication it states is valid for a model of the logic.
An implication is valid if it is true of a model under all type-compatible assignments
to variables.

\subsection{A reference frame model}
The section describes interpreter for the Haskell fragment which later will be used to check the soundness
of P-logic rules. It relies on Maybe monad to control the flow among alternate match as Haskell has explicit monads.
Also frame set of Haskell types is defined.
It is a set of representations of the saturated applications 
of its data constructors to elements of the frame sets of their argument types.

\subsection{Finite models for Haskell types}
Type constructions of the Haskell fragment are considered to show how each type or type construction
can be represented by a finite type in which to model some rule of P-logic.

\subsection{Modeling predicates}
The way to check the soundness of the rule with simulation of all type--compatile value assignment is
given. Notes about Univ and UnDef predicates are also supplied.

\subsection{Automated model checking of inference rules}
Checking the soundness of polymorphic inference rules with interpreter given in previous section is
described. Different steps of this process such as predicate assignment or choosing of a type
instance are provided in more or less details.

\section{Related Work}
As part of the Programatica project at the Pacific Software Research Center
a formal basis for reasoning about Haskell programs and automated tools for mechanizing such reasoning
are devoloping. Previous work on Miranda by Simon Thompson lacks ability to work with partialy
undefined or lazy data types hense Miranda itself provides no way to declare them.

Among verification verification tools Sparkle for lazy functional language Clean is outlined.
The Sparkle logic has a notation to express an undefined value but does not
provide modalities.

Stratego language from \texttt{http://stratego-language.org/} suggests algrebra for constructing complex data
types by the constructor congruences. This concept may be used in P-logic applied to the predicate
constructors and predicate congruences.

Larsen introduces weak-strong modality analogous to the one of P-logic
to discriminate \textit{must} and \textit{may} transitions in a process algebra. This analysis was generalized by
Huth, Jagadeesan and Schmidt. They provide a semantic interpretation of the modality in 
a more general framework.

Since all programming logics must confront the issue of undefined values induced by computational
environment and some other reasons partial logics that deal with undefinedness  have been studied
by many of groups. Among them are Owe, Gumb \& Lambert, Cheng \& Jones, Gries \& Schneider,
Konikowska and an excellent overview by Farmer.

\section{Conclusion}
The language fragment which concerns the paper is the patter-matching part of Haskell that has
impact on demand.
A formalization of the denotational and axiomatic semantics of Haskell pattern-matching is given. 
Unlike to ML with eager semantics the Haskell pattern-matching is much more complex.
Pattern-matching is essentially an eager activity, and is thus harmonious
with ML’s eager semantics.

The first part of this paper reports on part of a semantics for the whole of
Haskell. The denotational semantics was chosen because it allows evaluation of
P-logic expressions and sufficiently expressive to specify while language whith 
varying levels of formality operationally, denotationally, or informally: type classes
and overloading, polymorphism, polymorphic recursion, and mixed evaluation.
A pure domain-theoretic approach is sufficient in terms of expressivenes but lacks the abstraction for
a standart semantics. So frame semantics as a suitably abstract foundation for Haskell was
suggested.  The representation independence is extremely useful in the proof of soundness, allowing
to use model-checking over finite models of types for many rules.
Another virtue of frames as a semantic basis for Haskell is their close connection
to the semantics of ML polymorphism.  Overloading and polymorphic recursion can be neatly 
expressed in Ohori’s setting.

P-logic is a verification logic for all of Haskell, but the article has only provided 
here the part relative to Haskell’s fine control of demand. 
P-logic allows to formulate properties more precisely using both the weak and strong modalities.

The proof rules of P-logic are sufficiently subtle to validate in mind so the paper suggests the way to
mechanize the most detailed parts of a soundness proof.
The meta--theory that supports this automatic soundness checking is one of
the contributions of the paper.
\section*{Appendix}
The appendix consists of the detailed proof of two lemmas on associating and binding predicates to the pattern.
\end{document}
