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

    while :: Monad m => m Bool -> m a -> m ()
    while conde bodye = do
      cond <- conde
      if cond then bodye >> while conde bodye else return ()

The one that probably most closely matches the semantics of the pseudo-code would be:

    let f0 x = unsafePerformIO $ do
        iRef <- newIORef 17
        whileM_ (fmap (>0) $ readIORef iRef) $ do
            modifyIORef iRef (\ i -> i - 1)

        readIORef iRef

    let f1 x = runST $ do
        iRef <- newSTRef 17
        whileM_ (fmap (>0) $ readSTRef iRef) $ do
            modifySTRef iRef (\ i -> i - 1)

        readSTRef iRef

    let f2 x = go 17
      where
        go i | i > 0 = go (i - 1)
             | otherwise = i

    let f3 x = execState countdown 17
      where
        countdown = whileM_ (>0) $ modify (\ i -> i - 1)

In your function, "while i > 0 { i := i - 1 }" is clearly not referentially transparent. Attempting to transliterate in a way that preserves this expression, it is unsurprising that we wind up with expressions that depend on state. The State monad is one way of encapsulating this. Note that f3 and f2 are actually very similar. The execState function doesn't do any deep voodoo - a value of type "State s a" is a thin wrapper around a function of type "s -> (a, s)"; execState simply extracts this function, applies it to a value, and returns the second part of the output.

The actual definitions are equivalent to these (albeit slightly more complicated to keep things DRY w/ transformers):

    newtype State s a = State (s -> (a, s))

    execState (State f) s = let (_, s') = f s in s'

More precisely, since the argument isn't used it's type is unconstrained, and the result could be any numeric type, so they all actually have type (Num b => a -> b), but that can be used anywhere you're expecting an Int -> Int.

Sure, literally translating imperative procedures into Haskell code often needs the State monad since imperative procedures gratuitously use state modifications that are logically unnecessary for their function.

But I'm not sure why any meaning should be ascribed to this beyond "translate function, not code".

    f x = g 17 x
        where g i x = if i > 0 then g (i - 1) x else i

The example is intended to point towards an expressivity gap of the monadic encapsulation approach to effects, in that one can't (as far as I'm aware -- I have not programmed in Haskell) hide state usage, even when this is extensionally OK.

It is an open research question to define type/effect systems that (a) enable programmers to hide such benign state usage, (b) preserve type inference for interesting typing systems (say F-omega which is the heart of Haskell's types), and (c) are pragmatically viable.

You absolutely can do exactly that. Even without cheating (unsafePerformIO and friends), usually.

Could you point me towards an explanation how the hiding of stateful expressions works in Haskell in general?

Let me clarify my question (a bit). Are you saying one of the following is true?

(1) You are saying for any program M that uses state (i.e. M's type mentions the state monad in an essential way) but in a pure way, i.e. M's stateful behaviour is not visible from the outside, there is a context C[.] (not involving tricks like UnsafeIO) such that C[M] has the same behaviour as M (as seen from the outside), and C[M] has (essentially) the same type as M, except that the state monad is gone?

(2) There is a 'nice' translation function f on programs such that for any program M that uses state in a pure way (same as (1)), f(M) has the same behaviour as M (as seen from the outside), and f(M) has (essentially) the same type as M, except that the state monad is gone?

A fruitful way to look at monads is to say a value of type M (where M is an instance of Monad) is a program in a language. State is a language for describing stateful computation. Reader is a language for describing parameterized computation. ST is a language for describing controlled, local mutation. IO is a language for describing arbitrary side effects.

Most of these have pure interpreters, with the most generic typically called runM (so, runState, runReader, &c). The only place cheating comes in is unsafePerformIO - interpreting IO is the job of the runtime, which does it in a more controlled way relative to the rest of your program.

The type of the return value of an interpreter, of course, doesn't tell you what kind of program you ran - it just tells you the result.

For 1, to get from a value of type "State s a" to a value of type a, you simply call evalState and supply an initial state of type s.

For 2, you could look at the structure of the program and unwrap all (State s a) values to have type (s -> (a, s)), updating the various functions used to operate on (State s a) values to match.

In either case, you would not see State in the resulting type signature. In case 2, you would still need to provide an initial value of type s - you can't do much interesting with a function but apply it.

Note that the function in 2 is more theoretical than practical. You could in principle write it with Template Haskell, but since it doesn't change the behavior and you can just do 1 to change the type the same way there isn't reason to.

I still wonder how this would work with scope extrusion of references. Consider this little Ocaml program

    let ( impure, pure ) =
      let i = ref 0 in
      let impure x = ( i := !i + 1; x + !i ) in
      let pure x = (
        i := !i + 1;
        let res = !i + x in
        i := !i - 1;
        res - !i ) in
      ( impure, pure );;

Is it possible to do the same in Haskell? By "the same" I mean giving "pure" the type int -> int, despite using hidden state that is used elsewhere?

Something with a similar form that would be more realistic to ask for would be a cache for a pure-but-expensive function and some IO operations to inspect/manipulate that cache. I believe you would need a call to unsafePerformIO, but that could be a reasonable thing to do.