4 ms·

I think the point is that there is no good effect-union type; this has to be pieced together with monad transformers where you might have that types "Atransform

by drostie 12y ago

I think the point is that there is no good effect-union type; this has to be pieced together with monad transformers where you might have that types "Atransformer (Btransformer C)" is not equal to "Btransformer (Atransformer C)". This is, for example, why Haskell has one monolithic "IO" monad instead of one for hitting the filesystem, one for HTTP requests, one for IORefs, etc. Haskell does not, for example, represent the difference between program nondeterminism (reading a file and doing stuff differently based on its contents) and permanent side-effects on the file system (writing a file); and I'd say the reason that it doesn't do that is because NondeterministicT (FilesystemAlteredT Identity) x would be different from FilesystemAlteredT (NondeterministicT Identity) x. In some ways the granularity is nice because those two types are not isomorphic; but you might want to "erase" the granularity, which is not possible in Haskell. In terms of the "unioning" that you want, it's something like a dual of the unions that appear in typed exceptions: once you trace through some code you find out that it might fail via `FileNotFound` or `HTTP404`; this means that the relevant effects are `FileSystem :+: HTTP` in some sense.

tel 12y ago
I know there are a lot of solutions to this, but I've personally found the `mtl` mechanism in Haskell to be completely sufficient. I describe whatever effect languages I want my application bits to be able to operate over as separate type classes and then build one or more interpreters of these classes to run. Essentially it's mtl + Oleg's "Finally Tagless" mechanism [0] [1]. The problem with this mechanism is not felt by the application writer but instead the library writer. It forces you to instantiate (n x m) combinations of effects for your (concrete instantiators) x (effectful languages). For the core classes mtl bears this well, but it might explain why this technique is not as well represented in written libraries. That said, as an application writer the number of concrete instantiators is often between 1 and 3 so the pain is very reasonable. (Edit: I should add that there is another downside in the mtl method in that authors of these finally-tagless code fragments cannot choose priority order of effects---the interpreter is free to decide this on their own. There's nothing wrong with this as long as you, as interpreter writer, consider the burden of correctness. You should be anyway, though, so... It ends up being a minor pain point, imo.) [0] http://hackage.haskell.org/package/mtl [1] http://okmij.org/ftp/tagless-final/
- drostie 12y ago
  It took me a while to start to grok the "Finally Tagless" thing; thanks for that!
rtpg 12y ago
I'm kind of interested in knowing why you don't think that there isn't an isomorphism along the ordering of the monad transformers. Wouldn't it just be a question of rebuilding combinators so that they're targetting the right depth? Or am I missing something
- tel 12y ago
  I'll demonstrate the lack of an isomorphism via a counterexample. Consider MaybeT and WriterT (and the basic Identity monad for the bottom of our stack) newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) } newtype WriterT w m a = WriterT { runWriterT :: m (a, w) } newtype Identity a = Identity { runIdentity :: a } I'm going to claim that MaybeT (WriterT w Identity) is not isomorphic to WriterT w (MaybeT Identity). If we expand the first MaybeT (WriterT w Identity) a == WriterT w Identity (Maybe a) == Identity (Maybe a, w) == (Maybe a, w) And if we expand the second WriterT w (MaybeT Identity) a == MaybeT Identity (a, w) == Identity (Maybe (a, w)) == Maybe (a, w) So we can see that the Maybe is wrapped around something different in each stack. So now to the claim that there's no isomorphism should be obvious---any witnesses to the isomorphism f and g would have to have that for all w, f (g (Nothing, w)) = (Nothing, w), but since g :: (Maybe a, w) -> Maybe (a, w) cannot fabricate an `a`, it must be such that g (Nothing, w) = Nothing which means that f :: Maybe (a, w) -> (Maybe a, w) cannot determine the right `w` to return.

by drostie 12y ago

tel 12y ago

I know there are a lot of solutions to this, but I've personally found the `mtl` mechanism in Haskell to be completely sufficient. I describe whatever effect languages I want my application bits to be able to operate over as separate type classes and then build one or more interpreters of these classes to run. Essentially it's mtl + Oleg's "Finally Tagless" mechanism [0] [1]. The problem with this mechanism is not felt by the application writer but instead the library writer. It forces you to instantiate (n x m) combinations of effects for your (concrete instantiators) x (effectful languages). For the core classes mtl bears this well, but it might explain why this technique is not as well represented in written libraries. That said, as an application writer the number of concrete instantiators is often between 1 and 3 so the pain is very reasonable. (Edit: I should add that there is another downside in the mtl method in that authors of these finally-tagless code fragments cannot choose priority order of effects---the interpreter is free to decide this on their own. There's nothing wrong with this as long as you, as interpreter writer, consider the burden of correctness. You should be anyway, though, so... It ends up being a minor pain point, imo.) [0] http://hackage.haskell.org/package/mtl [1] http://okmij.org/ftp/tagless-final/

drostie 12y ago
It took me a while to start to grok the "Finally Tagless" thing; thanks for that!

rtpg 12y ago

I'm kind of interested in knowing why you don't think that there isn't an isomorphism along the ordering of the monad transformers. Wouldn't it just be a question of rebuilding combinators so that they're targetting the right depth? Or am I missing something

tel 12y ago
I'll demonstrate the lack of an isomorphism via a counterexample. Consider MaybeT and WriterT (and the basic Identity monad for the bottom of our stack) newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) } newtype WriterT w m a = WriterT { runWriterT :: m (a, w) } newtype Identity a = Identity { runIdentity :: a } I'm going to claim that MaybeT (WriterT w Identity) is not isomorphic to WriterT w (MaybeT Identity). If we expand the first MaybeT (WriterT w Identity) a == WriterT w Identity (Maybe a) == Identity (Maybe a, w) == (Maybe a, w) And if we expand the second WriterT w (MaybeT Identity) a == MaybeT Identity (a, w) == Identity (Maybe (a, w)) == Maybe (a, w) So we can see that the Maybe is wrapped around something different in each stack. So now to the claim that there's no isomorphism should be obvious---any witnesses to the isomorphism f and g would have to have that for all w, f (g (Nothing, w)) = (Nothing, w), but since g :: (Maybe a, w) -> Maybe (a, w) cannot fabricate an `a`, it must be such that g (Nothing, w) = Nothing which means that f :: Maybe (a, w) -> (Maybe a, w) cannot determine the right `w` to return.