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

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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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