Lambda the Ultimate

Phil's blog post is here.

By giving a comment, you document what the expectations of the type inference should be. Uncommenting the type annotation may end up restricting the genericity of the function. Or it may end up restricting the types of other functions in the unification process.

Basically he's saying that he wants genericity but with some comments about what the limits are when the code was constructed.

I only watched the first five minutes of Phil's talk (during which I learned how one pronounces "Principia"; I'm one of those readers who knows many, many words I've never heard anyone say aloud).

But your description of Phil's technique sounded like an experiment to me, intending to verify one's own independent reasoning, to get two readings on a value that should be the same, so each can verify the other. (So I thought your friend's question was similar to asking why double blind studies are better than open studies where expected results are known.)

There's a very good reason to do this, which isn't obvious from the academic result of getting a match after minimizing bias during an experiment. But even this part is valuable as a test cycle: a type match is the same as passing a runtime test in terms of giving you a data point on quality.

I've found that quality of code is often directly related to how much thought has gone into reasoning about whether it will work as intended, and the most effective reasoning is one that happens in your mind, and not in a tool. (A person considers many more ancilliary lines of reasoning than a minimal set necessary, and these end up informing other understandings about code, often giving insight into good and bad options like simplifications and risks.)

The other comments are essentially what I had in mind.

This relates to a concept I meant to mention in the talk. The "principal type" is the most general type of a given term. You might have over-specified the type signature, and won't otherwise see that. By commenting out the type first, the type inference algorithm in GHCI will give you the actual principal type, which might not be what you expected.