6 ms·

Thanks for your question. Consider this stateful program in pseudo-code def f x = let i = ref 17 in while i > 0 { i := i-1 } return i

by mafribe 11y ago

Thanks for your question. Consider this stateful program in pseudo-code def f x = let i = ref 17 in while i > 0 { i := i-1 } return i It is referentially transparent. The literal translation into Haskell needs the state monad, despite referential transparency.

tome 11y ago
Could you be more precise? The obvious way to translate this into Haskell is 'f x = 0'.
- mafribe 11y ago
  While f x = 0 is extensionally equal to the original program, it doesn't implement the algorithm in question (iteratively counting down a local reference).
  - tome 11y ago
    Ok, so how about f x = g 17 x where g i x = if i > 0 then g (i - 1) x else i
    - mafribe 11y ago
      The point of the example was to (1) use mutable state (hence force the state monad to show up in the function's type), but (2) in a way that defines a pure function. 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.
      - dllthomas 11y ago
        "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." You absolutely can do exactly that. Even without cheating (unsafePerformIO and friends), usually.
        mafribe 11y ago
        If this is always possible without cheating, then I have definitely misunderstood something about Haskell. 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?
        deleted 11y ago
        [deleted]
        dllthomas 11y ago
        I'm not sure I understand the distinction (quite possibly just 'cause it's early). 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.
dragonwriter 11y ago
> The literal translation into Haskell needs the state monad, despite referential transparency. 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".
tel 11y ago
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
- dllthomas 11y ago
  I think your "while" is "when".
  - tel 11y ago
    Oh, thanks! Good catch. Here's `while` while :: Monad m => m Bool -> m a -> m () while conde bodye = do cond <- conde if cond then bodye >> while conde bodye else return ()
dllthomas 11y ago
There are several candidate translations. Which you might choose depends on those constraints on the actual problem (instead of this pretend one) that make "f x = 0" not an eminently better solution. 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 Better would be to let Haskell help check that the mutation is local and no references escape: let f1 x = runST $ do iRef <- newSTRef 17 whileM_ (fmap (>0) $ readSTRef iRef) $ do modifySTRef iRef (\ i -> i - 1) readSTRef iRef There's the more idiomatic translation, where for something this simple we wouldn't bother with State: let f2 x = go 17 where go i | i > 0 = go (i - 1) | otherwise = i The literal translation using State is: let f3 x = execState countdown 17 where countdown = whileM_ (>0) $ modify (\ i -> i - 1) In all cases, the function as a whole is referentially transparent. 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' What I don't see, in any of this, is a problem (conceptual or practical) involving "destructors". Is your objection to the need to call execState (or its friends)?
- mafribe 11y ago
  Thanks. Do any of these renditions have the target type int -> int?
  - dllthomas 11y ago
    All of them. 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.

by mafribe 11y ago

tome 11y ago

Could you be more precise? The obvious way to translate this into Haskell is 'f x = 0'.

mafribe 11y ago
While f x = 0 is extensionally equal to the original program, it doesn't implement the algorithm in question (iteratively counting down a local reference).
- tome 11y ago
  Ok, so how about f x = g 17 x where g i x = if i > 0 then g (i - 1) x else i
  - mafribe 11y ago
    The point of the example was to (1) use mutable state (hence force the state monad to show up in the function's type), but (2) in a way that defines a pure function. 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.
    - dllthomas 11y ago
      "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." You absolutely can do exactly that. Even without cheating (unsafePerformIO and friends), usually.
      - mafribe 11y ago
        If this is always possible without cheating, then I have definitely misunderstood something about Haskell. 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?
        deleted 11y ago
        [deleted]
        dllthomas 11y ago
        I'm not sure I understand the distinction (quite possibly just 'cause it's early). 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.

dragonwriter 11y ago

> The literal translation into Haskell needs the state monad, despite referential transparency. 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".

tel 11y ago

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

dllthomas 11y ago
I think your "while" is "when".
- tel 11y ago
  Oh, thanks! Good catch. Here's `while` while :: Monad m => m Bool -> m a -> m () while conde bodye = do cond <- conde if cond then bodye >> while conde bodye else return ()

dllthomas 11y ago

There are several candidate translations. Which you might choose depends on those constraints on the actual problem (instead of this pretend one) that make "f x = 0" not an eminently better solution. 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 Better would be to let Haskell help check that the mutation is local and no references escape: let f1 x = runST $ do iRef <- newSTRef 17 whileM_ (fmap (>0) $ readSTRef iRef) $ do modifySTRef iRef (\ i -> i - 1) readSTRef iRef There's the more idiomatic translation, where for something this simple we wouldn't bother with State: let f2 x = go 17 where go i | i > 0 = go (i - 1) | otherwise = i The literal translation using State is: let f3 x = execState countdown 17 where countdown = whileM_ (>0) $ modify (\ i -> i - 1) In all cases, the function as a whole is referentially transparent. 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' What I don't see, in any of this, is a problem (conceptual or practical) involving "destructors". Is your objection to the need to call execState (or its friends)?

mafribe 11y ago
Thanks. Do any of these renditions have the target type int -> int?
- dllthomas 11y ago
  All of them. 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.