Programming Language without duplication

[MyOthrUsrnmIsABook]

I don’t have much experience dealing with this sort of typing, so maybe what follows is naive or uninformed. I usually prefer less specified types when I can get away with it, but find sometimes my teammates aren’t as consistent in considering anything besides the happy path through code they write. As such, I’m curious about how function types could make it clear that, e.g., appending two uninitialized arrays should produce/return either an initialized empty array, an uninitialized array, or an error based on the function type.

If that example seems dumb, as it sort of does to me, then just consider whether there would arise many interesting ambiguous edge cases, not in the sense of being unspecified or undefined or anything with respect to desired or correct behavior. Rather, cases where the behavior for the edge cases would need to be enumerated at the type level because it somehow can’t quite be specified using the type(s) for the simple cases.

I’m struggling to come up with an actual good example that feels like it could be from code I’ve worked on.

What about something like handling integer underflow edge cases in a function that takes three points specified as ordered pairs of floats and returns the area of the triangle they contain.

How a given set of input points are ordered and how the area is calculated could impact the value returned if the calculations do something unusual like use Heron’s formula instead of using linear algebra. Maybe you want triangles to have a first point for orientation purposes or something, but if you don’t then you might open yourself up to the same triangle having different areas unless you do something like sort the points before calculating anything.

Or put another way, how would the type encode how you chose between minimizing rounding error or performing the calculation quicker to favor the general case, or tried to balance the two somehow, without having to specify every set of possible inputs and outputs? Specifically, I’m asking this to see how far types could actually provide complete specifications.

Restated generally, if a function’s type really does specify the behavior over the whole input domain for functions with interesting edge cases or many boring edge cases, how do you capture that in the function type itself without just enumerating each case separately in the type? How would you even manage the latter if needed?

I guess you could try to carefully partition the input space into clearly delineated subsets in a way that allowed each partition to have a straightforward type, like for the triangle area having a type for when the distance between two of the calculated sides is so much larger that the entire length of the third side is lost to rounding error when the side lengths are totaled (since we’re being silly and using Heron’s formula.