Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!comp.vuw.ac.nz!brian
From: brian@comp.vuw.ac.nz (Brian Boutel)
Newsgroups: comp.lang.misc
Subject: RE: Dynamic typing (part 3)
Message-ID: <1991Apr15.233220.15725@comp.vuw.ac.nz>
Date: 15 Apr 91 23:32:20 GMT
References: <1707@optima.cs.arizona.edu><1991Apr11.053440.13401@comp.vuw.ac.nz>  <15APR91.00191631@uc780.umd.edu>
Sender: news@comp.vuw.ac.nz (News Admin)
Organization: Computer Science, Victoria University, Wellington, NewZealand
Lines: 67
Nntp-Posting-Host: antrim-hse.comp.vuw.ac.nz
Originator: brian@antrim-hse.comp.vuw.ac.nz


In article <15APR91.00191631@uc780.umd.edu>, cs450a03@uc780.umd.edu writes:
|> Brian Boutel writes:
|> 
|> >First, let me try to define what I mean ...
|> >- A type is a set of operations.
|> >- a value has type T if it understands all the operations of type T
|> 
|> Thus a value can have multiple types?
|> 

Yes, within a type hierarchy, a value may have a type and that type's
supertype and so on upwards.

|> 
|> >- Languages can be classified as untyped, dynamic typed, static typed...

|> I'm a little foggy here...  If a language has some run-time checking,
|> and some compile time checking, and doesn't catch some things, how
|> would you classify it.
|> 
|> [e.g. C on a machine that has some arithmetic exception hardware.]
|> 

I wuld classify C as statically typed, but see below.

|> 
|> >- Static typed means that a type is associated at compile time with
|> >each variable. (In a functional language, which is what interests me,
|> >this normally means with each defined function and by implication its
|> >formal parameters.)  It is possible at compile time to ensure that a
|> >value is never bound to a variable of the wrong type, and that only
|> >type-valid operations are performed on variables, thus preventing
|> >type violations.
|> 
|> How is this possible?  Especially in a machine with finite limits?
|> Note that arithmetic overflow means that addition can produce values
|> which don't have the type for addition.  You can't use subtraction to
|> generate a value for a function which does not accept 0, or negative
|> numbers, unless static analysis of the code reveals that this is ok.
|> Multiplication hits the overflow problem even harder.  Etc.
|> 
|> And that's just basic arithmetic.
|> 
|> Raul Rockwell

This is the cause of the misunderstanding between us. I was not
including arithmetic exceptions such as overflow or divide by zero as
type violations.
In the type systems I am talking about, the type Integer supports the
integer divide operation, (say, "div"), and the type of div is 
Integer X Integer -> Integer
This does not take account of the fact that the type of div should
really be 
Integer X NonZeroInteger -> Integer, where NonZeroInteger is a subtype
of Integer. So my type system has deficiencies, but it can still catch a
lot of errors at compile time that might otherwise get through testing.
I think that is worthwhile.

--brian

 
-- 
Internet: brian@comp.vuw.ac.nz
Postal: Brian Boutel, Computer Science Dept, Victoria University of Wellington,
        PO Box 600, Wellington, New Zealand
Phone: +64 4 721000   Fax: +64 4 712070