3 ms·

I guess more generally, it's about effects. The same rant could apply to any particular effect, because they share the property of being infectious: async, unsa

by lmkg 12y ago

I guess more generally, it's about effects. The same rant could apply to any particular effect, because they share the property of being infectious: async, unsafe (in C#, not Rust), throws (checked exceptions), IO, etc. My question is: In a language that has a first-class effect system, does the red/blue problem disappear? Does being able to generalize over effect allow you to avoid cutting the world in half, and allow you to compose effects easier?

malka 12y ago
At first, it reminded me about const-correctness in c++.
tel 12y ago
Absolutely, yes. For instance, here is an abstraction of code which reads and writes class Monad m => MonadTeletype m where writeLn :: String -> m () readLn :: m String Here is one which receives the current time class Monad m => MonadNow m where now :: m UTCTime And here is code which transparently combines them echoTime :: (MonadNow m, MonadTeletype m) => m () echoTime = do line <- readLn t0 <- now writeLine (show t0 ++ ": " ++ line) You then, when actually executing echoTime, have to create a monadic implementation which you prove to instantiate both MonadTeletype and MonadNow. For instance, we can always show that `echoTime` can be satisfied by the Haskell "sin bin" type, IO: instance MonadTeletype IO where writeLn = putStrLn readLn = getLine instance MonadTeletype IO where now = getCurrentTime That said, it's easy to write monadic languages like MonadTeletype and MonadNow which aren't trivially satisfied by IO. This occurs when you've imputed new meaning and language into your monad, which is really cool. IO is the "sum of all evils", but it's not terrifically expressive.
- pron 12y ago
  Except that's not an effect systems because you only have one real effect - the IO type. The challenge of effect systems is to describe effects and how they interact. For example, you'll have an effect that says "a lock is obtained" and one that says "a lock is released", and if you call them both, in the right order, in the same function, then that function has an effect of "mutating something under lock".
  - tel 12y ago
    Sure it is! The effect `(MonadTeletype m, MonadNow m) => m a` is just as real as IO. There's nothing special about IO except that the Haskell RTS knows how to interpret it. I could, for instance, build a pure interpreter of those effects into, say, a stream transformer or compile it into a different language (though we'd have to do some tricks to expose Haskell's name binding). If you want your lock obtained/lock released bit then you want indexed monads. It's easy enough to do, but the safety/complexity tradeoff in the Haskell community has landed on the other side of that... probably for more historical reasons than actual technical ones.
    - pron 12y ago
      > There's nothing special about IO except that the Haskell RTS knows how to interpret it. But that is what makes it an effect. Sure, you can model effects in a "hosted" language this way, but that's not what we mean by effects.
      - tel 12y ago
        I disagree. In force, the Haskell RTS is just a "model" of the IO effects as well. In particular, there are at least two such models, the GHCi interpreter and the GHC compiler! As another example, it'd be completely possible to write your own IO and interpret it in another language. You can read about this on Edward Kmett's blog where he talks about implementing IO for Ermine [0] http://www.tuicool.com/articles/I3EJVb http://www.tuicool.com/articles/I3EJVb Of course, there's something important that makes us want to differentiate "real world" side effects from internal "model effects". Ultimately, from a correctness and reasoning POV, there ought to be no difference. From a practical point of view, some models are more interesting or important than others. But as a compiler writer you're put right back into the same hot seat. [0] Unfortunately, his blog appears to be OOC right now, so here's a weird chinese mirror!

by lmkg 12y ago

malka 12y ago

At first, it reminded me about const-correctness in c++.

tel 12y ago

Absolutely, yes. For instance, here is an abstraction of code which reads and writes class Monad m => MonadTeletype m where writeLn :: String -> m () readLn :: m String Here is one which receives the current time class Monad m => MonadNow m where now :: m UTCTime And here is code which transparently combines them echoTime :: (MonadNow m, MonadTeletype m) => m () echoTime = do line <- readLn t0 <- now writeLine (show t0 ++ ": " ++ line) You then, when actually executing echoTime, have to create a monadic implementation which you prove to instantiate both MonadTeletype and MonadNow. For instance, we can always show that `echoTime` can be satisfied by the Haskell "sin bin" type, IO: instance MonadTeletype IO where writeLn = putStrLn readLn = getLine instance MonadTeletype IO where now = getCurrentTime That said, it's easy to write monadic languages like MonadTeletype and MonadNow which aren't trivially satisfied by IO. This occurs when you've imputed new meaning and language into your monad, which is really cool. IO is the "sum of all evils", but it's not terrifically expressive.

pron 12y ago
Except that's not an effect systems because you only have one real effect - the IO type. The challenge of effect systems is to describe effects and how they interact. For example, you'll have an effect that says "a lock is obtained" and one that says "a lock is released", and if you call them both, in the right order, in the same function, then that function has an effect of "mutating something under lock".
- tel 12y ago
  Sure it is! The effect `(MonadTeletype m, MonadNow m) => m a` is just as real as IO. There's nothing special about IO except that the Haskell RTS knows how to interpret it. I could, for instance, build a pure interpreter of those effects into, say, a stream transformer or compile it into a different language (though we'd have to do some tricks to expose Haskell's name binding). If you want your lock obtained/lock released bit then you want indexed monads. It's easy enough to do, but the safety/complexity tradeoff in the Haskell community has landed on the other side of that... probably for more historical reasons than actual technical ones.
  - pron 12y ago
    > There's nothing special about IO except that the Haskell RTS knows how to interpret it. But that is what makes it an effect. Sure, you can model effects in a "hosted" language this way, but that's not what we mean by effects.
    - tel 12y ago
      I disagree. In force, the Haskell RTS is just a "model" of the IO effects as well. In particular, there are at least two such models, the GHCi interpreter and the GHC compiler! As another example, it'd be completely possible to write your own IO and interpret it in another language. You can read about this on Edward Kmett's blog where he talks about implementing IO for Ermine [0] http://www.tuicool.com/articles/I3EJVb http://www.tuicool.com/articles/I3EJVb Of course, there's something important that makes us want to differentiate "real world" side effects from internal "model effects". Ultimately, from a correctness and reasoning POV, there ought to be no difference. From a practical point of view, some models are more interesting or important than others. But as a compiler writer you're put right back into the same hot seat. [0] Unfortunately, his blog appears to be OOC right now, so here's a weird chinese mirror!