hs2isa.tex revision 846fb262bddd024972b6d4820762bd85ebe0f352
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\documentclass{llncs}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\documentclass[a4paper,11pt]{article}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\textwidth 15.93cm
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\textheight 24cm
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\oddsidemargin 0.0cm
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\evensidemargin 0.0cm
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\topmargin 0.0cm
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{document}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\title{Translating Haskell to Isabelle}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\author{ Paolo Torrini\inst{1} \and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Christoph Lueth\inst{2}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Christian Maeder\inst{2}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Till Mossakowski\inst{2}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\institute{Verimag, Grenoble, {\tt Paolo.Torrini@imag.fr}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\and DFKI Lab Bremen, {\tt \{Christoph.Lueth,Christian.Maeder,Till.Mossakowski\}@dfki.de} }
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder\begin{abstract}
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder We present partial translations of Haskell programs to Isabelle that have
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder been implemented as part of the Heterogenous Tool Set. The the target logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is Isabelle/HOLCF, and the translation is based on a shallow embedding
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder % The AWE package has been used to support a translation of monadic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder %operators based on theory morphisms.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Introduction}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAutomating the translation from programming languages to the languagee of a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedergeneric prover may provide useful support for the formal development and the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederverification of programs. It has been argued that functional languages can
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermake the task of proving assertions about programs written in them easier,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederowing to the relative simplicity of their semantics
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{Thompson92,Thompson95}. The idea of translating Haskell programs, came
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto us, more specifically, from an interest in the use of functional languages
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfor the specification of reactive systems. Haskell is a strongly typed, purely
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfunctional language with lazy evaluation, polymorphic types extended with type
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconstructor classes, and a syntax for side effects and pseudo-imperative code
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederbased on monadic operators \cite{HaskellRep}. Several languages based on
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell have been proposed for application to robotics \cite{phh99,Hudak2003}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIn such languages, monadic constructors are extensively used to deal with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederside-effects. Isabelle is a generic theorem-prover implemented in SML
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersupporting several logics --- in particular,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle/HOL is the implementation in Isabelle of classical higher-order logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederbased on simply typed lambda calculus extended with axiomatic type classes. It
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprovides support for reasoning about programming functions, both in terms of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrich libraries and efficient automation.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle/HOLCF \cite{holcf} \cite{Paulson94isa,holcf} is Isabelle/HOL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconservatively extended with the Logic of Computable Functions --- a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederformalisation of domain theory.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederWe have implemented as functions of Hets translations of Haskell to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle/HOLCF following an approach based on shallow embedding,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermapping Haskell types to Isabelle ones, therefore taking full advantage of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle built-in type-checking. Hets \cite{MossaTh,HetsUG,Hets} is an
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell-based application designed to support heterogeneous specification and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe formal development of programs. It has an interface with Isabelle, and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrelies on Programatica \cite{Prog04} for parsing and static analysis of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell programs. Programatica already includes a translation to Isabelle/HOLCF which,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederin contrast to ours, is based on an object-level modelling of the type system
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOur translation to Isabelle/HOLCF covers at present Booleans, integers, basic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconstructors (function, product, list, \emph{maybe}), equality,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersingle-parameter type classes (with some limitations), \emph{case} and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{if} expressions, \emph{let} expressions without patterns, mutually
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrecursive data-types and functions.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%It relies on existing formalisations of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%lazy lists and \emph{maybe}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIt keeps into account partiality and laziness by
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfollowing, for the main lines, the denotational semantics of lazy evaluation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedergiven in \cite{winskel}. There are several limitations: \emph{Predulde} syntax
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis covered only partially; list comprension, \emph{where} expressions and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{let} with patterns are not covered; further built-in types and type
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederclasses are not covered; imports are not allowed; constructor type classes are
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedernot covered at all --- and so for monadic types beyond list and \emph{maybe}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOf all these limitations, the only logically deep ones are those related to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederclasses --- all the other ones are just a matter of implementation.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%The base translation to Isabelle-HOL is more limited, insofar as it covers
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder%only total primitive recursive functions. A better semantics with respect to
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%partiality could be obtained by lifting the type of function values with
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%\emph{option}, but this has not been pursued here. Still, \emph{option} has
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%been used to translate \emph{maybe}. On the other hand, laziness appears very
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%hard to be captured with Isabelle-HOL. It also seems hard to overcome the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%limitation to primitive recursion. Other limitations are similar to those
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%mentioned for the translation to Isabelle/HOLCF --- with the notable exception of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederConcerning related work, although there have been translations of
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederfunctional languages to first-order systems --- those to FOL of
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederMiranda \cite{Thompson95,Thompson89,Thompson95b} and Haskell
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{Thompson92}, both based on large-step operational semantics;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederthat of Haskell to Agda implementation of Martin-Loef type theory in
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{Abel} --- still, higher-order logic may be quite helpful in
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederorder to deal with features such as currying and polymorphism.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederMoreover, higher-order approaches may rely on denotational semantics
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder--- as for examples, \cite{Huff} translating Haskell to HOLCF, and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{Pollack} translating ML to HOL --- allowing for program
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederrepresentation closer to specification as well as for proofs
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercomparatively more abstract and general.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe translation of Haskell to Isabelle/HOLCF proposed in \cite{Huff} uses deep
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederembedding to deal with types. Haskell types are translated to terms, relying
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederon a domain-theoretic modelling of the type system at the object level,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederallowing explicitly for a clear semantics, and providing for an implementation
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthat can capture most features, including type constructor classes. In
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercontrast, we provide in the case of Isabelle/HOLCF with a translation that follows the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederlines of a denotational semantics under the assumption that type constructors
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederand type application in Haskell can be mapped to corresponding constructors
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederand built-in application in Isabelle without loss from the point of view of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederbehavioural equivalence between programs --- in particular, translating
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederHaskell datatypes to Isabelle ones.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederOur solution gives in general less expressiveness than the deeper
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederapproach --- however, when we can get it to deal with cases of interest, it
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedermight make proofs easier.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederSection 2 gives some background, section 3 introduces the system, section 4
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedergives the sublanguages of Haskell that can be translated, in section 5 we
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederdefine the two translations.
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%, in section 6 we sketch a denotational semantics
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%associated with the translation to Isabelle/HOLCF, in section 7 we show how translation
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%of monads is carried out with AWE.
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%\section{Translations in Hets}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%The Haskell-to-Isabelle translation in Hets requires GHC, Programatica,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%Isabelle and AWE. The application is run by a command that takes as arguments
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%a target logic and an Haskell program, given as a GHC source file. The latter
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%gets analysed and translated, the result of a successful run being an Isabelle
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%theory file in the target logic.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%The Hets internal representation of Haskell is similar to that of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%Programatica, whereas the internal representation of Isabelle is based on the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%ML definition of the Isabelle base logic, extended in order to allow for a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%simpler representation of Isabelle-HOL and Isabelle/HOLCF. Haskell programs and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%Isabelle theories are internally represented as Hets theories --- each of them
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%formed by a signature and a set of sentences, according to the theoretical
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%framework described in \cite{MossaTh}. Each translation, defined as
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%composition of a signature translation with a translation of all sentences, is
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%essentially a morphism from theories in the internal representation of the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%source language to theories in the representation of the target language.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\section{Translation of Types}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederIn Isabelle/HOL types are interpreted as sets (class \emph{type});
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfunctions are total and may not be computable. A non-primitive
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrecursive function may require discharging proof obligations already
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederat the stage of definition --- in fact, a specific relation has to be
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedergiven for a function to be proved total. In Isabelle/HOLCF each type
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis interpreted as a pointed complete partially ordered set (class
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{pcpo}) i.e. a set with a partial order which has suprema of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder$\omega$-chains and has a bottom. Isabelle's formalisation, based on
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederaxiomatic type classes \cite{Wenzel}, makes it possible to deal with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercomplete partial orders in quite an abstract way. Functions are
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedergenerally partial and computability can be expressed in terms of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercontinuity. Recursion can be expressed in terms of least fixed-point
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederoperator, and so, in contrast with Isabelle/HOL, function definition
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederdoes not depend on proofs. Nevertheless, proving theorems in
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederIsabelle/HOLCF may turn out to be comparatively hard. After being
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederspared the need to discharge proof obligations at the definition
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstage, one has to bear with assumptions on function continuity
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthroughout the proofs. A standard strategy is then to define as much
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederas possible in Isabelle/HOL, using Isabelle/HOLCF type constructors to
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederlift types only when this is necessary.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOur translation is defined recursively. It is based on a translation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof names for avoidance of name clashes that is not specified here. We
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederwrite $\alpha'$ for both the recursive translation of item $\alpha$
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederand the renaming according to the name translation. The translation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof types is given by the following rules:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{ll}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder a & \Longrightarrow \ 'a::\{pcpo\} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder () & \Longrightarrow \ unit \ \mbox{lift} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Bool & \Longrightarrow \ bool \ \mbox{lift} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Integer & \Longrightarrow \ int \ \mbox{lift} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \tau_{1} \to \tau_{2} & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ \tau'_{1} \ \verb@-->@ \ \tau'_{2}) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (\tau_{1},\tau_{2}) & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ (\tau'_{1} lprod \tau'_{2}) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHere, we rely on a specific Isabelle theory \emph{HsHOLCF} included in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe Hets distrubution. It defines the lifted products and lifted
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfunction spaces as follows:
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\begin{verbatim}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdefaultsort pcpo
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdomain ('a,'b) lprod = lpair (lazy lfst :: 'a) (lazy lsnd :: 'b)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdomain 'a Lift = Lift (lazy 'a)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertypes ('a, 'b) "-->" = "('a -> 'b) Lift" (infixr 0)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder liftedApp :: "('a --> 'b) => ('a => 'b)" ("_$$_" [999,1000] 999)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder (* application *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder "liftedApp f x == case f of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Lift $ g => g $ x"
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder liftedLam :: "('a => 'b) => ('a --> 'b)" (binder "Lam " 10)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (* abstraction *)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder "liftedLam f == Lift $ (LAM x . f x)"
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder!!!!!!!!!!!!!!!!1discuss seq etc.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent Classes
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Eq & \Longrightarrow \ Eq \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder K & \Longrightarrow \ K'
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von Schroeder\noindent Type schemas
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder$$\begin{array}{ll}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \ (ctx \Rightarrow \tau)'
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \ [(v'::s) / (v'::({K'} \cup s))] \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederHaskell type variables are translated to variables of class \emph{pcpo}. Each
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertype is associated to a sort in Isabelle, defined by the set of the classes of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederwhich it is member. Built-in types are translated to the lifting of ths
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercorresponding HOL type. The Isabelle/HOLCF type constructor \emph{lift} is used to
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederlift types to flat domains.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThe types of Haskell functions and product
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederare translated, respectively, to Isabelle/HOLCF function spaces and lazy product ---
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederi.e. such that $\bot = (\bot * \bot) \neq (\bot*~'a) \neq ('a * \bot)$. Type
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederconstructors are translated to corresponding Isabelle/HOLCF ones (notably, parameters
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederprecede type constructors in Isabelle syntax). \emph{Maybe} is
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertranslated to Isabelle/HOLCF-defined \emph{maybe} (the disjoint union of the lifted
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederunit type and the lifted domain parameter).\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{ll}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder x::\tau & \Longrightarrow \ x'::\tau' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder () & \Longrightarrow \ Def \ () \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder True & \Longrightarrow \ TT \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder False & \Longrightarrow \ FF \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \&\& & \Longrightarrow \ trand \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder || & \Longrightarrow \ tror \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder not & \Longrightarrow \ neg \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder c & \Longrightarrow \ Def \ c \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ fliftbin \ t \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder negate & \Longrightarrow \ flift2 \ - \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder {[]} & \Longrightarrow \ nil \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder t:ts & \Longrightarrow \ t'\#\#ts' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder head & \Longrightarrow \ HD \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder tail & \Longrightarrow \ TL \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder == & \Longrightarrow \ hEq \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder /= & \Longrightarrow \ hNEq \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Just & \Longrightarrow \ return \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Nothing & \Longrightarrow \ fail \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder C & \Longrightarrow \ C' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder f & \Longrightarrow \ f' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \backslash \overline{x} \ \to \ t & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ LAM \ \overline{x}'. \ t' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder t_1 \ t_2 & \Longrightarrow \ t'_1 \ \cdot \ t'_2 \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder fst & \Longrightarrow \ cfst \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder snd & \Longrightarrow \ csnd \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder let \ (x_1 = t_1; & \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \dots; & \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad x_n = t_n) \quad in \ t & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ If \ t' \ then \ t'_1 \ else \ t'_2 \ fi \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder case \ x \ of \ (p_1 \to t_1; & \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \qquad \ldots; & \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \qquad p_n \to t_n) & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \Rightarrow t'_n \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \mbox{is \ a \ complete \ match} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \Rightarrow t'_{n-1} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder p'_{n-1}, q_1, \ldots, q_k \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \qquad \mbox{complete \ match} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & case \ x' \ p'_{1} \Rightarrow t'_1 \ | \ \ldots \ | \ p'_n
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \Rightarrow t'_n \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \qquad \qquad \qquad | \ q_{1} \Rightarrow \bot \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | \ \ldots q_{k} \Rightarrow \bot \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \qquad \mbox{with} \ p'_1, \ldots, p'_{n}, q_1, \ldots, q_k \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \mbox{complete \ match}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederTerms of built-in type are translated using Isabelle/HOLCF-defined lifting function
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{Def}. The bottom element $\bot$ is used for undefined terms.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle/HOLCF-defined $flift1 :: \ ('a \Rightarrow 'b::pcpo) \Rightarrow ('a \ lift
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\to 'b)$ and $flift2 :: \ ('a \Rightarrow 'b) \Rightarrow ('a \ lift \to 'b \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlift)$ are used to lift operators, as well as the following, defined in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{HsHOLCF}.\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \Rightarrow ('a \ lift \to \ 'b \ lift \to \ 'c \ lift) $
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$fliftbin \ f \ == \ flift1 \ (\lambda x. \ flift2 \ (f \ x))$\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Boolean values are translated to values of \emph{bool lift}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(\emph{tr} in Isabelle/HOLCF) i.e. \emph{TT}, \emph{FF} and $\bot$, and Boolean
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconnectives to the corresponding Isabelle/HOLCF operators. Isabelle/HOLCF-defined \emph{If then
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder else fi} and \emph{case} syntax are used to translate conditional and case
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederexpressions, respectively. There are restrictions, however, on case
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederepressions, due to limitations in the translation of patterns; in particular,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe case term has to be a variable, and only simple patterns are allowed (no
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedernested ones). On the other hand, Isabelle sensitiveness to the order of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpatterns in case expressions is dealt with. Multiple function definitions are
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertranslated as definitions based on case expressions. In function definitions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederas well as in case expressions, both wildcards --- not available in Isabelle
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder--- and incomplete patterns --- not allowed --- are dealt with by elimination,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$\bot$ being used as default value in the latters. Only let expressions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederwithout patterns on the left are dealt with; where expressions, guarded
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederexpressions and list comprehension are not covered.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLists are translated to the domain \emph{seq} defined in library IOA.\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$domain \ 'a\ seq \ = \ nil \ | \ \#\# \ (HD :: \ 'a) \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(lazy \ TL :: \ 'a \ seq) $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Keyword \emph{lazy} ensures that $x \ \#\# \ \bot \ \neq \ \bot$,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederallowing for partial sequences as well as for infinite ones \cite{holcf}.\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Declarations
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \Longrightarrow \ class \ K' \ \subseteq
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ pcpo; \ Dec'_1; \ \ldots; \ Dec'_n \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ consts \ f' \ :: \ \phi' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ type \ \tau \ = \ \tau'_1 \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad domain \ \phi'_1 \ = \ C'_{11} \ d_{111} \ x'_1 \ \ldots \ d_{11i} \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder x'_i \ | \ \ldots \ | \ C'_{1p} \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder d_{1p1} \ y'_1 \ \ldots \ d_{1pj} \ y'_j \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad and \ \ldots \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad and \ \phi'_n \ = \ C'_{n1} \ d_{n11} \ w'_1 \ \ldots \ d_{n1h} \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder w'_h \ | \ \ldots \ | \ C'_{nq} \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder d_{nq1} \ z'_1 \ \ldots \ d_{nqk} \ z'_k \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Definitions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \overline{x}_1 \to \ t_1); \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder == \ LAM \ \overline{x}'. \ t' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (f_1 \ \overline{v_1} \ = \ t_1; \ \ldots;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ f_n \ \overline{v_n} \ = \ t_n) \ \Longrightarrow \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad fixrec \ f'_1 :: \phi'_1 \ =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ (LAM \ \overline{v_1}'. \ t'_1) \ and \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \quad \ldots \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \quad and \ f'_n :: \phi'_n \ =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ (LAM \ \overline{v_n}'. \ t'_n) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \mbox{with} \ f_1::\phi_1, \ldots, f_n::\phi_n \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \mbox{mutually \ recursive} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ \Longrightarrow \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad instance \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \in ctx\}, \ \ldots, \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \qquad \qquad \quad \quad
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad \qquad \mbox{with \ proof \ obligation}; \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad defs \ f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (ctx \Rightarrow \tau_n)' == t'_n
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFunction declarations use Isabelle keyword \emph{consts}. Datatype
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdeclarations in Isabelle/HOLCF are domain declarations and require explicitly
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdestructors. Mutually recursive datatypes relies on specific Isabelle syntax
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(keyword \emph{and}). Order of declarations is taken care of.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederNon-recursive definitions are translated to standard definitions using
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle keyword \emph{defs}. Recursive definitions rely on Isabelle/HOLCF package
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{fixrec} which provides nice syntax for fixed point definitions,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederincluding mutual recursion. Lambda abstraction is translated as continuous
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederabstraction (\emph{LAM}), function application as continuous application (the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{dot} operator), equivalent to lambda abstraction ($\lambda$) and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstandard function application, respectively, when all arguments are
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederClasses in Isabelle and Haskell are built quite differently. In Haskell, a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertype class is associated to a set of function declarations, and it can be
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinterpreted as the set of types where those functions are defined. In
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle, a type class has a single type parameter, it is associated to a set
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof axioms in a single type variable, and can be interpreted as the set of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertypes that satisfy those axioms.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederNot all the problems have been solved with
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroederrespect to arities that may conflict in Isabelle, although they correspond to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercompatible Haskell instantiations. Moreover, Isabelle does neither allow for
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedermulti-parameter classes, nor for type constructor ones, therefore the same
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertranslation method cannot be applied to them.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederDefined single-parameter classes are translated to Isabelle/HOLCF as subclasses of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{pcpo} with empty axiomatization. Methods declarations associated with
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederHaskell classes are translated to independent function declarations with
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederappropriate class annotation on type variables. In Isabelle, each instance
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederrequires proofs that class axioms are satisfied by the instantiating type ---
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederanyway, as long as there are no axioms proofs are trivial and proof obligation
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedermay be automatically discharged. Method definitions associated with instance
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederdeclarations are translated to independent function definitions, using type
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederannotation and relying on Isabelle overloading.
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederIn the internal representation of Haskell given by Programatica, function
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederoverloading is handled by means of dictionary parameters \cite{Jones93}. This
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedermeans that each function has additional parameters for the classes associated
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederto its type variables. In fact, dictionary parameters are used to decide, for
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedereach instantiation of the function type variables, how to instantiate the
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedermethods called in the function body. On the other hand, overloading in
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederIsabelle is obtained by adding explicitly type annotation to function
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederdefinitions --- dictionary parameters may thus be eliminated.
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederThe translation of built-in classes may involve axioms --- this is the case
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederfor equality. An Isabelle/HOLCF formalisation, based on the methods specification in
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\cite{HaskellRep}, has been given as follows in \emph{HsHOLCF} (\emph{neg}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederis lifted negation).\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder heq :: & 'a \ \to \ 'a \ \to \ tr \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder hneq :: & 'a \ \to \ 'a \ \to \ tr \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder$axclass \ Eq \ < \ pcpo$
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder$eqAx: heq \cdot p \cdot q \ = \ neg \cdot (hneq \cdot p \cdot q)$\\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\noindent Functions \emph{heq} and \emph{hneq} can be defined, for each
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederinstantiating type, with the translation of equality and inequality,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederrespectively. For each instance, a proof that the definitions satisfy
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{eqAx} needs to be given --- the translation will simply print out
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{sorry} (a form of ellipsis in Isabelle). The definition of default
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedermethods for built-in types and the associated proofs can be found in
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\subsection{HOL}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThe translation $\omega_s \ :: \ H_s \ \to \ HOL$ from programs in $H_s$
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederto theories in Isabelle/HOL extended with AWE can be defined with the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederfollowing set of rules.\\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder$$\begin{array}{ll}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder () & \Longrightarrow \ unit \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder a & \Longrightarrow \ 'a::\{type\} \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Bool & \Longrightarrow \ boolean \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Integer & \Longrightarrow \ int \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \tau_{1} \to \tau_{2} & \Longrightarrow
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \ \tau'_{1} \ \Rightarrow \ \tau'_{2} \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder (\tau_{1},\tau_{2}) & \Longrightarrow
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \ (\tau'_{1} * \tau'_{2}) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder {[\tau]} \ & \Longrightarrow \ \tau' \ list \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Maybe \ \tau & \Longrightarrow \ \tau' \ option \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Classes
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{ll}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Eq & \Longrightarrow \ Eq \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder K & \Longrightarrow \ K'
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Type schemas
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder$$\begin{array}{ll}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ (ctx \Rightarrow \tau)'
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ [(v'::s) / (v'::({K'} \cup s))] \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHere we highlight the main differences the translation to Isabelle/HOLCF and this,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersemantically rather more approximative one to Isabelle/HOL (thereafter simply
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHOL). Function type, product and list are used to translate the corresponding
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell constructors. Option types are used to translate \emph{Maybe}. Haskell
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdatatypes are translated to HOL datatypes. Type variables are of class
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederStandard lambda-abstraction ($\lambda $) and function application are used
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederhere, instead of continuous ones. Non-recursive definitions are treated in an
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederanalogous way as in the translation to Isabelle/HOLCF. However, partial functions and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederparticularly case expressions with incomplete patterns are not allowed.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIn HOL one has to pay attention to the distinction between \emph{primitive
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder recursive} functions (introduced by the keyword \emph{primrec}) and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedergenerally recursive ones. Termination is guaranteed for each primitive
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrecursive function by the fact that recursion is based on the datatype
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstructure of one of the parameters. In contrast, termination is no trivial
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermatter for recursion in general. A strictly decreasing measure needs to be
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederassociation with the parameters. This cannot be dealt with automatically in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedergeneral. Threferore here we restrict translation to primitive recursive
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederMutual primitive recursion is allowed for under additional restrictions ---
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermore precisely, given a set $F$ of functions: 1) all the functions in $F$ are
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrecursive in the first argument; 2) all recursive arguments in $F$ are of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersame type modulo variable renaming; 3) each type variable occurring in the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertype of a function in $F$ already occurs in the type of the first argument.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe third conditions is a way to ensure that we do not end up with type
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedervariables which occurs on the right hand-side but not on the left hand-side of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera definition. In fact, given mutually recursive functions $f_{1}, \ldots,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederf_{n}$ of type $A \rightarrow B_{1}, \ldots, A \rightarrow B_{n}$ after
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedervariable renaming, they are translated to projections of a new function of
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedertype $A \rightarrow (B_{1} * \ldots * B_{n})$ which is defined for cases of
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder$A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederexpression $nth_n \ t$ used in the translation rule is simply an informal
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederabbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederextracts the $n$-th projection from a tuple no shorter than $n$.\\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder$$\begin{array}{ll}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder x::\tau & \Longrightarrow \ x'::\tau' \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder () & \Longrightarrow \ () \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder True & \Longrightarrow \ True \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder False & \Longrightarrow \ False \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \&\& & \Longrightarrow \ \& \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder || & \Longrightarrow \ | \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder not & \Longrightarrow \ Not \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder c & \Longrightarrow \ c \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ t \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder negate \ x & \Longrightarrow \ - x \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder {[]} & \Longrightarrow \ {[]} \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder t:ts & \Longrightarrow \ t'\#ts' \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder head & \Longrightarrow \ hd \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder tail & \Longrightarrow \ tl \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder == & \Longrightarrow \ hEq \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder /= & \Longrightarrow \ hNEq \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder Just & \Longrightarrow \ Some \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder Nothing & \Longrightarrow \ None \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder return & \Longrightarrow \ return \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder bind & \Longrightarrow \ mbind \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder C & \Longrightarrow \ C' \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder f & \Longrightarrow \ f' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \backslash \overline{x} \ \to \ t & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ \lambda \ \overline{x}'. \ t' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder t_1 \ t_2 & \Longrightarrow \ t'_1 \ t'_2 \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder fst & \Longrightarrow \ fst \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder snd & \Longrightarrow \ snd \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder let \ (x_1 = t_1; & \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \qquad \dots; & \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad x_n = t_n) \quad in \ t & \Longrightarrow
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ if \ t' \ then \ t'_1 \ else \ t'_2 \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder case \ x \ of \ (p_1 \to t_1; \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder \qquad \qquad \ldots; & \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder \qquad \qquad p_n \to t_n) & \Longrightarrow
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \Rightarrow t'_n \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder \mbox{is \ a \ complete \ match} \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder & case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \Rightarrow t'_{n-1} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder p'_{n-1}, q_1, \ldots, q_k \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & \qquad \mbox{complete \ match}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent Declarations
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \Longrightarrow \ class \ K' \ \subseteq
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ type; \ Dec'_1; \ \ldots; \ Dec'_n \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ consts \ f' \ :: \ \phi' \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ type \ \tau \ = \ \tau'_1 \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \qquad datatype \ \phi'_1 \ = \ C'_{11} \ x'_1 \ \ldots \ x'_i \ | \ \ldots
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ y'_1 \ \ldots \ y'_j \\
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder \qquad and \ \ldots \\
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder \qquad and \ \phi'_n \ = \ C'_{n1} \ w'_1 \ \ldots \ w'_h \ | \ \ldots \ | \
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder \ z'_1 \ \ldots \ z'_k \\
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder \qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Definitions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \overline{x}_1 \to \ t_1); \
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder == \ \lambda \ \overline{x}'. \ t' \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder f_1 \ \ y_1 \ \overline{x_1} \ =
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder \ t_1; \ \ldots; \ f_n \ y_n \
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \overline{x_n} \ = \ t_n \ \Longrightarrow \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \qquad decl \ f_{new} ::
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (\sigma_1(ctx_1) \ \cup \ \ldots \ \cup \ \sigma_n(ctx_n)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ \Rightarrow \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \qquad \qquad \sigma_1(\tau_{1a}) \ \to \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (\sigma_1(\tau_1), \ldots, \sigma_n(\tau_n)))' \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad primrec \ f_{new} \ sp_1 \ =
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ (\lambda \ \overline{x_1}'. \ t'_1 [y'_1/sp_1], \ldots, \ \lambda \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \overline{x_n}'. t'_n [y'_n/sp_1]); \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \qquad \qquad \ldots; \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \qquad
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder f_{new} \ sp_k \ = \ (\lambda \ \overline{x_1}'. \ t'_1
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder [y'_1/sp_k], \ldots,
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ \lambda \ \overline{x_n}'. \ t'_n [y'_n/sp_k]); \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad defs \ f_1 \ x \ == \ nth_1 \ (f_{new} \ x); \ \ldots;
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ f_n \ x \ == \ nth_n \ (f_{new} \ x) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \mbox{with} \ f_1:: (ctx_1 \Rightarrow \tau_{1a} \to \tau_1),
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ \ldots, \ f_n::(ctx_n \Rightarrow \tau_{na} \to \tau_n) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \mbox{mutually \ recursive} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ \Longrightarrow \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad instance \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \qquad \quad \quad
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ldots, \ \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \mbox{with \ proof \ obligation}; \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad defs \quad
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (ctx \Rightarrow \tau_n)' == t'_n\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder instance \ Monad \ \tau \ where \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (def_{eta}; def_{bind}) \ \Longrightarrow \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad defs \quad def'_{eta}; \ def'_{bind}; \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad t\_instantiate \ Monad \ mapping \ m\_\tau' \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \mbox{where} \ m_\tau' \ \mbox{is \ defined \ as \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder theory \ morphism \ associating} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad MonadType.M, \ MonadOpEta.eta,
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \mbox{to} \ tau', \ def'_{eta}, \ def'_{bind} \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \mbox{respectively;}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederType classes are translated to subclasses of \emph{type}. An axiomatisation of
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederHaskell equality for total functions can be found in \emph{HsHOL}.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{ll}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder heq :: & 'a \ \to \ 'a \ \to \ bool \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder hneq :: & 'a \ \to \ 'a \ \to \ bool \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$axclass \ Eq \ < \ type$
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$eqAx: heq \ p \ q \ = \ Not \ (hneq \ p \ q)$\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederGiven the restriction to total functions, equality on built-in types can be
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederdefined as HOL equality.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\section{Semantics (for HOLCF)}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederDenotational semantics con be given as basis for the translation to Isabelle/HOLCF.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederEssentially, the claim here is that the expressions on the left hand-side of
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederthe following tables represent the denotational meaning of the Haskell
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederexpressions on the right hand-side, as well as of the Isabelle/HOLCF expressions to
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederwhich they are translated. The language on the left hand-side is still based
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederon Isabelle/HOLCF where type have been extended with abstraction ($\Lambda$) and fixed
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederpoint ($\mu$) in order to represent the denotational meaning of domain
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil a \rceil & = \ 'a::pcpo \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil () \rceil & = \ unit \ lift \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil Bool \rceil & = \ bool \ lift \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \lceil Integer \rceil & = \ int \ lift \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil \to \rceil & = \ \to \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil (,) \rceil & = \ * \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil [] \rceil & = \ seq \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil Maybe \rceil & = \ maybe \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \lceil T_1 \ T_2 \rceil & = \ \lceil T_1 \rceil \ \lceil T_2 \rceil \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder% \lceil TC \rceil & = & \mu X. (\Lambda \ v_1, \ldots, v_n.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% \ \lceil \tau_1 \rceil + \ldots + \lceil \tau_{k} \rceil)[X/TC] \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% \mbox{when \ there \ is \ a \ declaration} \ data \ TC \ v_1 \ \ldots \ v_n
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% \ = \ C_1::\tau_1 | \ldots |
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% C_k::\tau_k \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \lceil TC_{i} \rceil & = \ let \ F \ = \ \mu \ (X_1*\ldots*X_k). \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \quad ((\Lambda \ v_{11}, \ldots, v_{1m}.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ \lceil \tau_{11} \rceil + \ldots + \lceil \tau_{1p} \rceil),
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \quad (\Lambda \ v_{k1}, \ldots, v_{kn}. \ \ldots,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ \lceil \tau_{k1} \rceil + \ldots + \lceil \tau_{kq} \rceil))
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & in \ nth_i(F) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \quad \mbox{with} \ 0 < i \leq k, & \mbox{when} \ data \ TC_1 \ v_{11} \ \ldots \ v_{1m} \ = \ C_{11}::\tau_{11}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder | \ldots | C_{1p}::\tau_{1p}; \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \quad \ldots; \ data \ TC_k \ v_{k1} \ \ldots \ v_{kn} \ =
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ C_{k1}::\tau_{k1} | \ldots |
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder C_{kq}::\tau_{kq} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \mbox{are \ mutually \ recursive \ declarations} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe representation of term denotation is similar to what we get from the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedertranslation, except that for functions we give the representation of the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedermeaning of \emph{fixrec} definitions ($FIX$ is the Isabelle/HOLCF fixed point
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil x::a \rceil & = \ x'::\lceil a \rceil \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil c \rceil & = \ c' \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil \backslash x \ \to \ f \rceil & = \ LAM \ x_{t}. \ \lceil f \rceil \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \lceil (a,b) \rceil & = \ (\lceil a \rceil, \lceil b \rceil) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil t_1 \ t_2 \rceil & = \ \lceil t_1 \rceil \ \cdot \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil t_2 \rceil \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & = \ let \ \lceil
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil f_i \rceil & = \ let \ g \ =
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder FIX \ (x_1,\ldots,x_n). \
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (\lceil t_1 \rceil, \ldots, \lceil t_{n} \rceil [f_1/x_1,\ldots,f_n/x_n] \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & in \ nth_i (g) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \quad \mbox{with} \ 0 < i \leq n,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \mbox{where} \ f_1 = t_1, \ f_n = t_n \ \mbox{are \ mutually \ recursive
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder% \ldots \lceil a_{n} \rceil \ TyCons_{t}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Monads with AWE}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederA monad is a type constructor with two operations that can be specified
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederaxiomatically --- \emph{eta} (injective) and \emph{bind} (associative, with
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\emph{eta} as left and right unit) \cite{moggi89}. Isabelle does not have
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedertype constructor classes, therefore monads cannot be translated directly. The
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederindirect solution that we are pursuing, is to translate monadic types as types
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthat satisfy the monadic axioms. This solution can be expressed in terms of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedertheory morphisms --- maps between theories, associating signatures to
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersignatures and axioms to theorems in ways that preserve operations and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederarities, entailing the definition of maps between theorems. Theory morphisms
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederallow for theorems to be moved between theories by translating their proof
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederterms, making it possible to implement parametrisation at the theory level
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder(see \cite{AWE} for details). A \emph{parameterised theory} $\mathit{Th}$ has
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedera sub-theory $\mathit{Th}_P$ which is the parameter --- this may contain
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederaxioms, constants and type declarations. Building a theory morphism from
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$\mathit{Th}_P$ to a theory $I$ provides the instantiation of the parameter
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederwith $I$, and makes it possible to translate the proofs made in the abstract
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedersetting of $\mathit{Th}$ to the concrete setting of $I$ --- the result being
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederan extension of $I$. AWE is an extension of Isabelle that can assist in the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederconstruction of theory morphisms \cite{AWE}.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederA notion of monad \cite{AWE2} can be built in AWE by defining, on an abstract
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlevel, a hierarchy of theories culminating in \emph{Monad}, based on the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdeclaration of a unary type constructor $M$ (in \emph{MonadType}) with the two
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedermonad operations (contained in \emph{MonadOpEta} and \emph{MonadOpBind},
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederrespectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederspecific type constructor forms a monad, we have to construct a theory
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroedermorphism from \emph{MonadAxms} to the specific theory; this involves giving
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederspecific definitions of the operators, as well as discharging proof
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederobligations associated with specific instances of
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederthe axioms. The following gives an example. \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $data \ LS \ a \ = \ N \ | \ C \ a \ (LS \ a)$
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\noindent $instance \ Monad \ LS \ where$
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder return \ x & = \ C \ x \ N \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder x \ >>= \ f & = \ case \ x \ of \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & N \ \to \ N \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder & C \ a \ b \ \to \ cnc \ (f \ a) \ (b \ >>= \ f)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$cnc :: \ LS \ a \ \to \ LS \ a \ \to \ LS \ a $
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercnc \ x \ y & = \ case \ x \ of \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & N \ \to \ y \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & C \ w \ z \ \to \ cnc \ z \ (C \ w \ y)
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder\noindent These definitions are plainly translated to HOL, as follows. Note
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroederthat these are not overloaded definitions. \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder\noindent $datatype \ 'a \ LS \ = \ N \ | \ C \ 'a \ ('a \ LS)$
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder\noindent $consts $
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder$$\begin{array}{ll}
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder return\_LS & :: \ 'a \ \Rightarrow 'a \ LS \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder mbind\_LS & :: \ 'a \ LS \ \Rightarrow \ ('a \ \Rightarrow \ 'b \ LS) \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \Rightarrow \ 'b \ LS \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder cnc & :: \ 'a \ LS \ \Rightarrow \ 'a \ LS \ \Rightarrow \ 'a \ LS \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $defs $
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{l}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederreturn\_LS\_def : \ return\_LS:: \ ('a \ LS \ \Rightarrow 'a) \ == \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lambda x. \ C \ x \ N
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $primrec $
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroedermbind\_LS \ N & = \ \lambda f. \ N \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroedermbind\_LS \ (C \ pX1 \ pX2) & = \ \lambda f. \ cnc \ (f \ pX1) \ (mbind\_LS \ pX2 \ f)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $primrec $
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder$$\begin{array}{ll}
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroedercnc \ N & = \ \lambda b. \ b \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercnc \ (C \ pX1 \ pX2) & = \ \lambda b. \ cnc \ pX2 \ (C \ pX1 \ b)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent In order to build up the instantiation of \textit{LS} as a monad,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederhere it is defined the morphism $m\_LS$ from \emph{MonadType} to the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederinstantiating theory \emph{Tx}, by associating $M$ to $LS$.\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$thymorph \ m\_LS : \ MonadType \ \longrightarrow \ Tx $
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{l}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder maps \ [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder renames: \ [(MonadOpEta.eta \mapsto return\_LS),
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder (MonadOpBind.bind \mapsto mbind\_LS)] \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederRenaming is used in order to avoid name clashes in case of more than one
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedermonads --- here again, note the difference with overloading. Morphism
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\emph{m\_LS} is then used to instantiate the parameterised theory
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\emph{MonadOps}.\\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\noindent $t\_instantiate \ MonadOps \ mapping \ m\_LS$ \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\noindent This instantiation gives the declaration of the
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederinstantiated methods, which may now be defined.\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $defs $
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{l}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederLS\_eta\_def: \ LS\_eta \ == \ return\_LS \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederLS\_bind\_def: \ LS\_bind \ == \ mbind\_LS
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent In order to construct a mapping from \emph{MonadAxms} to
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedercase, by straightforward simplification). The translation will print out
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\emph{sorry} instead.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlemma \ LS\_lunit : & LS\_bind \ (LS\_eta \ x) \ t \ = \ t \ x \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlemma \ LS\_runit : & LS\_bind \ (t:: \ 'a \ LS) \ LS\_eta \ = \ t \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlemma \ LS\_assoc : & LS\_bind \ (LS\_bind \ (s:: \ 'a \ LS) \ t) \ u \ = \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & LS\_bind \ s \ (\lambda x. \ LS\_bind \ (t \ x) \ u) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederlemma \ LS\_eta\_inj : & LS\_eta \ x \ = \ LS\_eta \ y \ \Longrightarrow \ x \ = \ y
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent Now, the morphism from \emph{MonadAxms} to
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\emph{Tx} can be built, and then used to instantiate \emph{Monad}. This gives
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederautomatically access to the theorems proven in \emph{Monad} and, modulo
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederrenaming, the monadic syntax which is defined there. \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$thymorph \ mon\_LS : \ MonadAxms \ \longrightarrow \ Tx $
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder maps & [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & [(MonadOpEta.eta \ \mapsto \ Tx.LS\_eta), \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & (MonadOpBind.bind \ \mapsto \ Tx.LS\_bind)]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$t\_instantiate \ Monad \ mapping \ mon\_LS$\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$renames: \ [ \ldots ]$\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent The \emph{Monad} theory allows for the characterisation of
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedersingle parameter operators. In order to cover other monadic operators, a
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederpossibility is to build similar theories for type constructors of fixed arity.
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von SchroederAn approach altogether similar to the one shown for HOL could be used, in
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederprinciple, for Isabelle/HOLCF as well.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\section{Conclusion and future work}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederIsabelle does not allow for type constructor classes, therefore there is
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederhardly a way shallow embedding of Haskell types may extend to cover them.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThis limitation is particularly acute with respect to monads and \emph{do}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedernotation. The problem is brilliantly avoided in \cite{Huff} by resorting to a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederdeeper modelling of types.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%On the other hand, the main novelty in our work is
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%to rely on theory morphisms and on their implementation for Isabelle in the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%package AWE \cite{AWE}, in order to deal with special cases of monadic
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% Currently Hets provides with an extension of the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%base translation to Isabelle/HOL which uses AWE and covers state monad types
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%inclusive of \emph{do} notation. Due to present limitations of AWE, this
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%solution is available only for Isabelle/HOL at the moment, although in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%principle it could work for Isabelle/HOLCF as well.
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von SchroederThe main advantage of shallow embedding is to get as much as possible out of
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederthe automation currently available in Isabelle, especially with respect to
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedertype checking. Isabelle/HOLCF in particular provides with an expressive semantics
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedercovering lazy evaluation, as well as with a smart syntax --- also thanks to
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederthe \emph{fixrec} package. The main disadvantage lies with lack of type
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederconstructor classes. Anyway, it is possible to get around the obstacle, at
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederleast partially, by relying on an axiomatic characterisation of monads and on
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedera proof-reuse strategy that actually minimises the need for interactive
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederFuture work should use this framework for proving properties of Haskell
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederprograms. For monadic programs, we are also planning to use the monad-based
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdynamic Hoare and dynamic logic that already have been formalised in Isabelle
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\cite{Walter05}. Our translation tool from Haskell to Isabelle is part of the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederHeterogeneous Tool Set Hets and can be downloaded from
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\texttt{http://www.dfki.de/sks/hets}. More details about the translations can
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederbe found in \cite{Tlmm}.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%This translation, due to the character of the P-logic
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder%typing system, could be more easily carried out relying on some form
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%of universal quantification on type variables, or else further relying
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%on parametrisation.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\bibliographystyle{alpha} \bibliography{case}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederHere is a simple example. \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $ fn3 \ :: \ AC \ a \ b \to (a \to a) \to AC \ a \ b $
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfn3 \ k \ f & = \ case \ k \ of \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & Ct \ x \to Ct \ (f \ x) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & Rt \ x \ y \to Rt \ (fn4 \ x) \ y \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent $ fn4 \ :: \ AC \ a \ b \to AC \ a \ b $
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{ll}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederfn4 \ k & = \ case \ k \ of \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & Rt \ x \ y \to Rt \ (fn3 \ x \ (\backslash z \to z)) \ y \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & Ct \ x \to Ct \ x \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent It translates to HOL as follows.\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent $consts$
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{ll} fn3 \ :: & ('a, 'b) \ AC \Rightarrow ('a \Rightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder 'a) \Rightarrow
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ ('a, 'b) \ AC \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder fn4 \ :: & ('a, 'b) \ AC \Rightarrow
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ ('a, 'b) \ AC \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder fn3\_Xfn4\_X :: & ('a, 'b) \ AC \Rightarrow
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder \ (('a \Rightarrow 'a) \Rightarrow \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & ('a, 'b) \ AC) *
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ (('a \Rightarrow 'a) \Rightarrow
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ ('a, 'b) \ AC) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $defs$
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{lll}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederfn3\_def : & fn3 \ == \ \lambda k \ f. \ fst \ (( fn3\_Xfn4\_X :: \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \ ('a, 'b) \ AC \Rightarrow (('a \Rightarrow 'a) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \Rightarrow ('a, 'b) \ AC) * ((unit \Rightarrow unit) \Rightarrow \\
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder & ('a, 'b) \ AC) ) \ k) \ f \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder fn4\_def : & fn4 \ == \ \lambda k \ f. \ snd \ (( fn3\_Xfn4\_X :: \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & ('a, 'b) \ AC \Rightarrow \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) * \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) ) \ k) \ f \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $primrec$
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{lll}
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederfn3\_Xfn4\_X & (Ct \ pX1) \ = & (\lambda f. \ Ct \ (f \ pX1), \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder & & \lambda f. \ Ct \ pX1) \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfn3\_Xfn4\_X & (Rt \ pX1 \ pX2) & = \\
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder & (\lambda f. \ Rt \ (snd & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2, \\
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder & \lambda f. \ Rt \ (fst & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2) \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederIn the following, we give a definition of the sub-language of Haskell
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$H_c$ that is covered by the translation to Isabelle/HOLCF.\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{lll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & v & \mbox{type \ variable}\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & \tau_1 \to \tau_2 & \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & (\tau_1,\tau_2) & \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% & Either \ tau_1 \ tau_2 \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & Maybe \ \tau & \\
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder & T \ \tau_{1} \ \ldots \tau_{n} & \mbox{either \ datatype \ or \
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder defined \ type}
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder% & T \ \tau_{1} \ \ldots \ \tau_{n} \qquad \mbox{defined \ type}
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder\noindent Type classes
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{lll}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder K \ = & Eq & \mbox{with \ default \ methods} \ ==, \ /= \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & K & \mbox{defined \ type \ class} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent Contexts
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{lll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder ctx \ = & \{K \ v\} \ \cup \ ctx & \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \{\} & \mbox{empty \ context} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent Type schemas
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \phi \ = & ctx \Rightarrow \tau \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \qquad \mbox{where \ all \ variables \ in} \ ctx \ \mbox{are \ in} \ \tau
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent Simple patterns
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{lll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder sp \ = & \_ & \mbox{wildcard} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & v & \mbox{variable \ of \ datatype}\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & C \ \overline{v} & \mbox{case \ of \ datatype}
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder$$\begin{array}{lll} t \ =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & c \in \aleph & \mbox{Integer \ constant} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & t \in \{:,head,tail\} & \mbox{on list} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & t \in \{Just,Nothing\} & \mbox{on \ \emph{maybe} \ types} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & t \in \{fst,snd\} & \mbox{on \ pairs} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & x & \mbox{variable} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & f & \mbox{function \ symbol} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & C & \mbox{data \ constructor} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & if \ t \ then \ t_1 \ else \ t_2 \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & let \ (x_1 = t_1; \ \ldots; \ x_n = t_n) \ in \ t
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent Declarations
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder Decl \ = & type \ T \ \overline{v} \ = \ \tau \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder & data \ ctx \ \Rightarrow \ T \ \overline{v} \ =
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ C_{1} \ \overline{x}_1 \ | \ \ldots \ | \ C_{k} \ \overline{x}_k \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder% & \qquad \mbox{with} \ {\overline{x}}_1, {\overline{x}}_k \ \subseteq \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% \overline{v} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & ctx \ \Rightarrow \ f \ :: \ \tau \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder where \ (f_{1}:: \tau_{1}; \ldots; f_{n}::\tau_{n}) \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \qquad \mbox{where} \ \tau_{1}, \tau_{n} \
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \mbox{have \ only \ one \ type \ variable}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent Definitions
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder Def \ = & f \ \overline{v} \ = \ t \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & f \ \overline{v}_{1} \ sp_1 \ {\overline{w}}_{1} \ = \ t_1; \ \ldots;
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder \ f \ \overline{v}_{n} \ sp_n \ {\overline{w}}_{n} \ = \ t_n \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & instance \ ctx \Rightarrow K \ \tau \ where \
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (f_1 = t_1; \ldots; \ f_n = t_n) \\