[M3devel] static typing [WAS: JIT, WAS: Google Benchmark - anyone interested in an Modula 3 version?]

[Daniel Alejandro Benavides D.]

Hi all:
I think you are correct, the semantics model of statically typed languages make them better for production code, but for the development, is up to the developer to be able to specify them clearly succinctly (such as by intention) or write them as a part of the program, in case a machine does infer them automatically it doesn't mean you won't run them untyped, since it has a typed representation, still it's untyped language, clearly the correct semantics are driven as you say algorithmically, which can be a onerous time you wouldn't want to pay for that only.
As I said and from the context the problem is time (whether development, algorithm complexity), but for independent style point of view, you want to leave the most complicated parts not for the beginning or the last step in the development, just make it work for any idealization of work (like was Baby Modula-3), still may be interpreted and be too onerous, but in machine terms be a implementable option (i.e teaching programming), thus you can argue the time dependent feature is always something you may leave up also to the programmer.
If you why I would pick such a language for teaching I would ask your learner why would he take the time to lead the system towards what you want, instead of what he wants to leave out as a programmer related task, the typing framework you may want to apply to solve a particular problem. In that sense there is obviously a need for the programmer to develop such quick constructs or to renounce them (type checking could be potentially semi definable or semi decidable) which leads to more restrictions than assumptions, which is bad in my ideal again independent point of view but good in legal time.
So what to do, good question, towards that, I mean there shouldbe a typeful programming without ill-types burden and without the price of it.
Modula-3 is closer to that little performance burden but still some price to pay, that's why Baby Modula-3 idea came from I believe, little burden in compile time, little price to pay.
Such an idealization requires good work towards implementing Baby Modula-3+ 0,1,2, etc the type system to evolve from that idea to an actual  implementation, many parted from there as departed too, but still the typing frameworks unrelated to them are too provocative for the simple point of view, what it remains to do though is to make the Baby Modula-3 be trustful for the typeful programming but in practical terms and economical terms a reality, again first TODO there would be give equational reasoning semantics for Baby Modula-3 in a subset  of it or two growing it in the better fashion to be abstracted of such, to be able to define such sublanguage in terms of the decidable framework. Give some semantics for Modula-3 that define the exact solution to that problem and yet it could be hard to prove your systems is sound or safe and implementable (can't wait for this work to be done, but still how much it takes to be done and to be able to be doable in
 terms long compile time even harder), thus I can't see what is wrong with the typed or untyped Universe as soon there is such direct relation I don't see anything **wrong** here in doing so. 
To state this in better working implementation, there are two possibilities to either choose the best you can perform, or choose the best can be done. I prefer the later since it would mean you can type programs even beyond your expectations rapidly, which is to say somehow, your typing universe is infinite, rather than somehow a perspective could say is too restrictive (I'm not saying that of course, if I may say so). In that words, the best of both worlds, the unrealizable and the implementable. This is hard to say, we have Baby Modula-3, we would have such a growing kernel to type better anything else in this and even beyond the language (as SRC-RR-95 is about)
If I may say so, the work done by Cardelly in Fsub was to perform the logical deduction of such rules in accordance to such semantics of an implementation of Modula-3, I believe one could say baby Modula-3, see:
http://lucacardelli.name/Artifacts/Drawings/FSub/FSubCartoon.pdf
http://lucacardelli.name/Artifacts/Drawings/DynamicTypecheck/DynamicCartoon.pdf
http://lucacardelli.name/Artifacts/Drawings/Typing/TypingCartoon.pdf

If anyone wants to think more absurdly there are no proves that somebody cares that, or just think that's something undone, but not unrealizable, which is the proof we might want to solve:
http://books.google.com/books?id=vJBQX7V8O3sC&lpg=RA1-PA158&ots=1ZJvSIsaeR&dq=fsub%20cardelli&pg=RA1-PA157#v=onepage&q&f=false

Absurd doesn't mean unrealizable of course, just that it is undone. (I don't know but whose would call that honest programming, perhaps would ask Dr Greg Nelson) which is by itself a gift of God of the computer typing tasks I believe (not that I compared with Juno, but related better).

Thanks in advance

--- El dom, 10/7/11, Rodney M. Bates <rodney_bates at lcwb.coop> escribió:

> De: Rodney M. Bates <rodney_bates at lcwb.coop>
> Asunto: Re: [M3devel] static typing [WAS: JIT, WAS: Google Benchmark - anyone interested in an Modula 3 version?]
> Para: "m3devel" <m3devel at elegosoft.com>
> Fecha: domingo, 10 de julio, 2011 08:32
> 
> On 07/05/2011 09:06 AM, Hendrik Boom wrote:
> > If understand correctly, these results are about
> figuring out what types
> > the programmer meant if he failed to specify
> any.  My view is that the
> > programmer probably knew full well what he meant, and
> he might as well
> > say so, in the interest of clarity if nothing
> else.  I find programs
> > with secret types to be incomprehensible, even while
> I'm writing them.
> >
> > And getting error messages if what I wrote doesn't
> match what I
> > intended, and getting better run-time, well, those are
> wonderful
> > consequences.
> >
> > -- hendrik
> >
> 
> Yes, well said!
> 
> Here is a section of a draft of an article I have been
> working on, regarding
> why I think systematic dynamic typing in programming
> languages is, for everyday
> programming, a really bad idea.  It's just one of
> several arguments.
> 
> ------------------------------------------------------------------------
> 
> 1) Dynamic typing is seldom either needed or used.
> 
> The majority of variables (1) in sensible programs are what
> I call
> _algorithmically statically typed_.  By this, I mean,
> informally, that
> there is a natural type for the variable that can be
> inferred from its
> assignments and uses.  Moreover, this is a static
> property, i.e.,
> independent of the program's inputs, and thus can be
> inferred from the
> code alone.
> 
> Slightly more formally, it means that either assignments or
> uses of
> values that are not members of this type represent buggy
> behavior, or
> at best are pathological coding and irrelevant to correct
> behavior.
> In practice, this almost always means such assignments
> don't belong,
> and such uses will result in immediate crashes.
> 
> There are a lot of pathological cases that would belie my
> claim, but
> very few that represent either correct and useful program
> behavior or
> sensible coding style.  For more elaborate discussion
> of some such
> cases and even where they might occasionally be useful, see
> (I).
> 
> This concept applies to object-oriented programming. 
> The algorithmic
> static type of a variable is just a common supertype of the
> types the
> variable could take on.  This needs to be high enough
> in the class
> hierarchy to encompass all the useful values, but not so
> high that it
> includes anything lacking a method that could be invoked on
> the
> variable.  Rarely will this be the most-general type
> in the language.
> 
> In a statically typed language, the programmer will declare
> the
> variable with a type equal to its algorithmic static
> type.  I call
> this the variable's _linguistic static type_. 
> Otherwise, a compile
> error will almost always result.  In a dynamically
> typed language,
> nothing in the code gives the type explicitly, yet it is
> nevertheless
> a static property that is vital to a reader's
> understanding.  Often,
> it will be hard work for a reader to infer.
> 
> ------------------------------------------------------------------------
> 
> Rodney Bates
>