Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems

2011-06-07 Thread Alan Kay
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

Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems

2011-06-07 Thread David Barbour
On Sat, Jun 4, 2011 at 9:04 AM, Scott McLoughlin scottmc...@gmail.comwrote:

 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


Well, most static type systems aren't well designed for 'open' composition.
It is difficult, for example, to obtain a Haskell function from a plugin
resource. Without effective support for open composition, developers are
under pressure to duplicate services within each application or module.
 However, they'll end up duplicating services in diverse and subtly
incompatible ways (witness the plethora of collections types) so they'll
also need a lot of adapter code. The problem quickly snowballs, growing ever
more monolithic.

But static typing isn't the culprit. We could, presumably, design a static
type system suitable for open composition with loose coupling... though, we
may need to compromise on a  few useful features.
___
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

2011-06-06 Thread Alexis Read
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

Re: [fonc] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems

2011-06-04 Thread Michael Forster
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

2011-06-04 Thread Alan Kay
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

2011-06-04 Thread Michael Forster
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

2011-06-04 Thread Antoine van Gelder
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

2011-06-04 Thread Michael Forster
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

2011-06-04 Thread Scott McLoughlin

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

2011-06-04 Thread Toon Verwaest
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

2011-06-04 Thread BGB

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] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems

2011-06-04 Thread C. Scott Ananian
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

2011-06-04 Thread Alexis Read
 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] Static typing and/vs. boot strap-able, small kernel, comprehensible, user modifiable systems

2011-06-03 Thread Scott McLoughlin

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.


___
fonc mailing list
fonc@vpri.org
http://vpri.org/mailman/listinfo/fonc