Ah thanks, I seem to have missed a large chunk of back-reading. I thought that Maude could do semantic typing, eg. in the parameterized views section of the maude manual ( http://maude.cs.uiuc.edu/maude2-manual/html/maude-manualch15.html). Could you expand on what you meant with the semantic typing stuff?
As far as I understand OMeta, it's based on PEGs, and I understand it's non-determinitstic (and quite often non-terminating!), but I thought that PEGs required the target syntax to be unambiguous ie. in ambiguous cases there is a specified priority, so full context free grammars are out of reach (for say, natural language processing)? Maude's MSCP parser claims to be able to do this, and is apparently proven to interpret all possible analyses for each term (see http://maude.cs.uiuc.edu/maude1/manual/maude-manual-html/maude-manual_30.html ). I was interested in the "real specifications that execute to produce prototypes (and can be debugged)" aspect of programming. Being able to do this (and using meta-circularity to prove the whole software stack from the metal up), I'm guessing, would represent a big step forward. Thanks, Alexis On 5 June 2011 01:33, Alan Kay <alan.n...@yahoo.com> wrote: > I like Maude (and most of the stuff done by or influenced by Joe Goguen). > However, it is basically a term rewriting system that can overlap a bit with > equational semantics. Nothing wrong with that, but much of it is essentially > McCarthy's pure lisp semantics (nothing wrong with that either, but it does > not really extend into the areas I was describing). > > And OMeta is non-deterministic (as are most of the TWSs we've done, > including those that Ian Piumarta has used -- see his TCP example). > > Cheers, > > Alan > > ------------------------------ > *From:* Alexis Read <alexis.r...@gmail.com> > > *To:* Fundamentals of New Computing <fonc@vpri.org> > *Sent:* Sat, June 4, 2011 3:34:13 PM > > *Subject:* Re: [fonc] Static typing and/vs. boot strap-able, small kernel, > comprehensible, user modifiable systems > > >>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 > >
_______________________________________________ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
