[mbid]

You're describing my pet peeve with research in programming languages, or more generally use of abstractions in CS. What you're writing makes sense: Understand the structure of your problem, then think of similar problems you've seen before, finally try to abstract away details that are irrelevant for the solutions in each case. If you're lucky, all of these problems are an instance of one general one, and need to be solved only once. In your example, it's that IO and [] are both monads and thus share some structure.

What's often happening in PL theory, though, is that people start off with axioms/syntax and then mutilate the actual problem until it fits the syntax (still badly). That's how you get ridiculous stuff like "everything is an object" or "everything is a file". In PL theory, people will usually first make up some syntax/theory and then search for models. If physicists worked the same way, they'd write down random formulae and would then go out to find phenomena described by them. You'd probably read this comment on a cave wall.

[JoshCole]

Axiomatic formulations of a problem do not have the same goals as abstractions. They can appear similar on the surface, but one has to do with the laying of a foundation and the other is about problem simplification. One is about allowing great leaps in understanding after a great deal of derivation, the other about the reduction of work via problem equivalence. Criticizing someone for using an axiomatic formulation rather than a proper abstraction in programming language theory is like criticizing an architect for using pencil in laying his foundation on paper rather the much more appropriate cement at the construction site.

You don't get everything is an X because of axiomatic formulation. You get it for the same sort of reason that instead of spending ages describing the configurations of atoms in front of you, you throw all that out and call it a screen. Is everything still atoms? Yes! But we can call it a screen and that makes things massively easier to reason about and so we do it, because we like to reason well. But there are still benefits to thinking the other way, thinking from the very foundations. They are just different benefits, which is why we choose to think of problems from more than one perspective.

[mbid]

I didn't mean to critize all axiomatization but the concrete axiomatizations arrived at by PL research. In my opinion, one should start with a thorough understanding of the problem domain, and then try to come up with a syntax that allows expression of your intuition as faithfully as possible. Form follows function. Instead, I feel like PL research is often too focused on the concrete syntax considered, thus function follows form. Case in point: Building models for the syntax at hand is often an afterthought, done only to prove consistency. I'd argue that one should start with as precise an understanding of the intended models as possible, and then come with up with an axiomatization (thus, syntax) for the intended semantics.

For example, the notion of elementary topos has been invented because its creators wanted to capture the way Grothendieck toposes kind of behave like constructive sets. This I find very useful, and also the axiomatizations of elementary toposes. On the other hand, Martin-Löf type theory didn't have a formal semantics at first, then an erroneous one, and finally ~20 years later a kind of acceptable one. And its category of models is... not really interesting. Except for categories of assemblies, I don't know of a single model of ML type theory that's not also an elementary topos. And the interesting thing about assemblies is that they can be turned into objects of the associated topos... so yeah.

[joel_ms]

And yet MLTT led to Coq, Agda, Idris and Lean, while your ”PL practice” approach sounds like it would lead to, well, Go.

[theaeolist]

The "everything is an X" is what I call "foundationalism". It is a disease that started with Turing and Church, except that when they started it it was not a disease. But ever since people forgot that Y and "an encoding of Y as X" is not exactly the same thing. For some purposes it might be, but not for all purposes.

[marcosdumay]

Unsurprisingly, Physics get to decide what abstractions they use the same way developers decide what languages to create. They invent some notation, start describing everything they know on that notation, and if it's productive push it further and further until it breaks.

[fooker]

>If physicists worked the same way, they'd write down random formulae and would then go out to find phenomena described by them.

So, String Theory?

[mbid]

Kind of, from what I (complete physics noob) hear.