[isabelle-dev] [isabelle] Imperative_HOL: code generator setup for Haskell

[Christian Sternagel]

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
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ST.tgz
Type: application/x-compressed-tar
Size: 11504 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141014/7e9f6fde/attachment.bin>