Category Theory for Programmers (2014) [pdf]

> all those things you're mentioning are side effects and are captured by the same concept, of representing effects by carrying a parameter through a chain of function calls

No. The state and environment monads fall under that rubric, but many of the others are far removed from what you're describing. You can't implement backtracking in a purely functional way simply by passing around an extra parameter, because backtracking affects the control flow. Continuations are even stranger—they're not even algebraic!

> I'm not backing down from the core claim that Moggi realised that CT monads are a nice formalization of side effects in pure functional programming

No, Moggi's paper was about formalizing the semantics of impure programming languages. It wasn't until Wadler that we started using monads to model side effects in pure functional programming. Please read the actual research before citing it.

> > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary.

> This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems.

It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please!

> There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away.

OP is not claiming that the benefit of type inference is that it automatically "types characters".

> I have yet to meet a static typist enthusiast that doesn't parlay in these lies

I don't think it's necessary to bring a moral dimension into this discussion. Let's keep it technical please.

> It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please!

Great, let's stay in a weakly typed language -- and give the smallest of examples. This is so easy to come by it should be obvious that extrapolating this up to real business systems greatly magnifies cost. Here's weakly typed Java:

   Function countChars = str -> str.length();

That's a function that counts characters in a string. It compiles. Now let's drop the types:

   Function countChars = str -> str.length();

That is a correct definition of the same function but it doesn't compile. The compiler needs information to carry out its proof.

This extrapolates to infinite more examples and the cost in building actual business systems is profound.

Now carry this to a strongly typed system.

The general claim is that type inference will allow the second form to somehow magically pass the compiler.

Not true.

The type inference requires `length` to be formally declared before the compiler can pass the program. I.e., the compiler must be told about the types somewhere.

In a dynamically typed language I can late bind `length`; ie the compiler doesn't need to be "told" something that I, the programmer, have got fully covered by my own measures.

But the compiler doesn't know this. I've already done my proof of correctness (as I should). But because the compiler does not have context, I have to tell it something that has no innate value to me and what I'm delivering -- it only has value to the closed-room of the compiler. This is hostile to productivity and serves only my early commitment to having a type prover guard my every move.