Hacker News new | past | comments | ask | show | jobs | submit login

We can massively generalize this by calling "blue" "pure" and "red" "impure". The end result is essentially Haskell (but you can take it much further, too!).

---

There's something horrifyingly restrictive about having merely (blue -> pure, red -> impure), though. All "blue" functions behave roughly the same (e.g., very, very nicely and compositionally) but "red" functions come in many classes: async, stateful, exception-throwing, non-deterministic, CPS'd, IO-effectful, combinations of the prior.

What we want is a nice way of representing different kinds of red functions and how they all interact.

What we'd also like is a nice way of composing different kinds of red functions so that the bundled piece has a sensible kind of redness too and we can keep composing.

And this is exactly monads and monad transformers.

There are other ways to achieve this end as well all under the general name "Effect Typing". Very cool stuff.

But what I'd like to emphasize is that Java/C#/Go have not solved this larger problem. They each introduce a fixed number of "rednesses" and very specific ways that different kinds of red can be connected together. Monads are a generalizable solution.

The situation is exactly the same as HOFs themselves. We've had subroutines and functions for a long time, but first-order and higher-order functions are a marked increase in power since you can now refer to these "function things" directly.

Monads take the notion of "CPS Transform" and allow you to refer to it directly, to mark sections of code which use it and compose them intelligently. They allow you to invent your own kinds of redness on the fly and ensure that your custom colorations compose just as nicely as the built-in ones.

If this article is even slightly interesting then you owe it to yourself to learn much more about effect typing. It'll change your world.

(That and sum types, because nobody is served by a bunch of integers named Token.LEFT_BRACKET.)




Effect Typing and Monads are yet another colour for the lipstick you put on the pig. You still have non-composability (i.e. the async monad spreads through your code), you still have the complexity, you still don't have proper tracebacks without special runtime support, and you still have the inefficiency that Bob didn't actually mention (unwinding all those stacks all the time).

Languages with threads (Java, C#) don't quite solve the problem as their threads have other disadvantages, e.g. creating too many threads causing contention, though it's much less of a problem than people make it to be.

Go actually completely removes the problem - you don't get a nice tool to pack the problem into boxes more easily, you don't get a different fancy colour for your lipstick, you just don't have the problem at all - you wouldn't know it existed was it not for those other languages.

There might be a deeper lesson here about good, pragmatic engineering vs awesome computer language geekery.


Go's "good, pragmatic engineering" solution to the problem - lightweight threads, channels, and the communicating sequential processes model - is built on the back of decades of academic research, including programming languages research.

And now for some computer language geekery:

Go solves one "code color" problem (concurrency/asynchrony), by hard-coding the solution into the language. Go programs are written in a particular monad (the "Go" monad, if you will), and so have one color. Indeed, monads originally arose in the study of the semantics of imperative languages; to be imperative is to be inside a particular monad. This is exactly the "async monad spreading through your code" problem taken to its logical conclusion: just put everything in the same monad!

This hard-coding solution has very concrete advantages. For one, you don't need to think about separate colors and how to transition between them, combine them, define them, etc. (IOW, monads are complex; by picking one, you reduce cognitive load.) For another, it's easier to optimize your implementation and tooling for that monad (lightweight threads, useful tracebacks).

But PL academics aren't satisfied with this solution, because it only solves one color problem, and it solves it non-composably: you can't put the solution in a library, you have to invent a whole new language for it. That's the holy grail (some) PL research is chasing. It's a question of concrete benefits in the here-and-now versus abstract benefits in the hopeful-future. But it pays to remember that today's concrete benefits are yesterday's green-field research.


Indeed, Go only solves one problem by baking it into the language/runtime, it doesn't have a generic mechanism to solve similar problems.

But my point is that it solves the problem much better than monads do - in particular if you don't just look at the syntax/user interface level, but at the non-functional aspects, like debuggability, performance, etc.

I remember a time when Aspect Oriented Programming was all the rage, with point cuts etc to capture cross-cutting aspects of your program. AOP is certainly less generic than monads, but even with rather specialized tools, it turns out the two "killer apps" of AOP were much better served by runtime support in the VM (logging/debugging) and explicit code (transactions).

I'm skeptical about the holy grail that you describe. I see how it's attractive, but in my work experience, the pragmatics of solving a particular issue often turn out to be harder (sometimes much) than the theoretical aspects.

There's certainly influence from more theoretical research in all we do in CS, but for example with Go, it's only based on Hoare's CSP model in the most abstract sense, and its implementation of lightweight threads, its stack model etc are definitely in the domain of clever engineering, not breakthrough research.


"AOP is certainly less generic than monads, but even with rather specialized tools, it turns out the two "killer apps" of AOP were much better served by runtime support in the VM (logging/debugging) and explicit code (transactions)."

Indeed... beware the tech promoted with the same example over and over again. That's a huge red flag.


> This hard-coding solution has very concrete advantages.

True, but you missed the major disadvantage of doing everything in a monad: there may be horrible side-effect demons lurking in every line of code!

In my experience, the most egregious offenders are shared mutable state (AKA multithreading) and exceptions. Introducing multithreading or exceptions into an application which previously shunned them feels like switching to a whole different language; one where all our intuitions and guarantees can be undermined at any time.


This assumes that the primary problem is merely asynchronous code. If that's the main problem you're facing then there's no reason in the world to believe that having more distinction at no gain is the right tradeoff.

I'm not claiming that you must program in a language which distinguishes lipstick colors. I'm merely claiming that you can and that it's a valuable tool.

To respond to your concrete criticisms:

The non-composability you refer to is actually what I call composability itself. You want the isolation of effectful worlds so that you have different things to choose to compose in the first place. You can do this "horizontally" with binding or "vertically" with free products or lifting (or any number of other techniques). Without this distinction things "compose automatically", but only because you've decided to mix all of your colors and go with brown.

Proper tracebacks and stack unwinding can be a problem, but fundamentally these are problems of how you compile/interpret languages like this instead of semantically whether these languages allow you to express what you would like to at high fidelity. Both of those problems can be addressed, though. The degree to which they're painful in practice is also a question.

The comment about threads is somewhat off topic. There's nothing in what I was saying which precludes the introduction of nice green threads and competitive scheduling. You can implement Go in Haskell quite neatly, for instance.

But yes, I agree. If your problem is pure multithreading then languages like Go and Erlang make it go away completely. They do so by collapsing layers of semantics down to a single one (completely antithetical to the red/blue distinction here) but choosing one such that multithreading is nice.

This can be an excellent spot in solution space for many problems. I would never suggest otherwise.

But as long as we're ostensibly on the topic of "blue/red"-ness of your language then it's high time to talk about effect typing.


> Effect Typing and Monads are yet another colour for the lipstick you put on the pig.

When I started to read the essay, I thought that it would be an anti-typing screed (it's nothing to do with the author, whom I don't know!), with blue functions being untyped (or, pace Harper, unityped) and red functions being typed. An untyped function can call a typed function by ignoring the types; a typed function cannot call an untyped one, because that might violate its contract. If you buy this analogy, then your first sentence might equally well have said "typing is yet another colour for the lipstick you put on the pig"—but lightweight HM inference shows that is not so. Maybe we're just awaiting the revolutions in effect typing that languages like ML and derivatives, and Haskell, brought to typing itself?


Actually, you can call both ways - from statically typed to dynamically typed and back. This is the premise of the work done in Racket on contracts, and more generally of the "gradual typing" movement. Harper's "unityped" term suggests exactly how this can work. An untyped function takes arguments that are all of one type, and returns one of the same type (that type being the "dynamic" type that includes every possible value, and thus is useless for static checking).

To call an untyped function from typed code, simply cast all your arguments to this type (trivial, since it contains anything), and check its return value has the type you expect (throwing an error if it's of the wrong type). To call a statically typed function from untyped code, simply check the types of all the arguments you wish to pass to it (throwing an error if they don't match its signature), and cast the returned value to the dynamic type (again, trivial).

I'm glossing over a very important difficulty, which is that you can't dynamically check something of a function type -- if I'm handed a function, how do I know at runtime whether it's of type `int -> int`? I can't! So the solution is to "wrap" this function with a contract that delays checking until the function is actually called, at which point you can check the argument is an `int` and the result is an `int`.


> To call an untyped function from typed code, simply cast all your arguments to this type (trivial, since it contains anything), and check its return value has the type you expect (throwing an error if it's of the wrong type).

To me, as soon as a function includes dynamic checks, it ceases to be statically typed; so I would say that a function that operates this way becomes only dynamically typed.


Do you consider any function which may raise an error to be "dynamically typed", then? (For example, any function which performs an array index; or any function which performs I/O; or, to be absurd, any function which allocates memory (since memory is a finite resource that may run out).) If so, I understand the distinction you're making, but it's a very strong position; most people do not mean that when they say "statically typed". If not, I don't understand the distinction you're making.

Admittedly, gradual typing does not mean that calling into untyped code from typed code is "safe" from runtime type errors (although it is safe in the technical preservation-and-progress sense). But it gives you a partial guarantee: if a type error occurs, you know that the fault does not lie in the typed code. This aids debugging, and helps you port over existing codebases gradually. So it's still quite useful.


> Do you consider any function which may raise an error to be "dynamically typed", then? (For example, any function which performs an array index; or any function which performs I/O; or, to be absurd, any function which allocates memory (since memory is a finite resource that may run out).)

That's a good question! Yes, in an idealised sense, I do; but, in practice, I think that I would make an exception for functions where the error comes from the host system, not from the program. (For example, if I were too strict about it, then I would have to disallow even the safest of Haskell functions because it might be executed on a computer whose hard drive is failing.) Thus, I would call Haskell's `head` function dynamically typed.

> Admittedly, gradual typing does not mean that calling into untyped code from typed code is "safe" from runtime type errors (although it is safe in the technical preservation-and-progress sense).

I think that I don't understand the definition. Isn't encountering a runtime error precisely getting 'stuck' (in the "opposite-of-progress" sense)?


> I think that I don't understand the definition. Isn't encountering a runtime error precisely getting 'stuck' (in the "opposite-of-progress" sense)?

Sorry, perhaps I should have said "exception" rather than "error". Raising an exception is absolutely "safe"/progress-obeying, as long as your language specifies the behavior of exceptions. That the exception happens to be called a "TypeError" doesn't change anything.

Getting "stuck" means being in a state such that there's no defined next state - a state which the language spec doesn't cover. So most "dynamically-typed" languages are in fact safe in progress-and-preservation terms, because they have well-defined behavior in all cases. C, otoh, is "statically-typed" but unsafe, because you can write C code with undefined behavior.

(That dynamically typed languages can be (statically) typesafe should be unsurprising, since they're just statically-unityped languages. Nothing says a unityped language can't be typesafe, it's just a very uninteresting property!)


Total agreement generally, but I wanted to mention that the Any -> X downcasting is trouble sometimes. It is difficult to do this in a type-safe way (e.g. without accidentally introducing holes) and if you have typecasing universally then you lose parametricity, one of the most powerful tools in any polymorphic type theory.


(Late to the party; sorry)

> you can't dynamically check something of a function type

Another approach, besides contracts, (one that my lab is working on) relies on whole program type-checking and path-sensitive program analysis.


Go seems to have solved the IO problem, but what about the general asynchronous issue? How do you handle calling a function several thousand times on dozens of threads and combine the results?


How does Go solve "the IO problem"? (Probably what I want to ask is: which IO problem does Go solve? It can't be the one about purity and side-effects, and if it doesn't solve that...)


How do you do IO without stalling your whole program while it accesses the data, specifically the fact that the asynchronous call is terminated in your main loop, not where you are accessing the IO itself.


Is there any reason you couldn't just spin up so goroutines to do this?


Telling a hundred threads to do work is easy, figuring out how to sync all of the answers is the hard part.

I am not saying you can't pull it off, but the proposed solution doesn't simplify the complex part of those operations.


> We can massively generalize this by calling "blue" "pure" and "red" "impure". The end result is essentially Haskell (but you can take it much further, too!).

Yes, I wish I'd taken the time to work more Haskell into the post but this thing has been marinating on my hard drive for months and I wanted to just get it done before the Superbowl ended and the wife and kids got home.

> (That and sum types, because nobody is served by a bunch of integers named Token.LEFT_BRACKET.)

What said it was an integer? ;)


> What said it was an integer? ;)

Ha, well, totally fair. But, as long as this watercooler language is essentially "Javascript++", I'm not going to let it get away ensuring sum types are bolted on :)


Unfortunately, monads are a bad way of encapsulating and controlling effects. Effects are the most important -- and most bug prone -- of any interesting software aside from compilers, and monads take this central element and make it un-composable. This is why I don't like the current advanced type systems: they help most where they're least needed (the relatively bug-free portions of the code, namely data transformations), and don't help -- interfere, even -- where they're most needed. Effect systems -- if we can get them right and easy to use -- will be a great help. In the meantime, some of the most production-ready effect systems (though they're not general, but have to be built ad-hoc for a specific use) can be found in Java 8's pluggable type systems provided by the Checker framework[1]. It's got a rudimentary lock-use effect system and a GUI effect system (plus some other cool type systems, like physical units, immutability, security and even a linear type system for aliasing).

[1]: http://types.cs.washington.edu/checker-framework/current/che...


> Effects are the most important -- and most bug prone -- of any interesting software aside from compilers, and monads take this central element and make it un-composable.

Can you elaborate on this? Because, AFAICT, the big selling point for monads for dealing with effects is precisely composability.


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.


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/


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


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


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.


Monads themselves are composable via bind, but the values encapsulated by the monad are not. Consider there is no real converse to the return operator: once something has been wrapped by a monad, then it is forever stuck in that monadic world. That can be rather annoying, because in languages such as OCaml (not sure about Haskell &c), monad-like interfaces are a convenient abstraction, yet using them leads to highly idiosyncratic code. Rather similar to the sync/async, red/blue distinction in the original article.


Sure the values are. Any function `a -> b -> c` can be lifted into a function `m a -> m b -> m c` for any Monad. That's (part of) the exact thing that bind buys you.

"Escaping" from a monad is an artifact of a bad intuition. There's no reason for a monad (m a) to "contain" values a and thus no reason to believe that they can be removed.

Even Maybe is a sufficient model of this. I can make a whole big compositional pipeline with all kinds of compositions at the value level, but if my inputs are Nothing then there won't be anything to "pull out" at the end.

Ultimately, "monadic worlds" is a good intuition. Just realize that your monadic world may be a strange one when you pull it back into "your" world---the interpretation may not be obvious, it may demand something of you, and it may not look very much like the "values" you felt like you were playing around with.


Let's take a simple, quotidian example: logging and errors. I write functions that produce logs and may generate errors. If I were using monads, I'd have a log monad and an error monad. For logs, my functions would produce a value and a list of log messages. The monad would combine the list of messages. For errors, my functions return an OK and a value, or an error, and the monad short-circuits errors. Now I write functions that might produce both logs and errors. How do the two monads compose?


Of course there are two ways. The problem is that there is not enough information in the mere product of the two algebras to indicate what proper behavior is.

If you don't mind deferring the definition of "correct" to the interpreter writer then that intentional choice is captured by

    (MonadWriter Log m, MonadExcept m) => m a
If you want more controls then we need to start specifying laws. For instance, the following law distinguishes between the two instances

    throwError e >> m == throwError e
and this now clearly indicates that EitherT e (WriterT Log) is wrong while WriterT Log (Either e) is fine.

So how do we specify what additional laws are needed to cut down the free product of the effectful languages? Dunno, that's a hard one. You could clearly do it using dependent types, but that's still today very expensive.

But given that we literally lack proper information to make a choice it's very important that all of those choices are allowable. It's my position that there is no meaningful default. It's also my position that the `mtl` style free products are perfectly acceptable.


I would even go so far as to suggest that there are applications where we want the other ordering of these two.


Me too!


But in general, effects are not "the values encapsulated by the monad", so the fact that the values are "stuck" within the monad doesn't have any bearing on whether using monads to manage effects makes effects non-composable.


To be fair, I like pluggable type systems a lot. I don't think that privileged type systems are the end-all-be-all.

I disagree a lot that the current effect systems don't prevent errors, however. You're right that linear types are difficult to encode in Haskell at least, but you can get away with a lot of bang for relatively little buck even without them.

The right choice (or choices) in design space here is a big challenge. It'll be exciting to see new research as it develops. I'm especially excited to see what comes of Pfenning's Pi calculus linear types [0].

[0] To be clear, I don't know if they're "his" excepting that he appears to be doing a lot of modern research there and that's where I learned about them.




Applications are open for YC Winter 2020

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: