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

[Daniel Alejandro Benavides D.]

Hi all:
Thinking about this specific issues, it is somehow related to the idea of REPL (not simple CLI).

http://en.wikipedia.org/wiki/REPL
http://www.informatik-forum.at/archive/index.php/t-76842.html
BTW there I know of a Basic-like interpreter in Modula-3 but not sure what it conditions is (for managing or graphic items in a screen).
The most related thing I have heard of is of the way the programmer hint the compiler in Fortran (as M3 old friend told me, sorry buit I refuse to translate just for that in spanish about type inference: "... en fortran se hacía por la letra inicial. luego declarando explicitamente el tipo. luego de acuerdo a las expresiones en que se usan las variables, considerando los diferentes operadores. otros ? ..."), it basically explains the fortran accepted initial letter variable names and types for it's expressions, e.g records and then accordingly to its operators. 
though typing in type finite number language is somehow easier (sic), certainly you can write a compiler for a language with dynamic types I believe or at least bootstrap from it (or anyone else). Thus is possible to believe you can write some sort of compiler a.k.a baby Modula-3 sort of evaluator in it self (still functional there should be somehow a way to proceed to be imperative at later stage) or at least express it's type checker in an untyped one, such core could later expressed for the rest of the language, such an imperative one given its denotational semantics is the one of the "Core" language which there are evaluators one of them Athena which is metatheory tool
ftp://www.ai.mit.edu/pub/koud/athena.ps
 for defining such systems and check in terms of its denotational semantics its soundness, and what it makes to modular programming languages, which I believe the most complex part but in terms of functional languages doable at most of it, its type checker and if so compose algebraically it's definitions like a computer symbolic algebra system such as Maple, or that sort). This result is what I would call Modula-3 calculi and derive other calculus such as Abadi-Cardelli "A Theory of Objects", such a system to evolve naturally or artificially the language without putting at risk it's most complex abilities checked, theorems, etc, harder properties of it (for instance construct or compact the valid idiom of ESC/M3, etc). Such a system would allows us to define the type system and its "corresponding" algebraic symbolic system (some work is already done), similar experiences Compuserve had whit a Modula-like algebraic symbolic system called AML for Algebraic
 Manipulation Language (I wouldn't be surprised if its type system is the one of Modula-3 Module system, given that it's is one of the most important for algebraic symbolic systems, according to Dr. Cardelli Modula-3's one is vastly superior of what it most of them do currently, yet it's hard to type check at compile time like Generics or). Athenas's author argues some of the unsoundness in the Simplify Theorem prover came from the fact the first order logic (predicate calculus) is undecidable, and that may become a certain amount of time to check a given procedure, but with other logics, it might be less undecidable (if you can prove somehow that can switch it's decidable space to be equally or near e.g enough typable for that matters which is hard but AFAIK is not proved but what many somehow try to do manually and do some relatively good work at least of some complexity, but certainly they are not interested in unsound or undecidable cases as most of
 them are, whatever is worse, as Dr. Greg Nelson said "P-Space" hard to reason about it (certainly not the case for his data abstraction and information hiding valid module idiom), but nevertheless quite advanced work for such a system.

Thanks in advance

--- El dom, 24/7/11, Henning Thielemann <schlepptop at henning-thielemann.de> escribió:

> De: Henning Thielemann <schlepptop at henning-thielemann.de>
> Asunto: Re: [M3devel] static typing [WAS: JIT, WAS: Google Benchmark - anyone interested in an Modula 3 version?]
> Para: m3devel at elegosoft.com
> Fecha: domingo, 24 de julio, 2011 13:51
> On 10.07.2011 15:32, Rodney M. Bates
> wrote:
> 
> > 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.
> 
> By the way, I remember the HiSoft Basic compiler on ZX
> spectrum that allowed you to run BASIC programs in a test
> mode, where the types of the variables were determined. In a
> sense (ZX Spectrum) BASIC is statically typed, since names
> of string variables must end with '$' and all alphanumeric
> variable names denote floating point numbers. The HiSoft
> Basic compiler had a richer set of numeric types: signed and
> unsigned 8-bit and 16-bit numbers and floating point
> numbers. In the test run the compiler determined for every
> variable the most restrictive type that covers all numbers
> seen during the program execution.
>