Hi Alexis There is "more to Maude" than the last time I looked at it. Joe Goguen's very good idea was to make the base semantics of modules be executable in a term rewriting semantics that was also somewhat amenable to deduction and proof. Unless they've done more that I've missed, the rewriting (semi-executable) part is very similar in expression to pure lisp. A "semantic type" is e.g. "what a procedure accomplishes", and so the semantics of a procedure would generally be have to given via a procedure. This is still a good idea (and now an old one). I've been hoping for something more (truly) declarative to come along, which allows much stronger searching and matching to be done.
And, yep, non-deterministic is different than "all paths". However, this turned out not to be terribly useful in the past (the Oetinger parser at Harvard in the 60s could do all possible paths, but the weakness was in being able to interpret any of them. Cheers, Alan ________________________________ From: Alexis Read <alexis.r...@gmail.com> To: Fundamentals of New Computing <fonc@vpri.org> Sent: Mon, June 6, 2011 3:55:39 PM Subject: Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems 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
