[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