[isabelle-dev] [isabelle] Imperative_HOL: code generator setup for Haskell
c.sternagel at gmail.com
Tue Oct 14 14:29:26 CEST 2014
moved from isabelle-users
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
(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?
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 11504 bytes
Desc: not available
More information about the isabelle-dev