[Prev][Next][Index][Thread]
RE: type safety
On Sat, 1 Jan 2000, Corky Cartwright wrote:
> Either Xi and Pfenning only handle trivial cases or their type system
> must set a new record for complexity. A sophisticated approach to
> eliminating array bounds checks involves solving integer linear
> programming problems. Are you stating that all type systems
> that do not incorporate integer programming solvers are "very simple"?
I'd like to clear some (potential) misunderstanding here.
It is rather common for one to conclude that type-checking involving
integer programming is simply too involved. However, there are several
pitfalls here.
(1) My experience with DML-style dependent types indicates that the
generated constraints in practice are often trivial and can be solved
with a fast (but incomplete) method such as the simplex method on reals.
In theory, the simplex method is not polynomial, but in practice,
it is often superior to some existing polynomial approaches to linear
programming (e.g., Karmakar's (?) approach). This allows us to solve
only few hard constraints with expensive approaches such as the
Fourier-Motzkin variable elimination approach, the bound and branch
method, etc.
(2) It is hard to use dependent types everywhere (even if you *really*
want to). This means that you don't get a lot of constraints during
type-checking.
(3) As far as array bounds checking is concerned, there aren't many
"non-trivial" cases. All I can say is that I have tried many practical
examples, including Fast Fourier Transform, Heapsort, Gaussian
Elimination, Sparse Matrix multiplication, etc. You can find these
examples at:
http://www.ececs.uc.edu/~hwxi/Xanadu/Xanadu.html
Cheers,
--Hongwei
\~~~~/ \\ // \\ // @ Mail: hwxi@ececs.uc.edu
C-o^o, ))__|| \\__//_ // \\ Url: http://www.ececs.uc.edu/~hwxi
( ^ ) ))__|| \--/-\\ \\ Tel: +1 513 871 4947 (home)
/ \V\ )) || // \\ \\ Tel: +1 513 556 4762 (office)
------ // || o // \\ \\//Fax: +1 513 556 7326 (department)
Follow-Ups: