Defunctionalization: Everybody Does It, Nobody Talks About It(blog.sigplan.org) |
Defunctionalization: Everybody Does It, Nobody Talks About It(blog.sigplan.org) |
For anyone else who got nothing from the title.
One the fundamental UX, copy-writing, devops/sysadmin and programming axioms is:
Don’t make me think
e.g., reduce cognitive load by making knowledge works as easy to digest as possible using simple, familiar/conventional, intentional and clear patterns.
And in my experience, the Haskell codebases I've worked in best exemplify the axiom you mention. I've solved so many problems by barely using my brain thanks to FP.
The main prerequisite is a good attitude.
Just wondering (out loud) how you formalize language semantics so they can be consumed... I know about grammar formalisms (bnf/ebnf, antlr, peach/xsd/asn.1...) but what is the lingua franca of language semantics? Except for latex papers...
Another popular tool I'm aware of for this is Ott[1], which lets you write a high-level semantics description, much like you'd write in a LaTeX paper. It can then compile it to Coq, LaTeX, etc for further work. Ott is probably a much better place to start without getting too far into the weeds, if you want to write real high-level sketches.
In general, I (unfortunately) don't think there's anything like a "library" of language semantics definitions that are easily reusable or anything like that. Modular definitions of semantics that can be reused like a library/API is basically a programming language abstraction problem, but I'm not sure what the current forefront of research on that is. In general, very few languages have fully specified machine-checked semantics, or even unproven ones.
IIUC Serval uses an interpreter built in Rosette (?) to build a Symbolic execution tool.
I think the author is working on a generic semantic tool to generate all kinds of language tooling automatically ; I'll be sure to follow his work.
Why "instead?" Knowing more math is good, but I think the author is doing his students a disservice. You don't need to memorize refactoring catalogs, but if someone says "maybe you should use a visitor pattern here" it's helpful to look it up and know what it means. It's not deep, but this is the vocabulary of the programming profession, not noise, and we're not going to switch to speaking in abstract mathematics just because some people like math or see a deeper meaning in it.
Defunctionalization seems like it might be a useful addition to the catalog.
First, even if you can teach group theory or category theory to an 8-year-old, if you wind up with an 8-year-old who knows category theory but can't add, is that a win? No, it isn't. They need to be able to add in a way that they don't need group theory.
But, second, you can't in any meaningful way teach category theory, or even group theory, to an 8-year-old. But you can teach them to add.
So again, I say, concrete first, then abstractions. First because they can function better knowing one concrete form and no abstract than they can knowing the abstract and zero concrete forms. And second, they are able to learn the most-useful concrete form younger and with less background than they are able to learn the abstraction.