[Python-ideas] Pre-conditions and post-conditions

[Steven D'Aprano]

On Mon, Aug 27, 2018 at 11:00:22PM +1000, Chris Angelico wrote:

> Sometimes "type" doesn't mean the same thing to the language and to
> the human. Suppose you're trying to create a Python script that
> replicates a C program; you might want to declare that a variable is
> not of type "integer" but type "32-bit unsigned integer", with
> wrap-around. Or, wording it another way: "integer modulo 2**32". Is
> that an assertion of type, or of type and value? As a precondition to
> a function, requiring that a parameter be an integer no less than zero
> and no greater than 4294967295 is, in a sense, checking its type and
> its value; but it's kinda just asserting its type.

It is making an assertion about the value of an instance of type "int". 
Its not a separate type requiring an explicit coercion or cast. Its just 
a non-negative int less than 2**32.

If the compiler supports the concept of a 32-bit unsigned integer type, 
then of course we can change our implementation to use that type instead 
of our regular ints. But we can't expect to pass such a 32-bit unsigned 
integer to a function which expects a regular int unless they are 
duck-type compatible, or the compiler performs automatic coercions. 
(So-called "weak typing").

A better example is the one I gave earlier, of a graph with no cycles. 
There is a deep fundamental difference between a *statically checked* 
DAG with no cycles (a graph which can never contain a cycle because the 
compiler won't let you create one) and a *dynamically checked* DAG that 
merely has no cycles *now* (it may have had cycles earlier, and it might 
have cycles later, but right now it has none).

These are very different semantics, and Eiffel's contracts support the 
second kind: runtime value checks.



-- 
Steve