Types #0: why they are nice

Photo by Georg Eiermann

Types #1: dimensional refinements

Photo by Alok Sharma

Types #2: effect handling

Photo by NeONBRAND

Types #3: constraints and contracts