On Sat, Jun 6, 2015 at 1:14 PM, Jonathan S. Shapiro <s...@eros-os.org> wrote: > 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.
Right. Sort of. As programmers, we focus on the programs. But mathematically, it makes sense to have a type of right triangles (say) whether or not we have functions whose domain is the type of right triangles. We might just want to experiment with right triangles with pencil and paper. There are no functions on triangles, but we still care which triangles are right. When we attach preconditions and postconditions to a procedure, this is actually refining the procedure type! So requirements for algorithms working correctly is in fact a special case of refinement types, where we refine down from programs we can compile to programs that work (in the appropriate situation). What I'm trying to say is that thinking of refinement types as just a trick to express correctness of programs is an incomplete and programmer-centric viewpoint. Of course I understand that that is the application we're talking about. > 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. I agree that attaching properties to argument types can reduce clutter. But how is it a form of subsumption? > 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. Yes. > 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. No, I think they'd both do fine in that case. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
