(0) There is a single physical universe that contains all values.
(1) The role of types is to “carve out” fragments of this universe.
(2) Say you have two values `x` and `y` of types `A` and `B`. Because it is possible to form the union type `A | B`, to which both `x` and `y` belong, the only way to make sure `x` and `y` cannot be conflated with each other is to make them physically distinct elements of the universe.
On the other hand, abstract types make the following assumptions:
(0) Each type is a “world” of its own, defined in terms of its logical structure. The values of a type are a mere consequence of this logical structure. Hence, it doesn't make sense to try to “split” or “merge” types.
(1) It doesn't make sense to argue that an int is different from a string, because it's just as nonsensical as arguing that they are equal. What they are is incommensurable.
(2) Say you have type two different abstract types `A` and `B`. Because they could share an underlying representation type `T`, you cannot rely on values of different types having physically distinct representations.
---
Suppose we had a language with both union and abstract types. The contradictions between the assumptions behind union and abstract types would lead to hilarious consequences:
signature ERROR_CODE =
sig
type error_code
(* specification of operations on error codes *)
end
(* we use opaque ascription, so that the internal representation
* of error codes becomes inaccessible to external parties *)
structure ErrorCode :> ERROR_CODE =
struct
type error_code = int (* prosaic representation *)
(* implementation of operations on error codes *)
end
type union = error_code | int (* union *)
(* suppose we also have flow typing so that this example works *)
fun test (u : union) =
if u is error_code then
ErrorCode.printErrMsg u
else
printInt u
val _ = test 42
You'd expect this code to print the integer `42`, but it actually prints: ERR_DOUGLAS_ADAMS : The answer to the Ultimate Question of Life,
the Universe and Everything is the number forty-two.
Wasn't the fact error codes are internally represented as ints supposed to be unknowable to external parties?