Sometimes people talk about how type checkers in languages with expressive types donât just help avoid errors, they help you design your program. I imagine this might seem far fetched to those who havenât experienced it, so I thought Iâd share an example
Iâm working on a change to the purescript compiler where I want to store a typeâs roles in the type checking environment. This environment contains, amongst other things, a map of type names to information about that type
This information contains things like the typeâs data constructors, its kind, what sort of type it is (a variable, a data declaration, a type synonym, etc)
I initially tried changing the type information so that roles are always stored no matter what sort of type we are dealing with. The compiler told me which bits of the program I needed to update, so far so good.
I then realised while making these updates that I was having to come up with nonsense role data in quite a few places, which is often a sign that your data definitions are wrong
Went back to the data definitions and realised that I should only be storing this additional role data in two of the five possible cases, whereas previously I was storing it in all of them
Made that change, compiler again tells me everywhere I need to update, I no longer need to come up with nonsense data anywhere, everything works

It occurs to me that this example might not make a lot of sense to people who donât already do typed FP, which is a bit of a shame since I guess theyâre the target audience..?