Terry Reedy於 2012年1月5日星期四UTC+8上午4時22分03秒寫道： > 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.
Also it is easy to turn an indexed object to be an iterator by a function decorator that returns a generator in the object level without declaring a new class from a class written by others. Thus this can lead to a decoupled design of software among many contributors in an elegant way. I prefer a factorized decoupled blocks of modules to be completed by several programmers to build a package. > > -- > Terry Jan Reed -- http://mail.python.org/mailman/listinfo/python-list
