[isabelle] Imperative_HOL: code generator setup for Haskell

Dear Imperative HOLers,

maybe you could enlighten me on the following points:

1) In Heap_Monad.thy there is a Haskell preamble including

lengthArray :: STArray s a -> ST s Integer;
lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);

Shouldn't that be the above +1? I thought in Haskell the bounds state the lowest and highest *index* of an array. So an array created with bound (0, k) should have length k+1. Maybe I'm wrong?

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?

thanks in advance


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