Path: csiph.com!x330-a1.tempe.blueboxinc.net!usenet.pasdenom.info!weretis.net!feeder1.news.weretis.net!feeder.erje.net!newsfeed.xs4all.nl!newsfeed5.news.xs4all.nl!xs4all!newsgate.cistron.nl!newsgate.news.xs4all.nl!post.news.xs4all.nl!not-for-mail Return-Path: X-Original-To: python-list@python.org Delivered-To: python-list@mail.python.org X-Spam-Status: OK 0.000 X-Spam-Evidence: '*H*': 1.00; '*S*': 0.00; 'python,': 0.01; 'python.': 0.04; 'compiler': 0.07; 'received:verizon.net': 0.07; 'removes': 0.07; 'terry': 0.07; 'typed': 0.07; 'python': 0.08; 'attribute.': 0.09; 'comment,': 0.09; 'received:80.91': 0.09; 'received:80.91.229': 0.09; 'received:80.91.229.12': 0.09; 'received:gmane.org': 0.09; 'received:list': 0.09; 'received:lo.gmane.org': 0.09; 'runtime': 0.09; 'subject:python': 0.10; 'am,': 0.12; 'computation': 0.16; 'iterator': 0.16; 'passed.': 0.16; 'reedy': 0.16; 'subject:question': 0.17; 'wrote:': 0.18; 'int': 0.18; 'jan': 0.19; 'header:In-Reply-To:1': 0.22; 'indexing': 0.23; 'index': 0.24; 'classes': 0.26; 'function': 0.27; 'pass': 0.29; 'error': 0.29; 'pm,': 0.29; 'example': 0.29; 'array': 0.30; '-1,': 0.30; 'checking.': 0.30; 'followup': 0.30; 'types.': 0.30; 'dependent': 0.32; 'header:User- Agent:1': 0.33; 'header:X-Complaints-To:1': 0.33; 'there': 0.33; 'to:addr:python-list': 0.34; 'it.': 0.34; 'sense,': 0.34; 'addition,': 0.36; 'checks': 0.37; 'sequence': 0.37; 'subject:skip:p 10': 0.37; 'variables': 0.37; 'received:org': 0.38; 'url:org': 0.39; 'else': 0.39; 'define': 0.39; 'to:addr:python.org': 0.40; 'type': 0.61; 'types': 0.61; 'effective': 0.61; 'double': 0.61; 'program:': 0.67; 'collection': 0.69; 'packaged': 0.84; 'so:': 0.84; 'delay.': 0.91 X-Injected-Via-Gmane: http://gmane.org/ To: python-list@python.org From: Terry Reedy Subject: Re: python philosophical question - strong vs duck typing Date: Wed, 04 Jan 2012 15:22:03 -0500 References: Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-Gmane-NNTP-Posting-Host: pool-74-109-121-73.phlapa.fios.verizon.net User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:8.0) Gecko/20111105 Thunderbird/8.0 In-Reply-To: X-BeenThere: python-list@python.org X-Mailman-Version: 2.1.12 Precedence: list List-Id: General discussion list for the Python programming language List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Newsgroups: comp.lang.python Message-ID: Lines: 40 NNTP-Posting-Host: 2001:888:2000:d::a6 X-Trace: 1325708545 news.xs4all.nl 6974 [2001:888:2000:d::a6]:35866 X-Complaints-To: abuse@xs4all.nl Xref: x330-a1.tempe.blueboxinc.net comp.lang.python:18511 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