hs2isa.tex revision 6a4b188beb6b1e3bd94867074c27995a01f529c2
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
85b227b458a885d075f3934c210c7de0cc89ccffJonathan 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
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederadvantage of Isabelle built-in type-checking. Hets
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{MossaTh,HetsUG,Hets} is an Haskell-based application designed to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersupport heterogeneous specification and the formal development of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprograms. It has an interface with Isabelle, and relies on
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederProgramatica \cite{Prog04} for parsing and static analysis of Haskell
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprograms. Programatica already includes a translation to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle/HOLCF which, in contrast to ours, is based on an object-level
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermodelling of the type system \cite{Huff}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe paper is organised as follows: Section~\ref{sec:semantics} discusses
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe semantic background of the translation, while the subsequent sections
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederare devoted to the translation of types, datatypes, classes and function
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdefinitions, respectively.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Section 2 gives some background, section 3 introduces the system, section 4
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%gives the sublanguages of Haskell that can be translated, in section 5 we
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%define the two translations.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%, in section 6 we sketch a denotational semantics
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%associated with the translation to Isabelle/HOLCF, in section 7 we show how translation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%of monads is carried out with AWE.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Semantic Background of the Translation}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\label{sec:semantics}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederWe firstly describe the subset of Haskell that we cover.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederOur translation to Isabelle/HOLCF covers at present Booleans, integers, basic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconstructors (function, product, list, \emph{maybe}), equality,
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedersingle-parameter type classes (with some limitations), \emph{case} and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{if} expressions, \emph{let} expressions without patterns, mutually
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederrecursive data-types and functions.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%It relies on existing formalisations of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan 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
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederis covered only partially; list comprension, \emph{where} expressions and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{let} with patterns are not covered; further built-in types and type
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederclasses are not covered; imports are not allowed; constructor type classes are
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedernot covered at all --- and so for monadic types beyond list and \emph{maybe}.
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von SchroederOf all these limitations, the only logically deep ones are those related to
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederclasses --- all the other ones are just a matter of implementation.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederFor the translation, we have followed the informal description of the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederoperational semantics given in the Haskell report \cite{HaskellRep}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederHowever, it should be noted that there is no denotational semantics
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederof Haskell! This also has been confirmed in the answers to a query
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthat one of the authors has sent to the Haskell mailing list.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederHence, our translation to Isabelle/HOLCF can be seen as the first
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederdenotational semantics given to a large subset of Haskell 98.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThis also means that there is no notion of correctness of this
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertranslation, because it just \emph{defines} the denotational semantics.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederOf course, an interesting question is the coincidence of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederdenotational and operational semantics. However, this is beyond the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederscope of the paper.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%The base translation to Isabelle-HOL is more limited, insofar as it covers
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan 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
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%limitation to primitive recursion. Other limitations are similar to those
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%mentioned for the translation to Isabelle/HOLCF --- with the notable exception of
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%\section{Translations in Hets}
dfe355b50888d0dea1c12713288b652741844080Jonathan 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
dfe355b50888d0dea1c12713288b652741844080Jonathan 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.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Translation of Types}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederIn Isabelle/HOL types are interpreted as sets (class \emph{type});
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederfunctions are total and may not be computable. A non-primitive
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederrecursive function may require discharging proof obligations already
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederat the stage of definition --- in fact, a specific relation has to be
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan 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
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{pcpo}) i.e. a set with a partial order which has suprema of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$\omega$-chains and has a bottom. Isabelle's formalisation, based on
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan 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
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan 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
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederstage, one has to bear with assumptions on function continuity
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthroughout the proofs. A standard strategy is then to define as much
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederas possible in Isabelle/HOL, using Isabelle/HOLCF type constructors to
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederlift types only when this is necessary.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe provision of pcpos, domains and continuous functions by
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederIsabelle/HOLCF eases the translation of Haskell types and functions a
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederlot. However, special care is needed when trying to understand the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell semantics. If one reads the section of the Haskell report
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdealing with types and classes, one could come to the conclusion that
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera function space in Haskell can be mapped to the space of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercontinuous functions in Isabelle/HOLCF --- this would correspond to a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpurely lazy language. However, Haskell is a mixed eager and lazy
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlanguage, and it provides a function $seq$ that enforces eager
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederevaluation. This function is introduced in part 6 of the Haskell
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederreport, ``Predefined Types and Classes'', in section 6.2. We quote
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder However, the provision of $seq$ has important semantic consequences,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder because it is available at every type. As a consequence, $\bot$ is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder not the same as $\lambda x \rightarrow \bot$, since $seq$ can be
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder used to distinguish them.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIn order to enforce this distinction, each function space needs to be
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlifted. The same holds for products. We define these liftings in a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspecific Isabelle theory \emph{HsHOLCF} (included in the Hets
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdistrubution) as follows:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan 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)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedertypes ('a, 'b) "-->" = "('a -> 'b) Lift" (infixr 0)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder liftedApp :: "('a --> 'b) => ('a => 'b)" ("_$$_" [999,1000] 999)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (* application *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder "liftedApp f x == case f of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Lift $ g => g $ x"
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder liftedLam :: "('a => 'b) => ('a --> 'b)" (binder "Lam " 10)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder (* abstraction *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder "liftedLam f == Lift $ (LAM x . f x)"
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederOur translation of Haskell types to Isabelle types is defined
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrecursively. It is based on a translation of names for avoidance of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedername clashes that is not specified here. We write $\alpha'$ for both
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthe recursive translation of item $\alpha$ and the renaming according
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederto the name translation. The translation of types is given by the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfollowing rules:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder a & \Longrightarrow \ 'a::\{pcpo\} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder () & \Longrightarrow \ unit \ \mbox{lift} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder Bool & \Longrightarrow \ bool \ \mbox{lift} \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Integer & \Longrightarrow \ int \ \mbox{lift} \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \tau_{1} \to \tau_{2} & \Longrightarrow
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \ \tau'_{1} \ \verb@-->@ \ \tau'_{2}) \\
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von Schroeder (\tau_{1},\tau_{2}) & \Longrightarrow
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von Schroeder \ (\tau'_{1} ~lprod~ \tau'_{2}) \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder {[\tau]} \ & \Longrightarrow \ \tau' \ llist \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederBuilt-in types are translated to the lifting of ths corresponding HOL
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertype. The Isabelle/HOLCF type constructor \emph{lift} is used to lift
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertypes to flat domains. The type constructor $llist$ is dicussed in the
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\section{Translation of Datatypes}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederAs explained in the Haskell report \cite{HaskellRep}, section 4.2.3,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthe following four Haskell declarations
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{verbatim}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder data D1 = D1 Int
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder data D2 = D2 !Int
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder newtype N = N Int
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederhave four different semantics. Indeed, the correct translation to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{verbatim}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdomain D1 = D1 (lazy D1_1::"Int \mathit{lift}")
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdomain D2 = D2 (D2_1::"Int \mathit{lift}")
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertypes S = "Int \mathit{lift}"
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpcpodef N = "{x:: Int \mathit{lift} . True}"
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent In Isabelle/HOLCF, the keyword \emph{domain} defines a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(possibly recursive) domain as solution of the corresponding domain
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederequation. The keyword \emph{lazy} ensures that the constructor $D1$
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis non-strict, i.e.\ $D1 \ \bot \ \neq \ \bot$. The keyword
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{pcpodef} can be used to define sub-pcpos of existing pcpos;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederhere, we use it just to introduce an isomorphic copy of an existing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpcpo --- this is the semantic of Haskell \emph{newtype} definitions.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Note that the constructor for N is Abs_N, the selector Rep_N.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLists are translated to the domain \emph{llist}, defined as follows
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederin our prelude theory \emph{HsHOLCF}:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$domain \ 'a\ llist \ = \ nil \ | \ \#\# \ (lazy\ HD :: \ 'a) \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(lazy \ TL :: \ 'a \ llist) $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederallowing for partial list as well as for infinite ones \cite{holcf}.\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe general scheme for translation of mutually recursive lazy Haskell
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdatatypes to Isabelle/HOLCF domains is as follows:
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} \ (lazy~d_{111} ::\ x'_1) \ \ldots \ (lazy~ d_{11i} :: \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\>\>\>$ \ \ldots \ | \ $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\>\>\>$ C'_{1p} \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (lazy~ d_{1p1} :: \ y'_1) \ \ldots \ (lazy~ d_{1pj} :: \ y'_j) $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\>$ and \ \ldots $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\>$ and \ $\>$\phi'_n \ = \ C'_{n1} \ (lazy~ d_{n11} :: \ w'_1) \ \ldots \ (lazy~ d_{n1h}~:: \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder w'_h) \ | \ $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\>\>\>$\ldots \ | $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\>\>\>$\ C'_{nq} \
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder (lazy~ d_{nq1} :: \ z'_1) \ \ldots \ (lazy~ d_{nqk} :: \ z'_k) $\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHere, the $d_{nqk}$ are the selectors.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Translation of Kinds and Type Classes}
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
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan 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 SchroederHaskell type variables are translated to variables of class
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{pcpo}. Each type is associated to a sort in Isabelle (in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell, the same concept is called ``kind''), defined by the set of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe classes of which it is member.
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\noindent Definitions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{l}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstance \ 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 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
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertypes that satisfy those axioms.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederNot all the problems have been solved with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrespect to arities that may conflict in Isabelle, although they correspond to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercompatible Haskell instantiations. Moreover, Isabelle does neither allow for
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermulti-parameter classes, nor for type constructor ones, therefore the same
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertranslation method cannot be applied to them.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDefined single-parameter classes are translated to Isabelle/HOLCF as subclasses of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{pcpo} with empty axiomatization. Methods declarations associated with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell classes are translated to independent function declarations with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederappropriate class annotation on type variables. In Isabelle, each instance
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrequires proofs that class axioms are satisfied by the instantiating type ---
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederanyway, as long as there are no axioms proofs are trivial and proof obligation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermay be automatically discharged. Method definitions associated with instance
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdeclarations are translated to independent function definitions, using type
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederannotation and relying on Isabelle overloading.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIn the internal representation of Haskell given by Programatica, function
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederoverloading is handled by means of dictionary parameters \cite{Jones93}. This
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermeans that each function has additional parameters for the classes associated
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto its type variables. In fact, dictionary parameters are used to decide, for
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedereach instantiation of the function type variables, how to instantiate the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermethods called in the function body. On the other hand, overloading in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle is obtained by adding explicitly type annotation to function
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdefinitions --- dictionary parameters may thus be eliminated.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe translation of built-in classes may involve axioms --- this is the case
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfor equality. An Isabelle/HOLCF formalisation, based on the methods specification in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{HaskellRep}, has been given as follows in \emph{HsHOLCF} (\emph{neg}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis lifted negation).\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$$\begin{array}{ll}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder heq :: & 'a \ \to \ 'a \ \to \ tr \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder hneq :: & 'a \ \to \ 'a \ \to \ tr \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$axclass \ Eq \ < \ pcpo$
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder$eqAx: heq \cdot p \cdot q \ = \ neg \cdot (hneq \cdot p \cdot q)$\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\noindent Functions \emph{heq} and \emph{hneq} can be defined, for each
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstantiating type, with the translation of equality and inequality,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrespectively. For each instance, a proof that the definitions satisfy
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{eqAx} needs to be given --- the translation will simply print out
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\emph{sorry} (a form of ellipsis in Isabelle). The definition of default
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermethods for built-in types and the associated proofs can be found in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Translation of Function Definitions and Terms}
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.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan 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))$\\
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\noindent Boolean values are translated to values of \emph{bool lift}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder(\emph{tr} in Isabelle/HOLCF) i.e. \emph{TT}, \emph{FF} and $\bot$, and Boolean
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroederconnectives to the corresponding Isabelle/HOLCF operators. Isabelle/HOLCF-defined \emph{If then
85b227b458a885d075f3934c210c7de0cc89ccffJonathan 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
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederepressions, due to limitations in the translation of patterns; in particular,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthe case term has to be a variable, and only simple patterns are allowed (no
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedernested ones). On the other hand, Isabelle sensitiveness to the order of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederpatterns in case expressions is dealt with. Multiple function definitions are
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertranslated as definitions based on case expressions. In function definitions
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederas well as in case expressions, both wildcards --- not available in Isabelle
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder--- and incomplete patterns --- not allowed --- are dealt with by elimination,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder$\bot$ being used as default value in the latters. Only let expressions
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederwithout patterns on the left are dealt with; where expressions, guarded
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederexpressions and list comprehension are not covered.
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\noindent Definitions
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \overline{x}_1 \to \ t_1); \
dfe355b50888d0dea1c12713288b652741844080Jonathan 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'
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder == \ LAM \ \overline{x}'. \ t' \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder (f_1 \ \overline{v_1} \ = \ t_1; \ \ldots;
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \ f_n \ \overline{v_n} \ = \ t_n) \ \Longrightarrow \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \qquad fixrec \ f'_1 :: \phi'_1 \ =
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \ (LAM \ \overline{v_1}'. \ t'_1) \ and \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad \quad \ldots \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \qquad \quad and \ f'_n :: \phi'_n \ =
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \ (LAM \ \overline{v_n}'. \ t'_n) \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \qquad \mbox{with} \ f_1::\phi_1, \ldots, f_n::\phi_n \
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \mbox{mutually \ recursive} \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederFunction declarations use Isabelle keyword \emph{consts}. Datatype
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederdeclarations in Isabelle/HOLCF are domain declarations and require explicitly
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederdestructors. Mutually recursive datatypes relies on specific Isabelle syntax
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder(keyword \emph{and}). Order of declarations is taken care of.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederNon-recursive definitions are translated to standard definitions using
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederIsabelle keyword \emph{defs}. Recursive definitions rely on Isabelle/HOLCF package
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{fixrec} which provides nice syntax for fixed point definitions,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederincluding mutual recursion. Lambda abstraction is translated as continuous
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederabstraction (\emph{LAM}), function application as continuous application (the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\emph{dot} operator), equivalent to lambda abstraction ($\lambda$) and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederstandard function application, respectively, when all arguments are
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Example Proofs}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Conclusion and future work}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederConcerning related work, although there have been translations of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederfunctional languages to first-order systems --- those to FOL of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederMiranda \cite{Thompson95,Thompson89,Thompson95b} and Haskell
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{Thompson92}, both based on large-step operational semantics;
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan 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
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederorder to deal with features such as currying and polymorphism.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederMoreover, higher-order approaches may rely on denotational semantics
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder--- as for examples, \cite{Huff} translating Haskell to HOLCF, and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{Pollack} translating ML to HOL --- allowing for program
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrepresentation closer to specification as well as for proofs
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercomparatively more abstract and general.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe translation of Haskell to Isabelle/HOLCF proposed in \cite{Huff} uses deep
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederembedding to deal with types. Haskell types are translated to terms, relying
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederon a domain-theoretic modelling of the type system at the object level,
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederallowing explicitly for a clear semantics, and providing for an implementation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthat can capture most features, including type constructor classes. In
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercontrast, we provide in the case of Isabelle/HOLCF with a translation that follows the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlines of a denotational semantics under the assumption that type constructors
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederand type application in Haskell can be mapped to corresponding constructors
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederand built-in application in Isabelle without loss from the point of view of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederbehavioural equivalence between programs --- in particular, translating
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell datatypes to Isabelle ones.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederOur solution gives in general less expressiveness than the deeper
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederapproach --- however, when we can get it to deal with cases of interest, it
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermight make proofs easier.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIsabelle does not allow for type constructor classes, therefore there is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederhardly a way shallow embedding of Haskell types may extend to cover them.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThis limitation is particularly acute with respect to monads and \emph{do}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedernotation. The problem is brilliantly avoided in \cite{Huff} by resorting to a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdeeper modelling of types.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%On the other hand, the main novelty in our work is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%to rely on theory morphisms and on their implementation for Isabelle in the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%package AWE \cite{AWE}, in order to deal with special cases of monadic
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder% Currently Hets provides with an extension of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%base translation to Isabelle/HOL which uses AWE and covers state monad types
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%inclusive of \emph{do} notation. Due to present limitations of AWE, this
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%solution is available only for Isabelle/HOL at the moment, although in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%principle it could work for Isabelle/HOLCF as well.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe main advantage of shallow embedding is to get as much as possible out of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe automation currently available in Isabelle, especially with respect to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertype checking. Isabelle/HOLCF in particular provides with an expressive semantics
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercovering lazy evaluation, as well as with a smart syntax --- also thanks to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe \emph{fixrec} package. The main disadvantage lies with lack of type
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconstructor classes. Anyway, it is possible to get around the obstacle, at
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederleast partially, by relying on an axiomatic characterisation of monads and on
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera proof-reuse strategy that actually minimises the need for interactive
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFuture work should use this framework for proving properties of Haskell
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprograms. For monadic programs, we are also planning to use the monad-based
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdynamic Hoare and dynamic logic that already have been formalised in Isabelle
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{Walter05}. Our translation tool from Haskell to Isabelle is part of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHeterogeneous Tool Set Hets and can be downloaded from
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{http://www.dfki.de/sks/hets}. More details about the translations can
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederbe found in \cite{Tlmm}.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder%This translation, due to the character of the P-logic
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder%typing system, could be more easily carried out relying on some form
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder%of universal quantification on type variables, or else further relying
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder%on parametrisation.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\bibliographystyle{alpha} \bibliography{case}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\subsection{HOL}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThe translation $\omega_s \ :: \ H_s \ \to \ HOL$ from programs in $H_s$
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederto theories in Isabelle/HOL extended with AWE can be defined with the
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederfollowing set of rules.\\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder$$\begin{array}{ll}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder () & \Longrightarrow \ unit \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder a & \Longrightarrow \ 'a::\{type\} \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder Bool & \Longrightarrow \ boolean \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder Integer & \Longrightarrow \ int \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \tau_{1} \to \tau_{2} & \Longrightarrow
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \ \tau'_{1} \ \Rightarrow \ \tau'_{2} \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder (\tau_{1},\tau_{2}) & \Longrightarrow
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \ (\tau'_{1} * \tau'_{2}) \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder {[\tau]} \ & \Longrightarrow \ \tau' \ list \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder Maybe \ \tau & \Longrightarrow \ \tau' \ option \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan 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'
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\noindent Type schemas
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \ (ctx \Rightarrow \tau)'
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ [(v'::s) / (v'::({K'} \cup s))] \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederHere we highlight the main differences the translation to Isabelle/HOLCF and this,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersemantically rather more approximative one to Isabelle/HOL (thereafter simply
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederHOL). Function type, product and list are used to translate the corresponding
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederHaskell constructors. Option types are used to translate \emph{Maybe}. Haskell
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederdatatypes are translated to HOL datatypes. Type variables are of class
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederStandard lambda-abstraction ($\lambda $) and function application are used
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederhere, instead of continuous ones. Non-recursive definitions are treated in an
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederanalogous way as in the translation to Isabelle/HOLCF. However, partial functions and
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederparticularly case expressions with incomplete patterns are not allowed.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederIn HOL one has to pay attention to the distinction between \emph{primitive
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder recursive} functions (introduced by the keyword \emph{primrec}) and
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedergenerally recursive ones. Termination is guaranteed for each primitive
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederMutual primitive recursion is allowed for under additional restrictions ---
6df4343f46cc159371dfa671c5943354480f4e1cJonathan 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
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroedera definition. In fact, given mutually recursive functions $f_{1}, \ldots,
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroederf_{n}$ of type $A \rightarrow B_{1}, \ldots, A \rightarrow B_{n}$ after
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroedervariable renaming, they are translated to projections of a new function of
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroedertype $A \rightarrow (B_{1} * \ldots * B_{n})$ which is defined for cases of
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder$A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederexpression $nth_n \ t$ used in the translation rule is simply an informal
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederabbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederextracts the $n$-th projection from a tuple no shorter than $n$.\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder x::\tau & \Longrightarrow \ x'::\tau' \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder () & \Longrightarrow \ () \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder True & \Longrightarrow \ True \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder False & \Longrightarrow \ False \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \&\& & \Longrightarrow \ \& \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder || & \Longrightarrow \ | \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder not & \Longrightarrow \ Not \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder c & \Longrightarrow \ c \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ t \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder negate \ x & \Longrightarrow \ - x \\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder {[]} & \Longrightarrow \ {[]} \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder t:ts & \Longrightarrow \ t'\#ts' \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder head & \Longrightarrow \ hd \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder tail & \Longrightarrow \ tl \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder == & \Longrightarrow \ hEq \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder /= & \Longrightarrow \ hNEq \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder Just & \Longrightarrow \ Some \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder Nothing & \Longrightarrow \ None \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder return & \Longrightarrow \ return \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder bind & \Longrightarrow \ mbind \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder C & \Longrightarrow \ C' \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder f & \Longrightarrow \ f' \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \backslash \overline{x} \ \to \ t & \Longrightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ \lambda \ \overline{x}'. \ t' \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder t_1 \ t_2 & \Longrightarrow \ t'_1 \ t'_2 \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder fst & \Longrightarrow \ fst \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder snd & \Longrightarrow \ snd \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder let \ (x_1 = t_1; & \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \dots; & \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad x_n = t_n) \quad in \ t & \Longrightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ if \ t' \ then \ t'_1 \ else \ t'_2 \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder case \ x \ of \ (p_1 \to t_1; \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad \ldots; & \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \qquad p_n \to t_n) & \Longrightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \Rightarrow t'_n \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \mbox{is \ a \ complete \ match} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent Declarations
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \Longrightarrow \ class \ K' \ \subseteq
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ type; \ Dec'_1; \ \ldots; \ Dec'_n \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ consts \ f' \ :: \ \phi' \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ type \ \tau \ = \ \tau'_1 \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad datatype \ \phi'_1 \ = \ C'_{11} \ x'_1 \ \ldots \ x'_i \ | \ \ldots
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ y'_1 \ \ldots \ y'_j \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad and \ \ldots \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad and \ \phi'_n \ = \ C'_{n1} \ w'_1 \ \ldots \ w'_h \ | \ \ldots \ | \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ z'_1 \ \ldots \ z'_k \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent Definitions
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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 \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \overline{x}_1 \to \ t_1); \
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder == \ \lambda \ \overline{x}'. \ t' \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder f_1 \ \ y_1 \ \overline{x_1} \ =
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \ t_1; \ \ldots; \ f_n \ y_n \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \overline{x_n} \ = \ t_n \ \Longrightarrow \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad decl \ f_{new} ::
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder (\sigma_1(ctx_1) \ \cup \ \ldots \ \cup \ \sigma_n(ctx_n)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ \Rightarrow \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \qquad \qquad \qquad \qquad \sigma_1(\tau_{1a}) \ \to \
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder (\sigma_1(\tau_1), \ldots, \sigma_n(\tau_n)))' \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad primrec \ f_{new} \ sp_1 \ =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ (\lambda \ \overline{x_1}'. \ t'_1 [y'_1/sp_1], \ldots, \ \lambda \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \overline{x_n}'. t'_n [y'_n/sp_1]); \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \qquad \qquad \ldots; \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad \qquad \qquad
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder f_{new} \ sp_k \ = \ (\lambda \ \overline{x_1}'. \ t'_1
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder [y'_1/sp_k], \ldots,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ \lambda \ \overline{x_n}'. \ t'_n [y'_n/sp_k]); \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad defs \ f_1 \ x \ == \ nth_1 \ (f_{new} \ x); \ \ldots;
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ f_n \ x \ == \ nth_n \ (f_{new} \ x) \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad \mbox{with} \ f_1:: (ctx_1 \Rightarrow \tau_{1a} \to \tau_1),
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ \ldots, \ f_n::(ctx_n \Rightarrow \tau_{na} \to \tau_n) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \mbox{mutually \ recursive} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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 \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad instance \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \qquad \qquad \quad \quad
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ldots, \ \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \qquad \mbox{with \ proof \ obligation}; \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad defs \quad
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder (ctx \Rightarrow \tau_n)' == t'_n\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder instance \ Monad \ \tau \ where \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder (def_{eta}; def_{bind}) \ \Longrightarrow \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \qquad defs \quad def'_{eta}; \ def'_{bind}; \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad t\_instantiate \ Monad \ mapping \ m\_\tau' \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad \mbox{where} \ m_\tau' \ \mbox{is \ defined \ as \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder theory \ morphism \ associating} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \qquad MonadType.M, \ MonadOpEta.eta,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \qquad \mbox{to} \ tau', \ def'_{eta}, \ def'_{bind} \
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \mbox{respectively;}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederType classes are translated to subclasses of \emph{type}. An axiomatisation of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederHaskell equality for total functions can be found in \emph{HsHOL}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder heq :: & 'a \ \to \ 'a \ \to \ bool \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder hneq :: & 'a \ \to \ 'a \ \to \ bool \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$axclass \ Eq \ < \ type$
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$eqAx: heq \ p \ q \ = \ Not \ (hneq \ p \ q)$\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederGiven the restriction to total functions, equality on built-in types can be
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederdefined as HOL equality.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Semantics (for HOLCF)}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederDenotational semantics con be given as basis for the translation to Isabelle/HOLCF.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederEssentially, the claim here is that the expressions on the left hand-side of
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe following tables represent the denotational meaning of the Haskell
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederexpressions on the right hand-side, as well as of the Isabelle/HOLCF expressions to
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederpoint ($\mu$) in order to represent the denotational meaning of domain
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \lceil a \rceil & = \ 'a::pcpo \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil () \rceil & = \ unit \ lift \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil Bool \rceil & = \ bool \ lift \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil Integer \rceil & = \ int \ lift \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil \to \rceil & = \ \to \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil (,) \rceil & = \ * \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \lceil [] \rceil & = \ seq \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan 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 |
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder% C_k::\tau_k \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \lceil TC_{i} \rceil & = \ let \ F \ = \ \mu \ (X_1*\ldots*X_k). \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \quad ((\Lambda \ v_{11}, \ldots, v_{1m}.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ \lceil \tau_{11} \rceil + \ldots + \lceil \tau_{1p} \rceil),
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder & \quad (\Lambda \ v_{k1}, \ldots, v_{kn}. \ \ldots,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder | \ldots | C_{1p}::\tau_{1p}; \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \quad \ldots; \ data \ TC_k \ v_{k1} \ \ldots \ v_{kn} \ =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ C_{k1}::\tau_{k1} | \ldots |
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder C_{kq}::\tau_{kq} \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder & \mbox{are \ mutually \ recursive \ declarations} \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von SchroederThe representation of term denotation is similar to what we get from the
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroedertranslation, except that for functions we give the representation of the
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroedermeaning of \emph{fixrec} definitions ($FIX$ is the Isabelle/HOLCF fixed point
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder$$\begin{array}{ll}
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan 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 \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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 \ =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder FIX \ (x_1,\ldots,x_n). \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder (\lceil t_1 \rceil, \ldots, \lceil t_{n} \rceil [f_1/x_1,\ldots,f_n/x_n] \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & in \ nth_i (g) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \quad \mbox{with} \ 0 < i \leq n,
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder & \mbox{where} \ f_1 = t_1, \ f_n = t_n \ \mbox{are \ mutually \ recursive
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% \ldots \lceil a_{n} \rceil \ TyCons_{t}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedertheory morphisms --- maps between theories, associating signatures to
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedersignatures and axioms to theorems in ways that preserve operations and
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederwith $I$, and makes it possible to translate the proofs made in the abstract
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan 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
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederconstruction of theory morphisms \cite{AWE}.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederA notion of monad \cite{AWE2} can be built in AWE by defining, on an abstract
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan 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
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedermorphism from \emph{MonadAxms} to the specific theory; this involves giving
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederspecific definitions of the operators, as well as discharging proof
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederobligations associated with specific instances of
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe axioms. The following gives an example. \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent $data \ LS \ a \ = \ N \ | \ C \ a \ (LS \ a)$
6df4343f46cc159371dfa671c5943354480f4e1cJonathan 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 \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & C \ a \ b \ \to \ cnc \ (f \ a) \ (b \ >>= \ f)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$cnc :: \ LS \ a \ \to \ LS \ a \ \to \ LS \ a $
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercnc \ x \ y & = \ case \ x \ of \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & N \ \to \ y \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & C \ w \ z \ \to \ cnc \ z \ (C \ w \ y)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\noindent These definitions are plainly translated to HOL, as follows. Note
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederthat these are not overloaded definitions. \\
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\noindent $datatype \ 'a \ LS \ = \ N \ | \ C \ 'a \ ('a \ LS)$
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\noindent $consts $
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder$$\begin{array}{ll}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder return\_LS & :: \ 'a \ \Rightarrow 'a \ LS \\
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder mbind\_LS & :: \ 'a \ LS \ \Rightarrow \ ('a \ \Rightarrow \ 'b \ LS) \
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder \Rightarrow \ 'b \ LS \\
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder cnc & :: \ 'a \ LS \ \Rightarrow \ 'a \ LS \ \Rightarrow \ 'a \ LS \\
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\noindent $defs $
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder$$\begin{array}{l}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederreturn\_LS\_def : \ return\_LS:: \ ('a \ LS \ \Rightarrow 'a) \ == \
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder \lambda x. \ C \ x \ N
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\noindent $primrec $
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder$$\begin{array}{ll}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroedermbind\_LS \ N & = \ \lambda f. \ N \\
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroedermbind\_LS \ (C \ pX1 \ pX2) & = \ \lambda f. \ cnc \ (f \ pX1) \ (mbind\_LS \ pX2 \ f)
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\noindent $primrec $
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder$$\begin{array}{ll}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroedercnc \ N & = \ \lambda b. \ b \\
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroedercnc \ (C \ pX1 \ pX2) & = \ \lambda b. \ cnc \ pX2 \ (C \ pX1 \ b)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\noindent In order to build up the instantiation of \textit{LS} as a monad,
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederhere it is defined the morphism $m\_LS$ from \emph{MonadType} to the
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederinstantiating theory \emph{Tx}, by associating $M$ to $LS$.\\
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder$thymorph \ m\_LS : \ MonadType \ \longrightarrow \ Tx $
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder$$\begin{array}{l}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder maps \ [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder renames: \ [(MonadOpEta.eta \mapsto return\_LS),
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder (MonadOpBind.bind \mapsto mbind\_LS)] \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan 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
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\emph{m\_LS} is then used to instantiate the parameterised theory
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\emph{MonadOps}.\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent $t\_instantiate \ MonadOps \ mapping \ m\_LS$ \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\noindent This instantiation gives the declaration of the
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroederinstantiated methods, which may now be defined.\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent $defs $
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{l}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederLS\_eta\_def: \ LS\_eta \ == \ return\_LS \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederLS\_bind\_def: \ LS\_bind \ == \ mbind\_LS
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent In order to construct a mapping from \emph{MonadAxms} to
6df4343f46cc159371dfa671c5943354480f4e1cJonathan 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
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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 \ = \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & LS\_bind \ s \ (\lambda x. \ LS\_bind \ (t \ x) \ u) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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)]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$t\_instantiate \ Monad \ mapping \ mon\_LS$\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$renames: \ [ \ldots ]$\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent The \emph{Monad} theory allows for the characterisation of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersingle parameter operators. In order to cover other monadic operators, a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederpossibility is to build similar theories for type constructors of fixed arity.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederAn approach altogether similar to the one shown for HOL could be used, in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederprinciple, for Isabelle/HOLCF as well.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederHere is a simple example. \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & Rt \ x \ y \to Rt \ (fn4 \ x) \ y \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent $ fn4 \ :: \ AC \ a \ b \to AC \ a \ b $
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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 \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent It translates to HOL as follows.\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent $consts$
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll} fn3 \ :: & ('a, 'b) \ AC \Rightarrow ('a \Rightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder 'a) \Rightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ ('a, 'b) \ AC \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder fn4 \ :: & ('a, 'b) \ AC \Rightarrow
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ ('a, 'b) \ AC \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder fn3\_Xfn4\_X :: & ('a, 'b) \ AC \Rightarrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ (('a \Rightarrow 'a) \Rightarrow \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & ('a, 'b) \ AC) *
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \ (('a \Rightarrow 'a) \Rightarrow
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ ('a, 'b) \ AC) \\
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder\noindent $defs$
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{lll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfn3\_def : & fn3 \ == \ \lambda k \ f. \ fst \ (( fn3\_Xfn4\_X :: \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \ ('a, 'b) \ AC \Rightarrow (('a \Rightarrow 'a) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & \Rightarrow ('a, 'b) \ AC) * ((unit \Rightarrow unit) \Rightarrow \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & ('a, 'b) \ AC) ) \ k) \ f \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder fn4\_def : & fn4 \ == \ \lambda k \ f. \ snd \ (( fn3\_Xfn4\_X :: \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & ('a, 'b) \ AC \Rightarrow \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) * \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) ) \ k) \ f \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\noindent $primrec$
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{lll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfn3\_Xfn4\_X & (Ct \ pX1) \ = & (\lambda f. \ Ct \ (f \ pX1), \\
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder & & \lambda f. \ Ct \ pX1) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfn3\_Xfn4\_X & (Rt \ pX1 \ pX2) & = \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & (\lambda f. \ Rt \ (snd & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2, \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \lambda f. \ Rt \ (fst & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2) \\
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von SchroederIn the following, we give a definition of the sub-language of Haskell
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder$H_c$ that is covered by the translation to Isabelle/HOLCF.\\
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder$$\begin{array}{lll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & v & \mbox{type \ variable}\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \tau_1 \to \tau_2 & \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & (\tau_1,\tau_2) & \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% & Either \ tau_1 \ tau_2 \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder & Maybe \ \tau & \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & T \ \tau_{1} \ \ldots \tau_{n} & \mbox{either \ datatype \ or \
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder defined \ type}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% & T \ \tau_{1} \ \ldots \ \tau_{n} \qquad \mbox{defined \ type}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent Type classes
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder$$\begin{array}{lll}
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder K \ = & Eq & \mbox{with \ default \ methods} \ ==, \ /= \\
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder & K & \mbox{defined \ type \ class} \\
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder\noindent Contexts
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder$$\begin{array}{lll}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder ctx \ = & \{K \ v\} \ \cup \ ctx & \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \{\} & \mbox{empty \ context} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\noindent Type schemas
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{ll}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \phi \ = & ctx \Rightarrow \tau \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan 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} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & v & \mbox{variable \ of \ datatype}\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & C \ \overline{v} & \mbox{case \ of \ datatype}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder$$\begin{array}{lll} t \ =
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & c \in \aleph & \mbox{Integer \ constant} \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder & t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & t \in \{:,head,tail\} & \mbox{on list} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder & t \in \{Just,Nothing\} & \mbox{on \ \emph{maybe} \ types} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & t \in \{fst,snd\} & \mbox{on \ pairs} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & x & \mbox{variable} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & f & \mbox{function \ symbol} \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & C & \mbox{data \ constructor} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan 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
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$$\begin{array}{ll}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder Decl \ = & type \ T \ \overline{v} \ = \ \tau \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & data \ ctx \ \Rightarrow \ T \ \overline{v} \ =
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ C_{1} \ \overline{x}_1 \ | \ \ldots \ | \ C_{k} \ \overline{x}_k \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder% & \qquad \mbox{with} \ {\overline{x}}_1, {\overline{x}}_k \ \subseteq \
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder% \overline{v} \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & ctx \ \Rightarrow \ f \ :: \ \tau \\
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder where \ (f_{1}:: \tau_{1}; \ldots; f_{n}::\tau_{n}) \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \qquad \mbox{where} \ \tau_{1}, \tau_{n} \
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan 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;
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ f \ \overline{v}_{n} \ sp_n \ {\overline{w}}_{n} \ = \ t_n \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & instance \ ctx \Rightarrow K \ \tau \ where \
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder (f_1 = t_1; \ldots; \ f_n = t_n) \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder & \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ methods \ of} \ K
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\subsection{HOL}