# [isabelle] Haskell code generation for Imperative/HOL

• To: isabelle-users <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] Haskell code generation for Imperative/HOL
• From: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
• Date: Thu, 20 Oct 2016 21:50:01 +0000
• Accept-language: de-DE, de-AT, en-US

```Dear all,

I just played a bit around with Imperative/HOL and got into the following problem:

I want to use imperative HOL to run some imperative code within a functional program to increase the efficiency of some intermediate computation. So, in particular I need a function similar to Isabelle's âexecuteâ

The following theory describes the problems I ran into, and I would be grateful for any hints.

Cheers,
RenÃ

imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
"\$AFP/Show/Show_Instances"
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Code_Char"
begin

(* example monadic function: compute the head of a list via arrays *)
definition "head (xs :: nat list) = do {
a <- Array.of_list xs;
Array.nth a 0}"

lemma head_sound_as_effect: "xs â [] â effect (head xs) h (snd (Array.alloc xs h)) (hd xs)"
(* there clearly is a better proof by using the framework lemmas,
but this is not the problem *)
by (cases h, cases xs, auto simp: execute_simps effect_def
Array.alloc_def o_def Let_def Array.nth_def Array.length_def guard_def)

definition run_ST :: "'a Heap â 'a" where
[code del]: "run_ST h = fst (the (execute h (undefined ''heap'')))" (* or Heap.empty *)

(* run_ST admits to go outside the ST monad again and reason via the
functional result of the computation  *)
lemma run_ST_effect: assumes "â h. â h'. effect c h h' r"
shows "run_ST c = r"
proof -
from assms obtain h' where "effect c (undefined ''heap'') h' r" by auto
thus ?thesis unfolding run_ST_def effect_def by simp
qed

(* this code belongs into the code-setup for Heap, cf. the code-printing in Heap_Monad *)
code_printing constant run_ST â (Haskell) "RunST.runST"

definition "test = show (head_functional [17,90,2])"

(* the problem now is the type-signature in the generated code of

nth ::
forall a.
(Heapa a) => Heap.STArray Heap.RealWorld a ->
Nat -> Heap.ST Heap.RealWorld a;
nth a n = Heap.readArray a (integer_of_nat n);

and

head :: [Nat] -> Heap.ST Heap.RealWorld Nat;
a <- Heap.newListArray xs;
nth a zero_nat
};

because of the code_printing setup in Heap_Monad

type_constructor Heap â (Haskell) "Heap.ST/ Heap.RealWorld/ _"

The problem is that the type of the Haskell function runST is of
type forall a. ((forall s. ST s a) -> a), so that in particular the
state in the ST monad must be arbitrary, but not a fixed type like RealWorld.

So, the proper code-printing would be

type_constructor Heap â (Haskell) "Heap.ST/ s/ _"

two type parameters, one for state, the other for the return type).

Now there is the problem, that I don't know how to tell the code-generator
to observe the heap/ST type as binary, although it is unary in Isabelle.

In particular, the type of nth and head have to become

nth ::
forall a s.
(Heapa a) => Heap.STArray s a -> Nat -> Heap.ST s a;

head :: forall s. [Nat] -> Heap.ST s Nat;

where the s is quantified. Once one performs this change, compilation and
execution works as expected.

*)
end```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.