> 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 <tjre...@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 -- http://mail.python.org/mailman/listinfo/python-list
