Re: ADA Popularity Discussion Request

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 09 Sep 2004 20:47:54 -0400, jayessay wrote:

> Lionel Draghi <Lionel.nospam.Draghi@Ada-France.org> writes:
> 
>> jayessay wrote:
>> ...
>>> First, types are indeed part of program design in dynamic languages.
>>> In some respects they are even more important than in static languages
>>> as they exist at _all_ times: compile load (link) and run.  They are
>>> _always_ checked _all_ the time.  If you want to say "Ooo!  this has a
>>> performance hit", fine, but with current systems any such checks are
>>> basically in the noise.  OTOH, you can annotate a dynamic program with
>>> static type information and/or use type inference to remove this issue
>>> from most cases.
>> 
>> Jon,
>> 
>> I am trying my best to understand you without knowing Lisp, but I
>> don't. This is the second time you explain this, but you are to
>> abstract for me.
> 
> I'm not sure which part you are having trouble with.  Let's try this
> (admittedly somewhat handwavy, but intended to help get the ideas):
> 
> To a reasonable first approximation:
> 
> What is typed?
> 
> Static:  Variables and expressions (including literals and variables)

Come on, values are untyped?

> Dynamic: Values (the things you think of as "in a variable" or as the
>          result of the evaluation of an expression)
 
> Where/when is the "type"?
> 
> Static: In the compiler's symbol table and semantic analyzer; exists
>         during compilation.  Types do not exist at runtime.  To some
>         extent they are still around at link time in C++ in order for
>         template instantiation to work.

This is wrong. Types exist at run-time and there are operations on types at
run-time. In Ada there are view conversions. It is possible to create
objects of *unknown* at compile time types. See S'Class'Input attribute for
further information.
 
>         Important: Types are _not_ first class objects.

This was a design choice of Ada. This is not a property of statically typed
languages. One can well introduce types of types and have types as their
values. Static typing only means that objects of statically known types are
checked against this constraint (contract).

> Dynamic: In values; exists whenever a value exists - compiletime,
>          load/link time, and runtime.
> 
>         Important: Types _are_ first class objects, i.e., there are
>         _values_ which are _types_.  The types of these value types
>         are meta types.

You contradict yourself. When types are first class objects then types
types should be plain types and so, also be first class objects. Whether a
feasible type system can be built if everything is a first class object is
questionable. Probably one will have problems with Russel's paradox or else
some objects will be inconstructible / have undecidable types etc.

>  You can walk as far up the "logic ladder" as
>         you want with this.

This is another [IMO better] way, where there are firewalls between values
(first class objects), types (second class objects), types types (third
class objects) etc.

Anyway both alternatives have nothing to do with static analysis. When the
contract of an object of any class is statically known, it should be
checked. The contract of a constant is to have a known value. This is why
2+2 is known to be 4 prior run-time. At least my pocket calculator tells
so. (:-))

>         "Ontologically" there is no difference (they have the same
>         fundamental status) between these kinds of values and any
>         other, e.g., integers, class instances, etc.  You can bind
>         them, query them, create them, if (as in Common Lisp) you have
>         a meta object protocol (MOP) you can even _change_ them and
>         _alter_ the behavior of the type system.  There is a lot more
>         here.

Is meta object protocol an object? What is the type of the protocol? And
finally, is meta object protocol checked? Statically?

> What is checked?
> 
> Static: Variables (containers) conform to expressions

It is the contracts that are checked. Type checks is to narrow definition
of what is checked.

> Dynamic: Values conform to operations (functions operators, etc.)

Same as above.

> When are things checked?
> 
> Static: Mostly at compile time (though there are important exceptions)
> 
>         Examples: (Ada)
> 
>         x := a; The type of variable A is checked to conform
>         with the type of variable X, so that X is assured that
>         whatever the _value_ in A during runtime, it should be a
>         member of the type of X (conform to it).

Wrong, assignement in Ada may raise Constraint_Error at run-time.

>         x := a + b; the types of A & B are used to select a set of +
>         operator candidates whose result types are then checked
>         against the type of X to determine the unique operation (if it
>         exists) to use.

It depends. With multiple dispatch it is the type of x, of a and of b to
determine the operations + and :=. Anyway, in Ada if a and b are
class-wide, dispatching to + might fail at *run* time.

>         Generally, there is a good deal of copying of values going on
>         at runtime.  Variables exist only at compile time (though in
>         C++ there is some level of existence through link), they are
>         transformed to simply locations with enough space to hold
>         values of the variables type (as determined at compile
>         time)[2].

Your theory is wrong:

declare
   X : T'Class := Read_It_From_File (Stream);
        -- The size of X is unknown till run time 

> Dynamic: Mostly at runtime (though there are some useful exceptions).
> 
>          Examples: (Common Lisp)
> 
>         (let ((x a)) ...) the value _bound_ by (named by) A is _bound_
>         to X, so that X is also a _name_ for it within the scope of
>         the let.  Unless specifically requested, there are no type
>         checks being made in these cases since there is no need for it
>         - since a variable is just a binding (name) for a value it can
>         be used to name any value.  No copying is ever done.  You can
>         change or add a name to a value without opening a new scope by
>         means of setf, e.g., (setf x a)

declare
   X : T'Class renames Get_It;
      -- No copying, no specific type known

>         (let ((x (+ a b))) ...) the standard + operation is generic
>         (this is more analogous to an Ada function of a class wide
>         type, than to generics).  The dispatch mechanism checks the
>         types of A and B and either raises an exception if there is no
>         possible match or performs the operation[2].

No different from Ada's way of dispatching on multiple parameters. BTW, it
is actually a drawback of Ada that mutiple dispatch is limited to the cases
where types have same tag.

>         If the operation
>         is performed, the resulting value is _bound_ to X within the
>         scope of the let.
>
>         Values are never copied.  Variables typically do not exist at
>         runtime, with the important exception of dynamic variables
>         (full symbols).  Variables are basically transformed into
>         locations that reference values.

This is Lisp's problem. In Ada the programmer has a choice whether the
objects should have a by-value or by-reference semantics. Clearly, if you
want to put objects in a register, you will be in trouble with Lisp... 
 
> Is type consistency enforeced (is it type safe)?
> 
> Static: Mostly.  Casts, certain unchecked conversions, overlays can
>         all subvert this.

Unchecked conversion subverts nothing. It is as legal as any other
operation. It has the parameter profile, which is *checked*. It takes a
value of a distinct type and returns the result of another distinct type.
Note, types of the parameter profile tell nothing about the operation
semantics. So unchecked conversion is as good as any other. It is not
compiler's business to check program semantics.

> Dynamic: Yes, values cannot be interpreted as any type other than what
>          they are.

It is again Lisp's problems. Unchecked conversion have their place
regardless time and place types are checked.

-- 
Regards,
Dmitry Kazakov
www.dmitry-kazakov.de