moved from isabelle-users ************************* Dear all,
In the attached theory files I tried to follow the "let Haskell moan if it is not linear" approach. And on first sight it seems to work.
My motivation is to be able to use imperative code inside pure functions (in the sense that the result type is not "'a Heap"). E.g., for IsaFoR/CeTA it would be unrealistic to change the result type of all our check-functions into "'a Heap" for some 'a, just to be able, to use, e.g., more efficient unification via union-find with arrays.
What I did in the attached theory files is essentially make a copy of the Imperative/HOL development using "'a Heap" and adding an additional phantom type parameter 's (for state) *everywhere* (i.e., heap monad, array type and operations, ref type and operations, ...). Finally there is a function "runST :: (unit, 'a) st => 'a" (where "('s, 'a) st" more or less corresponds to the previous "'a Heap") which is code generated to Haskell's "runST :: (forall s. ST s a) -> a". It's logical definition is "runST c = (case execute c initial_state of Some (x, _) => x)" where "initial_state" is "State ST_Heap.empty" for the new datatypes
's state = State (heap : heap) (*heap is almost the same as the original heap)
and
(dead 's, 'a) st = ST (execute : "'s state => ('a * 's state) option")
Of course this approach only works for Haskell (more specifically for
compilers that support rank-2 types).
I guess the previous Imperative/HOL could be regained by instantiating 's to some concrete "RealWorld" token.
What do you think? cheers chris On 10/07/2014 05:52 PM, Florian Haftmann 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.[...]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
ST.tgz
Description: application/compressed-tar
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
