24   We present partial translations of Haskell programs to Isabelle that have
25   been implemented as part of the Heterogeneous Tool Set. The the target logic
28   % The AWE package has been used to support a translation of monadic
37 Automating translation from programming languages to the language of a generic
39 verification of programs. It has been argued that functional languages can
40 make the task of proving assertions about programs written in them easier,
41 owing to the relative simplicity of their semantics
42 \cite{Thompson92,Thompson95}. The idea of translating Haskell programs, came
43 to us, more specifically, from an interest in the use of functional languages
44 for the specification of reactive systems. Haskell is a strongly typed, purely
52 implementation in Isabelle of classical higher-order logic based on simply
54 support for reasoning about programming functions, both in terms of rich
57 Logic of Computable Functions --- a formalisation of domain theory.
59 We have implemented as functions of Hets translations of Haskell to
62 advantage of Isabelle built-in type-checking. Hets
65 formal development of programs. It has an interface with Isabelle, and
67 of Haskell programs.  Programatica already includes a translation to
69 modelling of the type system \cite{Huff}.
72 the semantic background of the translation, while the subsequent sections
73 are devoted to the translation of types, datatypes, classes and function
78 %gives the sublanguages of Haskell that can be translated, in section 5 we
82 %of monads is carried out with AWE.
84 \section{Semantic Background of the Translation}
87 We firstly describe the subset of Haskell that we cover.
93 %It relies on existing formalisations of
96 following, for the main lines, the denotational semantics of lazy evaluation
103 classes --- all the other ones are just a matter of implementation.
105 For the translation, we have followed the informal description of the
110 that there is no denotational semantics of Haskell! This also has
111 become clear after a query that one of the authors has sent to the
114 to a large subset of Haskell 98.  This also means that there is no
115 notion of correctness of this translation, because it just
117 question is the coincidence of denotational and operational semantics.
118 However, this is beyond the scope of the paper.
122 %partiality could be obtained by lifting the type of function values with
127 %mentioned for the translation to Isabelle/HOLCF --- with the notable exception of
137 %gets analysed and translated, the result of a successful run being an Isabelle
140 %The Hets internal representation of Haskell is similar to that of
141 %Programatica, whereas the internal representation of Isabelle is based on the
142 %ML definition of the Isabelle base logic, extended in order to allow for a
143 %simpler representation of Isabelle-HOL and Isabelle/HOLCF.  Haskell programs and
144 %Isabelle theories are internally represented as Hets theories --- each of them
145 %formed by a signature and a set of sentences, according to the theoretical
147 %composition of a signature translation with a translation of all sentences, is
148 %essentially a morphism from theories in the internal representation of the
149 %source language to theories in the representation of the target language.
153 \section{Translation of Types}
160 at the stage of definition --- in fact, a specific relation has to be
163 \emph{pcpo}) i.e. a set with a partial order which has suprema of
167 generally partial and computability can be expressed in terms of
168 continuity. Recursion can be expressed in terms of least fixed-point
178 The provision of pcpos, domains and continuous functions by
179 Isabelle/HOLCF eases the translation of Haskell types and functions a
181 Haskell semantics. If one reads the section of the Haskell report
183 a function space in Haskell can be mapped to the space of the
187 evaluation. This function is introduced in part 6 of the Haskell
191   However, the provision of $seq$ has important semantic consequences,
213   "liftedApp f x == case f of
221 Our translation of Haskell types to Isabelle types is defined
222 recursively.  It is based on a translation of names for avoidance of
224 the recursive translation of item $\alpha$ and the renaming according
225 to the name translation.  The translation of types is given by the
245 Built-in types are translated to the lifting of the corresponding HOL type.
250 \section{Translation of Datatypes}
273 (possibly recursive) domain as solution of the corresponding domain
276 \emph{pcpodef} can be used to define sub-pcpos of existing pcpos;
277 here, we use it just to introduce an isomorphic copy of an existing
278 pcpo --- this is the semantics of Haskell \emph{newtype} definitions.
285 values of type $N$ must be variable (which always matches), and the
287 applied to this variable whereever the corresponding value of type
313 The general scheme for translation of mutually recursive lazy Haskell
335   declaration of mutually recursive lazy domains does not work.
337   available in the development snapshot.} Order of declarations is
338 taken care of. In case of strict arguments (indicated with ! in
341 The translation scheme for definitions of type synonyms is simply as follows:
347 \section{Translation of Kinds and Type Classes}
349 Type classes in Isabelle and Haskell associate a set of functions to a
351 \emph{methods} of the class). In Isabelle, type classes are typically
352 further specified using a set of axioms; for example, the class
353 $\mathit{linorder}$ of total orders is specified using the usual total
356 actually consists of total orders only, and hence it would be
359 only thing that we assume is that it is a subclass of $pcpo$, because
361 translated to Isabelle/HOLCF as subclasses of \emph{pcpo} with empty
371 satisfy the axioms of the class. Since our translation only generates
372 classes without axioms (beyond those of $pcpo$), proofs are trivial
377 to belong to class $C$ may define the behaviour of $C$'s
379 normal Isabelle constant definitions, if the type of the
381 With this, we avoid an explicit handling of dictionaries, as
382 described in the static semantics of Haskell \cite{journals/jfp/Faxen02}.
389 A restriction of Isabelle is that it does not allow for constructor
407 Haskell type variables are translated to variables of class
409 Haskell, the same concept is called ``kind''), defined by the set of
410 the classes of which it is member.  
441 \section{Translation of Function Definitions and Terms}
443 Terms of built-in type are translated using Isabelle/HOLCF-defined lifting function
456 \noindent Boolean values are translated to values of \emph{bool lift} 
462 translation of patterns; in particular, only simple patterns are allowed (no
463 nested ones). On the other hand, Isabelle sensitiveness to the order of
482   \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
517 compatibility of map and composition.
542          (Lam qX1.  (Lam qX2. case qX2 of
550 The fixrec definition leads to a bunch of theorems, one for simplification.
556     (case x of lNil => lNil | 
566 expected lemmas about the behaviour of $map1$:
603 We provide a shallow embedding of Haskell to Isabelle/HOLCF, which can
604 be used for proving properties of Haskell programs.  This translation
608 The main advantage of our shallow approach is to get as much as
609 possible out of the automation currently available in Isabelle,
614 types have to be lifted due to the mixture of eager and lazy evaluation
615 that Haskell exhibits due to the presence of the $seq$ function.
617 such that explicit handling of dictionaries can be avoided.
619 The main disadvantage of our approach is the lack of type
622 characterisation of monads and on a proof-reuse strategy that actually
625 Concerning related work, although there have been translations of
626 functional languages to first-order systems --- those to FOL of
629 that of Haskell to Agda implementation of Martin-Loef type theory in
638 The translation of Haskell to Isabelle/HOLCF proposed in \cite{Huff}
640 to terms, relying on a domain-theoretic modelling of the type system
644 case of Isabelle/HOLCF with a translation that follows the lines of a
648 the point of view of behavioural equivalence between programs --- in
651 --- however, when we can get it to deal with cases of interest, it
656 %package AWE \cite{AWE}, in order to deal with special cases of monadic
658 % Currently Hets provides with an extension of the
660 %inclusive of \emph{do} notation.  Due to present limitations of AWE, this
665 Future work should use this framework for proving properties of
666 Haskell programs.  Also, the lacking support of constructor classes should
668 translation of constructor classes and monads, also covering \emph{do}
677 Isabelle is part of the Heterogeneous Tool Set Hets and can be
682 %This translation, due to the character of the P-logic
684 %of universal quantification on type variables, or else further relying
701 following set of rules.\\
738 datatypes are translated to HOL datatypes. Type variables are of class
742 here, instead of continuous ones. Non-recursive definitions are treated in an
750 structure of one of the parameters. In contrast, termination is no trivial
757 more precisely, given a set $F$ of functions: 1) all the functions in $F$ are
758 recursive in the first argument; 2) all recursive arguments in $F$ are of the
760 type of a function in $F$ already occurs in the type of the first argument.
762 variables which occurs on the right hand-side but not on the left hand-side of
764 f_{n}$ of type $A \rightarrow B_{1}, \ldots, A \rightarrow B_{n}$ after
765 variable renaming, they are translated to projections of a new function of
766 type $A \rightarrow (B_{1} * \ldots * B_{n})$ which is defined for cases of
767 $A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
769 abbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
809   case \ x \ of \ (p_1 \to t_1; \\
853   \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
909 Type classes are translated to subclasses of \emph{type}. An axiomatisation of
928 Essentially, the claim here is that the expressions on the left hand-side of
929 the following tables represent the denotational meaning of the Haskell
930 expressions on the right hand-side, as well as of the Isabelle/HOLCF expressions to
933 point ($\mu$) in order to represent the denotational meaning of domain
967 The representation of term denotation is similar to what we get from the
968 translation, except that for functions we give the representation of the
969 meaning of \emph{fixrec} definitions ($FIX$ is the Isabelle/HOLCF fixed point
1000 that satisfy the monadic axioms. This solution can be expressed in terms of
1003 arities, entailing the definition of maps between theorems. Theory morphisms
1009 $\mathit{Th}_P$ to a theory $I$ provides the instantiation of the parameter
1011 setting of $\mathit{Th}$ to the concrete setting of $I$ --- the result being
1012 an extension of $I$.  AWE is an extension of Isabelle that can assist in the
1013 construction of theory morphisms \cite{AWE}.
1015 A notion of monad \cite{AWE2} can be built in AWE by defining, on an abstract
1016 level, a hierarchy of theories culminating in \emph{Monad}, based on the
1017 declaration of a unary type constructor $M$ (in \emph{MonadType}) with the two
1022 specific definitions of the operators, as well as discharging proof
1023 obligations associated with specific instances of
1031   x \ >>= \ f & = \ case \ x \ of \\
1038 cnc \ x \ y & = \ case \ x \ of \\
1074 \noindent In order to build up the instantiation of \textit{LS} as a monad,
1086 Renaming is used in order to avoid name clashes in case of more than one
1093 \noindent This instantiation gives the declaration of the
1129 \noindent The \emph{Monad} theory allows for the characterisation of
1131 possibility is to build similar theories for type constructors of fixed arity.
1142 fn3 \ k \ f & = \ case \ k \ of \\
1149 fn4 \ k & = \ case \ k \ of \\ 
1193 In the following, we give a definition of the sub-language of Haskell
1233     & v & \mbox{variable \ of \ datatype}\\
1234     & C \ \overline{v} & \mbox{case \ of \ datatype}
1251   & case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\
1276   & \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ methods \ of} \ K
1282 In contrast, the following gives a definition of the Haskell sub-language
1310   & case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\
1339   & \qquad \mbox{methods \ of} \ K
1379   case \ x \ of \ (p_1 \to t_1; & \\

Indexes created Tue Jul 24 14:28:13 CEST 2018