4 ms·
When I’m writing Haskell I still practice Test Driven Development but I usually start with Type Driven Development. The richer the type system, the more expres
by agentultra 7y ago
When I’m writing Haskell I still practice Test Driven Development but I usually start with Type Driven Development.
The richer the type system, the more expressive the propositions I can encode, and the easier it is to write a proof — a term with a type that matches the proposition. Leaving me free to write only the tests that matter and eliminating the need to start with specifying degenerate cases.
You can express concepts like non-empty lists, constraints on kinds and types which encode the propositions you’d normally test by example using unit tests. It’s simply not necessary in some cases to start designing programs with unit tests when you have a type system like Haskell’s (or Idris’, Agda’s, or Lean’s, etc)
- johnday 7y agoThe hidden thing about Haskell that makes it super-powerful for expressing safe programs (in my experience) is not only that you can express tight propositions in the types. It's that Haskell makes it very easy to write total functions over wider types. When writing OOP code you often start with a number of base assumptions about the input and build the code around them. With Haskell, you make no such assumptions initially and either encode total functions (most of them!) or tighten the types until they match the true system requirements. There are some Prelude functions which violate this understanding (`head` being a classic example). Writing code without these as much as possible makes your code almost guaranteed robust right out of the gate.