Things I Was Wrong About: Types

Re:Things I Was Wrong About: Types by cle on Sunday September 27, 2020 @05:00PM (#24610098)

There’s a continuum for sure. Type systems have their own kind of cognitive load, because you have to learn them, how to model your invariants in them, how to understand error messages, avoid common pitfalls, etc. Type systems are usually quite “general” and abstract, and that always comes with cognitive load. Quite often reading the code of a parametrically-polymorphic Python function is way easier than understanding the generalized polymorphism constructs of an advanced static type system.

There are times when the cognitive load of a particular static type system is less than that of a dynamic one, for certain classes of programs and audiences, and times when it’s not. This is fine and we should encourage development of both kinds of type systems and a shared understanding of how to pick the right ones for the job (which is a discussion nearly always missing in these debates).

[ Parent | on HN ]

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 ]

Re:Things I Was Wrong About: Types by pvorb on Sunday September 27, 2020 @05:30PM (#24610281)

I don't buy this "choose the right tool for the job" thing. I'd always advise you to choose the tool that your company has the most knowledge in. If there's a problem that cannot be solved in that programming language, then you can look for a better tool. But you shouldn't pick a language that nobody else understands, just to save a few lines or some time when doing the initial implementation - just to realize that you now have to constantly keep up the knowledge to be able to support it.

[ Parent | on HN ]

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

I consider that one of the most important criteria when picking the right tool for the job (if you're writing something to be maintained by other people in a company).

[ Parent | on HN ]

Re:Things I Was Wrong About: Types by pvorb on Monday September 28, 2020 @01:08AM (#24613162)

Okay, maybe. But usually this is not part of the description of "choosing the right tool for the job".

[ Parent | on HN ]