Things I Was Wrong About: Types

Re:Things I Was Wrong About: Types by throwaway894345 on Sunday September 27, 2020 @05:36PM (#24610315)

For the most part this cognitive load already exists in order to write correct programs. Types don’t just appear when a type checker is present. Type systems only add on the additional burden of needing to understand the formalization of that intuition. It’s not an insignificant burden, but it’s a much smaller gap than learning to intuit about programming correctly in the first place.

[ Parent | on HN ]

Re:Things I Was Wrong About: Types by cle on Sunday September 27, 2020 @07:03PM (#24610932)

It depends on what you mean by "correct". If it means "it does what I need it to do and I can move on with my life", then no, the cognitive load doesn't already exist, and formalized type theory in many cases adds an incredible amount of cognitive load.

I know that in many cases "correct" means a lot more than that, such as in proper software engineering contexts when building a program/system that needs to live and evolve for a long time among many people. I write that kind of software all the time, and I always use static type systems for it.

But I also write a bunch of ad-hoc, one-time-use programs, and I'm very glad that I don't need to reason about abstract type theory in order to parse a CSV file and add up some columns to send to a colleague.

[ Parent | on HN ]

Re:Things I Was Wrong About: Types by throwaway894345 on Sunday September 27, 2020 @07:40PM (#24611186)

No one is talking about abstract type theory; we’re talking about the intuition you use to write maintainable, correct software including CSV munging.

[ Parent | on HN ]

Re:Things I Was Wrong About: Types by cle on Sunday September 27, 2020 @08:09PM (#24611416)

I don’t care if my throw away CSV munger is formally safe/sound or maintainable. I care if it gives me correct results, once, as quickly and effortlessly as possible. Which is why very few people fire up GHCi/rustic/javac for that, but instead use awk/shell/Python or something similar.

[ Parent | on HN ]

Re:Things I Was Wrong About: Types by zeveb on Sunday September 27, 2020 @11:18PM (#24612638)

OTOH, sometimes the CSV munger one writes today is still in use five years later, when the input CSV has a UTF-8 character for the first time, and suddenly it crashes and no-one knows where the bug could even be.

[ Parent | on HN ]

Re:Things I Was Wrong About: Types by cle on Monday September 28, 2020 @09:41PM (#24623350)

UTF-8 support is completely orthogonal to static typing. There are dynamically typed languages that handle it great, and statically typed languages which have garbage support for it.

In general I know what you mean though. “What if this CSV parser turns out to be really important?” If you think there’s a high probability of that, do it in a statically typed language then. 99.9% of data munging I’ve done have been throwaway programs to answer a question to inform some decision or help refine a mental model.

[ Parent | on HN ]

Re:Things I Was Wrong About: Types by throwaway894345 on Tuesday September 29, 2020 @08:57AM (#24627168)

Frequently that answer is important and you want extra confidence that you calculated it correctly.

[ Parent | on HN ]