\documentclass{llncs}

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

\textwidth 15.93cm

\textheight 24cm

\oddsidemargin 0.0cm

\evensidemargin 0.0cm

\topmargin 0.0cm

\begin{document}

\title{Translating Haskell to Isabelle}

\author{ Paolo Torrini, Verimag \\

{\tt Paolo.Torrini@imag.fr} \\

Christoph Lueth, DFKI Lab Bremen \\

{\tt Christoph.Lueth@dfki.de} \\

Christian Maeder, DFKI Lab Bremen \\

{\tt Christian.Maeder@dfki.de} \\

Till Mossakowski, DFKI Lab Bremen \\

{\tt Till.Mossakowski@dfki.de} \\

} \date{\today}

\maketitle

\begin{abstract}

We present partial translations of Haskell programs to Isabelle that have

been implemented as part of the Hets-Programatica system. The logics HOLCF

and Isabelle-HOL are targets --- under stronger restrictions in the latter

case --- to translations that are essentially based on a shallow embedding

approach. The AWE package has been used to support a translation of monadic

operators based on theory morphisms.

\end{abstract}

\sloppy

\section{Introduction}

\label{intro}

Automating the translation from programming languages to the languagee of a

generic prover may provide useful support for the formal development and the

verification of programs. It has been argued that functional languages can

make the task of proving assertions about programs written in them easier,

owing to the relative simplicity of their semantics

\cite{Thompson92,Thompson95}. The idea of translating Haskell programs, came

to us, more specifically, from an interest in the use of functional languages

for the specification of reactive systems. 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}. Several languages based on

Haskell have been proposed for application to robotics \cite{phh99,Hudak2003}.

In such languages, monadic constructors are extensively used to deal with

side-effects. Isabelle is a generic theorem-prover implemented in SML

supporting several logics --- in particular, Isabelle-HOL and its extension to

a theory of computable functions (HOLCF) \cite{Paulson94isa,holcf}.

We have implemented as functions of Hets translations of Haskell to

Isabelle-HOL and HOLCF following an approach based on shallow embedding,

mapping Haskell types to Isabelle ones, therefore taking full advantage of

Isabelle built-in type-checking. Hets \cite{TillHet,HetsUG,Hets} is an

Haskell-based application designed to support heterogeneous specification and

the formal development of programs. It has an interface with Isabelle, and

relies on Programatica \cite{Prog04} for parsing and static analysis of

Haskell programs. Programatica already includes a translation to HOLCF which,

in contrast to ours, is based on an object-level modelling of the type system

\cite{Huff}.

Our translation to HOLCF covers at present Booleans, integers, basic

constructors (function, product, list, \emph{maybe}), equality,

single-parameter type classes (with some limitations), \emph{case} and

\emph{if} expressions, \emph{let} expressions without patterns, mutually

recursive data-types and functions. It relies on existing formalisations of

lazy lists and \emph{maybe}. It keeps into account partiality and laziness by

following, for the main lines, the denotational semantics of lazy evaluation

given in \cite{winskel}. There are several limitations: \emph{Predulde} syntax

is covered only partially; list comprension, \emph{where} expressions and

\emph{let} with patterns are not covered; further built-in types and type

classes are not covered; imports are not allowed; constructor type classes are

not covered at all --- and so for monadic types beyond list and \emph{maybe}.

Of all these limitations, the only logically deep ones are those related to

classes --- all the other ones are just a matter of implementation.

The base translation to Isabelle-HOL is more limited, insofar as it covers

only total primitive recursive functions. A better semantics with respect to

partiality could be obtained by lifting the type of function values with

\emph{option}, but this has not been pursued here. Still, \emph{option} has

been used to translate \emph{maybe}. On the other hand, laziness appears very

hard to be captured with Isabelle-HOL. It also seems hard to overcome the

limitation to primitive recursion. Other limitations are similar to those

mentioned for the translation to HOLCF --- with the notable exception of

monads.

Isabelle does not allow for type constructor classes, therefore there is

hardly a way shallow embedding of Haskell types may extend to cover them.

This limitation is particularly acute with respect to monads and \emph{do}

notation. The problem is brilliantly avoided in \cite{Huff} by resorting to a

deeper modelling of types. On the other hand, the main novelty in our work is

to rely on theory morphisms and on their implementation for Isabelle in the

package AWE \cite{AWE}, in order to deal with special cases of monadic

operator. This solution gives in general less expressiveness than the deeper

approach --- however, when we can get it to deal with cases of interest, it

might make proofs easier. Currently Hets provides with an extension of the

base translation to Isabelle-HOL which uses AWE and covers state monad types

inclusive of \emph{do} notation. Due to present limitations of AWE, this

solution is available only for Isabelle-HOL at the moment, although in

principle it could work for HOLCF as well.

Section 2 gives some background, section 3 introduces the system, section 4

gives the sublanguages of Haskell that can be translated, in section 5 we

define the two translations, in section 6 we sketch a denotational semantics

associated with the translation to HOLCF, in section 7 we show how translation

of monads is carried out with AWE.

\section{Logics and translations}

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

based on simply typed lambda calculus extended with axiomatic type classes. It

provides support for reasoning about programming functions, both in terms of

rich libraries and efficient automation. In this respect, it has essentially

superseded Isabelle-FOL (classical first-order logic) as a standard.

Isabelle-HOL has an implementation of recursive total functions based on

Knaster-Tarski fixed-point theorem. HOLCF \cite{holcf} is Isabelle-HOL

conservatively extended with the Logic of Computable Functions --- a

formalisation of domain theory.

In Isabelle-HOL types can be interpreted as sets (class \emph{type});

functions are total and may not be computable. A non-primitive recursive

function may require discharging proof obligations already at the stage of

definition --- in fact, a specific relation has to be given for a function to

be proved total. In HOLCF each type can be interpreted as a pointed complete

partially ordered set (class \emph{pcpo}) i.e. a set with a partial order

which is closed w.r.t. $\omega$-chains and has a bottom. Isabelle

formalisation, based on axiomatic type classes \cite{Wenzel}, makes it

possible to deal with complete partial orders in quite an abstract way.

Functions are generally partial and computability can be expressed in terms of

continuity. Recursion can be expressed in terms of least fixed-point operator,

and so, in contrast with Isabelle-HOL, function definition does not depend on

proofs. Nevertheless, proving theorems in HOLCF may turn out to be

comparatively hard. After being spared the need to discharge proof

obligations at the definition stage, one has to bear with assumptions on

function continuity throughout the proofs. A standard strategy is then to

define as much as possible in Isabelle-HOL, using HOLCF type constructors to

lift types only when this is necessary.

Although there have been translations of functional languages to first-order

systems --- those to FOL of Miranda \cite{Thompson95,Thompson89,Thompson95b}

and Haskell \cite{Thompson92}, both based on large-step operational semantics;

that of Haskell to Agda implementation of Martin-Loef type theory in

\cite{Abel} --- still, higher-order logic may be quite helpful in order to

deal with features such as currying and polymorphism. Moreover, higher-order

approaches may rely on denotational semantics --- as for examples, \cite{Huff}

translating Haskell to HOLCF, and \cite{Pollack} translating ML to HOL ---

allowing for program representation closer to specification as well as for

proofs comparatively more abstract and general.

The translation of Haskell to HOLCF proposed in \cite{Huff} uses deep

embedding to deal with types. Haskell types are translated to terms, relying

on a domain-theoretic modelling of the type system at the object level,

allowing explicitly for a clear semantics, and providing for an implementation

that can capture most features, including type constructor classes. In

contrast, we provide in the case of HOLCF with a translation that follows the

lines of a denotational semantics under the assumption that type constructors

and type application in Haskell can be mapped to corresponding constructors

and built-in application in Isabelle without loss from the point of view of

behavioural equivalence between programs --- in particular, translating

Haskell datatypes to Isabelle ones.

\section{Translations in Hets}

The Haskell-to-Isabelle translation in Hets requires GHC, Programatica,

Isabelle and AWE. The application is run by a command that takes as arguments

a target logic and an Haskell program, given as a GHC source file. The latter

gets analysed and translated, the result of a successful run being an Isabelle

theory file in the target logic.

The Hets internal representation of Haskell is similar to that of

Programatica, whereas the internal representation of Isabelle is based on the

ML definition of the Isabelle base logic, extended in order to allow for a

simpler representation of Isabelle-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 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 theories in the representation of the target language.

Each translation relies on a specific Isabelle theory included in the Hets

distrubution --- \emph{HsHOLCF} for HOLCF and \emph{HsHOL} for HOL,

respectively, the latter of which uses AWE.

\section{Sublanguage definitions}

Programs can be regarded as theories in a language given by definitions of

type, class, type schemas (types with a context where variables are sorted by

class), patterns, terms, declarations (forming the signature --- including

function declaration, datatype declaration, type definition, as well as class

and method declaration) and definitions (forming the theory body --- including

function definition, as well as instance and method definition).

\subsection{HOLCF}

In the following, we give a definition of the sub-language of Haskell

$H_c$ that is covered by the translation to HOLCF.\\

\noindent Types

$$\begin{array}{lll}

\tau \ = () \\

& Bool \\

& Integer & \\

& v & \mbox{type \ variable}\\

& \tau_1 \to \tau_2 & \\

& (\tau_1,\tau_2) & \\

% & Either \ tau_1 \ tau_2 \\

& [\tau] & \\

& Maybe \ \tau & \\

& T \ \tau_{1} \ \ldots \tau_{n} & \mbox{either \ datatype \ or \

defined \ type}

% & T \ \tau_{1} \ \ldots \ \tau_{n} \qquad \mbox{defined \ type}

\end{array}$$

\noindent Type classes

$$\begin{array}{lll}

K \ = & Eq & \mbox{with \ default \ methods} \ ==, \ /= \\

& K & \mbox{defined \ type \ class} \\

\end{array}$$

\noindent Contexts

$$\begin{array}{lll}

ctx \ = & \{K \ v\} \ \cup \ ctx & \\

& \{\} & \mbox{empty \ context} \\

\end{array}$$

\noindent Type schemas

$$\begin{array}{ll}

\phi \ = & ctx \Rightarrow \tau \\

& \qquad \mbox{where \ all \ variables \ in} \ ctx \ \mbox{are \ in} \ \tau

\end{array}$$

\noindent Simple patterns

$$\begin{array}{lll}

sp \ = & \_ & \mbox{wildcard} \\

& v & \mbox{variable \ of \ datatype}\\

& C \ \overline{v} & \mbox{case \ of \ datatype}

\end{array}$$

\noindent Terms

$$\begin{array}{lll} t \ =

& t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\

& c \in \aleph & \mbox{Integer \ constant} \\

& t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\

& t \in \{:,head,tail\} & \mbox{on list} \\

& t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\

& t \in \{Just,Nothing\} & \mbox{on \ \emph{maybe} \ types} \\

& t \in \{fst,snd\} & \mbox{on \ pairs} \\

& (,) & \\

& x & \mbox{variable} \\

& f & \mbox{function \ symbol} \\

& C & \mbox{data \ constructor} \\

& if \ t \ then \ t_1 \ else \ t_2 \\

& case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\

& let \ (x_1 = t_1; \ \ldots; \ x_n = t_n) \ in \ t

\end{array}$$

\noindent Declarations

$$\begin{array}{ll}

Decl \ = & type \ T \ \overline{v} \ = \ \tau \\

& data \ ctx \ \Rightarrow \ T \ \overline{v} \ =

\ C_{1} \ \overline{x}_1 \ | \ \ldots \ | \ C_{k} \ \overline{x}_k \\

% & \qquad \mbox{with} \ {\overline{x}}_1, {\overline{x}}_k \ \subseteq \

% \overline{v} \\

& ctx \ \Rightarrow \ f \ :: \ \tau \\

& class \ K \

where \ (f_{1}:: \tau_{1}; \ldots; f_{n}::\tau_{n}) \\

& \qquad \mbox{where} \ \tau_{1}, \tau_{n} \

\mbox{have \ only \ one \ type \ variable}

\end{array}$$

\noindent Definitions

$$\begin{array}{ll}

Def \ = & f \ \overline{v} \ = \ t \\

& f \ \overline{v}_{1} \ sp_1 \ {\overline{w}}_{1} \ = \ t_1; \ \ldots;

\ f \ \overline{v}_{n} \ sp_n \ {\overline{w}}_{n} \ = \ t_n \\

& instance \ ctx \Rightarrow K \ \tau \ where \

(f_1 = t_1; \ldots; \ f_n = t_n) \\

& \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ methods \ of} \ K

\end{array}$$\\

\subsection{HOL}

In contrast, the following gives a definition of the Haskell sub-language

$H_s$ that is covered by the translation to HOL.\\

\noindent Types, Type classes, Contexts, Type schemas, Simple patterns,

Declarations

\emph{as before}\\

\noindent Type constructor classes

$Monad$\\

\noindent Terms

$$\begin{array}{lll} t \ =

& () & \\

& t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\

& c \in \aleph & \mbox{Integer \ constant} \\

& t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\

& t \in \{:,head,tail\} & \mbox{on list} \\

& t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\

& t \in \{Just,Nothing\} & \mbox{on \ Maybe} \\

& t \in \{return,bind\} & \mbox{on \ monadic \ types} \\

& t \in \{fst,snd\} & \mbox{on \ pairs} \\

& (,) & \\

& x & \mbox{variable} \\

& f & \mbox{function \ symbol} \\

& C & \mbox{data \ constructor} \\

& if \ t \ then \ t_1 \ else \ t_2 \\

& case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\

& \qquad \mbox{with} \ sp_1, \ldots, sp_n \ \mbox{complete \ match} \\

& let \ (x_1 = t_1; \ \ldots; \ x_n = t_n) \ in \ t

\end{array}$$

\noindent Definitions

$$\begin{array}{ll}

Def \ = & f \ \overline{v} \ = \ t \\

& \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive

\ recursive} \\

& f \ \overline{v}_1 \ sp_1 \ \overline{w}_1 \ = \ t_1; \ \ldots;

\ f \ \overline{v}_n \ sp_n \ \overline{w}_n \ = \ t_n \\

& \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive

\ recursive} \\

& f_1 \ v_1::\tau \ \overline{w_1} \ = \ t_1; \ ldots; \

f_n \ v_n::\tau \ \overline{w_n} \ = \ t_n \\

& \qquad \mbox{where} \ f_1::\phi_1, \ldots, f_n::\phi_n \ \mbox{are \

totally \ defined, \ mutually} \\

& \qquad \mbox{primitive \ recursive \ in \ the \ first \ argument, \ and \

forall} \\

& \qquad 0 < i \leq n \ \mbox{there \ exists \ type

\ variable \ renaming} \

\sigma_i \ \mbox{such} \\

& \qquad \mbox{that} \ \tau_1 = \sigma_i(\tau_i) \ \mbox{and \ all \ the \

variables \ in} \ \phi_i \ \mbox{appear \ in} \ \tau_i \\

& instance \ ctx \Rightarrow K \ \tau \ where \

(f_1 = t_1; \ldots; \ f_n = t_n) \\

& \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ totally \ defined, \

primitive \ recursive} \\

& \qquad \mbox{methods \ of} \ K

\end{array}$$\\

\section{Translation definitions}

We can define recursively a translation from an Haskell program to an Isabelle

theory along the line of theory morphisms \cite{MossaTh}. Here we can simply

take a translation $\omega \ :: \ L_1 \ \to \ L_2$ to be partially defined as

a set $\Omega$ of rules $r_{\in \Omega} :: L_1 \ \to \ L_2$ and a renaming

function $t$ that preserves names, up to avoidance of name clashes (in our

case, with Isabelle keywords), in the following sense: if $\alpha$ is a name

(either a variable or a constant, for either a term or a type), then $\omega =

t$; else, if there exists $r \in \Omega$ that matches $\alpha$ most closely,

$\omega(\alpha) \ =\ r(\alpha)$; else undefined. In the following we assume

$\omega$ to be total, we ignore $t$, we write $\alpha'$ for $\omega(\alpha)$

and we write rules in relational form, such as $\alpha \ \Longrightarrow \

r(\alpha)$.

\subsection{HOLCF}

The translation $\omega_c \ :: \ H_c \ \to \ HOLCF$ from programs in

$H_c$ to theories in HOLCF can be defined, semi-formally, with the

following set of rules.\\

\noindent Types

$$\begin{array}{ll}

a & \Longrightarrow \ 'a::\{pcpo\} \\

() & \Longrightarrow \ unit \ lift \\

Bool & \Longrightarrow \ bool \ lift \\

Integer & \Longrightarrow \ int \ lift \\

\tau_{1} \to \tau_{2} & \Longrightarrow

\ \tau'_{1} \ \to \ \tau'_{2} \\

(\tau_{1},\tau_{2}) & \Longrightarrow

\ (\tau'_{1} * \tau'_{2}) \\

{[\tau]} \ & \Longrightarrow \ \tau' \ seq \\

Maybe \ \tau & \Longrightarrow \ \tau' \ maybe \\

T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow

\ \tau'_1 \ \ldots \ \tau'_n \ T' \\

& \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\

\end{array}$$

\noindent Classes

$$\begin{array}{ll}

Eq & \Longrightarrow \ Eq \\

K & \Longrightarrow \ K'

\end{array}$$

\noindent Type schemas

$$\begin{array}{ll}

(\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow

\ (ctx \Rightarrow \tau)'

\ [(v'::s) / (v'::({K'} \cup s))] \\

\{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'

\end{array}$$\\

Haskell type variables are translated to variables of class \emph{pcpo}. Each

type is associated to a sort in Isabelle, defined by the set of the classes of

which it is member. Built-in types are translated to the lifting of its

corresponding HOL type. The HOLCF type constructor \emph{lift} is used to

lift types to flat domains. 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)$. Type

constructors are translated to corresponding HOLCF ones (notably, parameters

precede type constructors in Isabelle syntax). \emph{Maybe} is

translated to HOLCF-defined \emph{maybe} (the disjoint union of the lifted

unit type and the lifted domain parameter).\\

\noindent Terms

$$\begin{array}{ll}

x::\tau & \Longrightarrow \ x'::\tau' \\

() & \Longrightarrow \ Def \ () \\

True & \Longrightarrow \ TT \\

False & \Longrightarrow \ FF \\

\&\& & \Longrightarrow \ trand \\

|| & \Longrightarrow \ tror \\

not & \Longrightarrow \ neg \\

c & \Longrightarrow \ Def \ c \\

t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ fliftbin \ t \\

negate & \Longrightarrow \ flift2 \ - \\

{[]} & \Longrightarrow \ nil \\

t:ts & \Longrightarrow \ t'\#\#ts' \\

head & \Longrightarrow \ HD \\

tail & \Longrightarrow \ TL \\

== & \Longrightarrow \ hEq \\

/= & \Longrightarrow \ hNEq \\

Just & \Longrightarrow \ return \\

Nothing & \Longrightarrow \ fail \\

C & \Longrightarrow \ C' \\

f & \Longrightarrow \ f' \\

\backslash \overline{x} \ \to \ t & \Longrightarrow

\ LAM \ \overline{x}'. \ t' \\

t_1 \ t_2 & \Longrightarrow \ t'_1 \ \cdot \ t'_2 \\

(t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\

fst & \Longrightarrow \ cfst \\

snd & \Longrightarrow \ csnd \\

let \ (x_1 = t_1; & \\

\qquad \dots; & \\

\qquad x_n = t_n) \quad in \ t & \Longrightarrow

\ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\

if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow

\ If \ t' \ then \ t'_1 \ else \ t'_2 \ fi \\

case \ x \ of \ (p_1 \to t_1; & \\

\qquad \qquad \ldots; & \\

\qquad \qquad p_n \to t_n) & \Longrightarrow

\ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}

\Rightarrow t'_n \\

& \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \

\mbox{is \ a \ complete \ match} \\

& case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}

\Rightarrow t'_{n-1} \\

& \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n

\ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\

& \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,

p'_{n-1}, q_1, \ldots, q_k \\

& \qquad \mbox{complete \ match} \\

& case \ x' \ p'_{1} \Rightarrow t'_1 \ | \ \ldots \ | \ p'_n

\Rightarrow t'_n \\

& \qquad \qquad \qquad | \ q_{1} \Rightarrow \bot \

| \ \ldots q_{k} \Rightarrow \bot \\

& \qquad \mbox{with} \ p'_1, \ldots, p'_{n}, q_1, \ldots, q_k \

\mbox{complete \ match}

\end{array}$$\\

Terms of built-in type are translated using HOLCF-defined lifting function

\emph{Def}. The bottom element $\bot$ is used for undefined terms.

HOLCF-defined $flift1 :: \ ('a \Rightarrow 'b::pcpo) \Rightarrow ('a \ lift

\to 'b)$ and $flift2 :: \ ('a \Rightarrow 'b) \Rightarrow ('a \ lift \to 'b \

lift)$ are used to lift operators, as well as the following, defined in

\emph{HsHOLCF}.\\

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

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

$fliftbin \ f \ == \ flift1 \ (\lambda x. \ flift2 \ (f \ x))$\\

\noindent Boolean values are translated to values of \emph{bool lift}

(\emph{tr} in HOLCF) i.e. \emph{TT}, \emph{FF} and $\bot$, and Boolean

connectives to the corresponding HOLCF operators. HOLCF-defined \emph{If then

else fi} and \emph{case} syntax are used to translate conditional and case

expressions, respectively. There are restrictions, however, on case

epressions, due to limitations in the translation of patterns; in particular,

the case term has to be a variable, and only simple patterns are allowed (no

nested ones). On the other hand, Isabelle sensitiveness to the order of

patterns in case expressions is dealt with. Multiple function definitions are

translated as definitions based on case expressions. In function definitions

as well as in case expressions, both wildcards --- not available in Isabelle

--- and incomplete patterns --- not allowed --- are dealt with by elimination,

$\bot$ being used as default value in the latters. Only let expressions

without patterns on the left are dealt with; where expressions, guarded

expressions and list comprehension are not covered.

Lists are translated to the domain \emph{seq} defined in library IOA.\\

$domain \ 'a\ seq \ = \ nil \ | \ \#\# \ (HD :: \ 'a) \

(lazy \ TL :: \ 'a \ seq) $\\

\noindent Keyword \emph{lazy} ensures that $x \ \#\# \ \bot \ \neq \ \bot$,

allowing for partial sequences as well as for infinite ones \cite{holcf}.\\

\noindent Declarations

$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \

\Longrightarrow \ class \ K' \ \subseteq

\ pcpo; \ Dec'_1; \ \ldots; \ Dec'_n \\

f :: \phi \qquad \qquad \qquad \quad \Longrightarrow

\ consts \ f' \ :: \ \phi' \\

type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow

\ type \ \tau \ = \ \tau'_1 \\

(data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i

\ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\

\ldots; \\

data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h

\ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\

\qquad domain \ \phi'_1 \ = \ C'_{11} \ d_{111} \ x'_1 \ \ldots \ d_{11i} \

x'_i \ | \ \ldots \ | \ C'_{1p} \

d_{1p1} \ y'_1 \ \ldots \ d_{1pj} \ y'_j \\

\qquad and \ \ldots \\

\qquad and \ \phi'_n \ = \ C'_{n1} \ d_{n11} \ w'_1 \ \ldots \ d_{n1h} \

w'_h \ | \ \ldots \ | \ C'_{nq} \

d_{nq1} \ z'_1 \ \ldots \ d_{nqk} \ z'_k \\

\qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \

datatype}

\end{array}$$

\noindent Definitions

$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \

\ldots;

\ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\

\qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash

\overline{x}_1 \to \ t_1); \

\ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\

f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'

\

== \ LAM \ \overline{x}'. \ t' \\

\qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\

(f_1 \ \overline{v_1} \ = \ t_1; \ \ldots;

\ f_n \ \overline{v_n} \ = \ t_n) \ \Longrightarrow \\

\qquad fixrec \ f'_1 :: \phi'_1 \ =

\ (LAM \ \overline{v_1}'. \ t'_1) \ and \\

\qquad \quad \ldots \\

\qquad \quad and \ f'_n :: \phi'_n \ =

\ (LAM \ \overline{v_n}'. \ t'_n) \\

\qquad \mbox{with} \ f_1::\phi_1, \ldots, f_n::\phi_n \

\mbox{mutually \ recursive} \\

instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\

\qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)

\ \Longrightarrow \\

\qquad instance \\

\qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)

\in ctx\}, \ \ldots, \\

\qquad \qquad \qquad \quad \quad

\{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\

\qquad \qquad \mbox{with \ proof \ obligation}; \\

\qquad defs \ f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::

(ctx \Rightarrow \tau_n)' == t'_n

\end{array}$$\\

Function declarations use Isabelle keyword \emph{consts}. Datatype

declarations in HOLCF are domain declarations and require explicitly

destructors. Mutually recursive datatypes relies on specific Isabelle syntax

(keyword \emph{and}). Order of declarations is taken care of.

Non-recursive definitions are translated to standard definitions using

Isabelle keyword \emph{defs}. Recursive definitions rely on HOLCF package

\emph{fixrec} which provides nice syntax for fixed point definitions,

including mutual recursion. Lambda abstraction is translated as continuous

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

\emph{dot} operator), equivalent to lambda abstraction ($\lambda$) and

standard function application, respectively, when all arguments are

continuous.

Classes in Isabelle and Haskell are built quite differently. In Haskell, a

type class is associated to a set of function declarations, and it can be

interpreted as the set of types where those functions are defined. In

Isabelle, a type class has a single type parameter, it is associated to a set

of axioms in a single type variable, and can be interpreted as the set of

types that satisfy those axioms.

Not all the problems have been solved with

respect to arities that may conflict in Isabelle, although they correspond to

compatible Haskell instantiations. Moreover, Isabelle does neither allow for

multi-parameter classes, nor for type constructor ones, therefore the same

translation method cannot be applied to them.

Defined single-parameter classes are translated to HOLCF as subclasses of

\emph{pcpo} with empty axiomatization. Methods declarations associated with

Haskell classes are translated to independent function declarations with

appropriate class annotation on type variables. In Isabelle, each instance

requires proofs that class axioms are satisfied by the instantiating type ---

anyway, as long as there are no axioms proofs are trivial and proof obligation

may be automatically discharged. Method definitions associated with instance

declarations are translated to independent function definitions, using type

annotation and relying on Isabelle overloading.

In the internal representation of Haskell given by Programatica, function

overloading is handled by means of dictionary parameters \cite{Jones93}. This

means that each function has additional parameters for the classes associated

to its type variables. In fact, dictionary parameters are used to decide, for

each instantiation of the function type variables, how to instantiate the

methods called in the function body. On the other hand, overloading in

Isabelle is obtained by adding explicitly type annotation to function

definitions --- dictionary parameters may thus be eliminated.

The translation of built-in classes may involve axioms --- this is the case

for equality. A HOLCF formalisation, based on the methods specification in

\cite{HaskellRep}, has been given as follows in \emph{HsHOLCF} (\emph{neg}

is lifted negation).\\

$consts$

$$\begin{array}{ll}

heq :: & 'a \ \to \ 'a \ \to \ tr \\

hneq :: & 'a \ \to \ 'a \ \to \ tr \\

\end{array}$$

$axclass \ Eq \ < \ pcpo$

$eqAx: heq \cdot p \cdot q \ = \ neg \cdot (hneq \cdot p \cdot q)$\\

\noindent Functions \emph{heq} and \emph{hneq} can be defined, for each

instantiating type, with the translation of equality and inequality,

respectively. For each instance, a proof that the definitions satisfy

\emph{eqAx} needs to be given --- the translation will simply print out

\emph{sorry} (a form of ellipsis in Isabelle). The definition of default

methods for built-in types and the associated proofs can be found in

\emph{HsHOLCF}.

\subsection{HOL}

The translation $\omega_s \ :: \ H_s \ \to \ HOL$ from programs in $H_s$

to theories in Isabelle-HOL extended with AWE can be defined with the

following set of rules.\\

\noindent Types

$$\begin{array}{ll}

() & \Longrightarrow \ unit \\

a & \Longrightarrow \ 'a::\{type\} \\

Bool & \Longrightarrow \ boolean \\

Integer & \Longrightarrow \ int \\

\tau_{1} \to \tau_{2} & \Longrightarrow

\ \tau'_{1} \ \Rightarrow \ \tau'_{2} \\

(\tau_{1},\tau_{2}) & \Longrightarrow

\ (\tau'_{1} * \tau'_{2}) \\

{[\tau]} \ & \Longrightarrow \ \tau' \ list \\

Maybe \ \tau & \Longrightarrow \ \tau' \ option \\

T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow

\ \tau'_1 \ \ldots \ \tau'_n \ T' \\

& \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\

\end{array}$$

\noindent Classes

$$\begin{array}{ll}

Eq & \Longrightarrow \ Eq \\

K & \Longrightarrow \ K'

\end{array}$$

\noindent Type schemas

$$\begin{array}{ll}

(\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow

\ (ctx \Rightarrow \tau)'

\ [(v'::s) / (v'::({K'} \cup s))] \\

\{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'

\end{array}$$\\

Here we highlight the main differences the translation to HOLCF and this,

semantically rather more approximative one to Isabelle-HOL (thereafter simply

HOL). Function type, product and list are used to translate the corresponding

Haskell constructors. Option types are used to translate \emph{Maybe}. Haskell

datatypes are translated to HOL datatypes. Type variables are of class

\emph{type}.

Standard lambda-abstraction ($\lambda $) and function application are used

here, instead of continuous ones. Non-recursive definitions are treated in an

analogous way as in the translation to HOLCF. However, partial functions and

particularly case expressions with incomplete patterns are not allowed.

In HOL one has to pay attention to the distinction between \emph{primitive

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

generally recursive ones. Termination is guaranteed for each primitive

recursive function by the fact that recursion is based on the datatype

structure of one of the parameters. In contrast, termination is no trivial

matter for recursion in general. A strictly decreasing measure needs to be

association with the parameters. This cannot be dealt with automatically in

general. Threferore here we restrict translation to primitive recursive

functions.

Mutual primitive recursion is allowed for under additional restrictions ---

more precisely, given a set $F$ of functions: 1) all the functions in $F$ are

recursive in the first argument; 2) all recursive arguments in $F$ are of the

same type modulo variable renaming; 3) each type variable occurring in the

type of a function in $F$ already occurs in the type of the first argument.

The third conditions is a way to ensure that we do not end up with type

variables which occurs on the right hand-side but not on the left hand-side of

a definition. In fact, given mutually recursive functions $f_{1}, \ldots,

f_{n}$ of type $A \rightarrow B_{1}, \ldots, A \rightarrow B_{n}$ after

variable renaming, they are translated to projections of a new function of

type $A \rightarrow (B_{1} * \ldots * B_{n})$ which is defined for cases of

$A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The

expression $nth_n \ t$ used in the translation rule is simply an informal

abbreviation for the HOL function, defined in terms of $fst$ and $snd$, which

extracts the $n$-th projection from a tuple no shorter than $n$.\\

\noindent Terms

$$\begin{array}{ll}

x::\tau & \Longrightarrow \ x'::\tau' \\

() & \Longrightarrow \ () \\

True & \Longrightarrow \ True \\

False & \Longrightarrow \ False \\

\&\& & \Longrightarrow \ \& \\

|| & \Longrightarrow \ | \\

not & \Longrightarrow \ Not \\

c & \Longrightarrow \ c \\

t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ t \\

negate \ x & \Longrightarrow \ - x \\

{[]} & \Longrightarrow \ {[]} \\

t:ts & \Longrightarrow \ t'\#ts' \\

head & \Longrightarrow \ hd \\

tail & \Longrightarrow \ tl \\

== & \Longrightarrow \ hEq \\

/= & \Longrightarrow \ hNEq \\

Just & \Longrightarrow \ Some \\

Nothing & \Longrightarrow \ None \\

return & \Longrightarrow \ return \\

bind & \Longrightarrow \ mbind \\

C & \Longrightarrow \ C' \\

f & \Longrightarrow \ f' \\

\backslash \overline{x} \ \to \ t & \Longrightarrow

\ \lambda \ \overline{x}'. \ t' \\

t_1 \ t_2 & \Longrightarrow \ t'_1 \ t'_2 \\

(t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\

fst & \Longrightarrow \ fst \\

snd & \Longrightarrow \ snd \\

let \ (x_1 = t_1; & \\

\qquad \dots; & \\

\qquad x_n = t_n) \quad in \ t & \Longrightarrow

\ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\

if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow

\ if \ t' \ then \ t'_1 \ else \ t'_2 \\

case \ x \ of \ (p_1 \to t_1; \\

\qquad \qquad \ldots; & \\

\qquad \qquad p_n \to t_n) & \Longrightarrow

\ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}

\Rightarrow t'_n \\

& \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \

\mbox{is \ a \ complete \ match} \\

& case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}

\Rightarrow t'_{n-1} \\

& \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n

\ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\

& \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,

p'_{n-1}, q_1, \ldots, q_k \\

& \qquad \mbox{complete \ match}

\end{array}$$\\

\noindent Declarations

$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \

\Longrightarrow \ class \ K' \ \subseteq

\ type; \ Dec'_1; \ \ldots; \ Dec'_n \\

f :: \phi \qquad \qquad \qquad \quad \Longrightarrow

\ consts \ f' \ :: \ \phi' \\

type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow

\ type \ \tau \ = \ \tau'_1 \\

(data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i

\ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\

\ldots; \\

data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h

\ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\

\qquad datatype \ \phi'_1 \ = \ C'_{11} \ x'_1 \ \ldots \ x'_i \ | \ \ldots

\ | \ C'_{1p}

\ y'_1 \ \ldots \ y'_j \\

\qquad and \ \ldots \\

\qquad and \ \phi'_n \ = \ C'_{n1} \ w'_1 \ \ldots \ w'_h \ | \ \ldots \ | \

C'_{nq}

\ z'_1 \ \ldots \ z'_k \\

\qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \

datatype}

\end{array}$$

\noindent Definitions

$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \

\ldots;

\ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\

\qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash

\overline{x}_1 \to \ t_1); \

\ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\

f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'

\

== \ \lambda \ \overline{x}'. \ t' \\

\qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\

f_1 \ \ y_1 \ \overline{x_1} \ =

\ t_1; \ \ldots; \ f_n \ y_n \

\overline{x_n} \ = \ t_n \ \Longrightarrow \\

\qquad decl \ f_{new} ::

(\sigma_1(ctx_1) \ \cup \ \ldots \ \cup \ \sigma_n(ctx_n)

\ \Rightarrow \\

\qquad \qquad \qquad \qquad \sigma_1(\tau_{1a}) \ \to \

(\sigma_1(\tau_1), \ldots, \sigma_n(\tau_n)))' \\

\qquad primrec \ f_{new} \ sp_1 \ =

\ (\lambda \ \overline{x_1}'. \ t'_1 [y'_1/sp_1], \ldots, \ \lambda \

\overline{x_n}'. t'_n [y'_n/sp_1]); \\

\qquad \qquad \qquad \ldots; \\

\qquad \qquad \qquad

f_{new} \ sp_k \ = \ (\lambda \ \overline{x_1}'. \ t'_1

[y'_1/sp_k], \ldots,

\ \lambda \ \overline{x_n}'. \ t'_n [y'_n/sp_k]); \\

\qquad defs \ f_1 \ x \ == \ nth_1 \ (f_{new} \ x); \ \ldots;

\ f_n \ x \ == \ nth_n \ (f_{new} \ x) \\

\qquad \mbox{with} \ f_1:: (ctx_1 \Rightarrow \tau_{1a} \to \tau_1),

\ \ldots, \ f_n::(ctx_n \Rightarrow \tau_{na} \to \tau_n) \\

\qquad \mbox{mutually \ recursive} \\

instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\

\qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)

\ \Longrightarrow \\

\qquad instance \\

\qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)

\in ctx\}, \\

\qquad \qquad \qquad \quad \quad

\ldots, \ \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\

\qquad \qquad \mbox{with \ proof \ obligation}; \\

\qquad defs \quad

f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::

(ctx \Rightarrow \tau_n)' == t'_n\\

instance \ Monad \ \tau \ where \

(def_{eta}; def_{bind}) \ \Longrightarrow \\

\qquad defs \quad def'_{eta}; \ def'_{bind}; \\

\qquad t\_instantiate \ Monad \ mapping \ m\_\tau' \\

\qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\

\qquad \mbox{where} \ m_\tau' \ \mbox{is \ defined \ as \

theory \ morphism \ associating} \\

\qquad MonadType.M, \ MonadOpEta.eta,

\ MonadOpBind.bind \\

\qquad \mbox{to} \ tau', \ def'_{eta}, \ def'_{bind} \

\mbox{respectively;}

\end{array}$$\\

Type classes are translated to subclasses of \emph{type}. An axiomatisation of

Haskell equality for total functions can be found in \emph{HsHOL}.

$consts$

$$\begin{array}{ll}

heq :: & 'a \ \to \ 'a \ \to \ bool \\

hneq :: & 'a \ \to \ 'a \ \to \ bool \\

\end{array}$$

$axclass \ Eq \ < \ type$

$eqAx: heq \ p \ q \ = \ Not \ (hneq \ p \ q)$\\

Given the restriction to total functions, equality on built-in types can be

defined as HOL equality.

\section{Semantics (for HOLCF)}

Denotational semantics con be given as basis for the translation to HOLCF.

Essentially, the claim here is that the expressions on the left hand-side of

the following tables represent the denotational meaning of the Haskell

expressions on the right hand-side, as well as of the HOLCF expressions to

which they are translated. The language on the left hand-side is still based

on HOLCF where type have been extended with abstraction ($\Lambda$) and fixed

point ($\mu$) in order to represent the denotational meaning of domain

declarations.\\

$$\begin{array}{ll}

\lceil a \rceil & = \ 'a::pcpo \\

\lceil () \rceil & = \ unit \ lift \\

\lceil Bool \rceil & = \ bool \ lift \\

\lceil Integer \rceil & = \ int \ lift \\

\lceil \to \rceil & = \ \to \\

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

\lceil [] \rceil & = \ seq \\

\lceil Maybe \rceil & = \ maybe \\

\lceil T_1 \ T_2 \rceil & = \ \lceil T_1 \rceil \ \lceil T_2 \rceil \\

% \lceil TC \rceil & = & \mu X. (\Lambda \ v_1, \ldots, v_n.

% \ \lceil \tau_1 \rceil + \ldots + \lceil \tau_{k} \rceil)[X/TC] \\

% \mbox{when \ there \ is \ a \ declaration} \ data \ TC \ v_1 \ \ldots \ v_n

% \ = \ C_1::\tau_1 | \ldots |

% C_k::\tau_k \\

\lceil TC_{i} \rceil & = \ let \ F \ = \ \mu \ (X_1*\ldots*X_k). \\

& \quad ((\Lambda \ v_{11}, \ldots, v_{1m}.

\ \lceil \tau_{11} \rceil + \ldots + \lceil \tau_{1p} \rceil),

\ \ldots, \\

& \quad (\Lambda \ v_{k1}, \ldots, v_{kn}. \ \ldots,

\ \lceil \tau_{k1} \rceil + \ldots + \lceil \tau_{kq} \rceil))

[X_1/TC_1,\ldots,X_k/TC_k] \\

& in \ nth_i(F) \\

\quad \mbox{with} \ 0 < i \leq k, & \mbox{when} \ data \ TC_1 \ v_{11} \ \ldots \ v_{1m} \ = \ C_{11}::\tau_{11}

| \ldots | C_{1p}::\tau_{1p}; \\

& \quad \ldots; \ data \ TC_k \ v_{k1} \ \ldots \ v_{kn} \ =

\ C_{k1}::\tau_{k1} | \ldots |

C_{kq}::\tau_{kq} \\

& \mbox{are \ mutually \ recursive \ declarations} \\

\end{array}$$\\

The representation of term denotation is similar to what we get from the

translation, except that for functions we give the representation of the

meaning of \emph{fixrec} definitions ($FIX$ is the HOLCF fixed point

operator).\\

$$\begin{array}{ll}

\lceil x::a \rceil & = \ x'::\lceil a \rceil \\

\lceil c \rceil & = \ c' \\

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

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

\lceil t_1 \ t_2 \rceil & = \ \lceil t_1 \rceil \ \cdot \

\lceil t_2 \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 f_i \rceil & = \ let \ g \ =

FIX \ (x_1,\ldots,x_n). \

(\lceil t_1 \rceil, \ldots, \lceil t_{n} \rceil [f_1/x_1,\ldots,f_n/x_n] \\

& in \ nth_i (g) \\

\quad \mbox{with} \ 0 < i \leq n,

& \mbox{where} \ f_1 = t_1, \ f_n = t_n \ \mbox{are \ mutually \ recursive

\ definitions}

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

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

\end{array}$$

\section{Monads with AWE}

A monad is a type constructor with two operations that can be specified

axiomatically --- \emph{eta} (injective) and \emph{bind} (associative, with

\emph{eta} as left and right unit) \cite{moggi89}. Isabelle does not have

type constructor classes, therefore monads cannot be translated directly. The

indirect solution that we are pursuing, is to translate monadic types as types

that satisfy the monadic axioms. This solution can be expressed in terms of

theory morphisms --- maps between theories, associating signatures to

signatures and axioms to theorems in ways that preserve operations and

arities, entailing the definition of maps between theorems. Theory morphisms

allow for theorems to be moved between theories by translating their proof

terms, making it possible to implement parametrisation at the theory level

(see \cite{AWE} for details). A \emph{parameterised theory} $\mathit{Th}$ has

a sub-theory $\mathit{Th}_P$ which is the parameter --- this may contain

axioms, constants and type declarations. Building a theory morphism from

$\mathit{Th}_P$ to a theory $I$ provides the instantiation of the parameter

with $I$, and makes it possible to translate the proofs made in the abstract

setting of $\mathit{Th}$ to the concrete setting of $I$ --- the result being

an extension of $I$. AWE is an extension of Isabelle that can assist in the

construction of theory morphisms \cite{AWE}.

A notion of monad \cite{AWE2} can be built in AWE by defining, on an abstract

level, a hierarchy of theories culminating in \emph{Monad}, based on the

declaration of a unary type constructor $M$ (in \emph{MonadType}) with the two

monad operations (contained in \emph{MonadOpEta} and \emph{MonadOpBind},

respectively) and the relevant axioms (in \emph{MonadAxms}). To show that a

specific type constructor forms a monad, we have to construct a theory

morphism from \emph{MonadAxms} to the specific theory; this involves giving

specific definitions of the operators, as well as discharging proof

obligations associated with specific instances of

the axioms. The following gives an example. \\

\noindent $data \ LS \ a \ = \ N \ | \ C \ a \ (LS \ a)$

\noindent $instance \ Monad \ LS \ where$

$$\begin{array}{ll}

return \ x & = \ C \ x \ N \\

x \ >>= \ f & = \ case \ x \ of \\

& N \ \to \ N \\

& C \ a \ b \ \to \ cnc \ (f \ a) \ (b \ >>= \ f)

\end{array}$$

$cnc :: \ LS \ a \ \to \ LS \ a \ \to \ LS \ a $

$$\begin{array}{ll}

cnc \ x \ y & = \ case \ x \ of \\

& N \ \to \ y \\

& C \ w \ z \ \to \ cnc \ z \ (C \ w \ y)

\end{array}$$

\noindent These definitions are plainly translated to HOL, as follows. Note

that these are not overloaded definitions. \\

\noindent $datatype \ 'a \ LS \ = \ N \ | \ C \ 'a \ ('a \ LS)$

\noindent $consts $

$$\begin{array}{ll}

return\_LS & :: \ 'a \ \Rightarrow 'a \ LS \\

mbind\_LS & :: \ 'a \ LS \ \Rightarrow \ ('a \ \Rightarrow \ 'b \ LS) \

\Rightarrow \ 'b \ LS \\

cnc & :: \ 'a \ LS \ \Rightarrow \ 'a \ LS \ \Rightarrow \ 'a \ LS \\

\end{array}$$

\noindent $defs $

$$\begin{array}{l}

return\_LS\_def : \ return\_LS:: \ ('a \ LS \ \Rightarrow 'a) \ == \

\lambda x. \ C \ x \ N

\end{array}$$

\noindent $primrec $

$$\begin{array}{ll}

mbind\_LS \ N & = \ \lambda f. \ N \\

mbind\_LS \ (C \ pX1 \ pX2) & = \ \lambda f. \ cnc \ (f \ pX1) \ (mbind\_LS \ pX2 \ f)

\end{array}$$

\noindent $primrec $

$$\begin{array}{ll}

cnc \ N & = \ \lambda b. \ b \\

cnc \ (C \ pX1 \ pX2) & = \ \lambda b. \ cnc \ pX2 \ (C \ pX1 \ b)

\end{array}$$

\noindent In order to build up the instantiation of \textit{LS} as a monad,

here it is defined the morphism $m\_LS$ from \emph{MonadType} to the

instantiating theory \emph{Tx}, by associating $M$ to $LS$.\\

$thymorph \ m\_LS : \ MonadType \ \longrightarrow \ Tx $

$$\begin{array}{l}

maps \ [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\

renames: \ [(MonadOpEta.eta \mapsto return\_LS),

(MonadOpBind.bind \mapsto mbind\_LS)] \\

\end{array}$$

\noindent

Renaming is used in order to avoid name clashes in case of more than one

monads --- here again, note the difference with overloading. Morphism

\emph{m\_LS} is then used to instantiate the parameterised theory

\emph{MonadOps}.\\

\noindent $t\_instantiate \ MonadOps \ mapping \ m\_LS$ \\

\noindent This instantiation gives the declaration of the

instantiated methods, which may now be defined.\\

\noindent $defs $

$$\begin{array}{l}

LS\_eta\_def: \ LS\_eta \ == \ return\_LS \\

LS\_bind\_def: \ LS\_bind \ == \ mbind\_LS

\end{array}$$

\noindent In order to construct a mapping from \emph{MonadAxms} to

\emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this

case, by straightforward simplification). The translation will print out

\emph{sorry} instead.

$$\begin{array}{ll}

lemma \ LS\_lunit : & LS\_bind \ (LS\_eta \ x) \ t \ = \ t \ x \\

lemma \ LS\_runit : & LS\_bind \ (t:: \ 'a \ LS) \ LS\_eta \ = \ t \\

lemma \ LS\_assoc : & LS\_bind \ (LS\_bind \ (s:: \ 'a \ LS) \ t) \ u \ = \\

& LS\_bind \ s \ (\lambda x. \ LS\_bind \ (t \ x) \ u) \\

lemma \ LS\_eta\_inj : & LS\_eta \ x \ = \ LS\_eta \ y \ \Longrightarrow \ x \ = \ y

\end{array}$$

\noindent Now, the morphism from \emph{MonadAxms} to

\emph{Tx} can be built, and then used to instantiate \emph{Monad}. This gives

automatically access to the theorems proven in \emph{Monad} and, modulo

renaming, the monadic syntax which is defined there. \\

$thymorph \ mon\_LS : \ MonadAxms \ \longrightarrow \ Tx $

$$\begin{array}{ll}

maps & [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\

& [(MonadOpEta.eta \ \mapsto \ Tx.LS\_eta), \\

& (MonadOpBind.bind \ \mapsto \ Tx.LS\_bind)]

\end{array}$$

$t\_instantiate \ Monad \ mapping \ mon\_LS$\\

$renames: \ [ \ldots ]$\\

\noindent The \emph{Monad} theory allows for the characterisation of

single parameter operators. In order to cover other monadic operators, a

possibility is to build similar theories for type constructors of fixed arity.

An approach altogether similar to the one shown for HOL could be used, in

principle, for HOLCF as well.

\section{Conclusion and future work}

The main advantage of shallow embedding is to get as much as possible out of

the automation currently available in Isabelle, especially with respect to

type checking. HOLCF in particular provides with an expressive semantics

covering lazy evaluation, as well as with a smart syntax --- also thanks to

the \emph{fixrec} package. The main disadvantage lies with lack of type

constructor classes. Anyway, it is possible to get around the obstacle, at

least partially, by relying on an axiomatic characterisation of monads and on

a proof-reuse strategy that actually minimises the need for interactive

proofs.

Future work should use this framework for proving properties of Haskell

programs. For monadic programs, we are also planning to use the monad-based

dynamic Hoare and dynamic logic that already have been formalised in Isabelle

\cite{Walter05}. Our translation tool from Haskell to Isabelle is part of the

Heterogeneous Tool Set Hets and can be downloaded from

\texttt{http://www.dfki.de/sks/hets}. More details about the translations can

be found in \cite{Tlmm}.

%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}

\begin{comment}

Here is a simple example. \\

\noindent $ fn3 \ :: \ AC \ a \ b \to (a \to a) \to AC \ a \ b $

$$\begin{array}{ll}

fn3 \ k \ f & = \ case \ k \ of \\

& Ct \ x \to Ct \ (f \ x) \\

& Rt \ x \ y \to Rt \ (fn4 \ x) \ y \\

\end{array}$$

\noindent $ fn4 \ :: \ AC \ a \ b \to AC \ a \ b $

$$\begin{array}{ll}

fn4 \ k & = \ case \ k \ of \\

& Rt \ x \ y \to Rt \ (fn3 \ x \ (\backslash z \to z)) \ y \\

& Ct \ x \to Ct \ x \\

\end{array}$$

\noindent It translates to HOL as follows.\\

\noindent $consts$

$$\begin{array}{ll} fn3 \ :: & ('a, 'b) \ AC \Rightarrow ('a \Rightarrow

'a) \Rightarrow

\ ('a, 'b) \ AC \\

fn4 \ :: & ('a, 'b) \ AC \Rightarrow

\ ('a, 'b) \ AC \\

fn3\_Xfn4\_X :: & ('a, 'b) \ AC \Rightarrow

\ (('a \Rightarrow 'a) \Rightarrow \\

& ('a, 'b) \ AC) *

\ (('a \Rightarrow 'a) \Rightarrow

\ ('a, 'b) \ AC) \\

\end{array}$$

\noindent $defs$

$$\begin{array}{lll}

fn3\_def : & fn3 \ == \ \lambda k \ f. \ fst \ (( fn3\_Xfn4\_X :: \\

& \ ('a, 'b) \ AC \Rightarrow (('a \Rightarrow 'a) \\

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

& ('a, 'b) \ AC) ) \ k) \ f \\

fn4\_def : & fn4 \ == \ \lambda k \ f. \ snd \ (( fn3\_Xfn4\_X :: \\

& ('a, 'b) \ AC \Rightarrow \\

& (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) * \\

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

\end{array}$$

\noindent $primrec$

$$\begin{array}{lll}

fn3\_Xfn4\_X & (Ct \ pX1) \ = & (\lambda f. \ Ct \ (f \ pX1), \\

& & \lambda f. \ Ct \ pX1) \\

fn3\_Xfn4\_X & (Rt \ pX1 \ pX2) & = \\

& (\lambda f. \ Rt \ (snd & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2, \\

& \lambda f. \ Rt \ (fst & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2) \\

\end{array}$$

\end{comment}