This is a regionalized or "benign" effect. To the degree that this can be proven in Haskell's synthetic effect calculus it's OK. Since Haskell does have `unsafe

This is a regionalized or "benign" effect. To the degree that this can be proven in Haskell's synthetic effect calculus it's OK. Since Haskell does have `unsafePerformIO` we can, with great care, introduce new rules to the type system. This is how `ST` was created -- we need a primitive first while :: Monad m => m Bool -> m a -> m () while conde bodye = do cond <- conde if cond then bodye else return () -- then we can make a direct, verified pure translation f :: a -> Int f x = runST $ do i <- newSTRef 17 while (readSTRef i >>= \ival -> return (ival > 0)) $ do modifySTRef i (\ival -> ival - 1) ival <- readSTRef i return ival