<story><title>Implement with types, not your brain (2019)</title><url>https://reasonablypolymorphic.com/blog/typeholes/index.html</url></story><parent_chain><item><author>_bxg1</author><text>Rich Hickey once said something (with regards to TDD) like, &amp;quot;We have guard rails on highways, but that doesn&amp;#x27;t mean we just take our hands off the wheel because the rails will keep us on the road. Guard rails don&amp;#x27;t know where we actually want to go. We drive the car where we&amp;#x27;re trying to go, and the rails are only there for when things go wrong.&amp;quot;&lt;p&gt;I think a version of this applies to static types as well. Even under normal circumstances, I&amp;#x27;ve noticed at times my own thoughts getting lazy when refactoring statically-typed code. I don&amp;#x27;t &amp;quot;load&amp;quot; as much of the program into my brain as I would otherwise; I just change the part I want to change and then fairly thoughtlessly fix all the type errors. I don&amp;#x27;t think this is a good thing. The OP takes this to an absolute extreme.&lt;p&gt;Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a &lt;i&gt;generative&lt;/i&gt; tool for writing logic where &amp;quot;you&amp;#x27;re not entirely sure how&amp;quot; it works.</text></item><item><author>q3k</author><text>This way of writing Haskell, from my experience, results in write-only code. While it&amp;#x27;s nice that the compiler helped you figure out which obscure operators to use for your code to actually compile, it sucks for the next person trying to find the bug in your code. And just because the types check out doesn&amp;#x27;t mean it&amp;#x27;s free from bugs.&lt;p&gt;Code is also meant to be read and reasoned about by humans, not just by the compiler.</text></item></parent_chain><comment><author>jerf</author><text>&amp;quot;I don&amp;#x27;t think this is a good thing.&amp;quot;&lt;p&gt;How good a thing it is depends on how right you are when you do it. If your language is statically typed, but not very well, then it&amp;#x27;s a bad thing. But it&amp;#x27;s not just abstractly a bad thing because you are a lazy person who didn&amp;#x27;t choose to do useless cognitive work, it&amp;#x27;s a bad thing because you may be wrong. To give a specific example, if your type system forcibly adjoins NULL to all pointer types, you can&amp;#x27;t afford to take your hands off the wheel when dealing with pointer types and neglect that case. You &lt;i&gt;must&lt;/i&gt; think about it when using pointer types.&lt;p&gt;On the other hand, if you take your hands off the wheel for a moment, but you perform only type system manipulations that you have good and correct reasons to believe won&amp;#x27;t affect the behavior of the underlying code... then what&amp;#x27;s wrong with that?&lt;p&gt;I&amp;#x27;m guessing you&amp;#x27;ve used the former type of language more than the latter? Me too. I think you&amp;#x27;ve turned the justifiable fear you feel in that sort of language into a heuristic, which makes it easy to then forget the underlying problems. But there&amp;#x27;s no &lt;i&gt;particular&lt;/i&gt; virtue to &lt;i&gt;having&lt;/i&gt; to understand more of the program to do a manipulation than having to understand less. Proof: If that was &lt;i&gt;always&lt;/i&gt; true, then that recurses on itself until you shouldn&amp;#x27;t ever make a change until you understand the whole program completely in your head at once (if not the whole system it is running on). Even if that&amp;#x27;s true, it doesn&amp;#x27;t matter; we humans don&amp;#x27;t have the cognitive capacity for that, we &lt;i&gt;must&lt;/i&gt; window our understandings.&lt;p&gt;It isn&amp;#x27;t just the micro task of refactoring one particular function; it&amp;#x27;s completely common for me to undertake a type-driven refactoring of code where &lt;i&gt;just&lt;/i&gt; the type-driven aspects are plenty to fill my cognitive window. Especially since I&amp;#x27;m usually in a looser language and I really have to watch those darned forcibly-adjoined NULLs. If I&amp;#x27;m somehow &amp;quot;obligated&amp;quot; to understand more, the result isn&amp;#x27;t that I&amp;#x27;m going to have that understanding, the result is that my hand will be tied and I won&amp;#x27;t be able to do that refactoring because it&amp;#x27;ll blow out my cognitive budget.</text></comment>
<story><title>Implement with types, not your brain (2019)</title><url>https://reasonablypolymorphic.com/blog/typeholes/index.html</url></story><parent_chain><item><author>_bxg1</author><text>Rich Hickey once said something (with regards to TDD) like, &amp;quot;We have guard rails on highways, but that doesn&amp;#x27;t mean we just take our hands off the wheel because the rails will keep us on the road. Guard rails don&amp;#x27;t know where we actually want to go. We drive the car where we&amp;#x27;re trying to go, and the rails are only there for when things go wrong.&amp;quot;&lt;p&gt;I think a version of this applies to static types as well. Even under normal circumstances, I&amp;#x27;ve noticed at times my own thoughts getting lazy when refactoring statically-typed code. I don&amp;#x27;t &amp;quot;load&amp;quot; as much of the program into my brain as I would otherwise; I just change the part I want to change and then fairly thoughtlessly fix all the type errors. I don&amp;#x27;t think this is a good thing. The OP takes this to an absolute extreme.&lt;p&gt;Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a &lt;i&gt;generative&lt;/i&gt; tool for writing logic where &amp;quot;you&amp;#x27;re not entirely sure how&amp;quot; it works.</text></item><item><author>q3k</author><text>This way of writing Haskell, from my experience, results in write-only code. While it&amp;#x27;s nice that the compiler helped you figure out which obscure operators to use for your code to actually compile, it sucks for the next person trying to find the bug in your code. And just because the types check out doesn&amp;#x27;t mean it&amp;#x27;s free from bugs.&lt;p&gt;Code is also meant to be read and reasoned about by humans, not just by the compiler.</text></item></parent_chain><comment><author>agentultra</author><text>&amp;gt; Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a generative tool for writing logic where &amp;quot;you&amp;#x27;re not entirely sure how&amp;quot; it works.&lt;p&gt;You might be surprised to learn that this is not only possible but something research is definitely working towards.&lt;p&gt;In a language like Agda, for example, when there is enough type information available the compiler can fill in the holes for you with the obviously correct implementation.&lt;p&gt;The idea behind program synthesis drives this even further. Using type level specifications we can automatically derive the programs that meet those specifications. This is useful because the language of types is much more concise than the language of terms. For sufficiently difficult problems it&amp;#x27;s much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code!&lt;p&gt;It&amp;#x27;s still early on for this kind of technology but projects like Synquid[0] are making good headway.&lt;p&gt;Dependent-type theory also forms the basis of interactive theorem proving in Coq and Lean[1]. We use something like holes as the basis of proofs. Haskell&amp;#x27;s typed holes are quite a bit more loose but to me it feels very similar to working with such a system. I propose to Haskell there there exists an expression that satisfies a particular type and then I use the typed holes to fill in my obligations to provide a proof. The hole is my goal and the available objects in scope are my terms. It is a very effective tool for solving hard problems.&lt;p&gt;[0] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.csail.mit.edu&amp;#x2F;research&amp;#x2F;synquid-synthesis-liquid-types&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.csail.mit.edu&amp;#x2F;research&amp;#x2F;synquid-synthesis-liquid-...&lt;/a&gt;&lt;p&gt;[1] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;leanprover.github.io&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;leanprover.github.io&amp;#x2F;&lt;/a&gt;&lt;p&gt;&lt;i&gt;update&lt;/i&gt;: Links</text></comment>