[rq1]

Just create dummy wrappers to make a type level distinction. A Height and a a Width can be two separate types even if they’re only floats basically.

Or another (dummy) example transfer(accountA, accountB). Make two types that wrap the same type but one being a TargetAccount and the other SourceAccount.

Use the type system to help you, don’t fight it.

[jpc0]

Do you really want width and height or do you actually want dimensions or size? Same with transfer, maybe you wanted a transaction that gets executed. Worst case here use a builder with explicit function names.

[rq1]

I don’t really understand your point there.

Sound type systems are equivalent to proof systems.

You can use them to design data structures where their mere eventual existence guarantee the coherence and validity of your program’s state.

The basic example is “Fin n” that carries at compile time the proof that you made the necessary bounds checks at runtime or by construction that you never exceeded some bound.

Some languages allow you to build entire type level state machines! (eg. to represent these transactions and transitions)