python philosophical question - strong vs duck typing

[Devin Jeanpierre]

> where n,m are compiler variables used to define the dependent
> (paramaterized) types array(int,n) and int(n)/ The double use of n means
> that the compiler checks that length n of the array equals the length
> passed.
>
> My response: in Python, there is no need to pass concrete collection sizes
> because they are packaged with the collection at runtime as an attribute.
> So:
>
> 1) In Python, there is no need for such checking. In addition, the for-loop
> construct, 'for item in iterable:', removes the possibility of indexing
> errors.

Correct. This is a systems language, designed so that you do the least
work possible and store the least amount possible in memory. For that
reason it's one of the fastest languages on the language shootout,
with the least memory usage overall. (
http://shootout.alioth.debian.org/ )

That is, you can also simply do "A[k] = 3", and if the compiler can
prove that k is always less than the length of the list, then this
goes ahead without any extra work like a runtime check. This is
similar to what Cython does above, but Python always does the check --
and ATS makes this optimization a core feature of the language, and
predictable: you can force the compiler to try to do this, and if it
can't, you can try to provide more information so that it can. The
easiest way to prove it was provided above, by doing a runtime check
-- but there are other ways (e.g. the inference Cython did; convenient
constants; etc.)

This is probably less appealing to Python programmers, who (rightly)
don't really care about speed unless it becomes an issue. For them,
ATS also has more advanced features like proofs of adherence to
specification and so on (e.g. FIB above). On the other hand, ATS's
main focus is, as far as I can tell, being something that's "as fast
as C, and safer than Haskell". I don't think it's meant for
Pythonistas. :)   (I've seen it compared to Ada, as well)

I should also note that while Python stores the length information at
runtime, you can do that in ATS too (it has exceptions). In fact, ATS
has two array types: array0 keeps the size information at runtime, and
array does not. With array0, out-of-bounds index access results in a
runtime exception, with no compile-time checks performed.

I don't really want to undestate how awesome Python is, though. I have
long been of the opinion that C's attitude was unacceptable[**] -- if
you forget to check, things go drastically wrong in undefined and
unpredictable ways (that depend on your libc/compiler/etc.). Python
offers a way out: all errors are checked for by Python itself. This
makes your job easier and makes mistakes obvious. ATS is nowhere near
as easy in general. :)

Also, you make a good point about for loops. They are a wonderful
thing. :)   (ATS doesn't have them; it could get them in theory...)


[*] With the idea being that in Python you can get unexpected errors
at runtime, whereas in ATS you can try to prove they can't exist, at
compile time. E.g. take "AttributeError: None has no attribute
'split'" versus non-nullable types
[**] Unfortunately, C is still irreplaceable. ATS is never going to
win this one. I do think that dependent typing will eventually enter
the mainstream, though. It's a powerful concept we rely on implicitly
all the time, and I seem to be seeing more of it lately.

> 2) Python classes are, in a sense, or in effect, runtime dependent types.
> While the formal implementation type of a 'list' is just 'list', the
> effective computation type is 'mutable sequence of length n'. The type of an
> iterator is 'read-only sequence of indefinite length'. I find this an
> interesting way to look at Python.

I think that's reasonable. I don't think it would be outrageous to
promote this concept to how we do isinstance checks, but nobody but me
seems to like things like "except IOError(errno.EBADF): ...". (Usually
the if-statements aren't really more complicated, but IOError is an
exception (which is being rectified a different way)).

But yes, even without it being part of the language we can model it
that way. And it's something we do all the time. I think another good
example of that is the "k-tuple". k-tuples seem very different to
n-tuples, for n != k.

-- Devin

On Wed, Jan 4, 2012 at 3:22 PM, Terry Reedy <tjreedy at udel.edu> wrote:
> On 1/4/2012 1:37 AM, Terry Reedy wrote:
>>
>> On 1/3/2012 8:04 PM, Devin Jeanpierre wrote:
>
>
>>> [ An example of a simple dependently typed program:
>>> http://codepad.org/eLr7lLJd ]
>>
>>
>> Just got it after a minute delay.
>
>
> A followup now that I have read it. Removing the 40 line comment, the
> function itself is
>
> fun getitem{n,m:nat}(arr : array(int, n) ,
>  length : int(n), index : int m) : int =
>    if index < length then
>        arr[index]
>    else
>        ~1 (* -1, error *)
>
> where n,m are compiler variables used to define the dependent
> (paramaterized) types array(int,n) and int(n)/ The double use of n means
> that the compiler checks that length n of the array equals the length
> passed.
>
> My response: in Python, there is no need to pass concrete collection sizes
> because they are packaged with the collection at runtime as an attribute.
> So:
>
> 1) In Python, there is no need for such checking. In addition, the for-loop
> construct, 'for item in iterable:', removes the possibility of indexing
> errors.
>
> 2) Python classes are, in a sense, or in effect, runtime dependent types.
> While the formal implementation type of a 'list' is just 'list', the
> effective computation type is 'mutable sequence of length n'. The type of an
> iterator is 'read-only sequence of indefinite length'. I find this an
> interesting way to look at Python.
>
>
> --
> Terry Jan Reedy
>
> --
> http://mail.python.org/mailman/listinfo/python-list