% File: kri0.tex

% Author: Paolo Torrini <paolot@helios.dai.ed.ac.uk>

% Created: Mon Feb 15 1999

\documentclass{llncs}

%%\documentclass{/home/polh/Documents/Hs2Isa/llcns}

%%\documentstyle{/home/polh/Documents/Hs2Isa/llcns}

%%\documentclass[a4paper,12pt]{article}

\usepackage[dvips]{graphics}

\usepackage{amsfonts}

\usepackage{amssymb}

%\usepackage{psfig}

\usepackage{fancybox}

\usepackage{epsfig}

\usepackage{graphicx}

\usepackage{color}

%\usepackage{semrot}

%\input{newmacros}

% Use \includegraphics{*.eps} for pictures

\begin{document}

\title{Translating Haskell into Isabelle}

\author{Paolo Torrini, Till Mossakowski, Christian Maeder}

\institute {Informatik, Universitaet Bremen}

\date{}

\maketitle

\abstract{\scriptsize \bf Two partial translations of Haskell into Isabelle

higher-order logics have been implemented as functions of Hets, a

Haskell-based system for proof-management and program development that

allows for integration with other verification tools. Our application can

translate simple Haskell programs to HOLCF and, under stronger restrictions,

to HOL. Both translations use the static analysis of Programatica and are

based on a shallow embedding of denotations.}\\

% The translation of monads uses the AWE extension of Isabelle.}\\

\sloppy

\noindent

Translations between programming and specification languages, as well as the

corresponding integration of compilers, analyzers and theorem-provers, can

provide useful support to the formal development and verification of programs.

This task involves translating programs to a logic in which requirements can

be expressed, in order to prove the corresponding correctness statements.

Program translation should rest on a formal semantics of the programming

language allowing for proofs that are as easy as possible. In fact, it has

long been argued that functional languages, based on notions closer to

general, mathematical ones, can make the task of proving assertions on them

easier, owing to the relative clarity and simplicity of their semantics

\cite{Thompson92}.

In the following we are presenting automated translations of Haskell programs

into Isabelle higher-order logics that can be justified in terms of

denotational semantics. Haskell is a strongly typed, purely functional

language with lazy evaluation, polymorphic types extended with type

constructor classes, and a syntax for side effects and pseudo-imperative code

based on monadic operators \cite{HaskellRep}. The translations are

implemented as functions of Hets \cite{Hets}, an Haskell-based application

designed to support heterogeneous specification and formal development of

programs. Hets supplies with parsing, static analysis and proof management, as

well as with interfaces to various language-specific tools. As far as

interactive proofs are concerned, it relies on an interface with Isabelle, a

generic theorem-prover written in SML that includes the formalization of

several useful logics \cite{Paulson94isa}. Moreover, Hets relies on

Programatica \cite{Prog04} for the parsing and the static analysis of Haskell

programs. Programatica (built at OGI) is another Haskell-specific system for

formal development and it has a proof management on its own, including a

specification logic and translations to different proof tools, notably to

Isabelle \cite{Huff}, albeit following a different approach from ours (see

section~\ref{sec:Translations}).

\section{Isabelle}

Isabelle-HOL (hereafter HOL) is the implementation in Isabelle of classical

higher-order logic based on simply typed lambda calculus extended with

axiomatic type classes. It provides considerable support for reasoning about

programming functions, both in terms of rich libraries and efficient

automation. Since the late nineties, it has essentially superseded FOL

(classical first-order logic) in standard use. HOL has an implementation of

recursive functions based on Knaster-Tarski fixed-point theorem. All functions

are total; partiality may be dealt with by lifting types through the

\emph{option} type constructor.

On the other hand, HOLCF \cite{holcf} is HOL conservatively extended with the

logic of computable functions --- a formalization of domain theory. In HOL,

types --- elements of class \emph{type} --- are just sets; functions may not

be computable, and a recursive function may require discharging proof

obligations already at the stage of definition --- in fact, a specific measure

has to be given for the function to be proved monotonic. In contrast, HOLCF

has each type interpreted as an element of class \emph{pcpo} (pointed complete

partially ordered sets) i.e. as a set with a partial order which is closed

w.r.t. $\omega$-chains and has a bottom. In particular, the Isabelle

formalization of HOLCF is based on axiomatic type classes \cite{Wenzel},

making it possible to deal with complete partial orders in quite an abstract

way.

Domain theory offers a good basis for the semantical analysis of programming

languages. All functions defined over domains, including partial ones, are

continuous, therefore computable. Recursion can be expressed in terms of

least fixed-point operator, and so, in contrast with HOL, function definition

does not depend on proofs. Nevertheless, proving theorems may turn out to be

comparatively hard. After being spared the need to discharge proof

obligations at the stage of giving definitions, one has to bear with

assumptions over the continuity of functions while actually carrying out the

proofs. A standard strategy to get the best out of the two systems, is to

define as much as possible in HOL, using HOLCF type constructors to lift types

only when this is necessary.

\section{Translations}

\label{sec:Translations}

Translations can depend on the expressiveness of the target logic. As

examples, the translations into FOL of Miranda

\cite{Thompson95,Thompson89,Thompson95b} and Haskell \cite{Thompson92}, both

based on large-step operational semantics, appear to struggle with

higher-order features such as currying. The translation of Haskell to the Agda

implementation of Martin-Loef type theory in \cite{Abel} seems to struggle

with Haskell polymorphism. Higher-order logic may in fact quite help overcome

such obstacles. It also allows for higher-level approaches based on

denotational semantics, such as already proposed in \cite{Huff} for a

translation of Haskell into HOLCF, and in \cite{Pollack} for a translation of

ML into HOL. By using denotational semantics, one may hope to give

representations of programs that are closer to their specification, and to

give proofs that are relatively more abstract and general.

A shallow embedding into a logical language is one that relies heavily on its

extra-logical features, possibly taking advantage of built-in packages

provided with the implementation of that language, particularly with respect

to types and recursion. On the contrary, a deep embedding relies on the

logical definition of all the relevant notions. This may give a plus in

semantical clarity and possibly, provided the logic is expressive enough, in

generality as well. Taking advantage of built-in features, on the other hand,

may help make theorem proving less specific and tedious.

The translation of ML in \cite{Pollack} based on the definition of a class of

types with bottom elements in HOL gives an example of the deep sort. The

translation of Haskell to HOLCF proposed in \cite{Huff} relies on a generic

formalization of domain theory and particularly on the \emph{fixrec} package

for recursive functions, created to provide a friendly syntax covering also

mutually recursive definitions. However, in order to capture type constructor

classes --- an important feature of the Haskell type system --- a deep

embedding approach is used there, as well. Haskell types are translated to

terms, relying on a domain-theoretic modelling of the type system at the

object level. The practical drawback of this approach is that it leads to

plenty of the automation built into Isabelle type checking needing to be

reimplemented.

In contrast with \cite{Huff}, both the translations of Haskell to HOLCF and

HOL presented here are based on a shallow embedding approach. In the case of

HOLCF we use as well the \emph{fixrec} package. Moreover, we tend to rely as

much as possible on similarities between type systems, translating Haskell

types to HOLCF types in a comparatively direct way. Haskell classes are

translated to Isabelle axiomatic classes. Since we are trying to keep things

as simple as possible, the modelling we rely on is not very deep either: our

claim is that the equivalence between Haskell programs and their translation

to HOLCF can be justified up to the level of typeable output. This translation

covers a significant part of the syntax used in the Prelude, however there are

several limitations related to built-in types, pattern-matching, local

definitions, import and export. In particular, it does not cover type

constructor classes yet, although we have plans for an extention that should

address this aspect.

The translation to HOL, similar in matter of shallow approach, is nevertheless

much more limited. First, it only covers primitive recursive functions. This

limitation appears relatively hard to overcome, given the way syntax for full

recursion is defined in HOL. Moreover, we have to restrict to total functions.

Operational equivalence for a larger fragment could be obtained using option

types, but this is not pursued here.

\section{Translations in Hets}

Information about Hets may be found in \cite{HetsUG} and \cite{HetsUG}. The

Haskell-to-Isabelle translation requires GHC, Isabelle 2006 and Programatica.

The command to run the application is

\emph{hets -v[1--5] -t Haskell2Isabelle[HOLCF | HOL] -o thy out in.hs}

\noindent where arguments set options for verbosity, the logic, extension and name of

the output file, the last one being the input --- a Haskell program given as a

GHC file (\emph{in.hs}). This gets analyzed and translated, the result of a

successful run being an Isabelle theory file (\emph{out.thy}) in the given

logic.

%The application requires essentially Haskell GHC and Programatica. It

%is run by the command \emph{hets -t ... [h|hc] file.hs} where the

%options stand for HOL and HOLCF, respectively.

The internal representation of Haskell in Hets (modules \emph{Logic\_Haskell}

and \emph{HatAna}) is the same as in Programatica, whereas the internal

representation of Isabelle (modules \emph{Logic\_Isabelle} and \emph{IsaSign})

is essentially a Haskell reworking of the ML definition of Isabelle's own base

logic, extended in order to allow for a straightforward representation of HOL

and HOLCF.

Haskell programs and Isabelle theories are internally represented as Hets

theories --- each of them formed by a signature and a set of sentences,

according to the theoretical framework described in \cite{MossaTh}. Each

translation, defined in module \emph{Haskell2IsabelleHOLCF} as composition of

a signature translation with a translation of all sentences, is essentially a

morphism from theories in the internal representation of the source language

to those in the representation of the target language. The module

\emph{IsaPrint} contains functions for the pretty-printing of Isabelle

theories.

Each translation relies on an Isabelle theory, respectively \emph{HsHOLCF},

extending HOLCF, and \emph{HsHOL}, extending HOL, which contain some useful

notions --- notably definitions of lifting functions and an axiomatisation for

Haskell equality.

\section{Naming conventions} \label{section:nam}

Names of types as well as of terms are translated by a renaming function that

preserves them, up to avoidance of clashes with Isabelle keywords. We also

need to reserve a few names, as follows.

1) Names for type variables, in the translation to HOL: \emph{'vX}; any string

terminating with \emph{'XXn} where $n$ is an integer.

2) Names for term constants, in the translation to HOL: strings obtained by

joining together names of defined functions, using \emph{\_X} as end sequence

and separator.

3) Names for term variables, in both translations: \emph{pXn}, \emph{qXn},

with $n$ integer.

4) Names for type destructors, in the translation to HOLCF: \emph{C\_n},

where \emph{C} is a data constructor name and $n$ is an integer.

%Correspondingly, the translation function is defined as the

%composition of signature translation with the translation of all

%sentences.

%, has the

%structure of a morphism from Hets theories written in the language of

%the source internal representation to those in the language

%representation of the target language. Internally, the information

%about types is collected into a signature, whereas datatype

%declarations and definitions are associated with sentences.

% For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the

% module that contains the main translation function, carried out as

% composition of a signature morphism and a theory morphism.

% \emph{IsaSign.hs} contains the Hets representation of the Isabelle

% base logic and extensions.

% The general design of the translation functions, and particularly

% the two-layered recursion adopted for them, is similar to that used

% for the translation Haskell to Agda in Programatica.

\subsection{Types}

Our type translation are shallow and based on relative similarity of type

systems. Isabelle, as well as Haskell, is based on simple types with

polymorphism (which means, essentially, type variables, function and product

types). They both have built-in types for Boolean values and integers, and a

type constructor for lists. Both allows for sums, recursive and mutually

recursive types in the form of datatype declarations. Finally, they both have

a class mechanism --- although not quite the same.

The translation to HOLCF keeps into account partiality, i.e. the fact that a

function might be undefined for certain values, either because definition is

missing, or because the program does not terminate. It also keeps into

account laziness, i. e. the fact that by default function values in Haskell

are passed by name and evaluated only when needed. However, the idea that

underlies the translation is rather a simplifying one: although raising an

exception is different from running forever, and both are different from

stopping short of evaluation, still, from the point of view of the printable

output of ground types, these behaviours are similar and can be treated

semantically as such, i.e. using one and the same bottom element. So,

essentially, we are following the main lines of the ``crude'' denotational

semantics for lazy evaluation in \cite{winskel}, pp. 216--217.

% In order to ease the translation of some notions, the Isabelle

% theory \emph{HsHOLCF.thy}, that extends HOLCF has been defined and

% included in the Hets distribution.

% It is often convenient to define in Isabelle notions that match the

% translation of some itmes.

% Haskell datatype and function declarations are translated to

% declarations in HOLCF. Names are translated by a function that

% preserves them, up to avoidance of clashes with HOLCF keywords.

Haskell type variables are translated to HOLCF ones, of class \emph{pcpo}.

Each type in Isabelle has a sort, defined by the set of the classes of which

it is a member. Each built-in type is translated to the lifting of its

corresponding HOL type. The translation covers properly only Haskell Booleans

and unbounded integers, respectively associated to HOL Booleans and integers.

Bound integers and floating point numbers would require low-level modelling,

and have not been covered. Bounded integers are simply treated as unbounded.

The HOLCF type constructor \emph{lift} is used to lift HOL types to flat

domains. In the case of Booleans, HOLCF provides with type \emph{tr}, defined

as $bool \ lift$. In the case of integers, we define \emph{dInt} as $int \

lift$ in \emph{HsHOLCF}. The types of Haskell functions and product are

translated, respectively, to HOLCF function spaces and lazy product --- i.e.

such that $\bot = (\bot * \bot) \neq (\bot*'a) \neq ('a * \bot)$, consistently

with lazy evaluation. Type constructors are translated to corresponding HOLCF

ones (notably, parameters precede type constructors in Isabelle syntax). In

particular, lists are translated to the domain \emph{llist} defined in

\emph{HsHOLCF}.

% H%Rationals need to be

%imported in order to be used in Haskell, so they are not covered by

%the translation at the present stage (import has not been dealt with

%yet).

%and rationals.

Type translation to HOLCF, apart from mutual dependencies, may be summed up as

follows (where $t$ is a renaming function):

% Haskell datatype and function declarations are translated to

% declarations in HOLCF.

$$\begin{array}{lcl}

\lceil a \rceil & = & 'a_{t}::pcpo \\

\lceil Bool \rceil & = & tr \\

\lceil Integer \rceil & = & dInt \\

\lceil a \to b \rceil & = & \lceil a \rceil \to \lceil b \rceil \\

\lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\

\lceil [a] \rceil & = & \lceil a \rceil \ llist \\

\lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}

\end{array}$$

The translation to HOL is more crude. It takes into account neither partiality

nor laziness; therefore, we need to require that all functions in the program

are total ones. An account of partiality could be obtained, but here it is

not, using the \emph{option} type constructor to lift types, along lines

similar to those followed in HOLCF with \emph{lift}.

Haskell types are mapped into corresponding, unlifted HOL ones --- thus so for

Booleans and integers. All variables are of class \emph{type}. HOL function

type, product and list are used to translate the corresponding Haskell

constructors. Type translation to HOL, apart from mutual dependencies, may be

summed up as follows.

$$\begin{array}{lcl}

\lceil a \rceil & = & 'a_{t}::type \\

\lceil Bool \rceil & = & bool \\

\lceil Integer \rceil & = & int \\

\lceil a \to b \rceil & = & \lceil a \rceil \Rightarrow \lceil b \rceil \\

\lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\

\lceil [a] \rceil & = & \lceil a \rceil \ list \\

\lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}

\end{array}$$

\noindent Under each translation, function declarations

are associated, by using the keyword \emph{consts}, to the corresponding ones

in HOLCF and HOL, respectively. Datatype declarations are associated to the

corresponding ones, as well, but this involve some difference in the two

cases. In HOLCF datatype declarations define types of class \emph{pcpo} by the

keyword \emph{domain} (hence we may call them \emph{domain declarations}). In

HOL they define types of class \emph{type} by the keyword \emph{datatype}.

Notably, in contrast with Haskell and HOL, HOLCF datatype declarations require

an explicit introduction of destructors; these are provided automatically

according to the naming pattern in Section~\ref{section:nam}, point 4. Apart

from this aspect, the meta-level features of the the two type translations are

essentially similar.

Translation of mutually recursive datatypes, as the one shown in the following

example, relies on specific Isabelle syntax (using the keyword \emph{and}).\\

$data \ AType \ a \ b \ = \ ABase \ a \ | \ AStep \ (AType \ a \ b) \ (BType \ a \ b) $

$data \ BType \ a \ b \ = \ BBase \ b \ | \ BStep \ (BType \ a \ b) \ (AType \ a \ b) $\\

\noindent Translation to HOLCF gives the following.

$$\begin{array}{rr} domain & \ ('a::pcpo, 'b::pcpo) \ BType \ = \ BBase \ (BBase\_1::'b) \ | \\

& BStep \ (BStep\_1::('a, 'b) \ BType) \ (BStep\_2::('a, 'b) \ AType) \\

and & \ ('a::pcpo, 'b::pcpo) \ AType \ = \ ABase \ (ABase\_1::'a) \ | \\

& AStep \ (AStep\_1::('a, 'b) \ AType) \ (AStep\_2::('a, 'b) \ BType) \\

\end{array}$$

\noindent Translation to HOL gives the following.

$$\begin{array}{rll} datatype & \ ('a, 'b) \ BType & = \ BBase \ 'b \ | \\

& & BStep \ (('a, 'b) \ BType) \ (('a, 'b) \ AType) \\

and & \ ('a, 'b) \ AType & = \ ABase \ 'a \ | \\

& & AStep \ (('a, 'b) \ AType) \ (('a, 'b) \ BType) \\

\end{array}$$

\noindent In contrast with

Haskell, order of declarations matters in Isabelle, where they should always

be listed according to their dependency. Both translations take care of this

aspect automatically.

\subsection{HOLCF: Sentences}

Essentially, each function definition is translated to a corresponding ones.

Non-recursive definitions are translated to standard Isabelle definitions

(introduced by the keyword \emph{defs}), whereas the translation of recursive

definitions relies on the \emph{fixrec} package. Lambda abstraction is

translated as continuous abstraction (\emph{LAM}), function application as

continuous application (the \emph{dot} operator). These notions coincide with

the corresponding ones in HOL, i.e. with lambda abstraction (\emph{\%}) and

standard function application, whenever all arguments are continuous.

% As to the translation of terms containing either values or operators

% of built-in type, it is often the case that we translate them to

% lifted HOL operators. The lifting function is \emph{Def}; $\bot$ is

% used for the undefined case.

Terms of built-in type (Boolean and integer) are translated to lifted HOL

values, using the HOLCF-defined lifting function \emph{Def}. The bottom

element $\bot$ is used for all the undefined terms. We use the following

operator, defined in \emph{HsHOLCF}, to map binary arithmetic functions to

lifted functions over lifted integers.\\

$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)

\Rightarrow ('a \ lift \to \ 'b \ lift \to \ 'c \ lift) $

$fliftbin \ f \ == \ LAM \ y x. \ (flift1 \ (\%u. \ flift2 \ (\%v. \ f \ v \ u))) \cdot x \ \cdot y $\\

\noindent Boolean values are translated to values of \emph{tr} --- i.e.

\emph{TT}, \emph{FF} and $\bot$. Boolean connectives are translated to the

corresponding HOLCF lifted operators. HOLCF-defined \emph{If then else fi} and

\emph{case} syntax are used to translate conditional and case expressions,

respectively. There are some restrictions, however, on the latter, due to

limitations in the translation of patterns (see Section~\ref{sec:Patterns});

in particular, the case term should always be a variable, and no nested

patterns are allowed.

The translation of lists relies on the following domain, defined in \emph{HsHOLCF}.\\

$domain \ 'a\ llist \ = \ lNil \ | \ lCons \ (lHd :: \ 'a) \ (lTl :: \ 'a \ llist) $\\

\noindent Under the given interpretation, an infinite list as well as

an undefined one evaluate to $\bot$. However, the value of finite prefixes,

and particularly the printable output associated to them, will be the expected

one, since the model of evaluation is lazy.

Haskell allows for local definitions by means of \emph{let} and \emph{where}

expressions. Those \emph{let} expressions in which the left-hand side is a

variable are translated to similar Isabelle ones; neither other \emph{let}

expressions (i.e. those containing patterns on the left hand-side) nor

\emph{where} expressions are covered. The translation of terms (minus mutual

recursion) may be summed up, essentially, as follows:

$$\begin{array}{lcl}

\lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\

\lceil c \rceil & = & c_{t} \\

\lceil \backslash x \ \to \ f \rceil & = & LAM \ x_{t}. \ \lceil f \rceil \\

\lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\

\lceil f \ a_{1} \ldots a_{n} \rceil & = & FIX \ f_{t}. \ f_{t} \ \cdot \

\lceil a \rceil \ldots \cdot \ \lceil a_{n} \rceil \\

& & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\

\lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =

& let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil

% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil

% \ldots \lceil a_{n} \rceil \ TyCons_{t}

\end{array}$$

%In HOLCF, where every type is a domain and every function is

%continuous,

\noindent In HOLCF all recursive functions can be defined by fixpoint

operator --- a function that, given as argument the defining term abstracted

of the recursive call name, returns the corresponding recursive function.

Coding this directly turns out to be rather cumbersome, particularly in the

case of mutually recursive functions, where tuples of defining terms and

tupled abstraction would be needed. In contrast, the \emph{fixrec} package

allows us to handle fixpoint definitions in a way quite more similar to

ordinary Isabelle recursive definitions, providing also with friendly syntax

for mutual recursion. \\

\noindent $ fun1 \ :: \ (a \to c) \ \to \ (b \to d) \

\to \ AType \ a \ b \ \to \ AType \ c \ d $

$$\begin{array}{lll}

fun1 & f \ g \ k & = \ case \ k \ of \\

& ABase \ x & \to \ ABase \ (f \ x) \\

& AStep \ x \ y & \to \ AStep \ (fun1 \ f \ g \ x) \ (fun2 \ f \ g \

y)

\end{array} $$

$ fun2 \ :: \ (a \to c) \ \to \ (b \to d) \ \to \ BType \ a \ b \ \to \ BType \ c \ d $

$$\begin{array}{lll}

fun2 & f \ g \ k & = \ case \ k \ of \\

& BBase \ x & \to \ BBase \ (g \ x) \\

& BStep \ x \ y & \to \ BStep \ (fun2 \ f \ g \ x) \ (fun1 \ f \ g \ y)

\end{array} $$

\noindent As an example, the above code translates to HOLCF as follows.\\

\noindent $consts $

$$

\begin{array}{ll} fun1 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to 'd::pcpo) \ \to \\

& ('a::pcpo, 'b::pcpo) \ AType \ \to \ ('c::pcpo, 'd::pcpo) \ AType \\

fun2 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to

'd::pcpo) \ \to \\

& ('a::pcpo, 'b::pcpo) \ BType \ \to \ ('c::pcpo, 'd::pcpo) \ BType

\end{array}$$

$$\begin{array}{rccl}

fixrec & fun1 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\

& & & ABase \cdot pX1 \ => \ ABase \cdot (f \cdot pX1) \ | \\

& & & AStep \cdot pX1 \cdot pX2 \ => \\

& & & \ AStep \cdot (fun1 \cdot f \cdot g \cdot pX1) \cdot (fun2 \cdot f \cdot g \cdot pX2)) \\

and & fun2 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\

& & & BBase \cdot pX1 \ => \ BBase \cdot (g \cdot pX1) \ | \\

& & & BStep \cdot pX1 \cdot pX2 \ => \\

& & & \ BStep \cdot (fun2 \cdot f \cdot g \cdot pX1) \cdot (fun1 \cdot f \cdot g \cdot pX2)) \end{array}$$

\noindent The translation take care automatically of the fact that,

in contrast with Haskell, Isabelle requires patterns in case expressions to

follow the order of datatype declarations.

\subsection{HOL: Sentences}

Non-recursive definitions are treated in an analogous way as in the

translation to HOLCF. Standard lambda-abstraction ($\%$) and function

application are used here, instead of continuous ones. Partial functions, and

particularly case expressions with incomplete patterns, are not allowed. The

translation of terms (minus recursion and case expressions) may be summed up

as follows.

$$\begin{array}{lcl}

\lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\

\lceil c \rceil & = & c_{t} \\

\lceil \backslash x \ \to \ f \rceil & = & \% \ x_{t}. \ \lceil f \rceil \\

\lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\

\lceil f \ a_{1} \ldots a_{n} \rceil & = & f_{t} \ \lceil a \rceil \ldots \ \lceil a_{n} \rceil \\

& & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\

\lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =

& let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil

% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil

% \ldots \lceil a_{n} \rceil \ TyCons_{t}

\end{array}$$

\noindent Recursive definitions set HOL and HOLCF apart. In HOL one has to

pay attention to the distinction between primitive recursive functions

(introduced by the keyword \emph{primrec}) and generic recursive ones (keyword

\emph{recdef}). Termination is guaranteed for each of the former, by the fact

that recursion is based on the datatype structure of one of the parameters. In

contrast, termination is not a trivial matter for the latter. A strictly

decreasing measure needs to be provided, in association with the parameters of

the defined function. This requires a degree of ingenuity that cannot be

easily dealt with automatically. For this reason, the translation to HOL is

restricted to primitive recursive functions. Mutual recursion is allowed for

under some additional restrictions --- more precisely:

1) all the functions involved are recursive in the first argument;

2) recursive arguments are of the same type in each function.

\noindent

As an example, the translation of mutually recursive functions of type $a

\rightarrow b, \ldots a \rightarrow d$, respectively, introduces a new

function of type $a \rightarrow (b * \ldots * d)$ which is recursively

defined, for each case pattern, as the product of the values correspondingly

taken by the original ones. The following is a concrete example.

\\

\noindent $ fun3 \ :: \ AType \ a \ b \to (a \to a) \to AType \ a \ b $

$$\begin{array}{ll}

fun3 \ k \ f & = \ case \ k \ of \\

& ABase \ a \to ABase \ (f \ a) \\

& AStep \ a \ b \to AStep \ (fun4 \ a) \ b \\

\end{array}$$

\noindent $ fun4 \ :: \ AType \ a \ b \to AType \ a \ b $

$$\begin{array}{ll}

fun4 \ k & = \ case \ k \ of \\

& AStep \ x \ y \to AStep \ (fun3 \ x \ (\backslash z \to z)) \ y \\

& ABase \ x \to ABase \ x \\

\end{array}$$

\noindent The translation to HOL of these two functions gives the following.\\

\noindent $consts$

$$\begin{array}{ll}

fun3 \ :: & ('a::type, 'b::type) \ AType \Rightarrow ('a \Rightarrow

'a) \Rightarrow \\

& ('a, 'b) \ AType \\

fun4 \ :: & ('a::type, 'b::type) \ AType \Rightarrow ('a \Rightarrow

'a) \Rightarrow\\

& ('a, 'b) \ AType \\

fun3\_Xfun4\_X :: & ('a::type, 'b::type) \ AType \Rightarrow \\

& (('aXX1::type \Rightarrow 'aXX1::type) \Rightarrow \\

& ('aXX1, 'bXX1) \ AType) * \\

& (('aXX2::type \Rightarrow 'aXX2::type) \Rightarrow \\

& ('aXX2, 'bXX2) \ AType) \\

\end{array}$$

\noindent $defs$

$$\begin{array}{lll}

fun3\_def : & fun3 \ == \ \% k \ f. \ fst \ (( fun3\_Xfun4\_X :: \\

& \ ('a::type, 'b::type) \ AType \Rightarrow (('a \Rightarrow 'a) \\

& \Rightarrow ('a, 'b) \ AType) * ((unit \Rightarrow unit) \Rightarrow \\

& (unit, unit) \ AType) ) \ k) \ f \\

fun4\_def : & fun4 \ == \ \% k \ f. \ snd \ (( fun3\_Xfun4\_X :: \\

& ('a::type, 'b::type) \ AType \Rightarrow \\

& ((unit \Rightarrow unit) \Rightarrow (unit, unit) \ AType) * \\

& (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AType) ) \ k) \ f \\

\end{array}$$

\noindent $primrec$

$$\begin{array}{lll}

fun3\_Xfun4\_X & (ABase \ pX1) \ = & (\% f. \ ABase \ (f \ pX1), \\

& & \% f. \ ABase \ pX1) \\

fun3\_Xfun4\_X & (AStep \ pX1 \ pX2) & = \\

& (\% f. \ AStep \ (snd & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2, \\

& \% f. \ AStep \ (fst & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2) \\

\end{array}$$

\noindent One may note that the type of the recursive function,

for each of its call in the body of non-recursive definitions, is given by

instantiations where the Isabelle unit type is replaced for each type variable

which is not occurring on the right hand-side, i.e. for each variable which is

not constrained by the type of the defined function. This is required by

Isabelle, in order to avoid definitions from which inconsistencies could be

derivable. Other meta-level features are essentially common to both

translation.

\subsection{Patterns}

\label{sec:Patterns}

% not allowed in Isabelle with ordinary definitions (keyword

% \emph{Defs}), but it is allowed with the syntax for recursive ones.

Multiple function definitions using top level pattern matching are translated

as definitions based on a single case expression. This syntactical choice has

more to do with HOL than with HOLCF. In fact, multiple definitions in Isabelle

are only allowed with the syntax of recursive ones. In primitive recursive

definitions, HOL allows for patterns only in one parameter. Therefore, in

order to translate definitions having patterns in more than one, before

resorting to a more complex syntax (with tuples and \emph{recdef} instead of

\emph{primrec}), it turns out comparatively easier to internally deal with

multiple definitions as with case expressions. An example follows.

\\

\noindent $ctl \ :: \ Bool \to Bool \to Bool \to Bool$ \\

$ctl \ False \ a \ False \ = \ a $\\

$ctl \ True \ a \ False \ = \ False $\\

$ctl \ False \ a \ True = \ True $\\

$ctl \ True \ a \ True \ = \ a $\\

\noindent Translation to HOL gives the following.\\

\noindent $consts \ ctl :: \ bool \Rightarrow bool \Rightarrow bool \Rightarrow bool$\\

\noindent $defs$

$$\begin{array}{llll}

ctl\_def : & ctl \ == & \% qX1 \ qX2 \ qX3. & case \ qX1 \ of \\

& & False \Rightarrow case \ qX3 & of \\

& & & False \Rightarrow qX2 \\

& & & | \ True \Rightarrow True \\

& & | \ True \Rightarrow case \ qX3 & of \\

& & & | \ False \Rightarrow False \\

& & & True \Rightarrow qX2 \\

\end{array}$$

\noindent This example cannot be handled by the translation to

HOLCF, owing to the mapping of Boolean values to type \emph{tr}, which is not

a recursive datatype. The following, where a defined datatype is used instead

of Boolean, gives the closest alternative that can be dealt with.\\

\noindent $data \ TV \ = F \ | \ T $\\

\noindent $ctlx :: \ TV \to TV \to TV \to TV $ \\

$ctlx \ F \ a \ F \ = \ a $ \\

$ctlx \ T \ a \ F \ = \ F $ \\

$ctlx \ F \ a \ T \ = \ T $ \\

$ctlx \ T \ a \ T \ = \ a $\\

\noindent This translates to HOLCF as follows.\\

\noindent $domain \ TV \ = \ F \ | \ T $

\noindent $consts \ ctlx :: \ TV \to TV \to TV \to TV $\\

\noindent $defs$

$$\begin{array}{llll}

ctlx\_def : & ctlx \ == & LAM \ qX1 \ qX2 & qX3. \ case \ qX1 \ of \\

& & F \Rightarrow case \ qX3 & of \\

& & & F \Rightarrow qX2 \\

& & & | \ T \Rightarrow T \\

& & | \ T \Rightarrow case \ qX3 & of \\

& & & F \Rightarrow F \\

& & & | \ T \Rightarrow qX2 \\

\end{array}$$

\noindent

Support of patterns in definitions and case expressions is more restricted in

Isabelle than in Haskell. Nested patterns are overall disallowed. In case

expressions, the case term is required to be a variable. Both of these

restrictions apply to our translations. A further Isabelle limitation ---

sensitiveness to the order of patterns in case expressions --- is dealt with

automatically. Similarly, wildcards, not available in Isabelle, are dealt

with and may be used, in case expressions as well as in function definition,

though not in nested position. The translation to HOLCF can also handle

incomplete patters, also not allowed by Isabelle, in function definitions as

well as in case expressions, by using $\bot$ as default value. As nested

patterns are not covered, guarded expressions and list comprehension are

neither; anyway these can be avoided easily enough, using conditional

expressions and \emph{map} instead.

\subsection{Classes}

Conceptually, type classes in Isabelle are quite different from those in

Haskell. The former are associated with sets of axioms, whereas the latter

come with sets of function declarations. Moreover, Isabelle allows only for

classes with a single type parameter. Most importantly, Isabelle does not

allow for type constructor classes. The last limitation is rather serious,

since it makes hard to cope with essential Haskell features such as monads and

the \emph{do} notation. In alternative to the method proposed in \cite{Huff},

we would like to get around the obstacle by relying on an extension of

Isabelle based on theory morphism (see section~ \ref{sec:Monads}). The AWE

system \cite{AWE} is in fact an implementation of such an extension.

Defined classes are translated to Isabelle as classes with empty

axiomatization. Every class is declared as a subclass of \emph{type} --- also

in the case of HOLCF, in order to allow for instantiation with lifted built-in

types, as well. The translations stay simple and cover only classes with no

more than one type parameter --- one could probably do something more using

tuples, but this would surely involve considerable complication dealing with

conditional instantiations.

Instance declarations are translated to corresponding ones in Isabelle.

Isabelle instances in general require proofs that class axioms are satisfied

by the types, but as long as there are no axioms the proofs are trivial and

carried out automatically. Method declarations are translated to independent

function declarations with appropriate class annotation on type variables.

Method definitions associated with instance declarations are translated to

overloaded function definitions, using type annotation. An example follows.

\\

\noindent $class \ ClassA \ a \ where$

$abase :: \ a \to Bool $

$ astep :: \ a \to Bool $\\

\noindent $instance \ (ClassA \ a, \ ClassA \ b) \Rightarrow ClassA \ (AType \ a \ b) \ where $

$$\begin{array}{ll}

abase \ x \ = & case \ x \ of \\

& ABase \ u \ \to \ True \\

& \_ \ \to \ False \\

\end{array}$$

\noindent The translation of this code to HOLCF gives the following.\\

\noindent $axclass \ ClassA < type$

\noindent $instance \ AType::(\{pcpo, ClassA\}, \{pcpo, ClassA\}) \ ClassA$

$by \ intro\_classes$\\

\noindent $consts$

$$\begin{array}{ll}

abase :: & 'a::\{ClassA, pcpo\} \to tr \\

astep :: & 'a::\{ClassA, pcpo\} \to tr \\

default\_abase :: & 'a::\{ClassA, pcpo\} \to tr \\

default\_astep :: & 'a::\{ClassA, pcpo\} \to tr \\

\end{array}$$

\noindent $defs$

$$\begin{array}{rl}

AType\_abase\_def : \ abase :: & \\

('a::\{ClassA, pcpo\}, & 'b::\{ClassA, pcpo\}) \ AType \to tr \\

== & LAM x. \ case \ x \ of \\

& ABase \cdot pX1 \Rightarrow TT \ | \\

& AStep \cdot pX2 \cdot pX1 \Rightarrow FF \\

AType\_astep\_def : \ astep :: & \\

('a::\{ClassA, pcpo\}, & 'b::\{ClassA, pcpo\}) \ AType \to tr \\

& == default\_astep \\

\end{array}$$

\noindent Translation to HOL, on the other hand, gives the following.\\

\noindent $axclass \ ClassA < type$\\

\noindent $instance \ AType::(\{type, ClassA\}, \{type, ClassA\}) \ ClassA$

$by \ intro\_classes$\\

\noindent $consts$

$$\begin{array}{ll}

abase :: & 'a::\{ClassA, type\} \Rightarrow bool\\

astep :: & 'a::\{ClassA, type\} \Rightarrow bool\\

default\_abase :: & 'a::\{ClassA, type\} \Rightarrow bool\\

default\_astep :: & 'a::\{ClassA, type\} \Rightarrow bool\\

\end{array}$$

\noindent $defs$

$$\begin{array}{rl}

AType\_abase\_def : \ abase :: & \\

('a::\{ClassA, type\}, & 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\

== & \% x. \ case \ x \ of \\

& ABase \ pX1 \Rightarrow True \\

& | \ AStep \ pX2 \ pX1 \Rightarrow False \\

AType\_astep\_def : \ astep :: & \\

('a::\{ClassA, type\}, & 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\

== & default\_astep\\

\end{array}$$

\noindent

The additional functions declared for default use in method definition are

close mirrors of an internal feature of the Programatica representation.

In the Programatica internal representation of Haskell, for each function,

information about the class of type parameters is encoded by including in the

internal representation of the function some extra arguments (\emph{dictionary

parameters}) on top of the original ones. This is particularly useful in the

case of overloaded definitions. On the other hand, class information in

Isabelle can be represented by direct annotation on the arguments. Therefore,

the translation eliminates dictionary parameters and gives function

definitions based on their external representation instead. However, for each

definition, our translations gives a function explicitly annotated with its

type, inclusive of class annotation, in order to allow for overloading (just

for the sake of formatting, this type annotation has been delated in some of

the examples shown).

\subsection{Equality}

Equality is the only built-in class which is covered by the two translations.

Axiomatizations for the associated methods are provided in the base theories

--- \emph{HsHOLCF} and \emph{HsHOL}, respectively. Both axiomatizations are

based on the abstract definition of equality and inequality given in

\cite{HaskellRep}.

\\

\noindent $consts$

$$ \begin{array}{ll}

hEq :: & ('a::Eq) \ lift \ \to \ 'a \ lift \ \to \ tr \\

hNEq :: & ('a::Eq) \ lift \ \to \ 'a \ lift \ \to \ tr\\

\end{array}$$

\noindent $axioms$

$$\begin{array}{ll}

axEq: & ALL \ x. \ (hEq \cdot p \cdot q \ = \ Def \ x) \ = \\

& (hNEq \cdot p \cdot q \ = \ Def \ (\sim x)) \\

\end{array}$$

\noindent

The definition of Boolean equality in \emph{HsHOLCF} is obtained by lifting

HOL equality, so that $\bot$ is returned whenever one of the argument is

undefined.

\\

\noindent $tr\_hEq\_def: \ hEq \ == \ fliftbin \ (\% (a::bool) \ b. \ a \ = \ b)$\\

%ax1: & hEq \cdot p \cdot p \ == \ Def \ true \\

%ax2: & [| \ hEq \cdot q \cdot r \ = \ Def \ true; \ hEq \cdot p \cdot q \ = \ Def \ true \ |] \\

% & ==> \ hEq \cdot p \cdot r \ = \ Def \ true \\

\noindent

All built-in methods for built-in types are defined in a similar way.

In \emph{HsHOL} equality is axiomatized under the implicit assumption of

restricting to terminating programs.

\\

\noindent $consts$

$$\begin{array}{ll}

hEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\

hNEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\

\end{array}$$

\noindent $axioms$

$$\begin{array}{ll}

axEq: & hEq \ p \ q \ == \ \sim hNEq \ p \ q \\

\end{array}$$

\noindent Under that assumption, equality for built-in types can be

identified with HOL equality.

% ax1: & hEq \ p \ p \\

% ax2: & [| \ hEq \ q \ r; \ hEq \ p \ q \ |] ==> hEq \ p \ r \\

\subsection{Monads}

\label{sec:Monads}

Isabelle does not allow for classes of type constructors --- hence the problem

in representing monads. We could deal with this problem relying on an

axiomatization of monads that allows for the representation of monadic types

as an axiomatic class, as presented in \cite{Lueth}. Monadic types should be

translated to newly defined types that satisfy monadic axioms. This would

involve defining a theory morphism, as an instantiation of type variables in

the theory of monads. We are planning to rely on AWE \cite{AWE}, an

implementation of theory morphism on top of Isabelle base logic that may be

used to extend HOL as well.

\section{Conclusion}

The following is a list of features that are covered by our

translations.

\begin{itemize}

\item predefined types: Boolean, Integer.

\item predefined type constructors: function, Cartesian product, list.

\item declaration of recursive datatype, including mutually recursive ones.

\item predefined functions: equality, Boolean operators, connectives, list

constructors, head and tail list functions, arithmetic operators.

\item non-recursive functions, including conditional, \emph{case} and

\emph{let} and expressions (with restriction related to use of

patterns).

\item use of incomplete patterns (in HOLCF) and of wildcards in case

expressions.

\item total primitive recursive functions (in HOL) and partial recursive ones

(in HOLCF), including mutually recursive ones (with restrictions in the HOL

case).

\item single-parameter class and instance declarations.

% \item monad declarations and do notation.

\end{itemize}

The shallow embedding approach makes it possible to get most of the benefit

out of the automation currently available on Isabelle. Further work might

carry an extension to cover P-logic \cite{KiebPl}, a specification formalism

for Haskell programs that is included in the Programatica toolset.

%This translation, due to the character of the P-logic

%typing system, could be more easily carried out relying on some form

%of universal quantification on type variables, or else further relying

%on parametrisation.

\bibliographystyle{alpha}

\bibliography{case}

\end{document}

In our example,

translation gives the

following.\\

\noindent $consts$

$$ \begin{array}{ll}

fun1 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\

& ('a::type, 'b::type) \ Prelude\_AType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_AType \\

fun1\_Xfun2\_X & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \\

& (('bXX1::type \Rightarrow 'dXX1::type) \ \Rightarrow \\ & ('aXX1::type, 'bXX1::type) \ Prelude\_AType \ \Rightarrow \\ & ('cXX1::type, 'dXX1::type) \ Prelude\_AType) * \\

& (('bXX2::type \Rightarrow 'dXX2::type) \ \Rightarrow \\ & ('aXX2::type, 'bXX2::type) \ Prelude\_BType \ \Rightarrow \\ & ('cXX2::type, 'dXX2::type) \ Prelude\_BType) \\

fun2 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\

& ('a::type, 'b::type) \ Prelude\_BType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_BType \\

\end{array}$$

\noindent $defs$

$$ \begin{array}{ll}

fun1\_def : & fun1 \ == \ \% f. \% g. \% k. \ fst (fun1\_Xfun2\_X \ f) \ g \ k \\

fun2\_def : & fun2 \ == \ \% f. \% g. \% k. \ snd (fun1\_Xfun2\_X \ f) \ g \ k

\end{array}$$

\noindent $primrec$

$$ \begin{array}{ll}

fun1\_Xfun2\_X \ (ABase \ pX1) & = \ (\% g. \% k. \ ABase \ (f \ pX1)) \\

fun1\_Xfun2\_X \ (BBase \ pX1) & = \ (\% g. \% k. \ BBase \ (g \ pX1)) \\

fun1\_Xfun2\_X \ (AStep \ pX1 \ pX2) & = \ (\% g. \% k. \ AStep \\

& (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\

& (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\

fun1\_Xfun2\_X \ (BStep \ pX1 \ pX2) & = \ (\% g. \% k. \ BStep \\

& (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\

& (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\

\end{array}$$

\subsection{Equality: HOLCF}

\subsection{Equality: HOL}

...

...

Haskell classes and instances are translated to Isabelle,

respectively, as classes with empty axiomatisation and as instances

with trivial instantiation proof. The translation supports only

single-parameter classes --- in principle, more than one parameter

could be handled using tuples.

Built-in classes --- Eq and Ord in particular --- are translated to

newly defined classes in Isabelle; the corresponding axiomatisation

however here is not provided !!!

...

Functions declarations associated to classes are translated to

Isabelle as independent function declarations with appropriate class

annotation. Function definitions associated to instances are

translated as overloaded function definitions, relying on class

annotation of typed variables.

...

% ...xxx...!!! check out for stuff to include in Classes ---

Non-recursive definitions are translated to ordinary definitions (keyword

\emph{defs}), whereas recursive ones require specific keywords. The

type of the function, inclusive of class annotation, is included in

every definitions in order to allow for overloading.

%For values of

%built-in type, the lifting function is \emph{Def}; the undefined case

%collapses on $\bot$.

...

...

In HOLCF, where every type is a domain and every function is

continuous, all recursive functions can be defined by fixpoint

operator. This is essentially a function that, given as argument the

function definition body abstracted of the recursive call name,

returns the corresponding recursive function. Coding this directly

would be rather cumbersome, particularly in the case of mutually

recursive functions, where tuples of definition bodies and tupled

abstraction are needed. We can instead rely on the \emph{recdef}

package, which allows to handle fixpoint definitions like ordinary

recursive ones, offering nice syntax to deal with mutual recursion as

well.

...

\subsection{HOL: Type signature}

The present translation to HOL is very basic, and does take into

account neither partiality nor laziness. Essentially, it left to the

Haskell programmer to check that all the functions are total ones.

An account of partiality -- although possibly not aof laziness ---

could be obtained using the option type constructor to lift types,

along a similar line to lift. Here however we are presenting just a

plain version, mapping Haskell types in the corresponding unlifted HOL

types. All variables belong to the class type. Recursive and mutually

recursive data-types declarations are translated to HOL datatype

declaration.

...

\subsection{HOL: Function definitions}

Non-recursive definitions and let expressions are treated similarly as

in the translation to HOLCF. Recursive defitions is the topic that

really sets HOL and HOLCF apart. In HOL a distinction has to be drawn

between primitive recursive functions and generic recursive ones. In

the former, termination is guaranteed by the fact that recursive

definitions are strictly associated with the datatype structure of a

parameter. In the latter, termination needs to be proved. This must be

done, in a \emph{recdef} definition, by providing a measure for the

function parameter that can be proved to be strictly decreasing for

each occurrence of a recursive call in the definition. This requires a

degree of ingenuity that cannot be generally associated with an

automated translation.

For this reason, the translation of recursive functions to HOL is

restricted to primitive recursive ones. Mutually recursive functions

are allowed under additional restrictions. These are: all the

functions should be recursive in the first argument; this should be of

the same type for each of them; the constructors should be listed in

the same order in each of the case expressions; the variable names in

the case patterns are expected to be maintained.

The translation of mutually recursive functions $a \rightarrow b, \ldots a

\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$

defined, for each case pattern, as the product of the values

correspondingly taken by the original functions.

...

\subsection{Pattern matching}

Support of pattern-matching in Isabelle is more restricted than in

Haskell. Nested patterns are disallowed; case expressions are

sensitive to the order of the constructors, which should be the same

as in the datatype declaration. In particular, the case variable si

required to be a variable. Translation of pattern-matching is

potentially laborious. For this reason guarded expressions, list

comprehension and nested pattern-matching have been left out; they

should be replaced by the programmer, using conditional expressions

and map functions.

Function definition by top level pattern matching is not allowed in

Isabelle with ordinary definitions, but it is with those that are

explicitly declared to be recursive ones. However, particularly in HOL

primitive recursive definitions patterns are allowed in one parameter

only. In order to translate function definitions with patterns in more

than one parameter, without resorting to using tuples and more complex

definitions (\emph{recdef} instead of \emph{primrec}), our

translations turn a multiple definition by top level pattern matching

into a definition by case construct.

...

\subsection{Classes}

Haskell classes and instances are translated to Isabelle,

respectively, as classes with empty axiomatisation and as instances

with trivial instantiation proof. The translation supports only

single-parameter classes --- in principle, more than one parameter

could be handled using tuples.

Built-in classes --- Eq and Ord in particular --- are translated to

newly defined classes in Isabelle; the corresponding axiomatisation

however here is not provided !!!

...

Functions declarations associated to classes are translated to

Isabelle as independent function declarations with appropriate class

annotation. Function definitions associated to instances are

translated as overloaded function definitions, relying on class

annotation of typed variables.

...

\section*{Haskell2Isabelle}

The tool is designed to support the translation of simple but

realistic Haskell programs to HOLCF and, with some restriction, to

HOL. Not all the syntactical features of Haskell are covered yet,

although most of those used in the Prelude are. The most noticeable

limitations are related to built-in types, pattern-matching and local

definitions. There are additional and more substantial restrictions

in the case of HOL, related to termination and to recursion.

The application can be installed as part of Hets. It requires Haskell

GHC and Programatica. It is run by the command \emph{hets -t ...

[h|hc] file.hs} where the options stand for HOL and HOLCF,

respectively.

For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the

module that contains the main translation function, carried out as

composition of a signature morphism and a theory morphism.

\emph{IsaSign.hs} contains the Hets representation of the Isabelle

base logic and extensions.

The general design of the translation functions, and particularly the

two-layered recursion adopted for them, is similar to that used for

the translation Haskell to Agda in Programatica.

\subsection{Monads}

Isabelle does not allow for classes of type constructors, hence a

problem in representing monads. We can deal with this problem,

however, relying on an axiomatisation of monads that allows for the

presentation of monadic types as an axiomatic class, as provided in

\cite{}. Therefore, monadic types can be translated to newly defined

types that are constrained to satisfy the monadic axioms. This

constraining, carried out as an instantiation of type variables in the

theory of monads, takes the form of a theory morphism, and can be

carried out automatically by AWE, an implementation of parametrisation

and theory morphism on top of Isabelle basic logic, that may also be

used to extend HOL and HOLCF. The do notation can then be translated

by unpacking it into monadic operators. Attempting to translate

monadic notation without support AWE support will result in an error

message.

\section*{Conclusion}

The following is a list of constructs that are covered by all the

translations.

\begin{itemize}

\item predefined types: boolean, integer.

\item predifed type constructors: funtion, cartesian product, list.

\item declaration of recursive datatype, including mutually recursive ones.

\item predefined functions: equality, booelan constructors,

connectives, list constructors, head and tail list functions,

arithmetic operations.

\item non-recursive functions, including conditional,

let and case expressions.

\item use of incomplete patterns (HOLCF) and of wildcards in case

expressions.

\item total primitive recursive functions (HOL)

and partial recursive ones (HOLCF), including mutual ones (with

restrictions in the HOL case).

\item class and instance declarations.

\item monad declarations and do notation.

\end{itemize}

The shallow embedding approach used by our translations should allow

to take as much advantage as possible of the automation currently

available on Isabelle, particularly in HOL.

Further work should include extending the translation to cover the

whole of the Haskell Prelude. We hope that this will make it possible

to support the verification of functional robotics programs.

A further extension, in line with the work on Programtica, would be

the translation of P-logic. This translation, due to the character of

the P-logic typing system, could be more easily carried out relying on

some form of universal quantification on type variables, or else

further relying on parametrisation.

\bibliographystyle{alpha}

\bibliography{case}

\end{document}

\subsection{}

The translation of types is

Our general strategy for translating signatures is to map Haskell

types to Isabelle defined types.

the fact that Haskell expressions are

evaluated lazily, however it does not preserve The translation to HOL

does not, and moreover requires that all the functions defined in the

Haskell program are total ones...

All types have a sort in Isabelle, defined by the set of the classes

of which it is a member. In HOL, all types belong to the class type;

in HOLCF, they belong to class pcpo (pointed complete poset).

All Haskell function declarations are translated to Isabelle ones.

Type variables are assigned default sort type in HOL and pcpo in

HOLCF. Names get translated by a function that preserves them, up to

avoidance of clashes with Isabelle keywords.

The only built-in types that are properly covered are booleans,

unbounded integers and rationals. These get translated, in the case of

HOL, to Isabelle booleans, integers and rationals, respectively. Bound

integers and floating point numbers would require low-level modelling,

and have not been dealt with; anyway, bounded integers are accepted

and simply treated as unbounded by the application.

In the HOLCF translation, all built-in types get lifted to the

corresponding domains (pcpos), which by definion include the undefined

value, by using the lift HOLCF type constructor. In particular, type

boolean get translated to type tr (short for bool lift), and similarly

for types integer and rational.

Recursive data-types declarations can be translated to datatype

declarations in HOL. In HOLCF they can be translated to domain

declarations. The two structure are quite similar, except that in

domains, which are pcpo, all the parameters are required to be pcpos

as well. Morevover, Isabelle domain declarations require to introduce

names for destructors. Mutually recursive Haskell datatypes can be

translated to both logics, relying on the specific Isabelle syntax for

them.

A type class in Isabelle is conceptually quite different from one in

Haskell. The former is associated to a set of axioms, whereas the

latter is associated to a set of function declarations. Isabelle

classes may have at most a type parameter. Moreover, Isabelle does

not allow for type constructor classes. The last limitation is the

most serious of the three, since it makes quite hard to cope with

monads. We can get around this obstacle relying on a method for the

axiomatic encoding of monads in HOL that uses parametrisation.

Parametrisation based on theory morphism has been implemented, as a

conservative extension of various Isabelle logics, in AWE, a tool

designed to support proof reuse \cite{AWE}.

...

The \emph{lift} type constructor, in particular, lifts each HOL type

to a flat domain, by adding a bottom element to them. We are going to

use it to lift the basic types. For the product we are going to use

non-strict product.

...

Its

formalisation on Isabele relies on axiomatic type classes \cite{},

with \emph{pcpo} (pointed complete partial order) as the default

class, in which the type of continuous functions can be represented as

function spaces, allowing for an elegant interpretation of recursion

by fixpoint operator. HOL types may be lifted to \emph{pcpo} by simply

adding a bottom element to them. This is what the type constructor

\emph{lift} does, thus providing also a way of handling partiality ---

undefined cases can be mapped to the bottom element. HOLCF has also a

type constructor \emph{u} that allows to deal with laziness, by

guaranteeing $\bot \neq \smath{up} \$ (\bot)$.

\subsection{}

In the case of HOLCF, the logic provides a computational

interpretation of function types as domains. In HOL there is no such

facility, therefore either appropriate types for the translation are

introduced --- as in \cite{}, or considerable semantical restrictions

must be accepted --- this is also the case for one of the translation

to FOL proposed in \cite{}.

Depending on the expressiveness of the logic, the translation of the

programming language may be carried out at different levels of depth.

In general, the deeper is the embedding, the less it relies on

meta-level features of the target language. This may be a plus, either

from the point of view of semantic clarity, or from that of

expressiveness. Taking advantage of meta-level feaures, on the other

hand, may be useful in order to make the theorem proving less tedious,

by allowing more constant use of generic proof methods. It may also

ultimately affect positively the theorem prover economy, by

reinforcing the bias toward the development of proof methods that,

however specific, can be more easily integrated with generic ones.

% a point made in \cite{}. for example by allowing a straightforward

% operational interpretation ---

The translations of Haskell to HOLCF and HOL that we are presenting in

the following justify themselves in terms of denotational semantics.

The translation to HOLCF differs from that proposed in \cite{} in the

treatment of types. We translate Haskell types directly into HOLCF

ones, whereas they use HOLCF terms to embed Haskell types. We assume

that the HOLCF types are similar enough to the those of Haskell, in

order to guarantee the semantical correctness of our translations.

Moreover, we rely on axiomatic classes to translate Haskell types

classes.

Our approach has the advantage of giving a shallower embedding,

however it has the drawback of not bein complete --- notably, type

constructor classes are missing. We plan to handle in future this

problem (see section~\ref{sec:Monads}) by relying on an extension of

Isabelle based on morphism between theories. The translation into HOL

is essentialy only a first experiment, it handles types very

simplistically, relying on drastic semantical restrictions for

correcteness. Under those restrictions, however, it gives expressions

that are comparatively quite simple to work with.

A type class in Isabelle is conceptually quite different from one in

Haskell. The former is associated to a set of axioms, whereas the

latter is associated to a set of function declarations. Isabelle

classes may have at most a type parameter. Moreover, Isabelle does

not allow for type constructor classes. The last limitation is the

most serious of the three, since it makes quite hard to cope with

monads. We can get around this obstacle relying on a method for the

axiomatic encoding of monads in HOL that uses parametrisation.

Parametrisation based on theory morphism has been implemented, as a

conservative extension of various Isabelle logics, in AWE, a tool

designed to support proof reuse \cite{AWE}.

\subsection{Types}

HOLCF allows has types for computable functions --- defined as sets of

continuous functions of a type (!! fixpoints!!). It has a type

constructor \emph{lift} that lifts HOL types to \emph{pcpo}s, thus

providing a way of handling partiality --- undefined cases can be

mapped to the bottom element. It has also a type constructor \emph{u}

that allows to deal with laziness, by guaranteeing $\bot \neq

\smath{u}(\bot)$.

that can be used to embed Haskell function types.

The translation to HOLCF differs from that to HOL insofar as only the

first one relies on a denotational semantics for the full language,

keeping into account partiality and lazy evaluation, and associating

recursive functions to corresponding fixed points, using on the Fixrec

extension of HOLCF. The translation to HOL is more restrictive; it

does not keep into account any form of partiality, and it restricts

translation of recursive functions to the primitive recursive ones.

It would have been possible to give an account of partiality in HOL by

using option types. However, we chose to keep the HOL translation as

simple as possible for didactic purpose.

\subsection{maybe}

The translations of Haskell that we are presenting in the following,

we present translations of Haskell into some of the Isabelle logics.

These translations are implemented as part of Hets, and are based on a

shallow embedding approach quite different from that used in

Programatica. In our translations Haskell types are mapped to Isabelle

types. We are assuming that the type systems of HOL and HOLCF are

similar enough to the type system of Haskell, in order to guarantee

the semantical correctness of our translations. Moreover, we rely on

axiomatic classes to translate Haskell types classes.

A type class in Isabelle is conceptually quite different from one in

Haskell. The former is associated to a set of axioms, whereas the

latter is associated to a set of function declarations. Isabelle

classes may have at most a type parameter. Moreover, Isabelle does

not allow for type constructor classes. The last limitation is the

most serious of the three, since it makes quite hard to cope with

monads. We can get around this obstacle relying on a method for the

axiomatic encoding of monads in HOL that uses parametrisation.

Parametrisation based on theory morphism has been implemented, as a

conservative extension of various Isabelle logics, in AWE, a tool

designed to support proof reuse \cite{AWE}.

The translation to HOLCF differs from that to HOL insofar as only the

first one relies on a denotational semantics for the full language,

keeping into account partiality and lazy evaluation, and associating

recursive functions to corresponding fixed points, using on the Fixrec

extension of HOLCF. The translation to HOL is more restrictive; it

does not keep into account any form of partiality, and it restricts

translation of recursive functions to the primitive recursive ones.

It would have been possible to give an account of partiality in HOL by

using option types. However, we chose to keep the HOL translation as

simple as possible for didactic purpose.

\subsection{Type signature}

Our general strategy for translating signatures is to map Haskell

types to Isabelle defined types. The translation to HOLCF keeps into

account the fact that Haskell expressions are evaluated lazily. The

translation to HOL does not, and moreover requires that all the

functions defined in the Haskell program are total ones...

All types have a sort in Isabelle, defined by the set of the classes

of which it is a member. In HOL, all types belong to the class type;

in HOLCF, they belong to class pcpo (pointed complete poset).

All Haskell function declarations are translated to Isabelle ones.

Type variables are assigned default sort type in HOL and pcpo in

HOLCF. Names get translated by a function that preserves them, up to

avoidance of clashes with Isabelle keywords.

The only built-in types that are properly covered are booleans,

unbounded integers and rationals. These get translated, in the case of

HOL, to Isabelle booleans, integers and rationals, respectively. Bound

integers and floating point numbers would require low-level modelling,

and have not been dealt with; anyway, bounded integers are accepted

and simply treated as unbounded by the application.

In the HOLCF translation, all built-in types get lifted to the

corresponding domains (pcpos), which by definion include the undefined

value, by using the lift HOLCF type constructor. In particular, type

boolean get translated to type tr (short for bool lift), and similarly

for types integer and rational.

Recursive data-types declarations can be translated to datatype

declarations in HOL. In HOLCF they can be translated to domain

declarations. The two structure are quite similar, except that in

domains, which are pcpo, all the parameters are required to be pcpos

as well. Morevover, Isabelle domain declarations require to introduce

names for destructors. Mutually recursive Haskell datatypes can be

translated to both logics, relying on the specific Isabelle syntax for

them.

we present translations of Haskell into some of the Isabelle logics.

These translations are implemented as part of Hets, and are based on a

shallow embedding approach quite different from that used in

Programatica. In our translations Haskell types are mapped to Isabelle

types. We are assuming that the type systems of HOL and HOLCF are

similar enough to the type system of Haskell, in order to guarantee

the semantical correctness of our translations. Moreover, we rely on

axiomatic classes to translate Haskell types classes.

In the following, we present translations of Haskell into some of the

Isabelle logics. These translations are implemented as part of Hets,

and are based on a shallow embedding approach quite different from

that used in Programatica. In our translations Haskell types are

mapped to Isabelle types. We are assuming that the type systems of HOL

and HOLCF are similar enough to the type system of Haskell, in order

to guarantee the semantical correctness of our translations. Moreover,

we rely on axiomatic classes to translate Haskell types classes.

are those presented in \cite{}.

as well as in \cite{}

translation of Haskell

into FOL \cite{} and that into

In \cite{} Haskell is embedded in Martin-Loef

type theory, implemented on Agda.

is indeed a general difference between a lower level

approach based on operational semantics, followed in \cite{agda} and

\cite{miranda}, and a higher-level one, based essentially on

denotational semantics, followed in \cite{}

The correctness of such embeddings

always rests, ultimately, on the denotational semantics of Haskell,

and on the possibility to encode it in a logic under consideration.

\cite{Thompson95}. Indeed, Haskell --- a strongly typed, purely

functional language with lazy evaluation, based on a system of

polymorphic types extended with type constructor classes, where monads

allow for side effects and pseudo-imperative code \cite{Hudak} --- has

already been considered several times as a target for verification

\cite{...}.

All the above-mentioned works provide embeddings of Haskell, either

partial or total, into programming logic implemented on theorem

provers. The correctness of such embeddings always rests, ultimately,

on the denotational semantics of Haskell, and on the possibility to

encode it in a logic under consideration.

The tools, the logic and the ways in which the encoding can be done

may differ quite deeply. In \cite{} Haskell is embedded in Martin-Loef

type theory, implemented on Agda. All the other examples rely on

Isabelle, a generic theorem-prover written in SML that allows for the

formalisation of a variety of logics, including FOL, HOL and HOLCF

\cite{Paulson94isa}. The embedding in \cite{} rely on FOL, the

Isabelle implementation of classical first-order logic.

All the other examples \cite{...} rely on higher-order logic. HOL is

the implementation of classical higher-order logic based on simply

typed lambda calculus, extended with axiomatic type classes. HOLCF

\cite{holcf} is the extension of HOL with a formalisation of the

theory of computable functions (LCF) based on axiomatic type classes.

% In

% other words, we need to represent the program in a mechanised logic in

% which the requirements can be expressed, as well.

% The representation can take different forms. It is possible to

% associate the state-machine behavioural description to models in a

% logic. Another possibility is to represent the program in terms of a

% computational logic based on the operational semantics of the

% language.

% In both cases however, a significant part of the work has to

% be carried out before the actual verification may take place.

In order to verify a program, we need to associate its code to a

logical representation that allows for requirements to be expressed

and for proofs to be carried out. There are different ways to do this.

The way we carry this out here is to embed Haskell into an expressive

higher-order logic, together with providing an implementation of the

embedding that allows for an automated translation of Haskell. From

the theoretical point of view, the correctness of the embdedding

depends on the denotational semantics of the language. From the

practical point of view, once the program code can be translated

automatically to the logic, all the burden of the verification can

rest on the theorem proving.

Depending on the expressiveness of the logic, the translation of the

progrmaming language may be carried out at different levels of depth.

In general, the deeper is the embedding, the less it relies on

meta-level features of the target language. This may be a plus from

the point of view of semantic clarity. Taking advantage of meta-level

feaures, on the other hand, may be useful in order to make the theorem

proving less tedious.

Isabelle is a generic theorem-prover written in SML that allows for

the formalisation of a variety of logics \cite{Paulson94isa}.

Isabelle-HOL is the implementation of classical higher-order logic

based on simply typed lambda calculus, extended with axiomatic type

classes. Isabelle-HOLCF \cite{holcf} is the extension of HOL with a

formalisation of the theory of computable functions (LCF) based on

axiomatic type classes.

Hets \cite{Hets} is a parsing, static analysis and proof management

tool designed to interface with various language specific tools, in

order to support heterogeneous specification. In particular, for the

parsing and static analysis of Haskell programs Hets relies on

Programatica \cite{PTeam}, a tool that has its own proof management,

including a translation of Haskell to Isabelle-HOLCF.

The translations of Haskell that we are presenting in the following,

we present translations of Haskell into some of the Isabelle logics.

These translations are implemented as part of Hets, and are based on a

shallow embedding approach quite different from that used in

Programatica. In our translations Haskell types are mapped to Isabelle

types. We are assuming that the type systems of HOL and HOLCF are

similar enough to the type system of Haskell, in order to guarantee

the semantical correctness of our translations. Moreover, we rely on

axiomatic classes to translate Haskell types classes.

A type class in Isabelle is conceptually quite different from one in

Haskell. The former is associated to a set of axioms, whereas the

latter is associated to a set of function declarations. Isabelle

classes may have at most a type parameter. Moreover, Isabelle does

not allow for type constructor classes. The last limitation is the

most serious of the three, since it makes quite hard to cope with

monads. We can get around this obstacle relying on a method for the

axiomatic encoding of monads in HOL that uses parametrisation.

Parametrisation based on theory morphism has been implemented, as a

conservative extension of various Isabelle logics, in AWE, a tool

designed to support proof reuse \cite{AWE}.

The translation to HOLCF differs from that to HOL insofar as only the

first one relies on a denotational semantics for the full language,

keeping into account partiality and lazy evaluation, and associating

recursive functions to corresponding fixed points, using on the Fixrec

extension of HOLCF. The translation to HOL is more restrictive; it

does not keep into account any form of partiality, and it restricts

translation of recursive functions to the primitive recursive ones.

It would have been possible to give an account of partiality in HOL by

using option types. However, we chose to keep the HOL translation as

simple as possible for didactic purpose.

These translations are on the overall quite different from other ones

based on deep embeddings, particularly from the Programatica

translation of Haskell into HOLCF \cite{Huff}, where the type system

is modelled at the logical level, as well as from translations of

Miranda and Haskell into FOL (Isabelle classical first-order logic)

where higher-order features have to be dealt with less directly

\cite{Thompson95,Thompson92}.

\section*{The hs2thy tool}

(suggested change: from h2hf to hs2thy)

The tool is designed to support the translation of simple but

realistic Haskell programs to HOLCF and, with some restriction, to

HOL. Not all the syntactical features of Haskell are covered yet,

although most of those used in the Prelude are. The most noticeable

limitations are related to built-in types, pattern-matching and local

definitions. There are additional and more substantial restrictions

in the case of HOL, related to termination and to recursion.

The application can be installed as part of Hets. It requires Haskell

GHC and Programatica. It is run by the command \emph{h2hf

[h|hc|mh|mhc] file.hs} where the options stand, respectively, for

HOL, HOLCF, HOL extended with AWE and HOLCF extended with AWE.

For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the

module that contains the main translation function, carried out as

theory translation after a preliminary step of signature translation,

and \emph{IsaSign.hs} contains the internal representation of Isabelle

logics.

\subsection{Type signature}

Our general strategy for translating signatures is to map Haskell

types to Isabelle defined types. The translation to HOLCF keeps into

account the fact that Haskell expressions are evaluated lazily. The

translation to HOL does not, and moreover requires that all the

functions defined in the Haskell program are total ones...

All types have a sort in Isabelle, defined by the set of the classes

of which it is a member. In HOL, all types belong to the class type;

in HOLCF, they belong to class pcpo (pointed complete poset).

All Haskell function declarations are translated to Isabelle ones.

Type variables are assigned default sort type in HOL and pcpo in

HOLCF. Names get translated by a function that preserves them, up to

avoidance of clashes with Isabelle keywords.

The only built-in types that are properly covered are booleans,

unbounded integers and rationals. These get translated, in the case of

HOL, to Isabelle booleans, integers and rationals, respectively. Bound

integers and floating point numbers would require low-level modelling,

and have not been dealt with; anyway, bounded integers are accepted

and simply treated as unbounded by the application.

In the HOLCF translation, all built-in types get lifted to the

corresponding domains (pcpos), which by definion include the undefined

value, by using the lift HOLCF type constructor. In particular, type

boolean get translated to type tr (short for bool lift), and similarly

for types integer and rational.

Recursive data-types declarations can be translated to datatype

declarations in HOL. In HOLCF they can be translated to domain

declarations. The two structure are quite similar, except that in

domains, which are pcpo, all the parameters are required to be pcpos

as well. Morevover, Isabelle domain declarations require to introduce

names for destructors. Mutually recursive Haskell datatypes can be

translated to both logics, relying on the specific Isabelle syntax for

them.

\subsection{Function definitions}

Haskell function definitions are translated to corresponding Isabelle

ones. Non-recursive definitions are translated to ordinary definitions

(keyword \emph{defs}), whereas recursive ones require specific

keywords. The type of the function, inclusive of class annotation, is

included in each of its definitions in order to allow for overloading.

In the translation to HOLCF, when the Haskell value is of built-in

type, the translated value has the lifted corresponding type --- this

is either the case of a lifted value (where \emph{Def} is the lifting

function) or the case of the undefined value (\emph{UU}).

As to local definitions, they can be introduced in Haskell by let and

where expressions. Let expressions are translated to Isabelle let

expressions, whereas where expressions are not covered.

\subsection{Recursive definitions}

Recursive defitions is the topic that really sets HOL and HOLCF apart.

In HOLCF, where every type is a domain and every function is

continuous, all recursive functions can be defined by fixpoint

operator. This is essentially a function that, given as argument the

function definition body abstracted of the recursive call name,

returns the corresponding recursive function. Coding this directly

would be rather cumbersome, particularly in the case of mutually

recursive functions, where tuples of definition bodies and tupled

abstraction are needed. We can instead rely on the \emph{recdef}

package, which allows to handle fixpoint definitions like ordinary

recursive ones, offering nice syntax to deal with mutual recursion as

well.

The case of HOL is more compplex. There a distinction must be drawn

between primitive recursive functions and generic recursive ones. In

the formers, termination is guaranteed by the fact that recursive

definitions are strictly associated with the datatype structure of a

parameter. In the latters, termination needs to be proved. This can be

done, in a \emph{recdef} definition, by providing a measure for the

function parameter that can be proved to be strictly decreasing for

each occurrence of a recursive call in the definition. This requires a

generally unbounded amount of ingenuity and cannot be carried out by a

simple translation.

For this reason, the translation of recursive functions to HOL is

restricted to primitive recursive ones. Mutually recursive functions

are allowed under additional restrictions. These are: all the

functions should be recursive in the first argument, this should be of

the same type for each of them, the constructors should be listed in

the same order in each of the case expressions, and also the variable

names in the case patterns are expected to be maintained.

The translation of mutually recursive functions $a \rightarrow b, \ldots a

\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$

defined, for each case pattern, as the product of the values

correspondingly taken by the original functions.

\subsection{Pattern matching}

Support of pattern-matching in Isabelle is more restricted than in

Haskell. Nested patterns are disallowed; case expressions are

sensitive to the order of the constructors, which should be the same

as in the datatype declaration. In particular, the case variable si

required to be a variable. Translation of pattern-matching is

potentially laborious. For this reason guarded expressions, list

comprehension and nested pattern-matching have been left out; they can

be replaced without loss, anyway, using conditional expressions and

map functions.

Function definition by top level pattern matching is not allowed in

Isabelle with ordinary definitions, but it is with those that are

explicitly declared to be recursive ones. However, particularly in HOL

primitive recursive definitions patterns are allowed in one parameter

only. In order to translate function definitions with patterns in more

than one parameter, without resorting to using tuples and more complex

definitions (\emph{recdef} instead of \emph{primrec}), our

translations turn a multiple definition by top level pattern matching

into a definition by case construct.

\subsection{Classes}

Haskell classes and instances are translated to Isabelle,

respectively, as classes with empty axiomatisation and as instances

with trivial instantiation proof. The translation supports only

single-parameter classes --- in principle, more than one parameter

could be handled using tuples.

Built-in classes --- Eq and Ord in particular --- are translated to

newly defined classes in Isabelle; the corresponding axiomatisation

however here is not provided.

Functions declarations associated to classes are translated to

Isabelle as independent function declarations with appropriate class

annotation. Function definitions associated to instances are

translated as overloaded function definitions, relying on class

annotation of typed variables.

\subsection{Monads}

\label{sec:Monads}

Isabelle does not allow for classes of type constructors, hence a

problem in representing monads. We can deal with this problem,

however, relying on an axiomatisation of monads that allows for the

presentation of monadic types as an axiomatic class, as provided in

\cite{}. Therefore, monadic types can be translated to newly defined

types that are constrained to satisfy the monadic axioms. This

constraining, carried out as an instantiation of type variables in the

theory of monads, takes the form of a theory morphism, and can be

carried out automatically by AWE, an implementation of parametrisation

and theory morphism on top of Isabelle basic logic, that may also be

used to extend HOL and HOLCF. The do notation can then be translated

by unpacking it into monadic operators. Attempting to translate

monadic notation without support AWE support will result in an error

message.

\section*{Conclusion}

The following is a list of constructs that are covered by all the

translations.

\begin{itemize}

\item predefined types: boolean, integer.

\item predifed type constructors: funtion, cartesian product, list.

\item declaration of recursive datatype, including mutually recursive ones.

\item predefined functions: equality, booelan constructors,

connectives, list constructors, head and tail list functions,

arithmetic operations.

\item non-recursive functions, including conditional,

let and case expressions.

\item use of incomplete patterns (HOLCF) and of wildcards in case

expressions.

\item total primitive recursive functions (HOL)

and partial recursive ones (HOLCF), including mutual ones (with

restrictions in the HOL case).

\item class and instance declarations.

\item monad declarations and do notation.

\end{itemize}

The shallow embedding approach used by our translations should allow

to take as much advantage as possible of the automation currently

available on Isabelle, particularly in HOL.

Further work should include extending the translation to cover the

whole of the Haskell Prelude. We hope that this will make it possible

to support the verification of functional robotics programs.

A further extension, in line with the work on Programtica, would be

the translation of P-logic. This translation, due to the character of

the P-logic typing system, could be more easily carried out relying on

some form of universal quantification on type variables, or else

further relying on parametrisation.

\bibliographystyle{alpha}

\bibliography{case}

\end{document}

%Moreover, being such languages

%as Haskell, ML and Miranda closely modelled on typed lambda-calculus,

%their translations to specification formalisms, particularly to

%higher-order logics, turn out to be comparatively straighforward to be

%defined in the main lines --- although not so to be carried out in

%detail.

%, due to the richness in syntax, the specific way evaluation is

%implemented, as well as to issues associated with classes (Haskell),

%overloading and side effects.

%All functions are total in HOL. Partiality may be dealt with by

%lifting types through the \emph{option} type constructor. HOL has an

%implementation of recursive functions based on Tarski fixed-point

%theorem. Defining a recursive function requires giving a specific

%measure and proving monotonicity about it.

% HOL has an implementation of recursive functions, based on Tarski

% fixed-point theorem. Their definition in general requires specific

% measure to be given each time, for monotonicity to be proved.

% Moreover, partial functions are needed to programs that might not

% terminate, but in HOL all functions are total. Partiality may be

% dealt with by lifting types through \emph{option}, a type

% constructor in HOL. This inevitably complicates case expressions.

%There are different general approaches depending on the style of the

%semantics. The expressiveness of the logical language may also make a

%big difference.

The Haskell classes Eq and Ord are translated to corresponding classes

declared, respectively, in HsHOL.thy and HsHOLCF.thy. These classes

for the moment are taken to be absolutely generic ones (with empty

axiomatisation).

\subsection{Isabelle-HOL}

Isabelle-HOL as an implementation of classical higher-order logic

supports the definition of datatypes and recursive functions.

However, it distinguishes between primitive recursion (keyword

emph{primrec}), in which termination is trivially guaranteed by

decrease in the complexity of a parameter, and recursion (keyword

emph{recdef}) for which an appropriate specific measure must be

provided in order to get the termination proof to go through.

Moreover, HOL does not have a notion of undefined suitable for

computations --- therefore all functions have to be total.

This translation of recursive functions is restricted to total

primitive recursive functions that are recursive in their first

datatype argument. The Haskell definition should be a case expression

in which all the constructors are considered in their datatype

declaration order, save for the use of a wildcard.

%Wildcards cannot be used for constructor arguments.

%Moreover, the

%case variable should not be used in the specific case expression (just

%replace it with the specific case pattern).

Mutually recursive functions are allowed under additional

restrictions. All the functions should be recursive in the same type,

the constructors should be listed in the same order in each of the

case expressions, and also the variable names in the case patterns are

expected to be maintained.

The translation of mutually recursive functions $a \rightarrow b, \ldots a

\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$

defined, for each case pattern, as the product of the values

correspondingly taken by the original functions.

\subsection{Isabelle-HOLCF}

Isabelle-HOLCF is the implementation of the theory of computable

functions on top of higher-order logic, relying on axiomatic classes.

In comparison with HOL, the handling of partial functions is more

natural, and the presence of the fixpoint operator allows for a

general treatment of recursive functions. However, types in HOLCF can

be interpreted as pointed complete partial orders (pcpo), and this

requires all standard types to be lifted.

In the present translation, the type constructor \emph{lift} is used

to lift types, in association with the corresponding lifting function

\emph{Def} and with the undefined value \emph{UU}. Datatypes are

translated to domains --- complete with destructors from declaration.

The class \emph{pcpo} is added to the sort of each type variable.

Partial recursive functions (defined by case expressions), including

mutually recursive ones, are covered without any essential

restrictions, relying on the recdef package.

\end{document}

as well as an

operational, but is quite deep.

, insofar as

it builds into HOL a specific domain class for the interpretation of

Higher-level approaches relying on denotational

semantics

propose level

approaches based on large-step operational semantics, even if with

some complication when dealing with higher-order programming languages

such as those presented in \cite{} --- Miranda in FOL; \cite{} ---

Haskell in FOL; \cite{} --- Haskell in the Agda implementation of

Martin-Loef type theory. More expressiveness is usually required by

high-level approaches based on denotational semantics, such as those

presented in \cite{} --- Haskell in HOLCF and HOL; \cite{} --- ML in

HOL.

The main one, is which Depending on the

expressiveness of the logic, the translation of the programming

language may be carried out at different levels of depth. In general,

the deeper is the embedding, the less it relies on meta-level features

of the target language. This may be a plus, either from the point of

view of semantic clarity, or from that of expressiveness. Taking

advantage of meta-level feaures, on the other hand, may be useful in

order to make the theorem proving less tedious, by allowing more

constant use of generic proof methods. It may also ultimately affect

positively the theorem prover economy, by reinforcing the bias toward

the development of proof methods that, however specific, can be more

easily integrated with generic ones.

Some significantly different examples of functional programming

languages embedded into the logic of a theorem prover can be found in

\cite{} (Miranda on Isabelle), \cite{} (ML on Isabelle), \cite{}

(Haskell on Isabelle), \cite{} (Haskell on Agda). Example of lower

level approaches are given in \cite{}, where Haskell is translated

into the Agda implementation of Martin-Loef theory based on

operational rules and relies on operational semantics for correctness,

is followed in \cite{}, where Haskell is embedded into the Agda

implementation of Martin-Loef theory, as well as in the embeddings of

Miranda \cite{} and Haskell \cite{} into FOL (classical first-order

logic, until the middle of the nineties still probably the best

supported logic on Isabelle). Higher-level approaches, such as

presented in \cite{} (embedding ML into HOL), and in \cite{}

(embedding Haskell into HOLCF and into HOL), rely ultimately on

denotational semantics for correctenss. This, together with the

expressiveness allowed by higher-order logic for the formulation of

requirements, gives the considerable advantage of enabling proofs that

are more abstract and closer to mathematical intuition.

\subsection{}

method for the

axiomatic encoding of monads in HOL that uses parametrisation.

Parametrisation based on theory morphism has been implemented, as a

conservative extension of various Isabelle logics, in AWE, a tool

designed to support proof reuse \cite{AWE}.

it is not complete, and cannot be trivially completed ---

notably, type constructor classes have not been considered, since

Isabelle does not have them. However, we are expecting to deal with

this problem by relying on an extension of Isabelle based on theory

morphism (see section \ref{}) .