TL;DR: Make very specific types so nobody can use the wrong functions for them.
If you hang out in the Elm community a bit, you will know of a preference for creating your own enum types rather than using existing isomorphic ones. E.g., if you have a color that can be black or white, it is customary (no pun intended) to create a new type:
type Color = Black | White [...] color : Color
rather than using the standard boolean type:
colorIsBlack : Bool
despite the later requiring fewer lines of code.
I even had to look up if Elm uses
Boolean because I never frigging see it.
The main reason given for doing this is that it makes code easier to understand, but this is not the only argument.
If you use the same types for isomorphic data, e.g. you use a boolean rather than a color in the example above, that proof will only hold up to data isomorphism, not semantics.
A somewhat contrived examples:
If you're taking into account relativity theory, you should not be able to add up two velocities (speed of light being a maximum and such). But if you just use
Float as the type of a velocity, you do have a proof for correctness of such an operation. Indeed, it is correct as far as data isomorphism is concerned, but not correct in terms of semantics.
You could, instead, define your own type for velocities and the functions that come with it. It'd look a little bit like this in Elm:
module RelativityTheory exposing (Velocity, Energy, accelerate) type Velocity = Velocity Float type Energy = Energy Float accelerate : Energy -> Velocity -> Velocity [...]
By not exposing the inner structure of
Velocity, as you would by exposing
Velocity(...), you prevent any future error by you or your team-mates. Unless, you know, they try hard enough and actually modify the exposition.
The concept is similar to encapsulation in OOP principles.
More common examples in which these errors happen all the time: is a distance in km, miles, m, feet? Is a rotation in degrees, radials or turns? What is the encoding for this string?
Semantic type differentiation can help solve these problems.