The inhabitants of such a type are only used for their type. This might seem pointless but this allows us to symbolically execute a function proving its termination.

Think of TypeScript’s literal types, then think of Scala’s path-dependent types, if you go a little beyond them, you have expression types. They are singleton types with its only possible inhabitant being the result of the expression specified.

With union and intersection types the possible combinations are endless.

As you are propagating important objects, e.g. one representing the application state, or a context object, you never have to explicitly provide them. If need be just pull them out of the hat with the the-expression.