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