Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav08:immutable_abstract_data_types [2008/05/28 05:00] vkuncak created |
sav08:immutable_abstract_data_types [2008/05/28 05:03] (current) vkuncak |
||
---|---|---|---|
Line 27: | Line 27: | ||
Type safety is crucial for this to work: if we could cast another value into natSet using functions other than those declared, changing implementation could break. | Type safety is crucial for this to work: if we could cast another value into natSet using functions other than those declared, changing implementation could break. | ||
+ | |||
+ | ===== ADT Value Construction Consequence ===== | ||
In the sequel, the following consequence of type safety and abstraction will be relevant for us: | In the sequel, the following consequence of type safety and abstraction will be relevant for us: | ||
Line 32: | Line 34: | ||
**Value construction consequence:** Let $v$ be a value of an immutable ADT computed by a (potentially mutable) function in a type safe language. Then there exists a finite expression tree whose nodes are operations of ADT and whose leaves are either nullary operations of ADT or non-ADT values, such that this expression tree evaluates to value $v$. | **Value construction consequence:** Let $v$ be a value of an immutable ADT computed by a (potentially mutable) function in a type safe language. Then there exists a finite expression tree whose nodes are operations of ADT and whose leaves are either nullary operations of ADT or non-ADT values, such that this expression tree evaluates to value $v$. | ||
- | Note that this consequence does not rely on any properties of the function computing $v$. The function could be arbitrarily complex. The expression tree is the part of the computation that is relevant for computing $v$ (for non-ADT values, it need not keep track how they are computed). | + | Note that this consequence does not rely on any properties of the function computing $v$. The function could be arbitrarily complex, and need not terminate for all inputs, as long as we consider an evaluation that computed $v$. The expression tree is the part of the computation that is relevant for computing $v$ (for non-ADT values, it need not keep track how they are computed). |
In the previous example, we are sure that all natSet values computed in any code that uses the ADT are obtained by starting from empty and applying operations insert,remove,union. | In the previous example, we are sure that all natSet values computed in any code that uses the ADT are obtained by starting from empty and applying operations insert,remove,union. | ||