>>The extreme case of this -- where the variables are actually constrained to the specific values they are supposed to contain -- would be very useful if it could be made to generally work -- it amounts to declarative programming.
>>Another extreme case would concern procedures/methods (we've called it "semantic typing"). For example, we want to find an operator that will do something specific -- like the sine function -- and we type our local name for this so that the only value it can have is a procedure that will compute sine. We could think of this as a kind of unit test for resources, or we could think of this as search criteria. Ted Kaehler implemented the Squeak method finder to do some of this. You give it examples of relations and it finds the methods. So 3 . 4 . 7 will yield both "+" and "xor". 30 . 0.5 will find "degreeSine", etc. There is actually a language that does the above - Maude. It supports strong dynamic typing (or as they call it sorts and subsorts) with subset inclusion eg. integers < rational numbers < irrational numbers, so in the case of type mismatch it can fall back to a different type (and error sorts are the last in the chain by default). Maude is also an equational language, so the number type example above can be done natively, and you can formally prove the type soundness (no SQL injection style bugs here!). Maude is a declarative language that has paramatized modules ie. you can constrain the parameters by type, the language will do the type matching for you as per the semantic typing above (you can specify matching strategies similar to ometa but more flexible due to the non-determinitstic parser). Types can be extended along with the rest of the language in a clean fashion - the Full Maude language including the object types is written in Core Maude. btw for those that haven't used Oberon (or it's most recent incarnation at the ETH, Bluebottle), as far as I'm aware the static typing is used at compile time, but not after that. As all the modules are hot-pluggable in the OS though, you can easily change types by recompiling, and I guess you could do a form of dynamic typing by auto-compiling modules at runtime. Static typing puts restrictions on what you ultimately can do, but for most tasks KISS (keep it simple stupid) applies and static typing certainly helps on the debugging side! Bootstrapping really isn't a problem - Bluebottle is working proof of this. On 4 June 2011 16:08, Alan Kay <alan.n...@yahoo.com> wrote: > This issues were in conversations in the mid-60s when I was in grad school. > > One difference was that there was a computer (and more being thought of) -- > the Burroughs B5000 -- that removed one of the motivations for static typing > -- it implemented byte codes and 0 overhead dynamic type checking into the > hardware which was organized as what would have been called the first > capability architecture -- it was not crashable by a non-privileged > programmer). > > The semi-bug was that it was aimed at Algol/Simula like languages, so some > other ideas were less efficient. This was resolved at PARC by dynamic > microcoding of the VM (both on the mainframes and on the personal computers > we designed and built). The game here was that if the micro-CPU was always > waiting for memory to serve it (it was about 5 times faster) then you won > (dynamic type checking was not slowing anything down). > > This left the other question and possible motivation for static type > checking, which was: could the tradeoffs it imposed still wind up helping > the programmers more than bogging them down? > > The extreme case of this -- where the variables are actually constrained to > the specific values they are supposed to contain -- would be very useful if > it could be made to generally work -- it amounts to declarative programming. > > Another extreme case would concern procedures/methods (we've called it > "semantic typing"). For example, we want to find an operator that will do > something specific -- like the sine function -- and we type our local name > for this so that the only value it can have is a procedure that will compute > sine. We could think of this as a kind of unit test for resources, or we > could think of this as search criteria. Ted Kaehler implemented the Squeak > method finder to do some of this. You give it examples of relations and it > finds the methods. So 3 . 4 . 7 will yield both "+" and "xor". 30 . 0.5 will > find "degreeSine", etc. > > Examples are not enough for semantic typing, but we can see that with an > Internet of possible resources, it would be useful to be able to > characterize transformations in this way. > > Back to normal approaches to typing. This leaves us partly with what kinds > of bugs do you prefer and when do you want them to materialize?" kind of > questions. > > It's always seemed to me that what we really need to be working on is > something more like "real specifications that execute to produce prototypes > (and can be debugged) much more than weak schemes that are complex enough to > introduce severe cognitive load, but aren't comprehensive enough to come > close to paying their way. > > Cheers, > > Alan > ------------------------------ > *From:* C. Scott Ananian <csc...@laptop.org> > *To:* Fundamentals of New Computing <fonc@vpri.org> > *Sent:* Fri, June 3, 2011 9:56:21 PM > *Subject:* Re: [fonc] Static typing and/vs. boot strap-able, small kernel, > comprehensible, user modifiable systems > > On Fri, Jun 3, 2011 at 11:37 PM, Scott McLoughlin <scottmc...@gmail.com> > wrote: > > What is the relationship, positive and negative, between static > > typing in language design and user-transparent and modifiable > > systems bootstrapped from small kernels? > > "Small type systems" aren't very powerful, and tend to grate on their > users. So people dream of more powerful type systems, to let them > write more flexible code. Soon you're in Hindley-Milner territory or > fighting the halting theorem and your system isn't so small and > understandable any more. > > The solution seems to be a "pluggable types" system, which lets you > build a complicated and/or domain-specific static type system (or > several of them) from a small kernel (or a purely dynamic system). > AFAIK, this hasn't gotten a lot of attention from the research > community, partly because no one seems quite certain how to go about > building such a thing. Gilad Bracha seems to have done the most > thinking about it; see his position paper linked from: > http://bracha.org/Site/Newspeak.html > The bibliography of his position paper cites a number of other related > papers. > > I spend some time around 2007 trying to figure out how to write Java > 1.5's type system in terms of a smaller kernel type system. I didn't > get very far. (I made much more progress on the syntactic evolution > of Java 1.5 from Java 1.0.) There are links between type systems and > abstract interpretation (see http://lambda-the-ultimate.org/node/2208 > ); that may hold the key. > > Perhaps some others of the list can fill in more details. > --scott > > -- > ( http://cscott.net ) > > _______________________________________________ > fonc mailing list > fonc@vpri.org > http://vpri.org/mailman/listinfo/fonc > > _______________________________________________ > fonc mailing list > fonc@vpri.org > http://vpri.org/mailman/listinfo/fonc > >
_______________________________________________ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
