On Fri, Jun 5, 2015 at 3:47 AM, Keean Schupke <ke...@fry-it.com> wrote:
> My point was you do not want assertions on types, abstract or not. The > assertions belong on the functions, as it is the algorithms that have the > requirements not the data. > I think that comment is insightful, but not always correct. Think of this, for a moment, as a precondition/postcondition sort of problem. There are some pre/post conditions that are sanity requirements of the type. These need to be maintained by all functions/algorithms that manipulate objects of those types. Because they are properties of the type, the most sensible place to attach them is at the type definition. One example of such a type is an integer range type. All instances must satisfy the range constraint, even though the underlying representation chosen for the machine may be capable of representing other values. There are other pre/post conditions that are requirements of the algorithm. For example, it is a precondition of integer divide that the divisor must not be zero. This is a sanity requirement of the algorithm, but it is not a sanity requirement of integers generally. It seems to me that pre/post conditions of this form are most logically associated with the algorithm that requires or produces the condition. Both kinds of properties are ultimately properties that are required and maintained by algorithms. In that sense, what Keean says is correct. The argument for placing type-driven requirements on the type is economy of [human] expression and the desire to textually locate the property with its source. When a property is dictated by a type, there is no need to additionally express it as a pre/post constraint on the function. This form of subsumption sometimes helps to reduce clutter in type signatures, especially so given that some properties have a tendency to propagate upwards in the call tree to progressively enclosing signatures. My point is only that both concepts seem to have their place, and that the economy and localization of their textual capture seems in part to be a human factors issue in the design of the language. Incidentally, there is a further argument for attaching type-driven properties to types: polymorphism. This would allow (for example) a single algorithm to operate on multiple range-constrained types, which seems harder to write if the properties are required to attach to the algorithms. shap
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
