Lambda the Ultimate

Verbose? Not necessarily — Lennart Augustsson has shown how the overhead of Haskell for expressing imperative code over actual imperative programming can be quite light.

Tortured? Maybe. I guess the difficulty a lot of people have had grasping monads suggests that.

Silly? No. "Monadically pure" is a valuable property, as I think QuickCheck has shown.

I think the trouble is that Haskell represents a kind of "bait and switch" - people got turned onto Haskell because of Backus' vision and the beauty of examples like the Bird-Meertens formalism (It's not a specification! It's executable code!), but the reality of much Haskell programming is quite different.

Monads are actually a lovely way of writing imperative-style code; they make the actual structure of the computation more apparent. Even candied up with Haskell's do notation, the distinction between binding a variable with let x = ... vs. x <- ... is useful. There are some annoyances that come up when writing imperative-style Haskell, but monads are a net positive if anything. Also, variations on the State monad make for a very elegant way of threading values through a pure computation with conditional branching; much less tedious than passing around explicit state parameters.

The problem is just IO, with its hidden magic powers. Within monadic code, the runtime conspires with IO to conceal The Horrible Truth from a computation. Nothing inside that computation can tell that it isn't running in a nice, happy, purely functional monad*, something like "State ReallyComplicatedVirtualMachine a" instead of "IO a", but from the outside we're faced with the fact that IO actions have no sensible mathematical meaning, which irreparably taints all such values.

The resulting combination of "computations internally indistinguishable from pure code" and "unrestrained reliance on stateful operations with incoherent semantics" is indeed a very roundabout way of basically writing the same impure code you would in any other language. But, it integrates easily with Haskell code that really is pure, and it's sufficiently useful and convenient that it undermines much motivation for finding semantically coherent ways to express I/O. Which, coincidentally, is what Conal Elliott is interested in, such as various approaches to functional reactive programming that he's worked on. Unfortunately, last I checked he hasn't single-handedly solved the problem (yet).

*It is said that, in the forbidden grimoire System.IO.Unsafe, there is an incantation, scribed in blood, to reveal the world as it truly is--but that fully comprehending the truth will surely drive a computation mad.

I am wondering if the problem here is simply methodological. You can't depend on really long pure computations to methodologically mean anything in practice. That's why OO Analysis breaks things up into a 'problem domain'.

Apart from that, I think the 'madness' really comes from a desire to embed more serious software engineering properties than 'purity' into code. For example, liveness conditions that state the lifecycle of some variable w/ respect to some FSM, and then the requirement that when FSM a is in state A, that FSM b must be in state B.

But I suspect the even harder case is the full composition Conal and Roly are talking about, perhaps best demonstrated by any 'serious' data mining GUI, such as a purely functional description of Miller Trees or Hyperion's ProClarity Decomposition Tree - and the reflective case where the data mining UI itself is data mining what aspect of the data the user should be looking at.

The heart of the matter, from my impression, seems to be the ability to speak about what a piece of code means, in a rigorous sense, instead of merely what it does--or worse, what you think it does. As long as one can retain that ability, many other nice properties all but fall into your lap. Semantically incoherent I/O is anathema to this, because each point of contact with the outside world has at least the potential to undermine your expectations of the others.

Clearly things work well enough, most of the time, for most people, but it's not a very satisfying state of affairs. Purity helps in Haskell; well-designed object oriented architectures are also helpful. By analogy, overuse of the IO monad is detrimental in Haskell akin to how flagrant disregard for the LSP tends to break meaningful semantics in OOP inheritance hierarchies.

On the other hand, while Conal's work is interesting and valuable, it seems to me that overuse of IO is less damaging than the unavoidable, nigh-universal presence of ⊥, made all the more galling because large chunks of code in most Haskell programs could be easily proven to never evaluate to ⊥ given non-⊥ arguments, yet there is no sensible way to encode this in the type system! But that's another topic.

...it is actually possible to represent a pure, total sublanguage within ML or Haskell, thanks to data abstraction. It is not, however, practical, not unless you really adore the point-free combinatory programming style. :)

module type PURE =
sig
  (* The basic idea is that we expose type constructors and values 
     corresponding to the objects and maps of the category representing
     the programming langauge we want to model. In this example, we'll
     do the simply-typed lambda calculus plus coproducts and natural
     numbers with primitive recursion -- i.e., Godel's System T. *)

  type ('a,'b) hom     (* The type of the hom-set, i.e. the type of morphisms *)
  type one
  type ('a,'b) prod 
  type ('a,'b) coprod
  type ('a,'b) arrow
  type nat

  val id : ('a,'a) hom
  val compose : ('a,'b) hom -> ('b,'c) hom -> ('a,'c) hom

  val one : ('a,one) hom

  val prod : ('a,'b) hom -> ('a,'c) hom -> ('a, ('b,'c) prod) hom
  val fst : (('a,'b) prod, 'a) hom
  val snd : (('a,'b) prod, 'b) hom

  val coprod : ('a,'b) hom -> ('c,'b) hom -> (('a,'c) coprod, 'b) hom
  val inl : ('a, ('a,'b) coprod) hom
  val inr : ('a, ('b,'a) coprod) hom

  val curry : (('a,'b) prod, 'c) hom -> ('a, ('b,'c) arrow) hom
  val apply : ((('a,'b) arrow, 'a) prod, 'b) hom

  val zero : (one, nat) hom
  val succ : (nat, nat) hom
  val iter : (one, 'a) hom -> ('a, 'a) hom -> (nat, 'a) hom

  (* The "escape hatch" to get a pure value back into the ambient
     language *)

  val run : (one, nat) hom -> int 
end 

module Pure : PURE =
struct 
  (* The implementation is just a pure sublanguage of Ocaml that
     implements the total language. Type abstraction ensures we 
     can never cheat and leak an impure function into our denotation. *)
 
  type ('a,'b) hom = 'a -> 'b
  type one = unit
  type ('a,'b) prod = 'a * 'b
  type ('a,'b) coprod = Inl of 'a | Inr of 'b
  type ('a,'b) arrow = 'a -> 'b
  type nat = int

  let id x = x
  let compose f g x = g (f x)

  let one _ = ()

  let prod f g x = (f x, g x)
  let fst (a, _) = a
  let snd (_, b) = b
    
  let coprod f g = function Inl x -> f x | Inr y -> g y
  let inl x = Inl x
  let inr y = Inr y

  let curry f a = fun b -> f (a,b)
  let apply (f, a) = f a

  let zero () = 0
  let succ n  = n + 1

  let rec iter zero succ n = if n = 0 then zero() else succ (iter zero succ (n-1))

  let run f = f()
end

Oh, thank you very much for this. This is extremely cool. I am going to have to study this carefully and let it sink in properly. After-the-fact, it just seems too easy!! [Which is exactly why it is so cool].

Now I need to understand how to mix this up with finally-tagless, so that an implementation of the PURE signature (or something close) can in fact be a partial evaluator or a program transformer. Then how to make this composable (probably easier with Haskell type classes that ML modules for that last bit).

LSP is a very weak principle in the context of OOP, and its connection mostly exists due to harmful papers/websites such as the ones by Oleg Kiselyov. See: Subtyping, Subclassing, and Trouble with OOP. I feel bad linking this article, because it is such a complete waste of time to read and will damage your brain if you read it. In short, LSP relates types on the basis of their semantics, whereas inheritance relates classes on the basis of their implementations. If you do not understand this, and believe your compiler can type check for you inheritance relationships, then you are pretty much screwed insofar as writing good code goes, because the compiler literally is not doing work for you that you are under the false impression it will perform for you. (William Cook has an excellent paper, titled "Inheritance is not subtyping", which discusses the pitfalls of assuming a congruence between subclasses and subtypes.) Put another way, the only meaningful semantics of inheritance is that of property acquisition. Put another way, OOP *class* hierarchies are not about inheritance at all, and any belief of such is a fundamental misunderstanding of OOP. OOP class hierarchies are about generalization/specialization relationships, and substitutability criteria does not necessarily have to be LSP (although LSP is certainly sufficient, it is not necessary).

Why the long digression?

Because!...

...Well-designd objects are autonomous, and therefore behave as finite state automata. Composing behaviors out of them therefore, I would argue, looks much like IO monadic interactions. The real key, as I've already stated, is that you want to be able to statically enforce that an object will not respond to a message if the message is sent to it in the wrong state. e.g., duplicating a read message on a linearly typed resource.

Composable I/O automata sequences are not a problem, and in fact is theoretically sound. What you, and other Haskell'ers, seem to object to, is the fact you cannot say anything meaningful about these I/O interactions. THAT is the problem. And I am saying in OO Analysis (pre-coding phase), we solve that through problem domain decomposition, because if we can't break things down into simple Moore state machines, we probably don't understand the problem.

You have grown far too fond of those four words. We should join a group.

Hi, my name is Dave. I'm also trying to avoid unnecessary use of the phrase "Just to be clear" in my writing. What is your name?

;-)

I'm not sure who is confused regarding your first paragraph, but this:

Well-designd objects are autonomous, and therefore behave as finite state automata.

sounds like a non-sequitur to me.

... meant "Lovecraft?" :-)

Verbose? Not necessarily — Lennart Augustsson has shown how the overhead of Haskell for expressing imperative code over actual imperative programming can be quite light.

Could you point me to that benchmark? I would possibly love to use it to deconstruct something I've been working on.

I was really hand-waving here: Lennart has posted a fair bit about how to economically represent C-like code in Haskell in his weblog. This is, of course, anecdotal, despite Lennart's good credentials as someone who does not overclaim, and it is quite probable that typical C code, from, say, the Linux kernel, encodes horribly into monadic style.

For a starting point, look at his 2007 post, Programming in C, ummm, Haskell .

My understanding is that monads aren't a fundamental problem in a pure system like Haskell. For one thing, lists are also monads. The things that do cause problems are the unsafePerformIO category of "functions". If you exclude those altogether, then you do get functionally composable programs. It's just that your program can't be "run" because that's an impure operation. "main :: IO ()" just remains what it is - the specification of a computation.

In other words, Conal is providing a different category of connection points analogous to "main :: IO ()" - MVC GUIs - that are composable in ways analogous to values themselves and how they compose with functions. Instead of "main", you can build up using automatically generated interfaces. Taking apart seems to be problematic though, unless you have some degree of code introspection like lisps have.

Conal is specifically talking about the IO monad, because it provides a pure facade for imperative code. He's concerned about how using the IO monad means that writing Haskell code means programming imperatively: this applies whether or not unsafePerformIO is used.

[skip] uh, we agreed. Guess I've been running up that hill for too long. Monads are ADTs which can be used to sequence (abstract) computations. There's no magic, it's even doubtful it's a good concept.

i'm curious to learn what is the top dog candidate for replacing monads.

If the quality of a monad what you're interested in is "sequencing actions," then there's nothing wrong with function application.

Function application, of course, being also known as the identity monad...

Sequencing is quite possibly the least interesting thing about monadic structure, and I doubt they're ever used just for that, except in the degenerate case of IO--wherein the monadic structure enforces sequencing with a rigor that regular function application doesn't really allow in Haskell without the use of onerous boilerplate code.

The interesting uses of monads are when you splice extra computation in between applications, or automagically pipe extra data along for the ride, or whatnot.

Function application, of course, being also known as the identity monad...

No.

Sequencing is quite possibly the least interesting thing about monadic structure,

Sequencing is what makes imperative code possible.

and I doubt they're ever used just for that, except in the degenerate case of IO--wherein the monadic structure enforces sequencing with a rigor that regular function application doesn't really allow

What's not rigorous about function application. I cannot possibly imagine it not being rigorous. You don't believe in math?

in Haskell without the use of onerous boilerplate code.

Duh, FRP, Event list processing, Combinatorial point-free pogramming. What's interesting about a monad exactly?

The interesting uses of monads are when you splice extra computation in between applications, or automagically pipe extra data along for the ride, or whatnot.

Which can be dealt with in a gazillion other ways.

Not a fruitful discussion. Open your eyes, learn some math.

Well, "interesting" is a subjective word, so at least this part of the discussion is quibbling over terminology.

Function application does not necessarily sequence events in a lazy language, and neither do monads. If you don't believe me, I have some examples in my post Fun with the Lazy State Monad, which uses the lazy state monad in a rather unusual way to implement Jones and Gibbon's breadth-first labeling algorithm. The list monad and the logic monad offer plenty of other examples that don't fit neatly into the term "sequencing".

Basically, monads can sequence things or enforce linearity or a number of other properties, but they don't have to either. It all depends on the exact nature of return and bind and the monadic actions in your effect basis.

Function application does not necessarily sequence events in a lazy language, and neither do monads

Which is actually a point which I made a few times, so a monad is nothing more than one template to do things in a certain way. Insisting that it is a good way is just akin to insisting that a list is the only and best manner of dealing with collections of data. It is not the only way, there are other manners, and general need not imply best, or practical, or fit for all purposes.

[And from my view, from all that I read, there are more wrong than right interpretations of what a monad is. Stupidity annoys me.]

i think people who are comfortable with monads and category theory are sometimes also comfortable with using and advertising the advantages of other structures cf. arrows, or the typeclassopedia, so it isn't as if everybody is stuck only on monads.

on the other hand, i think the majority of programmers have a hard enough time understanding monads alone, and so they are unlikely to then be able to / want to continue on that path into learning about and using other seemingly complicated and confusing and abstruse things.

(it is interesting that people have different kinds of complexity they are willing and i guess to some degree able to grasp. there are folks who love monads but might hate baseball statistics.)

I know a sales pitch when read one, just don't go overboard. I can't stand that it even passes scientific scrutiny. For the rest, some people excel at seeing things which are just not there - I guess it goes under the file 'feeling smart.' Now I like thinking by abduction as a scientific process, but if a metaphorical comparison to a mathematical structure fails on so many accounts, the structure -in its early days- wasn't even well understood by mathematicians, and programmers start believing it is some silver bullet, and it just closes their eyes to better manners of writing code, then drop the metaphore.

i was only trying to point out how i see the current reality of how people view monads, at the two ends of the spectrum: some people grok them and go on to even more things from category theory, whereas at the other end of the spectrum people are still befuddled by them.

in actuality, i know that i don't really grok monads, and i've only sorta barely used them. i can see how they are used and how they are useful. i don't grok what else might be good alternatives, i haven't thought about it enough or read about it enough. i'm always happy to see "xyz sucks" screeds because they tend to help me understand things more holistically. so i'm happy to try to learn more about your perspective vis a vis monads.

Well, as far as I can track the GHC tale, it all started out with one problem: We need to do IO functionally and pure. For that, the world state needed to be bound, and sequentially updated in a temporal fashion. The resulting thing was stuck into a typeclass, and -because of some superficial resemblance- was called an (IO) Monad.

Subsequently, all category theorists popped the champagne -since they found some use for theory,- and it has been a can of worms ever since to explain why monads matter (or not), what the difference is between a mathematical structure, and its uses in functional programming, where the analogy breaks, and why we shouldn't bother about it too much and just program the right abstraction instead of caring about superficial resemblances.

From a programmer's perspective, when dealing with encapsulated state, you just need start states and functions which take (part of) a state and any number of arguments and update that state according to some operator, returning a new state. You're free in choosing your operators -need not be bind- and how they should handle state, you're free in choosing whether to return a state, or something else, you're free in returning different states, you're free in so many things that even trying to reduce it all to monads (half of monads used in programming probably aren't since they don't satisfy monad laws, which doesn't matter anyway) just is illogical.

One thing where the IO Monad model fails, for example, is event-driven task-oriented _time bounded_ programming. It's easy to patch up solutions for that which don't necessarily resemble a monad, and give better, stringent, behavior.

If it will work better than what Haskell offers today, no idea. But that's exactly for scientists to find out, right?

[And from my view, from all that I read, there are more wrong than right interpretations of what a monad is. Stupidity annoys me.]

From my impression, many Ph.D.'s in computer science, who have wrote papers on applications of Haskell or tools for Haskell, have the interpretation that monads are all about sequencing. This viewpoint is probably the result of the fact that human beings reason by analogy and naturally assume consistency, unless they are experts. Experts are trained to have a fine eye for detail and have a much wider recognition of features and an accordingly stronger vocabulary for describing those features. This is true across all professions.

I don't think this is stupidity -- it is simply unfortunate ignorance. Most people don't even realize the extent to which, when they learn something, they grope for analogies. It is only after they've been doing something for 10,000 hours that they have a distinct understanding of what they are doing, assuming they progressively form better habits and increased understanding.

A Ph.D. student said to me not long ago, confessing, "I don't understand what the difference is between [Haskell's] Nothing and [C#'s] null." This honestly surprised the heck out of me, since he was incredibly bright. So I explained it. One feature explained, and hopefully as a result he has a much richer vocabulary for thinking about problems and explaining solutions.

If you find yourself repeating yourself, then set-up a tiddlywiki and use a plug-in for static site publication. Then simply link to your viewpoint when you feel annoyed. Letting annoyance build up gets me sometimes, too, but this is just one strategy I am actively taking to deal with it. I also find the writing process therapeutic.

I hoped someone would make the connection before I mentioned it — thanks!

The suggestion in the Hyland/Power paper doesn't propose a separation of IO from the heart of the program, but rather a taming of IO by separating it from the control flow aspects of monads: the point being that monads are "operationally polluted" approaches to algebraic IO.

The question is: what will the 2018 language standard for Bill, the functional language that is based on Lawvere theories in the way Haskell is based on monads, look like? Will it be Backusian in the way Conal wants?

I think Conal is saying something new here, even if he is only adding a little to what has been said before.

I'd like to encourage you to post links to similar discussions you have seen, though.