10 ms·

"Some conceptual problems not yet solved, e.g. destructors for state monads" I'm not sure what you're talking about here - could you elaborate? My best guess

"Some conceptual problems not yet solved, e.g. destructors for state monads" I'm not sure what you're talking about here - could you elaborate? My best guess would be that by "state monads" you mean streaming libraries like pipes and conduit, where there have indeed been some interesting questions around finalization. Calling these "state monads" is surprising enough that I seek clarification, however. Regarding those libraries, I don't know the current status of that discussion (which mostly took place a couple years back) but I do know the libraries themselves are quite useful.

mafribe 12y 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 12y ago
  Could you be more precise? The obvious way to translate this into Haskell is 'f x = 0'.
  - mafribe 12y 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 12y 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 12y 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 12y 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 12y 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 12y ago
        [deleted]
- dragonwriter 12y 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 12y 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 12y ago
    I think your "while" is "when".
    - tel 12y 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 12y 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 12y ago
    Thanks. Do any of these renditions have the target type int -> int?
    - dllthomas 12y 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.

mafribe 12y 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 12y ago
Could you be more precise? The obvious way to translate this into Haskell is 'f x = 0'.
- mafribe 12y 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 12y 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 12y 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 12y 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 12y 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 12y ago
        [deleted]
dragonwriter 12y 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 12y 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 12y ago
  I think your "while" is "when".
  - tel 12y 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 12y 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 12y ago
  Thanks. Do any of these renditions have the target type int -> int?
  - dllthomas 12y 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.