Live data from Hacker News

Monads and Intensionality – Lucid is not an aberration

billwadge.wordpress.com

21–30 of 38 posts

Re: Monads and Intensionality – Lucid is not an aberration

#21
I find this entire discussion to be indicative of a deeper disconnect within "programming culture" [insofar as such a thing exists]. Broadly, it seems to me there are are (a) folks who value mathematics and the ability to reason about programs using mathematics, and (b) folks who do not see the value of being able to reason about programs.

I personally fall into the (a) camp, since I work on compilers and formal verification. Monads are mathematically useful when trying to define the semantics of a programming language. This mathematical usefulness translates into useful API design [which I personally see as the hallmark of all functional programming techniques].

On the other hand, if one does not care about or want to abstract over a very generic notion of a side-effect, yes, monads are useless. You can go your entire life without needing to know what one is. And that's okay.

Why does side (a) side feel the need to pressure side (b) into learning all of their mathematical tools? Why does side (b) see side (a) as "being difficult" or "being obtuse on purpose"?

As far as I can tell, the two groups do not even share the same axioms about how we should build and reason about programs. Monads are a red herring.

- Real world example of where monads are used to reason about programs: Inside the VE-LLVM codebase, which provides a formal model of LLVM in Coq to prove certain properties of certain algorithms used with LLVM corred, a monad is used: https://github.com/vellvm/vellvm-legacy/blob/e4c22d795974ba7.... Much of the reasoning around sequential side-effecting semantics is phrased in this language.

Re: Monads and Intensionality – Lucid is not an aberration

#22
post #21

I find this entire discussion to be indicative of a deeper disconnect within "programming culture" [insofar as such a thing exists]. Broadly, it seems to me there are are (a) folks who value mathematics and the ability to reason about programs using mathematics, and (b) folks who do not see the value of being able to reason about programs. I personally fall into the (a) camp, since I work on compilers and formal veri…

We don't see the value in it because as of yet nobody has explained what the value is in an accessible way. That link, for example, is completely incomprehensible. Had you not mentioned what it's for, I couldn't even venture to guess as to what it does. Even with a description, I still don't know what it actually does, why it's structured that way, or what value there is in it.

From our side of the fence, FP concepts appear dense and obtuse the way they're currently explained. Until that changes, we'll remain divided.

Re: Monads and Intensionality – Lucid is not an aberration

#23
post #16

Earlier quoted context omitted.

Well, this shows one simplistic partial syntactic solution to a few common problems. Partial because it does not handle errors in the continuation example, and simplistic because it only works at the function level, it's not clear how this would look like when 'distributed' through a large code base, like cross-cutting concerns typically are. Not to mention, it's not clear how to compose all of these separate solutio…

> Well, this shows one simplistic partial syntactic solution to a few common problems. It's not just syntactic - the different cases genuinely do implement a common interface. > Partial because it does not handle errors in the continuation example Nor does the non-monad version, so it's a fair comparison. > simplistic because it only works at the function level, it's not clear how this would look like when 'distribut…

> It's not just syntactic - the different cases genuinely do implement a common interface.

Do notation is a syntactic solution, it is not an object of the runtime.

> Nor does the non-monad version, so it's a fair comparison.

The initial version does explicitly handle errors. The async/await based version also handles errors (any exceptions thrown by intermediate functions will be thrown by whoever is trying to use the results). What will the do-notation continuation version do with any errors returned by the intermediate functions?

> Sure, but again, a problem that exists even more strongly if these are implemented as (non-monad) language features (e.g. if my language has both continuations and exceptions, what happens when some continuation-based code throws an exception).

Not really - it is usually very clear how exceptions integrate with other control flow features such as continuations or, much more easily, promises or async/await (full continuations a la scheme call/cc happen to not work with exceptions, but they break any other control flow feature anyway, so that's not very surprising).

> The point is that you can get rid of a whole bunch of complex language features and language keywords, and write everything in terms of plain functions and values (in particular, the result is that you can refactor fearlessly because everything follows the normal rules of the language). You don't have to look at anything large scale to see the benefit of that.

I completely disagree with the idea that language keywords make refactoring difficult in any way, or that a language with less syntax is always easier to work with. Even the designers of Haskell disagree with this, as they have included both do-notation and list comprehensions, instead of letting programmers simply use bind and return. Even in Lisp, which doesn't have any syntax sugar in the base language, designers always add DSLs and Reader macros to add syntax back into the language.

Re: Monads and Intensionality – Lucid is not an aberration

#24
post #21

I find this entire discussion to be indicative of a deeper disconnect within "programming culture" [insofar as such a thing exists]. Broadly, it seems to me there are are (a) folks who value mathematics and the ability to reason about programs using mathematics, and (b) folks who do not see the value of being able to reason about programs. I personally fall into the (a) camp, since I work on compilers and formal veri…

We don't see the value in it because as of yet nobody has explained what the value is in an accessible way. That link, for example, is completely incomprehensible. Had you not mentioned what it's for, I couldn't even venture to guess as to what it does. Even with a description, I still don't know what it actually does, why it's structured that way, or what value there is in it. From our side of the fence, FP concepts…

I think what you have to understand is that monad is quite an abstract concept. It is possible to give a specific example of a monad, but from the specific example, you won't fully understand it.

Here's the first sentence in the documentation for Java's Comparable interface: "This interface imposes a total ordering on the objects of each class that implements it."

This assumes people know what a total ordering is. Total ordering is an abstract mathematical concept, not really more or less abstract than a monad. Clearly then, people don't have problems grasping abstract concepts. They just learn the definition and possibly bunch of examples and they're done.

I think the real divide happens because people in programming praxis are simply skeptical to the claim that monads are a useful abstract concept to learn and use in programming. Many years ago, some of them probably thought they don't need to know what a total ordering is.

I don't think anything can be done with the skepticism other than either take the claim at a face value, and accept that monads are a useful concept, or verify that claim by learning Haskell for instance.

Re: Monads and Intensionality – Lucid is not an aberration

#25

Earlier quoted context omitted.

We don't see the value in it because as of yet nobody has explained what the value is in an accessible way. That link, for example, is completely incomprehensible. Had you not mentioned what it's for, I couldn't even venture to guess as to what it does. Even with a description, I still don't know what it actually does, why it's structured that way, or what value there is in it. From our side of the fence, FP concepts…

I think what you have to understand is that monad is quite an abstract concept. It is possible to give a specific example of a monad, but from the specific example, you won't fully understand it. Here's the first sentence in the documentation for Java's Comparable interface: "This interface imposes a total ordering on the objects of each class that implements it." This assumes people know what a total ordering is. To…

Therein lies the problem. Until a Feynman with the skill to teach this in an accessible way takes on the subject, we'll remain at an impasse. This is really a UX problem.

"If you can't explain it simply, you don't know it well enough"

- Albert Einstein

Re: Monads and Intensionality – Lucid is not an aberration

#26

Earlier quoted context omitted.

> I don't understand why having a formal model for that commonality is so important. So generic libraries can be built and abstracting frequently used operations over many different data types. I've never implemented a monad myself outside of a toy project and am by no means an expert, but it's quite nice to be able to transfer certain knowledge on lists to options or futures. Similar to generic interfaces like a col…

Sure, but what generic libraries can you meaningfully built above optional, list, either, futures? Do-notation is one, but what else?

There are a lot of simple examples right in `Control.Monad`. As soon as I know that something provides the `Monad` interface, I know that I can use things like `mapM`, `foldM`, `replicateM`, `filterM`, `forever`, `sequence`, `zipWithM`, the list goes on...

Certainly not all of these are useful in every case - eg. `forever` needs your action to do something or you're just hanging forever.

But it's a toolbox that's easy to reach for, and which applies to a large pile of things. And when you can structure a new function only in terms of things in that toolbox, you've added another thing to the toolbox. See, for instance, `monad-loops` for more.

Exploring pairs of utility function and Monad instance can be interesting, asking (eg.) "what does `unfoldM` mean when I use it with `State`?"

Re: Monads and Intensionality – Lucid is not an aberration

#27
Nice read. I'm not familiar with Lucid, so invocations of "fby" and so forth went over my head, but finding that there's an abstraction available to encapsulate and explain a lot of behaviour in a consistent way is always a good win.

The "output monad" described is usually called the Writer monad - you can append to a log, but you can't do anything based on what was in it. It can be generalised from strings to any monoid - a domain that has an empty value and an associative concatenation function.

The IO monad, as another commenter said, is a kind of state monad where the state is something ineffable from within the computing environment: it's the state of the world outside the program. But there's no need to rush to trying to fit the IO monad to this model - we can start with the "reader monad".

An element of D* for the reader monad is a function from an element of some specified domain R to an element of D. The mapping from D to D* is a constant function that produces D no matter what the argument to the function in D* is. D's elements are functions from R to D* so the collapse is function composition and therefore associative. Likewise, f* from D* to E* is function composition, which composes, obeys the embedding of D into D* and since both collapse and embedding functions is function composition f* * (s')V == f* (s'V).

The reader monad is sometimes called the environment monad, because there's some environment (the value from R) that is available to all computation. The key thing it gives us for this article's model of monads is that elements of D* don't have to just be pairs, they can be functions.

Sort of combining the Reader and Writer monads gives us a monad where an element of D* is a function from an element of the domain S to a pair from (D, S). The embedding from D to D* is the function that copies its input state to its output pair. The collapse from D is composition with application. An element of D* * is a function S -> (D* , S), or S -> (S -> (D, S), S); apply the function in the pair to the state in the pair and you get S -> (D, S). D* * * is the further nesting of this structure, S -> (S -> (S -> (D, S), S), S). Evaluating this is associative: either way you will pass the initial state through each function in the same order to get the final output state. Embedding a function also satisfies the laws; effectively it will transform the final output D and leave the state S alone.

The collapsing of State to ensure its functions are always evaluated in the same order is how the IO monad provides sequentiality of effects. The state is "everything outside the program" - the user, the keyboard, the network, the operating system, even parts of the interpreter state that are not typically open to program inspection, perhaps allocations or bit-level representations.

An element of D* for the IO monad can read from the state of "everything outside", seeing whether the operating system has a character in its console input buffer perhaps. It can modify the state of "everything outside" by writing a character to the OS console buffer. And it preserves the order of these things because of how collapse is defined.

It also needs a magic interpreter that can provide the initial state of the world and maintain it as the program updates that state, along with magic primitives that can make changes to an ineffable "real world" state.

Re: Monads and Intensionality – Lucid is not an aberration

#28
post #9
post #2

It's unfortunate that so many people in the software profession have a negative attitude towards these concepts. Despite its unfortunately alien name, monad is a great abstraction for patterns that come up often in this field. > So what is the IO monad, the most famous of them all? IO is the State monad where the state is the entire universe.

> IO is the State monad where the state is the entire universe. Maybe in the early days, but that doesn't really describe how it works these days (in particular, async exceptions). In practice it's been used as a "sin bin" type for any side effect that we don't know how to model nicely.

Are you referring to the argument that Haskell's IO type is insufficiently granular to distinguish between something like erasing a disk and something like catching an async exception, or that the language's first-class feature set should be extended to things like async exceptions so they don't need to be part of "the rest of the universe" ?

Re: Monads and Intensionality – Lucid is not an aberration

#29
post #7

Earlier quoted context omitted.

Wouldn't infinite streams more naturally form a comonad than a monad, though? They're coinductive types.

Depends how you're using them. Apparently Lucid finds this "diagonal" approach to streams - which is not the normal way of streams in most programming languages - to be useful, in which case the monad model is a good fit.

How else could you combine infinite streams?

Re: Monads and Intensionality – Lucid is not an aberration

#30

Earlier quoted context omitted.

We don't see the value in it because as of yet nobody has explained what the value is in an accessible way. That link, for example, is completely incomprehensible. Had you not mentioned what it's for, I couldn't even venture to guess as to what it does. Even with a description, I still don't know what it actually does, why it's structured that way, or what value there is in it. From our side of the fence, FP concepts…

I think what you have to understand is that monad is quite an abstract concept. It is possible to give a specific example of a monad, but from the specific example, you won't fully understand it. Here's the first sentence in the documentation for Java's Comparable interface: "This interface imposes a total ordering on the objects of each class that implements it." This assumes people know what a total ordering is. To…

> Clearly then, people don't have problems grasping abstract concepts. They just learn the definition and possibly bunch of examples and they're done.

I think the crux is explaining how the abstraction is useful. The Comparable interface doc explains it in the very next sentence: Lists (and arrays) of objects that implement this interface can be sorted automatically by Collections.sort (and Arrays.sort). Every Java programmer can understand this and see its purpose

The difference is that in Java and most other languages abstract mathematical concepts are treated as means to an end, not a goal in itself.

Post reply on HN