Re: [isabelle] Imperative_HOL: code generator setup for Haskell



Hi Christian,


On 07/10/14 15:11, Christian Sternagel wrote:
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.

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 runST.

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.

Best,
Andreas




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