Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!newstop!exodus!rbbb.Eng.Sun.COM!chased From: chased@rbbb.Eng.Sun.COM (David Chase) Newsgroups: comp.lang.misc Subject: Re: Optional static typing limits Message-ID: <11770@exodus.Eng.Sun.COM> Date: 18 Apr 91 00:30:00 GMT References: <8493:Apr1719:30:0791@kramden.acf.nyu.edu> Sender: news@exodus.Eng.Sun.COM Organization: Sun Microsystems, Mt. View, Ca. Lines: 70 brnstnd@kramden.acf.nyu.edu (Dan Bernstein) writes: >I propose we focus on just one problem: What should a type system look >like in order to allow everything people want to do with types? In other >words, what kinds of constraints should the programmer be able to >express upon objects (in the general sense, not the OO sense) in order >to achieve both safety and generality? > >Let's not argue whether dynamic typing is necessary. Let's just do what >we have to so that it's obviously unnecessary. (Is that too upbeat for >comp.lang.misc readers?) It might be overambitious to make it "unnecessary". "Rarely necessary" should suffice. Unless you want to make a religious issue out of it, you might make some allowances for what could be done by a suitably-designed optimizer (or type-inference engine) instead of unduly burdening the programmer in the name of mandatory efficiency. Anyhow, check out "Type-dependent Parameter Inference" by Cormack and Wright, in the June 1990 SIGPLAN Notices (conference proceedings of PLDI). I read it recently, and found it quite interesting. I didn't understand all of it, but I'm working on it. See also "Typeful Programming" by Cardelli, Digital Systems Research Center report # 45. Their address (since this might not be in your local library) is Digital Systems Research Center 130 Lytton Avenue Palo Alto, CA 94301 You might also look at Report #10, "A Polymorphic \lambda-calculus with Type:Type". Same author. William Cook (formerly of HP, now at Apple) may have published something on this subject in the last couple of years, but the last time I remember asking him about it, he told me to go read Cardelli's papers. Here's a list of the Russell papers: Two by Demers and Donahue in the 1980 POPL. Boehm, Demers & Donahue, "An informal description of Russell", Cornell CS department TR 80-430. Demers & Donahue, "Data Types are Values", Cornell CS dept TR 79-393 (possibly also a Xerox PARC blue&white -- I'm misplaced my copy of this) Demers & Donahue, "The semantics of Russell, an exercise in abstract data types". Cornell CS TR 80-431. Hook, "Understanding Russell - A first attempt", Semantics of Data Types (Proceedings), Springer-Verlag Lectuer Notes in Computer Science #173. Boehm, Demers & Donahue, "A Programmer's Introduction to Russell", Rice CS tech report TR85-16. Boehm, "Type Inference in the Presence of Type Abstraction", SIGPLAN Notices, Jul7 1989 (PLDI Conference proceedings). If you're serious about type systems and type theory, go read these papers. The authors put a lot of thought into them, and the authors are not stupid people. And no, I won't digest them for the net in ten easy installments - I don't have the time, and that's not what I'm paid to do. David Chase Sun