Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
On Fri, Jun 3, 2011 at 10:37 PM, Scott McLoughlin scottmc...@gmail.com wrote: For many, many moons, I've examined the early Smalltalk books, small bootstrap Forth systems, Lisp based systems (implementing a large subset of CL decades ago) and the like. In recent years, I've taken an interest in type systems and typed functional languages. What is the relationship, positive and negative, between static typing in language design and user-transparent and modifiable systems bootstrapped from small kernels? Any elucidation or pointers to prior research greatly appreciated. - S. In addition to the other pointers mentioned, here are some variations on the theme: A soft-typing system for Erlang http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.5.6211rep=rep1type=pdf Typed Racket: Racket with Static Types docs.racket-lang.org/ts-guide/index.html Note: This is just the user's guide for a working implementation, but the Racket (formerly PLT Scheme) group has put a lot of thought and work into gradual typing. And -- because you can't know where you're going unless you know where you've been -- I assume you've read Pierce's Types and Programming Languages (http://www.cis.upenn.edu/~bcpierce/tapl/) and, possibly, Kiselyov's article Type Arithmetics (http://okmij.org/ftp/Computation/type-arithmetics.html). Cheers, Mike ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
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
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
On Sat, Jun 4, 2011 at 9:52 AM, Scott McLoughlin scottmc...@gmail.com wrote: [...] So I'll rephrase my question in this manner. We can imagine a Smalltalk or Lisp or Forth machine. Can we imagine a machine predicated on a statically typed language - a Haskell machine, or OCaml Machine or whatever - in the same way??? Why or why not? If the type system is Turing complete (e.g. Haskell's extended type system), you now have two languages to implement. I can't recall the specific topics, but, over on lambda-the-ultimate.org, there have been numerous and interesting discussions about the barriers to bootstrapping via metacircular interpreters (as in Lisp) in languages with Turing complete type systems. Mike ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
On 04 Jun 2011, at 16:52 , Scott McLoughlin wrote: So I'll rephrase my question in this manner. We can imagine a Smalltalk or Lisp or Forth machine. Can we imagine a machine predicated on a statically typed language - a Haskell machine, or OCaml Machine or whatever - in the same way??? Two interesting Haskell machines: http://programatica.cs.pdx.edu/House/ http://halvm.org/ Also: http://hackage.haskell.org/package/hans - antoine -- http://7degrees.co.za/~antoine ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
On Sat, Jun 4, 2011 at 10:08 AM, Alan Kay alan.n...@yahoo.com wrote: [...] 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. A specific case only, but a useful one: SQL. (Even if it is an ad-hoc, informally-specified, bug-ridden, slow implementation of half of the relational model.) 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. [...] 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. A small step along the path? Haskell's type system and the Hoogle Haskell API search engine: http://haskell.org/hoogle/ Regards, Mike ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
Kind Folks, I just feel obligated to say that I had absolutely no intention of introducing the far too well-worn debate between untyped, latently typed and manifestly typed languages. My intention was to far more specifically ask: why small core, user comprehensible and modifiable, and boot-strapable systems seem to be the province of either latently typed (Smalltak, Lisp, Scheme, Icon (?), etc.) or untyped (Forth, B (?)) languages rather than... ...manifestly typed languages (wide variety - C++, D, Oberon, Haskell, Standard ML and oodles more). This is a very highly contextual question, I believe apropos of this mailing list. Mucho thanks again, in advance. - S. On 6/4/2011 11:27 AM, Michael Forster wrote: On Sat, Jun 4, 2011 at 10:08 AM, Alan Kayalan.n...@yahoo.com wrote: [...] 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. A specific case only, but a useful one: SQL. (Even if it is an ad-hoc, informally-specified, bug-ridden, slow implementation of half of the relational model.) 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. [...] 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. A small step along the path? Haskell's type system and the Hoogle Haskell API search engine: http://haskell.org/hoogle/ Regards, Mike ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
I think you answered your own question. A small core is small since it is limited to what is required to make it run. This eases development and lets you focus on what's important and interesting. On Jun 4, 2011 6:06 PM, Scott McLoughlin scottmc...@gmail.com wrote: Kind Folks, I just feel obligated to say that I had absolutely no intention of introducing the far too well-worn debate between untyped, latently typed and manifestly typed languages. My intention was to far more specifically ask: why small core, user comprehensible and modifiable, and boot-strapable systems seem to be the province of either latently typed (Smalltak, Lisp, Scheme, Icon (?), etc.) or untyped (Forth, B (?)) languages rather than... ...manifestly typed languages (wide variety - C++, D, Oberon, Haskell, Standard ML and oodles more). This is a very highly contextual question, I believe apropos of this mailing list. Mucho thanks again, in advance. - S. On 6/4/2011 11:27 AM, Michael Forster wrote: On Sat, Jun 4, 2011 at 10:08 AM, Alan Kayalan.n...@yahoo.com wrote: [...] 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. A specific case only, but a useful one: SQL. (Even if it is an ad-hoc, informally-specified, bug-ridden, slow implementation of half of the relational model.) 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. [...] 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. A small step along the path? Haskell's type system and the Hoogle Haskell API search engine: http://haskell.org/hoogle/ Regards, Mike ___ 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
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
On 6/3/2011 8:37 PM, Scott McLoughlin wrote: For many, many moons, I've examined the early Smalltalk books, small bootstrap Forth systems, Lisp based systems (implementing a large subset of CL decades ago) and the like. In recent years, I've taken an interest in type systems and typed functional languages. What is the relationship, positive and negative, between static typing in language design and user-transparent and modifiable systems bootstrapped from small kernels? Any elucidation or pointers to prior research greatly appreciated. well, whether or not any of this is helpful or not, I don't know. also, most of this is based on my own experience, which apparently some people disagree with (for example, before when I claimed that to implement a C compiler was hugely more of a PITA than a JavaScript style VM, some people got all up in arms over the matter...). in my own language/VM effort, I am mostly using a hybridized typesystem, which basically resembles a statically typed system (most variables have assigned types), but one can just as easily use dynamic types (via the 'var' or 'variant' type). the static types then serve one of several roles: as optimization hints (allowing skipping type checking, or use native machine types for variables); as a means of performing static type checking (ideally, to detect if the programmer made a big botch-up or typo early on, as a major drawback of dynamic types is often that one may often accidentally end up typing very brain-damaged code, but this will not be caught until much later, such as at run-time, or until stumbled across). currently, much of the present VM itself mostly uses dynamic types internally though. the merits of dynamic typing are: generally, these are much easier to work with, and can be much more expressive with a lot less implementation effort. for example, with a mostly statically typed VM, then generally complex semantics require a seemingly somewhat more complex implementation. whereas, with dynamic types, beyond some the costs of implementing the typesystem itself, the creation of complex mechanics or systems becomes much easier (as nearly everything tends to decompose much more easily into its fundamental parts). the above is true even for seemingly unrelated things, like implementing scoping semantics, or the FFI. my last attempt to implement one of my style of scope systems (with the following types of scopes: lexical, dynamic, object, package, toplevel, and delegate), using plain static typing (mostly motivated by the idea of VM performance) proved exceedingly painful. the main alternative is simply to use a recursive lookup at runtime, and maybe optimize subsequent lookups via a hash table. as for type declarations, my personal preference is the creation of simple C/Java/... style explicit/manifest typing. a major reason here is that it makes it very obvious what type each variable should be at any given point, and is generally easy to understand and work with. this is in contrast to inferred type systems, or a type-system like the one in Haskell, which personally I found nearly impossible to understand or use. and, really, there is an easy solution to most non-trivial cases: just fall back to variant/dynamic types. then, either the VM will use type-inference to optimize it, or will just use dynamic type-checking if the VM can't figure it out either, or (maybe) complain if the programmer is doing something which will invariably result in a runtime type-check failure. some people had accused me though of endorsing Java style bondage type systems, but generally this is not the case (partly this is because I tend to use a lot more implicit type coercion as well, rather than the more Java-like must manually cast everything or get a type-error style). in most cases, where people will probably use static type declarations is those cases where what the type should be are fairly obvious, and if the type is not obvious, then don't declare it as such. seems obvious enough?... also I hold the belief that declaring things also works as a memory aid, since otherwise a person may forget just what sort of types they put in the variables, or worse yet, resort to using Hungarian-notation as a memory aide. and, in my case, the difference between int x; and var x; is not exactly huge. note: my present language isn't really functional though, as its design is mostly influenced by JavaScript, ActionScript, Java, C#, and C. less directly, other influences include Scheme, Self, and Erlang. it has a few misc FPL features (lexical scope, first class functions/methods, closures, tail-call optimization, ...) but this isn't really its design focus. it is also being used generally fairly tightly with C at the moment, as its design features a fairly lightweight/transparent FFI, and is really rather the opposite of the Java-style make ones' own self-contained island
Re: [fonc] Alternative Web programming models?
On 04/06/2011, at 6:59 AM, Michael Forster wrote: On Fri, Jun 3, 2011 at 3:35 PM, C. Scott Ananian csc...@laptop.org wrote: [...] I'm assuming you didn't mean to be insulting. Yes, unstructured database is a bit of an oxymoron, and I intentionally used the words in this clever way, which humans can not only interpret with ease but often find amusing. ... or conflate with ease making for easy confusion among those who don't know better. Biologist choose, carefully, to speak of phenotype or genotype. Category theorists speak of a monad and its specific laws rather than, loosely, of a container thingy. Neurosurgeons are immensely careful to say postganglionic or preganglionic fiber rather than just nerve since the difference can lead to paralysis. And, everyday, people in computing industry and academia speak and reason with a sloppiness that would get a medical intern kicked off a rotation. That's pop culture. Regards, Mike A database can be more or less RIGID, and it's fairly understandable that structured means this in this context. The fact that a database IS a database automatically implies that it has SOME structure. If it wasn't a database, it'd be a piece of paper, which in turn actually has a structure, too. You're being a bit obstructionist, I fear, and I'm not entirely sure why you are being this way. I think computing is nowadays the domain of the populace (popular), so it's inevitable that a culture that evolves around computing will gain traction as being fairly popular. Yes, it sucks from one point of view. This is what we have to deal with, but it's also quite good, because we get to deal with more of the middle of the bell curve of the populace (and therefore the general level of the consciousness-awareness of humanity) than most. Our domain has so much cross-cutting concerns that it has more chance than others of becoming a truly multidisciplinary science. More-so even perhaps than psychology. This forces us to be clear, even when we're not necessarily using the most precise words, and also at the same time to appreciate an ability to listen more attentively to others. Hopefully ;-) Your sincerely Half Troll Julian. ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems
On Sat, Jun 4, 2011 at 2:12 PM, John Nilsson j...@milsson.nu wrote: Is static types really an intensic property of the language? In my mind any language can be statically typed. It is just more or less hard to do. Again, please read Gilad Bracha's position paper. He concisely enumerates the ways in which a decision to make a statically typed language inherently affects the design of other parts of the language. Similarly, a dynamically-typed language will allow design decisions that rule out static typing. He does a good job giving examples of the sorts of interactions that may occur. --scott -- ( http://cscott.net ) ___ fonc mailing list fonc@vpri.org http://vpri.org/mailman/listinfo/fonc
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
