Great phrase from Conor McBride -- I like to think of types as warping our gravity, so that the direction we need to travel [to write correct programs] becomes "downhill".

I rely on the use of rich types to infer much of the software I write -- to just "derive" fragments of the software from its type specification, and get on with the interesting work. No room for hacks or misadventure to creep in, since there's only a few possible programs with the correct type.

And after years of richly typed programming, it is easy to forget how unusual - and luxurious - this engineering methodology is.
Shared publiclyView activity