hs2isa.tex revision 7e80cfe2052409faa4ff745448c2f5ec8dd909f9
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\documentclass{llncs}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%\documentclass[a4paper,11pt]{article}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\textwidth 15.93cm
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\textheight 24cm
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\oddsidemargin 0.0cm
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\evensidemargin 0.0cm
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\topmargin 0.0cm
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\begin{document}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\title{Translating Haskell to Isabelle}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\author{ Paolo Torrini, Verimag \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {\tt Paolo.Torrini@imag.fr} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Christoph Lueth, DFKI Lab Bremen \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {\tt Christoph.Lueth@dfki.de} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Christian Maeder, DFKI Lab Bremen \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {\tt Christian.Maeder@dfki.de} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Till Mossakowski, DFKI Lab Bremen \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {\tt Till.Mossakowski@dfki.de} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini} \date{\today}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{abstract}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini We present partial translations of Haskell programs to Isabelle that have
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini been implemented as part of the Hets-Programatica system. The logics HOLCF
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini and Isabelle-HOL are targets --- under stronger restrictions in the latter
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini case --- to translations that are essentially based on a shallow embedding
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini approach. The AWE package has been used to support a translation of monadic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini operators based on theory morphisms.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{abstract}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Introduction}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAutomating the translation from programming languages to the languagee of a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinigeneric prover may provide useful support for the formal development and the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniverification of programs. It has been argued that functional languages can
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimake the task of proving assertions about programs written in them easier,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniowing to the relative simplicity of their semantics
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\cite{Thompson92,Thompson95}. The idea of translating Haskell programs, came
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinito us, more specifically, from an interest in the use of functional languages
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifor the specification of reactive systems. Haskell is a strongly typed, purely
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunctional language with lazy evaluation, polymorphic types extended with type
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniconstructor classes, and a syntax for side effects and pseudo-imperative code
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibased on monadic operators \cite{HaskellRep}. Several languages based on
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell have been proposed for application to robotics \cite{phh99,Hudak2003}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn such languages, monadic constructors are extensively used to deal with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniside-effects. Isabelle is a generic theorem-prover implemented in SML
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisupporting several logics --- in particular, Isabelle-HOL and its extension to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinia theory of computable functions (HOLCF) \cite{Paulson94isa,holcf}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniWe have implemented as functions of Hets translations of Haskell to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle-HOL and HOLCF following an approach based on shallow embedding,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimapping Haskell types to Isabelle ones, therefore taking full advantage of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle built-in type-checking. Hets \cite{TillHet,HetsUG,Hets} is an
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell-based application designed to support heterogeneous specification and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe formal development of programs. It has an interface with Isabelle, and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirelies on Programatica \cite{Prog04} for parsing and static analysis of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell programs. Programatica already includes a translation to HOLCF which,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniin contrast to ours, is based on an object-level modelling of the type system
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniOur translation to HOLCF covers at present Booleans, integers, basic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniconstructors (function, product, list, \emph{maybe}), equality,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisingle-parameter type classes (with some limitations), \emph{case} and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{if} expressions, \emph{let} expressions without patterns, mutually
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirecursive data-types and functions. It relies on existing formalisations of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilazy lists and \emph{maybe}. It keeps into account partiality and laziness by
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifollowing, for the main lines, the denotational semantics of lazy evaluation
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinigiven in \cite{winskel}. There are several limitations: \emph{Predulde} syntax
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniis covered only partially; list comprension, \emph{where} expressions and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{let} with patterns are not covered; further built-in types and type
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniclasses are not covered; imports are not allowed; constructor type classes are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrininot covered at all --- and so for monadic types beyond list and \emph{maybe}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniOf all these limitations, the only logically deep ones are those related to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniclasses --- all the other ones are just a matter of implementation.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe base translation to Isabelle-HOL is more limited, insofar as it covers
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinionly total primitive recursive functions. A better semantics with respect to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipartiality could be obtained by lifting the type of function values with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{option}, but this has not been pursued here. Still, \emph{option} has
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibeen used to translate \emph{maybe}. On the other hand, laziness appears very
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinihard to be captured with Isabelle-HOL. It also seems hard to overcome the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilimitation to primitive recursion. Other limitations are similar to those
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimentioned for the translation to HOLCF --- with the notable exception of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle does not allow for type constructor classes, therefore there is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinihardly a way shallow embedding of Haskell types may extend to cover them.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThis limitation is particularly acute with respect to monads and \emph{do}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrininotation. The problem is brilliantly avoided in \cite{Huff} by resorting to a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideeper modelling of types. On the other hand, the main novelty in our work is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinito rely on theory morphisms and on their implementation for Isabelle in the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipackage AWE \cite{AWE}, in order to deal with special cases of monadic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinioperator. This solution gives in general less expressiveness than the deeper
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniapproach --- however, when we can get it to deal with cases of interest, it
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimight make proofs easier. Currently Hets provides with an extension of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibase translation to Isabelle-HOL which uses AWE and covers state monad types
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinclusive of \emph{do} notation. Due to present limitations of AWE, this
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisolution is available only for Isabelle-HOL at the moment, although in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniprinciple it could work for HOLCF as well.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniSection 2 gives some background, section 3 introduces the system, section 4
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinigives the sublanguages of Haskell that can be translated, in section 5 we
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefine the two translations, in section 6 we sketch a denotational semantics
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniassociated with the translation to HOLCF, in section 7 we show how translation
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof monads is carried out with AWE.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Logics and translations}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle-HOL is the implementation in Isabelle of classical higher-order logic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibased on simply typed lambda calculus extended with axiomatic type classes. It
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniprovides support for reasoning about programming functions, both in terms of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirich libraries and efficient automation. In this respect, it has essentially
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisuperseded Isabelle-FOL (classical first-order logic) as a standard.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle-HOL has an implementation of recursive total functions based on
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniKnaster-Tarski fixed-point theorem. HOLCF \cite{holcf} is Isabelle-HOL
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniconservatively extended with the Logic of Computable Functions --- a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniformalisation of domain theory.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn Isabelle-HOL types can be interpreted as sets (class \emph{type});
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunctions are total and may not be computable. A non-primitive recursive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunction may require discharging proof obligations already at the stage of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefinition --- in fact, a specific relation has to be given for a function to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibe proved total. In HOLCF each type can be interpreted as a pointed complete
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipartially ordered set (class \emph{pcpo}) i.e. a set with a partial order
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwhich is closed w.r.t. $\omega$-chains and has a bottom. Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniformalisation, based on axiomatic type classes \cite{Wenzel}, makes it
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipossible to deal with complete partial orders in quite an abstract way.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFunctions are generally partial and computability can be expressed in terms of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicontinuity. Recursion can be expressed in terms of least fixed-point operator,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand so, in contrast with Isabelle-HOL, function definition does not depend on
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproofs. Nevertheless, proving theorems in HOLCF may turn out to be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomparatively hard. After being spared the need to discharge proof
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniobligations at the definition stage, one has to bear with assumptions on
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunction continuity throughout the proofs. A standard strategy is then to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefine as much as possible in Isabelle-HOL, using HOLCF type constructors to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilift types only when this is necessary.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAlthough there have been translations of functional languages to first-order
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisystems --- those to FOL of Miranda \cite{Thompson95,Thompson89,Thompson95b}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand Haskell \cite{Thompson92}, both based on large-step operational semantics;
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithat of Haskell to Agda implementation of Martin-Loef type theory in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\cite{Abel} --- still, higher-order logic may be quite helpful in order to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideal with features such as currying and polymorphism. Moreover, higher-order
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniapproaches may rely on denotational semantics --- as for examples, \cite{Huff}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslating Haskell to HOLCF, and \cite{Pollack} translating ML to HOL ---
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniallowing for program representation closer to specification as well as for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproofs comparatively more abstract and general.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe translation of Haskell to HOLCF proposed in \cite{Huff} uses deep
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniembedding to deal with types. Haskell types are translated to terms, relying
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinion a domain-theoretic modelling of the type system at the object level,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniallowing explicitly for a clear semantics, and providing for an implementation
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithat can capture most features, including type constructor classes. In
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicontrast, we provide in the case of HOLCF with a translation that follows the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilines of a denotational semantics under the assumption that type constructors
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand type application in Haskell can be mapped to corresponding constructors
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand built-in application in Isabelle without loss from the point of view of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibehavioural equivalence between programs --- in particular, translating
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell datatypes to Isabelle ones.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\section{Translations in Hets}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe Haskell-to-Isabelle translation in Hets requires GHC, Programatica,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle and AWE. The application is run by a command that takes as arguments
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinia target logic and an Haskell program, given as a GHC source file. The latter
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinigets analysed and translated, the result of a successful run being an Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitheory file in the target logic.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe Hets internal representation of Haskell is similar to that of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniProgramatica, whereas the internal representation of Isabelle is based on the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniML definition of the Isabelle base logic, extended in order to allow for a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisimpler representation of Isabelle-HOL and HOLCF. Haskell programs and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle theories are internally represented as Hets theories --- each of them
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniformed by a signature and a set of sentences, according to the theoretical
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniframework described in \cite{MossaTh}. Each translation, defined as
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicomposition of a signature translation with a translation of all sentences, is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniessentially a morphism from theories in the internal representation of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisource language to theories in the representation of the target language.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniEach translation relies on a specific Isabelle theory included in the Hets
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidistrubution --- \emph{HsHOLCF} for HOLCF and \emph{HsHOL} for HOL,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirespectively, the latter of which uses AWE.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Sublanguage definitions}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniPrograms can be regarded as theories in a language given by definitions of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype, class, type schemas (types with a context where variables are sorted by
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniclass), patterns, terms, declarations (forming the signature --- including
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunction declaration, datatype declaration, type definition, as well as class
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand method declaration) and definitions (forming the theory body --- including
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunction definition, as well as instance and method definition).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{HOLCF}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn the following, we give a definition of the sub-language of Haskell
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$H_c$ that is covered by the translation to HOLCF.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Types
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \tau \ = () \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & Integer & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & v & \mbox{type \ variable}\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \tau_1 \to \tau_2 & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (\tau_1,\tau_2) & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% & Either \ tau_1 \ tau_2 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & [\tau] & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & Maybe \ \tau & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & T \ \tau_{1} \ \ldots \tau_{n} & \mbox{either \ datatype \ or \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini defined \ type}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% & T \ \tau_{1} \ \ldots \ \tau_{n} \qquad \mbox{defined \ type}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Type classes
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini K \ = & Eq & \mbox{with \ default \ methods} \ ==, \ /= \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & K & \mbox{defined \ type \ class} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Contexts
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini ctx \ = & \{K \ v\} \ \cup \ ctx & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \{\} & \mbox{empty \ context} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Type schemas
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \phi \ = & ctx \Rightarrow \tau \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{where \ all \ variables \ in} \ ctx \ \mbox{are \ in} \ \tau
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Simple patterns
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini sp \ = & \_ & \mbox{wildcard} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & v & \mbox{variable \ of \ datatype}\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & C \ \overline{v} & \mbox{case \ of \ datatype}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Terms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll} t \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & c \in \aleph & \mbox{Integer \ constant} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{:,head,tail\} & \mbox{on list} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{Just,Nothing\} & \mbox{on \ \emph{maybe} \ types} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{fst,snd\} & \mbox{on \ pairs} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & x & \mbox{variable} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & f & \mbox{function \ symbol} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & C & \mbox{data \ constructor} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & if \ t \ then \ t_1 \ else \ t_2 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & let \ (x_1 = t_1; \ \ldots; \ x_n = t_n) \ in \ t
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Declarations
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Decl \ = & type \ T \ \overline{v} \ = \ \tau \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & data \ ctx \ \Rightarrow \ T \ \overline{v} \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ C_{1} \ \overline{x}_1 \ | \ \ldots \ | \ C_{k} \ \overline{x}_k \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% & \qquad \mbox{with} \ {\overline{x}}_1, {\overline{x}}_k \ \subseteq \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \overline{v} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ctx \ \Rightarrow \ f \ :: \ \tau \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & class \ K \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini where \ (f_{1}:: \tau_{1}; \ldots; f_{n}::\tau_{n}) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{where} \ \tau_{1}, \tau_{n} \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \mbox{have \ only \ one \ type \ variable}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Definitions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Def \ = & f \ \overline{v} \ = \ t \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & f \ \overline{v}_{1} \ sp_1 \ {\overline{w}}_{1} \ = \ t_1; \ \ldots;
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ f \ \overline{v}_{n} \ sp_n \ {\overline{w}}_{n} \ = \ t_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & instance \ ctx \Rightarrow K \ \tau \ where \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (f_1 = t_1; \ldots; \ f_n = t_n) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ methods \ of} \ K
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{HOL}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn contrast, the following gives a definition of the Haskell sub-language
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$H_s$ that is covered by the translation to HOL.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Types, Type classes, Contexts, Type schemas, Simple patterns,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \emph{as before}\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Type constructor classes
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Terms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll} t \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & c \in \aleph & \mbox{Integer \ constant} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{:,head,tail\} & \mbox{on list} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{Just,Nothing\} & \mbox{on \ Maybe} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{return,bind\} & \mbox{on \ monadic \ types} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & t \in \{fst,snd\} & \mbox{on \ pairs} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & x & \mbox{variable} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & f & \mbox{function \ symbol} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & C & \mbox{data \ constructor} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & if \ t \ then \ t_1 \ else \ t_2 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{with} \ sp_1, \ldots, sp_n \ \mbox{complete \ match} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & let \ (x_1 = t_1; \ \ldots; \ x_n = t_n) \ in \ t
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Definitions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Def \ = & f \ \overline{v} \ = \ t \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ recursive} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & f \ \overline{v}_1 \ sp_1 \ \overline{w}_1 \ = \ t_1; \ \ldots;
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ f \ \overline{v}_n \ sp_n \ \overline{w}_n \ = \ t_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ recursive} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & f_1 \ v_1::\tau \ \overline{w_1} \ = \ t_1; \ ldots; \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f_n \ v_n::\tau \ \overline{w_n} \ = \ t_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{where} \ f_1::\phi_1, \ldots, f_n::\phi_n \ \mbox{are \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini totally \ defined, \ mutually} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{primitive \ recursive \ in \ the \ first \ argument, \ and \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad 0 < i \leq n \ \mbox{there \ exists \ type
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ variable \ renaming} \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \sigma_i \ \mbox{such} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{that} \ \tau_1 = \sigma_i(\tau_i) \ \mbox{and \ all \ the \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini variables \ in} \ \phi_i \ \mbox{appear \ in} \ \tau_i \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & instance \ ctx \Rightarrow K \ \tau \ where \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (f_1 = t_1; \ldots; \ f_n = t_n) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ totally \ defined, \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini primitive \ recursive} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{methods \ of} \ K
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Translation definitions}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniWe can define recursively a translation from an Haskell program to an Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitheory along the line of theory morphisms \cite{MossaTh}. Here we can simply
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitake a translation $\omega \ :: \ L_1 \ \to \ L_2$ to be partially defined as
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinia set $\Omega$ of rules $r_{\in \Omega} :: L_1 \ \to \ L_2$ and a renaming
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunction $t$ that preserves names, up to avoidance of name clashes (in our
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicase, with Isabelle keywords), in the following sense: if $\alpha$ is a name
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(either a variable or a constant, for either a term or a type), then $\omega =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinit$; else, if there exists $r \in \Omega$ that matches $\alpha$ most closely,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$\omega(\alpha) \ =\ r(\alpha)$; else undefined. In the following we assume
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$\omega$ to be total, we ignore $t$, we write $\alpha'$ for $\omega(\alpha)$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand we write rules in relational form, such as $\alpha \ \Longrightarrow \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{HOLCF}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe translation $\omega_c \ :: \ H_c \ \to \ HOLCF$ from programs in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$H_c$ to theories in HOLCF can be defined, semi-formally, with the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifollowing set of rules.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Types
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini a & \Longrightarrow \ 'a::\{pcpo\} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini () & \Longrightarrow \ unit \ lift \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Bool & \Longrightarrow \ bool \ lift \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Integer & \Longrightarrow \ int \ lift \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \tau_{1} \to \tau_{2} & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \tau'_{1} \ \to \ \tau'_{2} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (\tau_{1},\tau_{2}) & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (\tau'_{1} * \tau'_{2}) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {[\tau]} \ & \Longrightarrow \ \tau' \ seq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Maybe \ \tau & \Longrightarrow \ \tau' \ maybe \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Classes
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Eq & \Longrightarrow \ Eq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini K & \Longrightarrow \ K'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Type schemas
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (ctx \Rightarrow \tau)'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ [(v'::s) / (v'::({K'} \cup s))] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell type variables are translated to variables of class \emph{pcpo}. Each
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype is associated to a sort in Isabelle, defined by the set of the classes of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwhich it is member. Built-in types are translated to the lifting of its
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicorresponding HOL type. The HOLCF type constructor \emph{lift} is used to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilift types to flat domains. The types of Haskell functions and product
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare translated, respectively, to HOLCF function spaces and lazy product ---
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinii.e. such that $\bot = (\bot * \bot) \neq (\bot*~'a) \neq ('a * \bot)$. Type
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniconstructors are translated to corresponding HOLCF ones (notably, parameters
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniprecede type constructors in Isabelle syntax). \emph{Maybe} is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslated to HOLCF-defined \emph{maybe} (the disjoint union of the lifted
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniunit type and the lifted domain parameter).\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Terms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini x::\tau & \Longrightarrow \ x'::\tau' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini () & \Longrightarrow \ Def \ () \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini True & \Longrightarrow \ TT \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini False & \Longrightarrow \ FF \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \&\& & \Longrightarrow \ trand \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini || & \Longrightarrow \ tror \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini not & \Longrightarrow \ neg \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini c & \Longrightarrow \ Def \ c \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ fliftbin \ t \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini negate & \Longrightarrow \ flift2 \ - \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {[]} & \Longrightarrow \ nil \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini t:ts & \Longrightarrow \ t'\#\#ts' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini head & \Longrightarrow \ HD \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini tail & \Longrightarrow \ TL \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini == & \Longrightarrow \ hEq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini /= & \Longrightarrow \ hNEq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Just & \Longrightarrow \ return \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Nothing & \Longrightarrow \ fail \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini C & \Longrightarrow \ C' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f & \Longrightarrow \ f' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \backslash \overline{x} \ \to \ t & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ LAM \ \overline{x}'. \ t' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini t_1 \ t_2 & \Longrightarrow \ t'_1 \ \cdot \ t'_2 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fst & \Longrightarrow \ cfst \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini snd & \Longrightarrow \ csnd \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini let \ (x_1 = t_1; & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \dots; & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad x_n = t_n) \quad in \ t & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ If \ t' \ then \ t'_1 \ else \ t'_2 \ fi \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini case \ x \ of \ (p_1 \to t_1; & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \ldots; & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad p_n \to t_n) & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Rightarrow t'_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \mbox{is \ a \ complete \ match} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Rightarrow t'_{n-1} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini p'_{n-1}, q_1, \ldots, q_k \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{complete \ match} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & case \ x' \ p'_{1} \Rightarrow t'_1 \ | \ \ldots \ | \ p'_n
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Rightarrow t'_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \qquad \qquad | \ q_{1} \Rightarrow \bot \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini | \ \ldots q_{k} \Rightarrow \bot \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{with} \ p'_1, \ldots, p'_{n}, q_1, \ldots, q_k \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \mbox{complete \ match}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniTerms of built-in type are translated using HOLCF-defined lifting function
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{Def}. The bottom element $\bot$ is used for undefined terms.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHOLCF-defined $flift1 :: \ ('a \Rightarrow 'b::pcpo) \Rightarrow ('a \ lift
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\to 'b)$ and $flift2 :: \ ('a \Rightarrow 'b) \Rightarrow ('a \ lift \to 'b \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilift)$ are used to lift operators, as well as the following, defined in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{HsHOLCF}.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Rightarrow ('a \ lift \to \ 'b \ lift \to \ 'c \ lift) $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$fliftbin \ f \ == \ flift1 \ (\lambda x. \ flift2 \ (f \ x))$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Boolean values are translated to values of \emph{bool lift}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(\emph{tr} in HOLCF) i.e. \emph{TT}, \emph{FF} and $\bot$, and Boolean
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniconnectives to the corresponding HOLCF operators. HOLCF-defined \emph{If then
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini else fi} and \emph{case} syntax are used to translate conditional and case
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniexpressions, respectively. There are restrictions, however, on case
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniepressions, due to limitations in the translation of patterns; in particular,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe case term has to be a variable, and only simple patterns are allowed (no
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrininested ones). On the other hand, Isabelle sensitiveness to the order of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipatterns in case expressions is dealt with. Multiple function definitions are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslated as definitions based on case expressions. In function definitions
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinias well as in case expressions, both wildcards --- not available in Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini--- and incomplete patterns --- not allowed --- are dealt with by elimination,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$\bot$ being used as default value in the latters. Only let expressions
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwithout patterns on the left are dealt with; where expressions, guarded
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniexpressions and list comprehension are not covered.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniLists are translated to the domain \emph{seq} defined in library IOA.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$domain \ 'a\ seq \ = \ nil \ | \ \#\# \ (HD :: \ 'a) \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(lazy \ TL :: \ 'a \ seq) $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Keyword \emph{lazy} ensures that $x \ \#\# \ \bot \ \neq \ \bot$,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniallowing for partial sequences as well as for infinite ones \cite{holcf}.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Declarations
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Longrightarrow \ class \ K' \ \subseteq
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ pcpo; \ Dec'_1; \ \ldots; \ Dec'_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ consts \ f' \ :: \ \phi' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ type \ \tau \ = \ \tau'_1 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad domain \ \phi'_1 \ = \ C'_{11} \ d_{111} \ x'_1 \ \ldots \ d_{11i} \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini x'_i \ | \ \ldots \ | \ C'_{1p} \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini d_{1p1} \ y'_1 \ \ldots \ d_{1pj} \ y'_j \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad and \ \ldots \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad and \ \phi'_n \ = \ C'_{n1} \ d_{n11} \ w'_1 \ \ldots \ d_{n1h} \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini w'_h \ | \ \ldots \ | \ C'_{nq} \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini d_{nq1} \ z'_1 \ \ldots \ d_{nqk} \ z'_k \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Definitions
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \overline{x}_1 \to \ t_1); \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini == \ LAM \ \overline{x}'. \ t' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (f_1 \ \overline{v_1} \ = \ t_1; \ \ldots;
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ f_n \ \overline{v_n} \ = \ t_n) \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad fixrec \ f'_1 :: \phi'_1 \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (LAM \ \overline{v_1}'. \ t'_1) \ and \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \quad \ldots \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \quad and \ f'_n :: \phi'_n \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (LAM \ \overline{v_n}'. \ t'_n) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{with} \ f_1::\phi_1, \ldots, f_n::\phi_n \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \mbox{mutually \ recursive} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad instance \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \in ctx\}, \ \ldots, \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \qquad \quad \quad
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \mbox{with \ proof \ obligation}; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad defs \ f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (ctx \Rightarrow \tau_n)' == t'_n
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFunction declarations use Isabelle keyword \emph{consts}. Datatype
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideclarations in HOLCF are domain declarations and require explicitly
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidestructors. Mutually recursive datatypes relies on specific Isabelle syntax
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(keyword \emph{and}). Order of declarations is taken care of.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniNon-recursive definitions are translated to standard definitions using
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle keyword \emph{defs}. Recursive definitions rely on HOLCF package
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{fixrec} which provides nice syntax for fixed point definitions,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniincluding mutual recursion. Lambda abstraction is translated as continuous
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniabstraction (\emph{LAM}), function application as continuous application (the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{dot} operator), equivalent to lambda abstraction ($\lambda$) and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinistandard function application, respectively, when all arguments are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniClasses in Isabelle and Haskell are built quite differently. In Haskell, a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype class is associated to a set of function declarations, and it can be
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinterpreted as the set of types where those functions are defined. In
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle, a type class has a single type parameter, it is associated to a set
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof axioms in a single type variable, and can be interpreted as the set of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitypes that satisfy those axioms.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniNot all the problems have been solved with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirespect to arities that may conflict in Isabelle, although they correspond to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicompatible Haskell instantiations. Moreover, Isabelle does neither allow for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimulti-parameter classes, nor for type constructor ones, therefore the same
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslation method cannot be applied to them.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniDefined single-parameter classes are translated to HOLCF as subclasses of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{pcpo} with empty axiomatization. Methods declarations associated with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell classes are translated to independent function declarations with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniappropriate class annotation on type variables. In Isabelle, each instance
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirequires proofs that class axioms are satisfied by the instantiating type ---
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinianyway, as long as there are no axioms proofs are trivial and proof obligation
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimay be automatically discharged. Method definitions associated with instance
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideclarations are translated to independent function definitions, using type
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniannotation and relying on Isabelle overloading.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn the internal representation of Haskell given by Programatica, function
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinioverloading is handled by means of dictionary parameters \cite{Jones93}. This
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimeans that each function has additional parameters for the classes associated
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinito its type variables. In fact, dictionary parameters are used to decide, for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinieach instantiation of the function type variables, how to instantiate the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimethods called in the function body. On the other hand, overloading in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle is obtained by adding explicitly type annotation to function
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefinitions --- dictionary parameters may thus be eliminated.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe translation of built-in classes may involve axioms --- this is the case
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifor equality. A HOLCF formalisation, based on the methods specification in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\cite{HaskellRep}, has been given as follows in \emph{HsHOLCF} (\emph{neg}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniis lifted negation).\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini heq :: & 'a \ \to \ 'a \ \to \ tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini hneq :: & 'a \ \to \ 'a \ \to \ tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$axclass \ Eq \ < \ pcpo$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$eqAx: heq \cdot p \cdot q \ = \ neg \cdot (hneq \cdot p \cdot q)$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Functions \emph{heq} and \emph{hneq} can be defined, for each
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinstantiating type, with the translation of equality and inequality,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirespectively. For each instance, a proof that the definitions satisfy
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{eqAx} needs to be given --- the translation will simply print out
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{sorry} (a form of ellipsis in Isabelle). The definition of default
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimethods for built-in types and the associated proofs can be found in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{HsHOLCF}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{HOL}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe translation $\omega_s \ :: \ H_s \ \to \ HOL$ from programs in $H_s$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinito theories in Isabelle-HOL extended with AWE can be defined with the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifollowing set of rules.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Types
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini () & \Longrightarrow \ unit \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini a & \Longrightarrow \ 'a::\{type\} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Bool & \Longrightarrow \ boolean \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Integer & \Longrightarrow \ int \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \tau_{1} \to \tau_{2} & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \tau'_{1} \ \Rightarrow \ \tau'_{2} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (\tau_{1},\tau_{2}) & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (\tau'_{1} * \tau'_{2}) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {[\tau]} \ & \Longrightarrow \ \tau' \ list \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Maybe \ \tau & \Longrightarrow \ \tau' \ option \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Classes
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Eq & \Longrightarrow \ Eq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini K & \Longrightarrow \ K'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Type schemas
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (ctx \Rightarrow \tau)'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ [(v'::s) / (v'::({K'} \cup s))] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHere we highlight the main differences the translation to HOLCF and this,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisemantically rather more approximative one to Isabelle-HOL (thereafter simply
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHOL). Function type, product and list are used to translate the corresponding
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell constructors. Option types are used to translate \emph{Maybe}. Haskell
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidatatypes are translated to HOL datatypes. Type variables are of class
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniStandard lambda-abstraction ($\lambda $) and function application are used
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinihere, instead of continuous ones. Non-recursive definitions are treated in an
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinianalogous way as in the translation to HOLCF. However, partial functions and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniparticularly case expressions with incomplete patterns are not allowed.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn HOL one has to pay attention to the distinction between \emph{primitive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini recursive} functions (introduced by the keyword \emph{primrec}) and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinigenerally recursive ones. Termination is guaranteed for each primitive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirecursive function by the fact that recursion is based on the datatype
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinistructure of one of the parameters. In contrast, termination is no trivial
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimatter for recursion in general. A strictly decreasing measure needs to be
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniassociation with the parameters. This cannot be dealt with automatically in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinigeneral. Threferore here we restrict translation to primitive recursive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniMutual primitive recursion is allowed for under additional restrictions ---
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimore precisely, given a set $F$ of functions: 1) all the functions in $F$ are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirecursive in the first argument; 2) all recursive arguments in $F$ are of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisame type modulo variable renaming; 3) each type variable occurring in the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype of a function in $F$ already occurs in the type of the first argument.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe third conditions is a way to ensure that we do not end up with type
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinivariables which occurs on the right hand-side but not on the left hand-side of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinia definition. In fact, given mutually recursive functions $f_{1}, \ldots,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinif_{n}$ of type $A \rightarrow B_{1}, \ldots, A \rightarrow B_{n}$ after
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinivariable renaming, they are translated to projections of a new function of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype $A \rightarrow (B_{1} * \ldots * B_{n})$ which is defined for cases of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniexpression $nth_n \ t$ used in the translation rule is simply an informal
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniabbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniextracts the $n$-th projection from a tuple no shorter than $n$.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Terms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini x::\tau & \Longrightarrow \ x'::\tau' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini () & \Longrightarrow \ () \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini True & \Longrightarrow \ True \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini False & \Longrightarrow \ False \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \&\& & \Longrightarrow \ \& \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini || & \Longrightarrow \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini not & \Longrightarrow \ Not \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini c & \Longrightarrow \ c \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ t \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini negate \ x & \Longrightarrow \ - x \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {[]} & \Longrightarrow \ {[]} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini t:ts & \Longrightarrow \ t'\#ts' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini head & \Longrightarrow \ hd \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini tail & \Longrightarrow \ tl \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini == & \Longrightarrow \ hEq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini /= & \Longrightarrow \ hNEq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Just & \Longrightarrow \ Some \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Nothing & \Longrightarrow \ None \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini return & \Longrightarrow \ return \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini bind & \Longrightarrow \ mbind \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini C & \Longrightarrow \ C' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f & \Longrightarrow \ f' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \backslash \overline{x} \ \to \ t & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \lambda \ \overline{x}'. \ t' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini t_1 \ t_2 & \Longrightarrow \ t'_1 \ t'_2 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fst & \Longrightarrow \ fst \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini snd & \Longrightarrow \ snd \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini let \ (x_1 = t_1; & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \dots; & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad x_n = t_n) \quad in \ t & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ if \ t' \ then \ t'_1 \ else \ t'_2 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini case \ x \ of \ (p_1 \to t_1; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \ldots; & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad p_n \to t_n) & \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Rightarrow t'_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \mbox{is \ a \ complete \ match} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Rightarrow t'_{n-1} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini p'_{n-1}, q_1, \ldots, q_k \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \qquad \mbox{complete \ match}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Declarations
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Longrightarrow \ class \ K' \ \subseteq
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ type; \ Dec'_1; \ \ldots; \ Dec'_n \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ consts \ f' \ :: \ \phi' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ type \ \tau \ = \ \tau'_1 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad datatype \ \phi'_1 \ = \ C'_{11} \ x'_1 \ \ldots \ x'_i \ | \ \ldots
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ | \ C'_{1p}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ y'_1 \ \ldots \ y'_j \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad and \ \ldots \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad and \ \phi'_n \ = \ C'_{n1} \ w'_1 \ \ldots \ w'_h \ | \ \ldots \ | \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ z'_1 \ \ldots \ z'_k \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Definitions
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \overline{x}_1 \to \ t_1); \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini == \ \lambda \ \overline{x}'. \ t' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f_1 \ \ y_1 \ \overline{x_1} \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ t_1; \ \ldots; \ f_n \ y_n \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \overline{x_n} \ = \ t_n \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad decl \ f_{new} ::
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (\sigma_1(ctx_1) \ \cup \ \ldots \ \cup \ \sigma_n(ctx_n)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \Rightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \qquad \qquad \sigma_1(\tau_{1a}) \ \to \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (\sigma_1(\tau_1), \ldots, \sigma_n(\tau_n)))' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad primrec \ f_{new} \ sp_1 \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (\lambda \ \overline{x_1}'. \ t'_1 [y'_1/sp_1], \ldots, \ \lambda \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \overline{x_n}'. t'_n [y'_n/sp_1]); \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \qquad \ldots; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \qquad
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f_{new} \ sp_k \ = \ (\lambda \ \overline{x_1}'. \ t'_1
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini [y'_1/sp_k], \ldots,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \lambda \ \overline{x_n}'. \ t'_n [y'_n/sp_k]); \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad defs \ f_1 \ x \ == \ nth_1 \ (f_{new} \ x); \ \ldots;
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ f_n \ x \ == \ nth_n \ (f_{new} \ x) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{with} \ f_1:: (ctx_1 \Rightarrow \tau_{1a} \to \tau_1),
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \ldots, \ f_n::(ctx_n \Rightarrow \tau_{na} \to \tau_n) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{mutually \ recursive} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad instance \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \in ctx\}, \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \qquad \quad \quad
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ldots, \ \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \mbox{with \ proof \ obligation}; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad defs \quad
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (ctx \Rightarrow \tau_n)' == t'_n\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini instance \ Monad \ \tau \ where \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (def_{eta}; def_{bind}) \ \Longrightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad defs \quad def'_{eta}; \ def'_{bind}; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad t\_instantiate \ Monad \ mapping \ m\_\tau' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{where} \ m_\tau' \ \mbox{is \ defined \ as \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini theory \ morphism \ associating} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \qquad \mbox{to} \ tau', \ def'_{eta}, \ def'_{bind} \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \mbox{respectively;}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniType classes are translated to subclasses of \emph{type}. An axiomatisation of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell equality for total functions can be found in \emph{HsHOL}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini heq :: & 'a \ \to \ 'a \ \to \ bool \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini hneq :: & 'a \ \to \ 'a \ \to \ bool \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$axclass \ Eq \ < \ type$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$eqAx: heq \ p \ q \ = \ Not \ (hneq \ p \ q)$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniGiven the restriction to total functions, equality on built-in types can be
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefined as HOL equality.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Semantics (for HOLCF)}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniDenotational semantics con be given as basis for the translation to HOLCF.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniEssentially, the claim here is that the expressions on the left hand-side of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe following tables represent the denotational meaning of the Haskell
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniexpressions on the right hand-side, as well as of the HOLCF expressions to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwhich they are translated. The language on the left hand-side is still based
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinion HOLCF where type have been extended with abstraction ($\Lambda$) and fixed
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipoint ($\mu$) in order to represent the denotational meaning of domain
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideclarations.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil a \rceil & = \ 'a::pcpo \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil () \rceil & = \ unit \ lift \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil Bool \rceil & = \ bool \ lift \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil Integer \rceil & = \ int \ lift \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil \to \rceil & = \ \to \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil (,) \rceil & = \ * \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil [] \rceil & = \ seq \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil Maybe \rceil & = \ maybe \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil T_1 \ T_2 \rceil & = \ \lceil T_1 \rceil \ \lceil T_2 \rceil \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \lceil TC \rceil & = & \mu X. (\Lambda \ v_1, \ldots, v_n.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \ \lceil \tau_1 \rceil + \ldots + \lceil \tau_{k} \rceil)[X/TC] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \mbox{when \ there \ is \ a \ declaration} \ data \ TC \ v_1 \ \ldots \ v_n
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \ = \ C_1::\tau_1 | \ldots |
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% C_k::\tau_k \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil TC_{i} \rceil & = \ let \ F \ = \ \mu \ (X_1*\ldots*X_k). \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \quad ((\Lambda \ v_{11}, \ldots, v_{1m}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \lceil \tau_{11} \rceil + \ldots + \lceil \tau_{1p} \rceil),
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \quad (\Lambda \ v_{k1}, \ldots, v_{kn}. \ \ldots,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ \lceil \tau_{k1} \rceil + \ldots + \lceil \tau_{kq} \rceil))
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & in \ nth_i(F) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \quad \mbox{with} \ 0 < i \leq k, & \mbox{when} \ data \ TC_1 \ v_{11} \ \ldots \ v_{1m} \ = \ C_{11}::\tau_{11}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini | \ldots | C_{1p}::\tau_{1p}; \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \quad \ldots; \ data \ TC_k \ v_{k1} \ \ldots \ v_{kn} \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ C_{k1}::\tau_{k1} | \ldots |
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini C_{kq}::\tau_{kq} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \mbox{are \ mutually \ recursive \ declarations} \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{array}$$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe representation of term denotation is similar to what we get from the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslation, except that for functions we give the representation of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimeaning of \emph{fixrec} definitions ($FIX$ is the HOLCF fixed point
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil x::a \rceil & = \ x'::\lceil a \rceil \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil c \rceil & = \ c' \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil \backslash x \ \to \ f \rceil & = \ LAM \ x_{t}. \ \lceil f \rceil \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil (a,b) \rceil & = \ (\lceil a \rceil, \lceil b \rceil) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil t_1 \ t_2 \rceil & = \ \lceil t_1 \rceil \ \cdot \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil t_2 \rceil \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & = \ let \ \lceil
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lceil f_i \rceil & = \ let \ g \ =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini FIX \ (x_1,\ldots,x_n). \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (\lceil t_1 \rceil, \ldots, \lceil t_{n} \rceil [f_1/x_1,\ldots,f_n/x_n] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & in \ nth_i (g) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \quad \mbox{with} \ 0 < i \leq n,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \mbox{where} \ f_1 = t_1, \ f_n = t_n \ \mbox{are \ mutually \ recursive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ definitions}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \ldots \lceil a_{n} \rceil \ TyCons_{t}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Monads with AWE}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniA monad is a type constructor with two operations that can be specified
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniaxiomatically --- \emph{eta} (injective) and \emph{bind} (associative, with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{eta} as left and right unit) \cite{moggi89}. Isabelle does not have
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype constructor classes, therefore monads cannot be translated directly. The
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniindirect solution that we are pursuing, is to translate monadic types as types
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithat satisfy the monadic axioms. This solution can be expressed in terms of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitheory morphisms --- maps between theories, associating signatures to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisignatures and axioms to theorems in ways that preserve operations and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniarities, entailing the definition of maps between theorems. Theory morphisms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniallow for theorems to be moved between theories by translating their proof
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniterms, making it possible to implement parametrisation at the theory level
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(see \cite{AWE} for details). A \emph{parameterised theory} $\mathit{Th}$ has
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinia sub-theory $\mathit{Th}_P$ which is the parameter --- this may contain
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniaxioms, constants and type declarations. Building a theory morphism from
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$\mathit{Th}_P$ to a theory $I$ provides the instantiation of the parameter
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwith $I$, and makes it possible to translate the proofs made in the abstract
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisetting of $\mathit{Th}$ to the concrete setting of $I$ --- the result being
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinian extension of $I$. AWE is an extension of Isabelle that can assist in the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniconstruction of theory morphisms \cite{AWE}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniA notion of monad \cite{AWE2} can be built in AWE by defining, on an abstract
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilevel, a hierarchy of theories culminating in \emph{Monad}, based on the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideclaration of a unary type constructor $M$ (in \emph{MonadType}) with the two
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimonad operations (contained in \emph{MonadOpEta} and \emph{MonadOpBind},
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirespectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinispecific type constructor forms a monad, we have to construct a theory
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimorphism from \emph{MonadAxms} to the specific theory; this involves giving
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinispecific definitions of the operators, as well as discharging proof
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniobligations associated with specific instances of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe axioms. The following gives an example. \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $data \ LS \ a \ = \ N \ | \ C \ a \ (LS \ a)$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $instance \ Monad \ LS \ where$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini return \ x & = \ C \ x \ N \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini x \ >>= \ f & = \ case \ x \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & N \ \to \ N \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & C \ a \ b \ \to \ cnc \ (f \ a) \ (b \ >>= \ f)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$cnc :: \ LS \ a \ \to \ LS \ a \ \to \ LS \ a $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicnc \ x \ y & = \ case \ x \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & N \ \to \ y \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & C \ w \ z \ \to \ cnc \ z \ (C \ w \ y)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent These definitions are plainly translated to HOL, as follows. Note
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithat these are not overloaded definitions. \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $datatype \ 'a \ LS \ = \ N \ | \ C \ 'a \ ('a \ LS)$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini return\_LS & :: \ 'a \ \Rightarrow 'a \ LS \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini mbind\_LS & :: \ 'a \ LS \ \Rightarrow \ ('a \ \Rightarrow \ 'b \ LS) \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \Rightarrow \ 'b \ LS \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini cnc & :: \ 'a \ LS \ \Rightarrow \ 'a \ LS \ \Rightarrow \ 'a \ LS \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $defs $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{l}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinireturn\_LS\_def : \ return\_LS:: \ ('a \ LS \ \Rightarrow 'a) \ == \
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \lambda x. \ C \ x \ N
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $primrec $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimbind\_LS \ N & = \ \lambda f. \ N \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimbind\_LS \ (C \ pX1 \ pX2) & = \ \lambda f. \ cnc \ (f \ pX1) \ (mbind\_LS \ pX2 \ f)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $primrec $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicnc \ N & = \ \lambda b. \ b \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicnc \ (C \ pX1 \ pX2) & = \ \lambda b. \ cnc \ pX2 \ (C \ pX1 \ b)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent In order to build up the instantiation of \textit{LS} as a monad,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinihere it is defined the morphism $m\_LS$ from \emph{MonadType} to the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinstantiating theory \emph{Tx}, by associating $M$ to $LS$.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$thymorph \ m\_LS : \ MonadType \ \longrightarrow \ Tx $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{l}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini maps \ [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini renames: \ [(MonadOpEta.eta \mapsto return\_LS),
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (MonadOpBind.bind \mapsto mbind\_LS)] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniRenaming is used in order to avoid name clashes in case of more than one
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimonads --- here again, note the difference with overloading. Morphism
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{m\_LS} is then used to instantiate the parameterised theory
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{MonadOps}.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $t\_instantiate \ MonadOps \ mapping \ m\_LS$ \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent This instantiation gives the declaration of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinstantiated methods, which may now be defined.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $defs $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{l}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniLS\_eta\_def: \ LS\_eta \ == \ return\_LS \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniLS\_bind\_def: \ LS\_bind \ == \ mbind\_LS
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent In order to construct a mapping from \emph{MonadAxms} to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicase, by straightforward simplification). The translation will print out
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{sorry} instead.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilemma \ LS\_lunit : & LS\_bind \ (LS\_eta \ x) \ t \ = \ t \ x \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilemma \ LS\_runit : & LS\_bind \ (t:: \ 'a \ LS) \ LS\_eta \ = \ t \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilemma \ LS\_assoc : & LS\_bind \ (LS\_bind \ (s:: \ 'a \ LS) \ t) \ u \ = \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & LS\_bind \ s \ (\lambda x. \ LS\_bind \ (t \ x) \ u) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilemma \ LS\_eta\_inj : & LS\_eta \ x \ = \ LS\_eta \ y \ \Longrightarrow \ x \ = \ y
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Now, the morphism from \emph{MonadAxms} to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{Tx} can be built, and then used to instantiate \emph{Monad}. This gives
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniautomatically access to the theorems proven in \emph{Monad} and, modulo
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirenaming, the monadic syntax which is defined there. \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$thymorph \ mon\_LS : \ MonadAxms \ \longrightarrow \ Tx $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini maps & [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & [(MonadOpEta.eta \ \mapsto \ Tx.LS\_eta), \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$t\_instantiate \ Monad \ mapping \ mon\_LS$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$renames: \ [ \ldots ]$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent The \emph{Monad} theory allows for the characterisation of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisingle parameter operators. In order to cover other monadic operators, a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipossibility is to build similar theories for type constructors of fixed arity.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAn approach altogether similar to the one shown for HOL could be used, in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniprinciple, for HOLCF as well.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Conclusion and future work}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe main advantage of shallow embedding is to get as much as possible out of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe automation currently available in Isabelle, especially with respect to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype checking. HOLCF in particular provides with an expressive semantics
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicovering lazy evaluation, as well as with a smart syntax --- also thanks to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe \emph{fixrec} package. The main disadvantage lies with lack of type
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniconstructor classes. Anyway, it is possible to get around the obstacle, at
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinileast partially, by relying on an axiomatic characterisation of monads and on
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinia proof-reuse strategy that actually minimises the need for interactive
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFuture work should use this framework for proving properties of Haskell
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniprograms. For monadic programs, we are also planning to use the monad-based
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidynamic Hoare and dynamic logic that already have been formalised in Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\cite{Walter05}. Our translation tool from Haskell to Isabelle is part of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHeterogeneous Tool Set Hets and can be downloaded from
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{http://www.dfki.de/sks/hets}. More details about the translations can
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibe found in \cite{Tlmm}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%This translation, due to the character of the P-logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%typing system, could be more easily carried out relying on some form
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%of universal quantification on type variables, or else further relying
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%on parametrisation.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\bibliographystyle{alpha} \bibliography{case}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{document}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{comment}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHere is a simple example. \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $ fn3 \ :: \ AC \ a \ b \to (a \to a) \to AC \ a \ b $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifn3 \ k \ f & = \ case \ k \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & Ct \ x \to Ct \ (f \ x) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & Rt \ x \ y \to Rt \ (fn4 \ x) \ y \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $ fn4 \ :: \ AC \ a \ b \to AC \ a \ b $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifn4 \ k & = \ case \ k \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & Rt \ x \ y \to Rt \ (fn3 \ x \ (\backslash z \to z)) \ y \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & Ct \ x \to Ct \ x \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent It translates to HOL as follows.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll} fn3 \ :: & ('a, 'b) \ AC \Rightarrow ('a \Rightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini 'a) \Rightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ ('a, 'b) \ AC \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fn4 \ :: & ('a, 'b) \ AC \Rightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ ('a, 'b) \ AC \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fn3\_Xfn4\_X :: & ('a, 'b) \ AC \Rightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (('a \Rightarrow 'a) \Rightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ('a, 'b) \ AC) *
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ (('a \Rightarrow 'a) \Rightarrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ ('a, 'b) \ AC) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifn3\_def : & fn3 \ == \ \lambda k \ f. \ fst \ (( fn3\_Xfn4\_X :: \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \ ('a, 'b) \ AC \Rightarrow (('a \Rightarrow 'a) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \Rightarrow ('a, 'b) \ AC) * ((unit \Rightarrow unit) \Rightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ('a, 'b) \ AC) ) \ k) \ f \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fn4\_def : & fn4 \ == \ \lambda k \ f. \ snd \ (( fn3\_Xfn4\_X :: \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ('a, 'b) \ AC \Rightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) * \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) ) \ k) \ f \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $primrec$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{lll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifn3\_Xfn4\_X & (Ct \ pX1) \ = & (\lambda f. \ Ct \ (f \ pX1), \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & \lambda f. \ Ct \ pX1) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifn3\_Xfn4\_X & (Rt \ pX1 \ pX2) & = \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (\lambda f. \ Rt \ (snd & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2, \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \lambda f. \ Rt \ (fst & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2) \\