4 ms·

Both. When I start adding type annotations, I'm usually aiming for a speed-up but more often it leads to reorganization and rationalization of the code. The co

Both. When I start adding type annotations, I'm usually aiming for a speed-up but more often it leads to reorganization and rationalization of the code. The code becomes more streamlined and beautiful. The post below resonates with me. He calls it 'programming by teaching', where you gradually shape a program to solve your problem. I think of it as 'programming by learning', where the Lisp way of developing helps me learn about my problem. It's only when you have the final version of your code that you fully understand the problem by seeing its solution in front of you. https://news.ycombinator.com/item?id=11834887 https://news.ycombinator.com/item?id=11834887

catnaroek 10y ago
What I do can also be called “programming by learning”, but it has a fundamentally different flavor than what Lispers do. I present my ideas to the Poly/ML REPL as a hopefully coherent argument, and it tells me whether, at the very least, the argument is internally consistent. ML doesn't “know” about my specific problem domain, but it does know logic, and it's very good at nit-picking, which makes up for my human inability to exhaustively pay attention to an ever-growing number of tricky details. Furthermore, ML has all of nominal, structural and abstract types, which lets me “steer the reasoning” in the desired direction: (0) Nominal types correspond to primitive domain entities. (1) Structural types correspond to compound entities, built from simpler ones. (2) Abstract types regulate the interaction between different subdomains of a larger domain. The net result is that the REPL's feedback helps me identify those parts of the problem domain where my understanding is weak. Not only the REPL's feedback, of course. For instance, if my program contains unreachable code paths, it means that I haven't yet found the right abstractions. The philosophy behind this methodology is that: (0) The cost of having a wrong program is actually larger than that of having no program, because it takes too much effort to identify the wrong parts so that one can fix them. (1) When the size a program exceeds a certain threshold, it becomes impossible for ordinary human reasoning to determine with full certainty that a program contains no errors. Only formal logic can help, and only machines can do formal logic at a large scale. (2) It isn't practical to tackle large problems without a properly enforced separation of concerns. --- By the way, ironically, I never make an explicit type annotation, except perhaps, perhaaaps, at module boundaries. Figuring out the boring details of how to connect the pieces of a puzzle is a job for computers (type inference), not humans.

catnaroek 10y ago

What I do can also be called “programming by learning”, but it has a fundamentally different flavor than what Lispers do. I present my ideas to the Poly/ML REPL as a hopefully coherent argument, and it tells me whether, at the very least, the argument is internally consistent. ML doesn't “know” about my specific problem domain, but it does know logic, and it's very good at nit-picking, which makes up for my human inability to exhaustively pay attention to an ever-growing number of tricky details. Furthermore, ML has all of nominal, structural and abstract types, which lets me “steer the reasoning” in the desired direction: (0) Nominal types correspond to primitive domain entities. (1) Structural types correspond to compound entities, built from simpler ones. (2) Abstract types regulate the interaction between different subdomains of a larger domain. The net result is that the REPL's feedback helps me identify those parts of the problem domain where my understanding is weak. Not only the REPL's feedback, of course. For instance, if my program contains unreachable code paths, it means that I haven't yet found the right abstractions. The philosophy behind this methodology is that: (0) The cost of having a wrong program is actually larger than that of having no program, because it takes too much effort to identify the wrong parts so that one can fix them. (1) When the size a program exceeds a certain threshold, it becomes impossible for ordinary human reasoning to determine with full certainty that a program contains no errors. Only formal logic can help, and only machines can do formal logic at a large scale. (2) It isn't practical to tackle large problems without a properly enforced separation of concerns. --- By the way, ironically, I never make an explicit type annotation, except perhaps, perhaaaps, at module boundaries. Figuring out the boring details of how to connect the pieces of a puzzle is a job for computers (type inference), not humans.