Yeah, things start to break down when you include bottom (and fix id = _|_ since it diverges).
I'm not sure exactly how to work with polymorphism in the function as subset model you described, but I'm guessing it would be something like this:
Let id_A ⊆ A x A s.t for all a ∈ A, (a, a) ∈ id_A.
If A = ∅, then id_A = ∅, which is exactly the result we'd expect, so I don't see any issue.
> the empty type can also be interpreted as the type of non-terminating computations
This is true, in a sense, but also a little bit misleading I think, since technically every type in Haskell is the set of terminating value with that type plus _|_
>If A = ∅, then id_A = ∅, which is exactly the result we'd expect, so I don't see any issue.
The issue isn't with the example you gave, but with the idea in general that being able to produce a term of a given type in Haskell means that that type is necessarily inhabited.
>This is true, in a sense, but also a little bit misleading I think, since technically every type in Haskell is the set of terminating value with that type plus _|_
Well, ⊥ is empty, so naturally every type is itself plus ⊥. In fact, that leads to an important observation, which is that any computation in Haskell could potentially be non-terminating, not just those with type Void—and so it's really not the inclusion of the bottom type that causes things to break down, but the ability to produce non-terminating computations (more specifically, non-coterminating, i.e. non-productive "lazy" computations).
Unfortunately, the alternative—making it impossible to produce non-terminating computations—is more than anything a matter of rejecting everything the compiler can't prove terminates, which is kind of limiting, termination being undecidable in the general case. On the other hand, the sorts of computations humans design are generally much more well-structured than an arbitrary Turing machine, and so probably much easier to prove (co)termination for.
I'm not sure exactly how to work with polymorphism in the function as subset model you described, but I'm guessing it would be something like this:
Let id_A ⊆ A x A s.t for all a ∈ A, (a, a) ∈ id_A.
If A = ∅, then id_A = ∅, which is exactly the result we'd expect, so I don't see any issue.
> the empty type can also be interpreted as the type of non-terminating computations
This is true, in a sense, but also a little bit misleading I think, since technically every type in Haskell is the set of terminating value with that type plus _|_