Email Gateway (Aug 22 2022 at 14:18): Email Gateway (Aug 22 2022 at 14:18):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
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”
or Haskell’s “runST”.
The following theory describes the problems I ran into, and I would be grateful for any hints.
Cheers,
René
theory Head_Imperative
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)"
unfolding head_def
(* 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
Heap_Monad.heap_def Array.set_def Array.get_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
definition "head_functional xs = run_ST (head xs)"
lemma head_sound_as_functional_program: "xs ≠ [] ⟹ head_functional xs = hd xs"
unfolding head_functional_def
using run_ST_effect head_sound_as_effect by metis
(* this code belongs into the code-setup for Heap, cf. the code-printing in Heap_Monad *)
code_printing constant run_ST ⇀ (Haskell) "RunST.runST"
code_printing code_module "RunST" ⇀ (Haskell)
‹import qualified Control.Monad.ST;
runST = Control.Monad.ST.runST;›
definition "test = show (head_functional [17,90,2])"
export_code test in Haskell module_name Head
(* 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;
head xs = do {
a <- Heap.newListArray xs;
nth a zero_nat
};
because of the code_printing setup in Heap_Monad
type RealWorld = Control.Monad.ST.RealWorld;
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/ _"
where "s" is some additional type variable. (ST in Haskell requires
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
Email Gateway (Aug 22 2022 at 14:19):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
A small update:
one can use
code_printing code_module "RunST" ⇀ (Haskell)
‹import qualified Control.Monad.ST;
import qualified System.IO.Unsafe;
runST = System.IO.Unsafe.unsafePerformIO . Control.Monad.ST.stToIO;›
to make the generated code compile. However, this seems a bit odd to use
the unsafePerformIO-operation where there is the safe runST in Haskell.
Cheers,
René
PS: The problem appears both in Isabelle2016 and Isabelle2016-1-RC0
Email Gateway (Aug 22 2022 at 14:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rene,
Am 21.10.2016 um 08:16 schrieb Thiemann, Rene:
A small update:
one can use
code_printing code_module "RunST" ⇀ (Haskell)
‹import qualified Control.Monad.ST;
import qualified System.IO.Unsafe;
runST = System.IO.Unsafe.unsafePerformIO . Control.Monad.ST.stToIO;›to make the generated code compile. However, this seems a bit odd to use
the unsafePerformIO-operation where there is the safe runST in Haskell.
this indeed is the core of the problem: there is a safe runST in
Haskell, but I have found no way to express this adequately in the HOL
type system. Early code generation setups for Imperative HOL attempted
this but that never worked out.
Hope this helps,
Florian
Cheers,
RenéPS: The problem appears both in Isabelle2016 and Isabelle2016-1-RC0
Am 20.10.2016 um 23:50 schrieb Thiemann, Rene <Rene.Thiemann@uibk.ac.at>:
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”
or Haskell’s “runST”.The following theory describes the problems I ran into, and I would be grateful for any hints.
Cheers,
Renétheory Head_Imperative
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)"
unfolding head_def
(* 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
Heap_Monad.heap_def Array.set_def Array.get_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
qeddefinition "head_functional xs = run_ST (head xs)"
lemma head_sound_as_functional_program: "xs ≠ [] ⟹ head_functional xs = hd xs"
unfolding head_functional_def
using run_ST_effect head_sound_as_effect by metis(* this code belongs into the code-setup for Heap, cf. the code-printing in Heap_Monad *)
code_printing constant run_ST ⇀ (Haskell) "RunST.runST"code_printing code_module "RunST" ⇀ (Haskell)
‹import qualified Control.Monad.ST;
runST = Control.Monad.ST.runST;›definition "test = show (head_functional [17,90,2])"
export_code test in Haskell module_name Head(* 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;
head xs = do {
a <- Heap.newListArray xs;
nth a zero_nat
};because of the code_printing setup in Heap_Monad
type RealWorld = Control.Monad.ST.RealWorld;
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/ _"
where "s" is some additional type variable. (ST in Haskell requires
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
Last updated: Apr 26 2024 at 12:28 UTC