Re: [isabelle] Imperative_HOL: code generator setup for Haskell
On 07/10/14 15:11, Christian Sternagel wrote:
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.
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?
However, one could think of a different serialisation for Haskell. I see three problems:
1. 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
2. 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.
3. 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and