[<<][staapl][>>][..]

Sun Sep 28 09:31:47 CEST 2008

Union types

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
explosion.

[Reply][About]

[<<][staapl][>>][..]