On Sun, 18 Feb 2018 19:38:03 -0500, Dennis Lee Bieber wrote: > On Mon, 19 Feb 2018 00:09:40 +0000 (UTC), Steven D'Aprano > <steve+comp.lang.pyt...@pearwood.info> declaimed the following: > > >>Or more realistically, suppose you want your type system to ensure that >>you don't lay off the wrong workers: >> >>"employee records where the length of employment is greater than six >>months but less than five years, AND the salary is greater than $100,000 >>or less than $40,000, AND the average number of paid sick days taken per >>year over the last three years is less than five, AND the number of >>reprimands is zero in the last year and less than two in the last five >>years, AND the position in the last two stack rankings was in the top >>fifty percent" >> > That's not a data type -- that's an SQL query... > > The data type is still "employee"
Dennis, you've missed the context. We're discussing the claim that given a sufficiently fine-grained type- system, type checkers can prove any program is correct. Under that scenario, we need separate types for integers, positive integers, negative-or-positive-integers-but-not-zero, employees, employees with seniority, employees with reprimands on their file, employees with three or more reprimands on their file, etc. Every tiny distinction between data values becomes a type, and (so the claim goes) the type checker can prove that your program is 100% bug free. You will never accidentally fire the wrong person, because the compiler won't let you call file_employee(x) if x is the wrong type of employee. Of course its nonsense, but that's the claim I'm discussing. -- Steve -- https://mail.python.org/mailman/listinfo/python-list