Lambda the Ultimate

Weeding out freshmen is a proud tradition...

I fail to see the connection. I'm talking about the state of programming not about school.

I think I have much the same experience.

But it also makes me sad. Mainly because when I see other people writing crappy code (that I have to live with or might want to wish to use) then I have to see if I can figure out how to get them to see when things are crappy on their own. So formalisms and reasoning and commentary and all that need to come together to improve things across the board.

If you start too concrete, abstracting later is apt to be a pain. If you start too abstract, concretizing later is apt to be a pain. There are also conceptual problems at both ends of the spectrum: too concrete and you get lost in details, too abstract and you're in a rudderless sea of "generalized abstract nonsense".

(On a side note, I'm amazed google gives me nothing domain-specific for "how many category theorists does it take to screw in a lightbulb?"; surely category theorists, at least, should be creative enough for that.)

Personally I enjoy the process of abstracting, but the process of concreteicising is much more of a pain. Possibly because many of the possible instantiations of an abstraction aren't things you'd /want/ to do. While a single concrete thing can embody many different abstractions simultaneously and is also something you may want to use later. I assume that the best place to start is the level that seems most real to the learner, and then expand both up and down to the more distant things.

Whereas you go from category theory to topos theory to intuitionistic logic, and there you are at Curry-Howard with zero additional cruft you then have to disavow/remove/explain away.

This is simply not true, or true at the level "a compiler is an arrow." I am not interested in people who can explain to me that compilers are arrows, I am interested in people who can explain how to implement compilers. Neither is there anything in category theory which helps you study set theory or different logics particularly well.

I dunno about anyone else, but I'm done with programming pop culture, and even academic computer science that just takes the inappropriate classical mathematical/logical foundations as givens. We know what the better frameworks are, and refusing to use them as foundations does a disservice to students and practitioners alike.

This is a straw man. Except for practitioners of category theory there is no-one who really believes that it can be a practical foundation for math. It's simply too sloppy, no grammar, no logic, nobody really knows what it does. Abstract nonsense.

People can do category theory, I don't care, but I don't think it adds a lot to most students skillsets, time they could have spend better learning other topics, and I don't think it contributes a lot to CS in general.

My impression is that category theory is useful for having shorter proofs in what would be set theory on topics like cs.

If I ever have to go to the foundation of set theory and write a bunch of proofs in order to write a computer program, you will be the first to know.

So yes, it's not a practical tool to a programmer any more than ZFC is useful in real life.

Better differential equations to implement a control system? Better Bayesian theory/fuzzy logic/neural networks? Better scheduling solutions for real-time systems? Better analysis of the performance of algorithms? Better guarantees over the properties of protocols? Better user interface theory? (I could go on for a while) ...

You talk about programmers, I talk about CS, and even within the foundations of CS it is a niche topic at best only suited for studying some algebraic properties or functional compositions.

It's not very useful to anyone.

It is probably useful to someone (as you state).

As an aside, is there really such a thing as "generically useful CS foundations" anymore? It seems to me that programming and even CS has already divided into many different topics, each with their own foundational core that has very little overlap beyond engineering/science/math basics.

Algorithms and their complexity, or feasibility, seems to remain central to almost all CS does. It's hard to come up with examples where complexity doesn't rear its ugly head.

Apart from that, I think most CS students are better of with general knowledge of applied math than foundational issues. Dijkstra once pushed an agenda that programmers should be able to prove everything, hence CS adopted the foundational research from the mathematicians.

But history seems to have taken another course than that what Dijkstra envisioned. Math is still important, a computer is an expensive calculator, but I am not sure CS students are better of being able to implement fluid dynamics simulators than anything else. Seems more relevant than being able to reproduce the Hilbert program.

> Neither is there anything in category theory which helps you study set theory or different logics particularly well.

If you don't know why this is spectacularly wrong, there's literally nothing I can do to help you.

> It's simply too sloppy, no grammar, no logic, nobody really knows what it does.

That's hysterical. Literally.

Prove me wrong and we can talk. Am I supposed to take your word for it? Where are the proof checkers based on category theory?

Addendum: To make my position clear again. Category theory is highly informal and that sloppy that I have described it here sometimes as an informalism. Math about math, I still haven't seen anything yet in category theory which has prompted me to change my mind.

> Prove me wrong and we can talk.

I don't have to prove anything to you. You're impervious to being informed.

> Am I supposed to take your word for it?

No; you're supposed to read nearly anything Bart Jacobs has written, and Categories for Types, and Practical Foundations of Mathematics, and the HOTT book, and... there's an extensive literature on this for you to avail yourself of. But I'm well aware that you won't, because it would subvert your extremely willful ignorance.

that you have made a grand statement with no backing. It is irrelevant whether you think marco is

impervious to being informed.

So why should I spend my valuable time reading anything from Bart Jacobs? What influence in practical terms has he had on anything? Since I have never come across him in my extensive reading - who is he and what does he bring to the table that would further my interest in trying to understand what he is presenting? What practical applications would his work provide me in doing anything for customers or clients?

If your responses are meaningful then I have an additional area in which I can expand my knowledge base.

Simple question: Tell me what you think a type describes in category theory. You don't know, right? No idea whether it's something syntactical or denotes some proper construct, no idea what that construct really would be in what semantic domain.

And I have about two dozen more questions I can ask you about the proper underpinning of category theory. Substitution principles? Assumed notion of equality? Do we have a category of categories, and what rules that out (syntactically)? What logic is used to describe it? Does an application denote a rewrite? ..

Okay. No idea what a type denotes in category theory. That's fine right? No idea what a type describes in ordinary math, anyway; something set theoretic. In a similar fashion you can still use category theory to study superficial properties of algebras. And come up with nice manners of describing abstract categories sometimes in a point free style, I'll grant you that.

But the only reason I think category theory has anything to do with foundations of mathematics is that it is the only setting in which algebras are studied in a particular manner, and that's about it.

So, you are a far cry from founding math on the basis of category theory. Stated differently, (I believe they are trying exactly that these days) they'll have a large amount of problems to solve.

Maybe that'll pan out. I don't have high hopes for it. And once you start defining what, for instance, types are, you have no idea whether all results still hold. It simply works that way.

People can do category theory, I don't care, but I don't think it adds a lot to most students skillsets, time they could have spend better learning other topics, and I don't think it contributes a lot to CS in general.

Probably the most discussed pure abstraction of the past 30 years was developed using category theory. Haskell definitely wouldn't be where it is without it.

Haskell definitely wouldn't be where it is without it.

Haskell: "I resemble that remark."

Haskell definitely wouldn't be where it is now without Monads. It would be in another place. As the first major language to embrace purity at all cost, they would have (sooner not later) come up with a nice alternative way of looking at things. I don't take it as a given that this other place would have been worse.

I think claiming we'd be in a better place would be a tough sell. Monads were already 12 years old by that point, type and effect systems were brand new and crude, and uniqueness types as found in Clean just didn't fit with Haskell's goals.

I'm not sure what else could have slipped into that place. Perhaps this? Oleg demonstrated that to have a nice translation with delimited continuations a few years later, and which would later become algebraic effects and handlers. That was a long road though. Would not having monads have accelerated that journey much?

I'm just observing that necessity is the mother of invention and we might be better off now if we hadn't had monads back then. Even if something like monads were discovered, we might have at least avoided monad transformers... :)

If you do a lot of functional programming a monad really is a naturally occurring construct. I already knew it before people popularized the categorical name. (In the sense that overloading a constant and function application to calculate within a certain frame was not a new idea.)

The route probably was that a popular FP construct was given a categorical underpinning. It usually goes that way. And I always found the categorical underpinning of monads nonsensical. But I guess that's known on this site, and I forgot half the reasons why.

The route probably was that a popular FP construct was given a categorical underpinning. It usually goes that way. And I always found the categorical underpinning of monads nonsensical. But I guess that's known on this site, and I forgot half the reasons why.

This is not right. The history goes roughly as follows:

1. Godemont invents monads in 1958, under the name "standard construction".

2. In 1963, Bill Lawvere applies them to model constructions in formal algebra -- basically, he works out how to use monads to model substitution in theories of languages without binders, like the formal language of monoids, groups, and rings.

3. In the late 1960s (roughtly 1968-1969), Dana Scott and Christopher Strachey invent denotational semantics. Initially, they work in very concrete models of languages (Scott's D-infinity model of the lambda calculus was initially defined in terms of complete lattices and continuous functions, and then weakened to CPOs).

4. Throughout the 1970s, denotational models of more and more effectful languages -- state, control, concurrency, and IO -- are invented.

5. As the complexity of the languages under study goes up, people begin using a variety of semantic structures -- not just lattices and domains, but also metric spaces and so on. To organize the structure common to all of these approaches, people begin using categorical methods. Michael Smyth and Gordon Plotkin's 1982 paper The Category-Theoretic Solution of Recursive Domain Equations is a good example that remains relevant to this day. (I learned how to solve domain equations from it, in fact.)

6. In 1989, Eugenio Moggi recognized that there was a common structure to how effects are modelled in semantics -- namely, monads -- and showed how this worked for a very wide variety of effects.

7. Shortly after publication of this work, Phil Wadler recognized that Moggi's semantics could be used to replace Haskell's IO system (which had a very clumsy CPS-based API), with a much simpler monadic API. See his 1992 paper The essence of functional programming. This led to the adoption of monadic IO in Haskell 1.3, in 1996.

8. In his PhD thesis, Andrejz Filinski proved a representation theorem for definable monadic effects -- he proved that delimited continuations (or alternately, full continuations plus state) could be used to implement and definable monadic effect.

9. Shortly after the turn of the millenium (2001-2003), Gordon Plotkin and John Power proposed using Lawvere's idea of modelling substitution on trees with monads to turn an algebraic theories of effects directly into a categorical semantics of effects.

10. A few years later, Matija Pretnar (first with Gordon Plotkin and then Andrej Bauer) made use of Filinski's representation theorem for effects to invent "effect handlers". The idea was that you could separate the definition of an effect from its use by client code, and dynamically control how effects get implemented. See Sam Lindley, Ohad Kammar and Nicolas Oury's 2013 paper Handlers in Action.

So far, the theory has preceded the application, not just once, but *twice*. Furthermore, I'm pretty sure this will happen at least once more -- in his work on call-by-push-value, Paul Blain Levy has shown how the decomposition of a monad into an adjunction naturally splits semantics into a living in a pair of categories, one for values and another category of algebras for effects, which is sure to shape the design of the next generation of functional language.

I'd thought the point intended was that monads as a practical technique are separate from the mathematical structure and can and do occur to programmers without being provided to them. The history of the mathematical ideas is the most documentable part of the history, but not necessarily the whole story. I don't mean to take sides on the point; just hoping to facilitate clarity. Of possible relevance: You Could Have Invented Monads! (And Maybe You Already Have.)

Well. It's somewhat of a natural occurring construct like fold. I.e., if you start doing FP naively then you naturally start of with lists, and at some point you realize, if I have a list then it's natural to fold it with an operator. Take some list [2, 7, 3] then a lot of computations will have the form (2 + (7 + 3)) for some operator +.

And then you start thinking about what you'ld do with an empty list, and how you'ld fold a list with an operator which associates differently, etc. And how you'ld fold trees. The idea of folding a structure naturally occurs and naturally generalizes into a lot of different directions. (And the dual also naturally occurs, if you can fold you can also unfold, that's a really trivial realization.)

And the same is true for the monad, at least that definition of monad such as it was popularized by Wadler, and a number of other people.

I.e., I would call naturally occurring some central realization that fundamental to functional programming are values and functions. So if you overload that, the construction of a constant and function application, you can generate arbitrary calculations within any domain.

So, IF you define the construction of a value within a domain with some abstract injection operator (unit of type 'a -> M a'), and overload function application with some abstract function (bind of type '(a -> M b) -> M a -> M b'), THEN you're set to do any computation within an arbitrary domain M. (If you erase M in the types you see you simply overloaded the notion of constant construction and function application.)

With a bit of twiddling with types the monad popularized in Haskell is simply a naturally occurring construct; a lot like fold, map, filter are.

I do agree category theory takes that notion further, but also at the expense that you need to understand that (steep to understand) framework and that framework seems to imply you need to abide to the algebraic laws seemingly required by that theory. Whereas I would say one has simply overloaded constant creation and function application for some specific domain M, and you're free to abuse that idea further in any form you see fit as a programmer.

(The latter is what I don't like about category theory. It seems to shoehorn practitioners into a certain manner of doing things. If I look at folding a tree I am going to fold left-to-right and right-to-left as if it was a list (every container is a list), but also along its algebraic constructors, and also depth-first, and breadth-first. Similarly, for monads, it often makes a lot of sense to approach some calculations algebraically and define multiple binds for a specific domain, for instance.)

Shouldn't we let all sides inform each other in a melange that gives us a richer result than any single approach would have? The number of non-formalized things in the world that people do and then end up with broken horrible shyte is beyond measure, and I for one love it when somebody smart takes the time to formalize some things so we can know wtf we are actually doing and what the ramifications are. On the other hand, of course I don't want ivory tower constructs to be obtuse and basically non-performant. Blend the strengths. I would never throw anything out. I might not have time to learn it, but I am always extremely chuffed when somebody else brings whatever they can bring!

I mean, that's one of the main reasons LtU is so precious to me: the depth and breadth and variety of insights that can come together and interplay here!

Hey, you are the audience and you're supposed to applaud the party line! Otherwise, you might disappear overnight and the next day people will start quietly inquiring where you went.

Quietly inquiring? Who would dare? If someone is disappeared for bucking the party line, cautious citizens will play along, surely?

It does seem we may be at risk of overdramatizing, doesn't it.

Just wait and see what will happen once I am in power.

I went through 6.001 near the beginning, when it was photocopied Lecture Notes.

Alan Kay founded a group in the late 2000s to work on the "right math" for radically simplifying software, based on choosing appropriate mathematical formalisms, among other things.

They implemented a networking stack in something like 2K of RAM.

I haven't seen the PI's Final Report - it may still be "in preparation", but the NSF funded Alan Kay's "Viewpoints" project for five years.

You can see artifacts at VPRI.org, including papers written as recently as 2017.

I'd love to find a funding source to get Alan Kay, Gregor Kiczales, Alan Borning, and some other folks together to collaborate on a "Unified Programming Environment" just to see how far you can take the VPRI's ideas from research to implementation.

Syntax is fleeting, but Meta-Object Protocols seem useful in this effort. I haven't read about them recently enough to know if they are a complete solution.