Email Gateway (Aug 19 2022 at 16:15): Email Gateway (Aug 19 2022 at 16:15):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Imperative HOLers,
maybe you could enlighten me on the following points:
1) In Heap_Monad.thy there is a Haskell preamble including
lengthArray :: STArray s a -> ST s Integer;
lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
Shouldn't that be the above +1? I thought in Haskell the bounds state
the lowest and highest index of an array. So an array created with
bound (0, k) should have length k+1. Maybe I'm wrong?
2) How would we actually use an "imperative" function from inside some
pure function? Can there be a mapping to runST for Haskell (I guess that
would not be safe, since there's no rank-2 types in Isabelle/HOL)? Any
thoughts or further explanations?
thanks in advance
chris
Email Gateway (Aug 19 2022 at 16:15):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Christian,
With the current setup, you cannot. If you look at the code_printing declarations in
Heap_Monad, you will see that the heap type is mapped to ST RealWorld. That means that
heap values are meant to be used with stToIO rather than runST.
However, one could think of a different serialisation for Haskell. I see three problems:
The type of runST requires that the ST parameter is polymorphic, but Heap in
Imperative_HOL does not have such a type parameter. You could replace Heap.RealWorld in
the Heap's serialisation with some literal type variable. To avoid clashes, this type
variable must not be used by the code generator. For example, you could use some fancy
unicode characters that the code generator does not use. I have not tried this, but I
would expect that the types of the generated functions are general enough to be passed to
runST.
execute takes an initial state, runST does not. Hence, you would have to implement some
glue code that converts the initial state accordingly. The easiest way is probably to
define a function runST as "runST f = map_option fst (execute f s)" and serialise that.
References into the heap must not be passed between different invocations of runST.
AFAIK, reference types are tagged with the state type in Haskell. That is, if you
nevertheless serialise a function that returns a reference, Haskell's type system should
prevent you from applying runST to it. Hence, you can generate code that does not compile
afterwards. From the point of view on partial correctness, this is sound.
Best,
Andreas
Email Gateway (Aug 19 2022 at 16:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
well, experimentally the second position of getBounds seems indeed to be
the length, not the highest index. You may want to make two, three
examples to convince yourself.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
2) How would we actually use an "imperative" function from inside some
pure function? Can
there be a mapping to runST for Haskell (I guess that would not be
safe, since there's no
rank-2 types in Isabelle/HOL)? Any thoughts or further explanations?
With the current setup, you cannot. If you look at the code_printing
declarations in Heap_Monad, you will see that the heap type is mapped to
ST RealWorld. That means that heap values are meant to be used with
stToIO rather than runST.
[...]
That is, if you nevertheless serialise a function that
returns a reference, Haskell's type system should prevent you from
applying runST to it. Hence, you can generate code that does not compile
afterwards. From the point of view on partial correctness, this is sound.
Initially I have been so optimistic to follow that »let Haskell moan if
it is not linear« approach, but there have been technical problems which
could not been solved within the existing infrastructure. The details I
do not remember, but maybe the hg history knows more.
Florian
signature.asc
Last updated: Apr 25 2024 at 01:08 UTC