On Sun, 18 Feb 2018 08:02:10 +1100, Chris Angelico wrote:
[...]
>> The usual response to that is to make ever-finer-grained types, until
>> the type-system can prove the code is correct.
>>
>> integers
>> positive integers
>> positive integers greater than 10
>> positive integers greater than 10 but less than 15003
>> positive odd integers greater than 10 but less than 15003
>> positive odd integers greater than 10 but less than 15003 divisible
>> by 17
>>
>> Of course, this has a few minor (ha!) difficulties... starting with the
>> hardest problem in computer science, naming things.
>
> Naming things isn't a problem if we're working with a type inference
> system.
It is as soon as you need to name a type in order to document it, talk
about it to other human beings, or declare it for the type system. (Type
inference can only go so far -- you do sometimes need to give it hints.)
> On the flip side, if your last example is purely type inference,
> it's not really a type checking system - it's a holistic static
> analysis. You can't say "TypeError: spamminess must be less than 15003"
> without also saying "oh but that might be a bug in this function, since
> it's meant to be able to take numbers >= 15003".
That's *always* a problem with type systems, regardless of whether type
inference is used or not. If I declare that a function takes a list, then
the type checker will complain if I pass it a tuple. That's what type
checkers do.
But they do it even if the algorithm (or source code!) is perfectly
capable of using the same steps for working with both lists and tuples.
In older languages like Pascal you have to write something like this to
satisfy the compiler:
# using Python syntax for symplicity
def listtail(x: list):
return x[1:]
def tupletail(x: tuple):
return x[1:]
then remember to call listtail(alist) and tupletail(atuple) as
appropriate. This meaningless make-work to satisfy the compiler is one of
the biggest problems with older static type-systems, and is one of the
things that object oriented programming is intended to solve.
More modern statically typed languages may include some form of type-
dispatch, where you still have to write the tail function twice:
def tail(x:list):
return x[1:]
def tail(x:tuple):
return x[1:]
but now you use the same name for both and the compiler can automatically
use the right one.
Another modern solution is the idea of explicit union types, so you can
say that x must be a list *or* a tuple.
An alternate solution is to give up on the static typing and use dynamic
typing, which in turn allows us to introduce duck-typing as a strategy.
> Some of the type names CAN be generated algebraically.
Sure, but only the most boring, uninteresting kinds of types can be so
named. The point is that "sufficiently fine-grained types" can be
arbitrarily complex. If a human finds it hard to give it a meaningful
name, no algorithm will do it either. Consider:
"positive odd integers greater than 10 but less than 15003 divisible by
17 except for 850, 867 and 1394; or primes that aren't Mersenne primes".
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"
and so on. It is not practical for a type system to be "sufficiently fine-
grained": that would require the type system to be as flexible and Turing
complete as the language itself (and consequently as bug-ridden as the
rest of our code). We cannot expect the type system to find interesting
bugs, like flagging the best performers for layoff instead of the worst.
It will mostly find only boring bugs like trying to add 1 + "one".
[...]
> Oh wait. We're talking about programmers here. Malicious has nothing on
> the rampant stupidity...
>
> https://thedailywtf.com/articles/What_Is_Truth_0x3f_
:-)
--
Steve
--
https://mail.python.org/mailman/listinfo/python-list
