python philosophical question - strong vs duck typing

[Devin Jeanpierre]

> This strikes me as petty hair-splitting.

Maybe it is! I don't know what "petty" means.

> 1. By tacking on the qualification, I was acknowledging that someone,
> somewhere, might controvert it. If you allow for arbitrary redefinitions of
> words, you could claim that any statement is an opinion. So what?

I don't know where the original definition of "strong typing" came
from. My experience has been that everyone has their own definition --
some people redefine it when faced with absurd consequences of their
original definition, but usually to something roughly similar. I
believe that people redefine it because to say your language is
"weakly typed" sounds, well, like a weakness, or like an insult. It
raises my hairs when people phrase it like that, anyway.

> 2. It ignores the context established by the OP who began with 'Let's say we
> wanted to type strongly in Python' and continued with a question about
> declarations and compilation specifically to C or C++.
>
> In that context, I think my statement qualifies as a fact.

I agree, what I said there does ignore it. This is why I made a point
of quoting you a second time, when you specifically referred to the
OP, and stating my agreement. Sorry for any misunderstanding. As far
as your correction to the OP goes, I am in favor. Aside from the small
nit that applies to a statement if you take it out of context.

> Can you give an actual example of such a definition of 'strongly typed
> object' that excludes Python objects?

I'd love to, but I neglected to above because I don't really know
where we share ideas, and I wouldn't want to jump ahead and say
something that seems outlandish. I hope I've done a decent enough job
below. Stop me if I say something you don't agree with.

Here's a short version: The term often refers to a continuum, where
some languages are "stronger" than others, but there is no objective
definition of "strong" -- it's like asking how big is "big", or how
smart is "smart". The actual choice of what continuum strength refers
to varies between people -- some specify it as "reinterpretation of
bits in memory", in which case every dynamic language in the world is
strongly typed (so I'll move on from that), or some as "implicit
conversions between types", which is iffy because any function or
overloaded operator can silently convert types (at least in Python),
meaning the language is as weak as the user (?). But they're both kind
of reasonable and held by a few people, and it's easy to see how maybe
somebody used to significantly more strict rules (OCaml, for example)
might accuse Python of not being all that strong. So you see it isn't
really a change of definition, it's a redrawing of the lines on a
continuum. The OCaml people are reasonable for saying what they say,
because their point of reference is their favorite language, just as
ours is ours. To us, maybe Haskell and OCaml are insanely
strong/"strict", to them, we're insanely weak.

Here's another take, more in line with what I really meant: the
continuums expressed above aren't universal either. IME they're chosen
by dynamic typing advocates, which are worried about code readability
and certain styles of immensely common errors that come from
lower-level languages like C. Static typing advocates (at least in the
functional programming language family) are instead concerned about
correctness. For them, type systems are a way to reduce the number of
errors in your code _in general_, not just the specific cases of type
coercion or memory-safety. In this particular sense, Python is not
very far from C -- it saves us from things that can crash the entire
process or give us incorrect results rather than alerting us of a
problem, but usually only so that we can encounter them in a more
recoverable form. For example, out-of-bounds array access can no
longer alter various parts of your stack and ruin the entire program
state, but it is still a possible error. Static typing advocates say
that strong typing can completely eliminate some types of errors, and
the sensible time to detect such errors is at compile-time.

This is absolutely an origin for the conflation of static vs strong
typing, and it's hard to differentiate them in this sense, primarily
because this notion of strong typing basically requires static typing
for powerful results. On the other hand, you can clearly have
"stronger" languages at runtime -- there are plenty of errors Python
prevents, that C does not, even though python is dynamically typed and
C is not. So Python's type system is clearly stronger than C. I hope
this illustrates that strong and static are two different things even
under this definition -- it's just that, most of the time, to really
prevent an error, you prevent it from ever happening at compile-time.

Type systems exist which are much "stronger" in what they can protect
you against. As an extreme example, one might take a dependently-typed
language. A statically dependently typed language can protect you
against out-of-bounds array access with a proof at compile time. In
fact, a statically-dependently-typed language can do things like prove
that two different implementations of the same function are in fact
implementations of the same function -- this is neat for implementing
a non-recursive version of a recursive function, and verifying the
change doesn't influence semantics.

It's definitely true that there is something here that Python's types
cannot do, at least not without extremely heavily mangling
(technically __instancecheck__ means that type objects are turing
complete, but I request that we ignore that). These are the sorts of
types that can, in a very real sense, replace unit tests. Just the
fact that your program typechecks is proof that certain properties
hold, and those properties can be very soothing, such as that example
of proving two algorithms return the same output. (There is an
argument to be made that automated tests are better value for money. I
don't really know, I've never seen actual accounts of attempting this,
and I've never done it myself.)

One last note about static vs dynamic vs strong typing: I do believe
that a strongly typed dynamic+statically typed language is possible
and a good thing. For statically typed code, run-time checks are
disabled (speed), for dynamically typed code they are enabled, and all
the while you can make relatively sophisticated queries about the type
of a thing using an interactive interpreter (somewhat similar to
unifying things in the prolog interpreter, in my view).


So now that we've gotten this far, here's my proposition: It is
reasonable to consider type systems in terms of how many errors they
eliminate in your programs, rather than just readability/memory-safety
concerns. Also, it is reasonable to have relatively strict standards,
if you're used to a very "strong" type system. Such a person might,
very reasonably, decide that Python is quite weak. Python eliminates
memory-safety concerns, and makes things like array-access problems
more obvious, but it eliminates very few errors. Other type systems
can eliminate much larger categories of errors -- admittedly, most
likely at the expense of development speed and/or flexibility.


I admit that a lot of what I said here is putting words in other
peoples' mouths, if you object, pretend I said it instead. I am, after
all, a fan of ATS at the moment, and thus have some interest in
ridiculously strongly typed languages ;)


*phew*. That took a lot of time. I hope I haven't lost your attention.

[ An example of a simple dependently typed program:
http://codepad.org/eLr7lLJd ]

-- Devin



On Tue, Jan 3, 2012 at 4:42 PM, Terry Reedy <tjreedy at udel.edu> wrote:
> On 1/3/2012 4:06 PM, Devin Jeanpierre wrote:
>>>
>>> Python objects are strongly typed, in any sensible meaning of the term.
>>
>>
>> There are people that hold definitions of strong typing that preclude
>> Python. Those people think their definition is reasonable, but at the
>
>
> Can you give an actual example of such a definition of 'strongly typed
> object' that excludes Python objects?
>
>
>> same time haven't confused static typing with strong typing. I guess
>> the problem is that this boils down to opinion, but you're stating it
>> as incontrovertible fact.
>
>
> This strikes me as petty hair-splitting.
>
> 1. By tacking on the qualification, I was acknowledging that someone,
> somewhere, might controvert it. If you allow for arbitrary redefinitions of
> words, you could claim that any statement is an opinion. So what?
>
> 2. It ignores the context established by the OP who began with 'Let's say we
> wanted to type strongly in Python' and continued with a question about
> declarations and compilation specifically to C or C++.
>
> In that context, I think my statement qualifies as a fact.
>
>
> --
> Terry Jan Reedy
>
> --
> http://mail.python.org/mailman/listinfo/python-list