2 ms·
Code is also meant to be read and reasoned about by humans, not just by the compiler. And thinking with types helps you to do that. Satisfying the type checker
by agentultra 7y ago
Code is also meant to be read and reasoned about by humans, not just by the compiler.
And thinking with types helps you to do that. Satisfying the type checker doesn't guarantee a program is functionally correct but it does reject a large number of obviously incorrect programs from being considered. And with holes it can guide use towards the likely correct program.
From TFA:
> I’m not going to say that blindly filling in type holes always works, but I’d say maybe 95% of the time?
It's a tool. If you don't know how to implement something a good first approximation is understanding it's shape and filling in the holes. I think this is the spirit of what the article is demonstrating.
Writing the program so that it's clear is the next step. The final example, `zoop` is renamed to `foldr` once we realize what we're working with. This is how I often work with Haskell in practice: I know the types and shapes of values I need to produce and I work with the compiler to write an expression that fits the type. Then I rewrite for clarity and intent.