RC W4D5 - Types: tests that you get for free?

If you search for “there is more than one way to do it”, the link that comes up top on Google is this one from WikiWikiWeb (which I learned is different from Wikipedia). It’s an expansive take on the expressiveness vs interpretability discussion. In English you could write ‘fast’ vs ‘quick’ vs ’swift’ and the meaning would be more apt in different contexts, which was my take away from this excerpt on Perl.

Its inventor, LarryWall, is trained as a linguist. He has this crazy notion that sometimes phrasing a sentence differently might make its meaning clearer…

Next I learned from the Python vs Ruby page that Ruby inherits from Smalltalk and Perl, believing that 'everything is an object' and ’there is more than one way to do it’, whereas Python inherits from the Algol family. I didn’t have Smalltalk and Algol in my categorization, and ChatGPT added them to the respective groups as expected.

Re: experimenting with Idris, it was not easy. I signed up to present as a way to force myself to talk about a distinctive facet of the language. I managed to weave a thread around types as 'tests that you get for free' (detailed below), but I'll need a proper project or use case as motivation to overcome the pain points and get deeper into the (experimental) language. Naturally it doesn't help it's not the easiest language to look up on Google (try it!).

For the functional programming study group, I read up (and later wrote on) effect systems. In the remaining pockets of time, I watched more Graham Hutton on Haskell, Bartosz Milewski on category theory, and Andrej Karpathy on generative models. 

The Friday presentation was titled 'Types: tests that you get for free?’. I started by talking about my last role where the main codebase was in TypeScript, the data stack that I mainly worked on was in Python, and initially my changes to the main codebase was one-off or piecemeal. I learned a lot about TypeScript when I later ported a section of the codebase into Python, and picked up a number of things on Python types too!

Python is dynamically-typed, but you can optionally type-annotate your code. For example, you can represent a list of ints as `List[int]`, and running mypy tells you if the code type-checks OK. If you represent your list as a `Sequence[int]`, however, mypy will complain when you try to make changes to the list (say by mutating an existing value or appending to the list) since `Sequence` is read-only.

At RC I’ve had the chance to go from Python to Haskell to (a little bit of) Idris. Suppose you’re trying to append an int to a list of strings. While mypy will complain when you run the type-check, the code will run successfully as Python is weakly typed. In strongly-typed Haskell, compilation will fail when you try to do the same thing.

With Idris you can go even further. The canonical example introduces a `Vect` type, which is like a list but has the length of the list in its definition. This means you can create a function that concatenates two `Vect`, the first on length n and the second m, and returns a `Vect` of length n + m. Suppose there was a typo and the first `Vect` is concatenated to itself, the compilation will fail since the lengths don’t add up.

In fact you can go even further with Idris to write proofs. The powerful type checker is able to run proofs by induction say. I briefly mentioned proofs but didn't follow up to talk about type-driven development. It's like test-driven development but with types. In Idris you get to go further in exploring the shape of the program (analogous to denotation design) and have the type checker to 'write the code for you'.

What’s also interesting is instead of types describing values, types in Idris are first class and exist in the same namespace as values. In Idris `if True then Int else String` run successfully but fails in Haskell.

To circle back to the title, I quoted Edwin Brady (the creator of Idris) from the book Type-Driven Development.

The difference is that, unlike tests, which can usually only be used to show the presence of errors, types (used appropriately) can show the absence of errors. But although types reduce the need for tests, they rarely eliminate it entirely.

The idea here is that when you write tests, you need to have a sense what errors you’re trying to guard against. With types, you’re ‘constraining’ the space of what’s possible. In the example of List vs Sequence in Python, these guardrails can even be more ergonomic (hence more likely to be added). That being said, neither tests or types provide fail-safe guardrails in all cases.