Sun Sep 28 09:31:47 CEST 2008
One could see disjoint union types as a means to control conditional
branching by keeping its effects local. Unadulterated dynamic
"decision making" makes static analysis untractable since different
branches of a "case" statement might have a completely behaviour.
Union types with corresponding exhaustive "case" statements control
this exponential explosion of possible paths through the code by
joining branches back together: at the type level, each branch does
essentially the same thing, allowing the identification of a union ->
union map as a "local conditional branch" construct.
So in essence: one puts in a little bit more effort to design types
(approximate behaviour) in order to be able to prove things about the
behaviour of a program without executing it. An essential tool to
make this practical when conditional branching is present is to
abstract conditionals as union types, avoiding behaviour search space