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
