Dylan type-safety 
Author Message
 Dylan type-safety

A discussion has come up in some other newsgroups (comp.lang.object a few
weeks ago, comp.lang.eiffel yesterday) about whether Dylan has strong static
type-checking.  My impression, as a relative newbie, is that it doesn't:
even if you scrupulously declare the types of all your variables and
methods, you can easily write code that causes run-time type errors with no
warning from the compiler, and with no indication in the code that you're
doing anything dangerous.

Now, most strongly-typed languages do give you some way to explicitly
circumvent type-checking (the "dynamic" type in Cecil, a downcast in Java).
These constructs can cause run-time errors if used carelessly -- but the
programmer has to make an explicit choice to use them.  Any code that avoids
these constructs will never cause a run-time type error.  It seems to me
that Dylan is much less explicit about identifying code that could cause
run-time type errors.

Of course, many people are perfectly happy with a dynamically-typed language
such as Smalltalk, and if Dylan sees itself as another language in that
category, I have no objection.  But Dylan programmers do seem to identify it
as a strongly-typed language -- or rather, as an optionally strongly-typed
language, in which you can prevent run-time type errors by following a
certain coding discipline.  I'm not convinced that is the case.

Here's a sample of some code that causes the kind of problem I'm talking
about:

  define abstract class <bird> (<object>) end;
  define class <sparrow> (<bird>) end;
  define class <penguin> (<bird>) end;

  define generic fly (b :: <bird>) => ();

  define method fly (s :: <sparrow>) => ()
    format-out("Sparrow flying!");
  end method fly;

  // don't define fly (p :: <penguin>) -- penguins can't fly!

  define method get-bird() => (bird :: <bird>)
    make(<penguin>);
  end method get-bird;

  define function do-it()
    let bird = get-bird();  // compiler doesn't know it's a penguin
    fly(bird);              // causes run-time dispatch failure
  end function do-it;

When I compile this sample with HD, in "production" mode, I don't get any
warnings.  But it causes a run-time dispatch failure.  Basically, the
<penguin> class fails to live up to its contract.  The failure should be
obvious to the compiler (or linker) in this case.  In other cases, it might
be harder to tell -- with multiple dispatch, the question of contractual
responsibility becomes much thornier.  But it seems that the HD compiler
doesn't make any attempt to catch this kind of error, and as far as I can
tell, the language definition doesn't require it to do so.

The Cecil language addresses these issues by defining a sophisticated type
system on top of the normal OO class system.  The purpose of Cecil's types
is precisely to define these sorts of contracts and let the compiler ensure
that they are fulfilled properly.  Dylan's types seem superficially similar
to Cecil's, but based on my experience I'd have to say that they don't
provide the same kind of safety that Cecil's do.

Another way to describe the problem is that Dylan's types define
implementations but not interfaces.  In Cecil, classes (actually objects)
define implementations, and types define interfaces.  In more traditional OO
languages like Eiffel (ignoring all the CAT problems for the sake of this
discussion), classes define interfaces and may define implementations as
well.  Real type-safety comes from having clearly-defined interfaces, which
Dylan doesn't support.

Can somebody prove me wrong, or shed more light on this issue?



Tue, 08 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Dylan is dynamically typed.  With the specializers on variables,
though, the programmer may give more type information to the compiler.
What the compiler chooses to do with that information is somewhat
open-ended.  To simplify a little, suppose there is some code such as

  ...
  let a :: <foo> = b;
  ...

A simple, purely dynamic, implementation would look up the value for
the variable b, check that instance?(b, <foo>), and, if so, assign
that value to a.  All type errors would be detected at run time.

A more sophisticated approach would be to analyze the code to try to
figure out the types of all values that flow into b.  Possibly (and
especially if the programmer makes good use of type annotation) the
compiler may figure out that all possible values of b will be of type
<foo>.  For example, maybe the preceding line is

   define method m (b :: <foo>)

In this case, the compiler may omit the type check before the
assignment.   Alternatively, the compiler may deduce that all possible
values of b will _not_ be an instance of <foo>;  in which case a
compile time error would be signalled.  Finally of course, the
compiler may not be able to tell, and some sort of dynamic type check
will be necessary.

One more thing that the compiler could do with the results of its
analysis is to tell the programmer what it deduced.  If the compiler
indicates all points where either a type check or a possibly-failing
dynamic dispatch occur, then code which has none of these points could
legitimately be called "statically type correct".

Harlequin Dylan has a similar feature -- code coloring (see View/Color
Dispatch Optimizations) in the HD Editor.  This technically colors
code according to optimizations applied to call sites.  Since code
cannot be directly called or inlined if there is a possibility of
dispatch failure, an "optimized" call site can be viewed as type
correct.

 Harry> A discussion has come up in some other newsgroups (comp.lang.object a few
 Harry> weeks ago, comp.lang.eiffel yesterday) about whether Dylan has strong static
 Harry> type-checking.  My impression, as a relative newbie, is that it doesn't:
 Harry> even if you scrupulously declare the types of all your variables and
 Harry> methods, you can easily write code that causes run-time type errors with no
 Harry> warning from the compiler, and with no indication in the code that you're
 Harry> doing anything dangerous.

--

Sullivan  http://www.ai.mit.edu/~gregs/



Tue, 08 Jan 2002 03:00:00 GMT  
 Dylan type-safety
Thanks for the thorough reply.  Let me make sure I understand everything
you're saying correctly:

Quote:

>What the compiler chooses to do with that information is somewhat

open-ended.

Does "open-ended" mean "not specified in the language definition"?  I.e.,
one valid compiler might accept a piece of code while another (smarter)
compiler might reject the same code as being non-type-safe?

Quote:
>Alternatively, the compiler may deduce that all possible
>values of b will _not_ be an instance of <foo>;  in which case a
>compile time error would be signalled.

So should the compiler signal an error if it can prove that _some_ execution
path will yield a value not of type <foo>, or only if it can prove that
_every_ execution path will yield a value not of type foo?  Is it even
realistic to try to prove such a thing in a language with multiple
inheritance, where a value may simultaneously conform to several unrelated
types?  That is, even if b is declared to be of unrelated type <bar>, its
value could be of a common subtype <foobar>.  I don't see how a compiler
could ever prove that the value of b will _not_ conform to <foo>, even
assuming just a single execution path.  (I suppose it could prove it if it
could trace the construction of the value all the way back to the underlying
make call and ensure that this make wasn't overloaded; but I don't think
that's feasible in most cases.)

Quote:
>If the compiler
>indicates all points where either a type check or a possibly-failing
>dynamic dispatch occur, then code which has none of these points could
>legitimately be called "statically type correct".

Do you think that most real-world Dylan code is statically type correct in
this sense?  Is this a concept that Dylan programmers care about?

Quote:
>Harlequin Dylan has a similar feature -- code coloring (see View/Color
>Dispatch Optimizations) in the HD Editor.  This technically colors
>code according to optimizations applied to call sites.  Since code
>cannot be directly called or inlined if there is a possibility of
>dispatch failure, an "optimized" call site can be viewed as type
>correct.

Interesting.  Are there common cases of code that is provably type-correct
but can't be optimized in this way?  I would guess that there are.  If so,
it would be unreasonable for a project leader to insist that all the code in
the project satisfy this "color-test".  Such insistence would probably
prevent programmers from using common OO paradigms.  In other words,
optimization is a sufficient but not necessary condition for type-safety, so
it's not always a useful way to check whether your code is type-safe.

Also, in cases where there's an error, this technique would localize it
incorrectly.  In my bird/penguin/flying example, it's not wrong to call
fly(bird) when bird is of type <penguin> -- after all, bird is of type
<bird> and there's a fly generic function on <bird>.  What's really wrong is
to declare the type <penguin> but fail to define a fly method for it.
Traditional OO languages would catch this error easily and identify it as a
problem with the <penguin> class.  But it seems that Dylan doesn't really
consider this an error, and if you coax the compiler into calling it an
error, it will say that the error is in the call to fly(bird) (which may be
in an entirely different module, written by a different programmer, who now
must dig into the definitions of <bird> and <penguin> and the fly generic
function to figure out what went wrong).

Again, I don't mean to be harshly critical of Dylan here, any more than I
would criticize Smalltalk for the same kinds of problems.  I'm simply
arguing that what Dylan provides isn't static type-safety as it's normally
understood.  Or as Lyn A Headley put it in comp.lang.eiffel yesterday,
"Maybe you guys have a different definition of static typing... I think
Dylan has a distinctly dynamically-typed feel to it."



Tue, 08 Jan 2002 03:00:00 GMT  
 Dylan type-safety


Quote:

>>What the compiler chooses to do with that information is somewhat
>>open-ended.

>Does "open-ended" mean "not specified in the language definition"?  I.e.,
>one valid compiler might accept a piece of code while another (smarter)
>compiler might reject the same code as being non-type-safe?

The Dylan language is specified in terms of runtime behavior.  Warnings
generated by the compiler are not specified by the language definition.
They are considered to be part of the development environment.

That said, the culture of the Dylan is evolving in the direction of
the providing more and more compile time analysis and feedback.
People recognize its value.

...

Quote:
>Again, I don't mean to be harshly critical of Dylan here, any more than I
>would criticize Smalltalk for the same kinds of problems.  I'm simply
>arguing that what Dylan provides isn't static type-safety as it's normally
>understood.  Or as Lyn A Headley put it in comp.lang.eiffel yesterday,
>"Maybe you guys have a different definition of static typing... I think
>Dylan has a distinctly dynamically-typed feel to it."

I would agree that Dylan has a dynamic feel to it, and I would agree
that many or most Dylan programs cannot be fully statically typed.
However, it is definitely the case that it is possible to write
Dylan programs that *are* fully statically typed.  Anyone who tells
you otherwise has not taken the time to learn the language.

Let's take a very simple example:

  define method add-two-integers (x :: <integer>, y :: <integer>)
    x + y;
  end method add-two-integers;

  define method attempt-the-impossible (z :: <list>)
    add-two-integers (z, z);
  end method attempt the impossible;

Two points about this example:

  The compiler can analyze add-two-integers, deduce the exact concrete
type of x and y, understand the set of available methods in the '+'
generic function, and inline the call to '+'.  This is possible because
the <integer> class is sealed, and so it cannot be given additional
subclasses, and because the '+' generic function is sealed over a
domain that includes <integer>.  In point of fact, Harlequin Dylan
makes this operation, and so integer arithmetic is often as efficient
as it is in C or Pascal or Assembly language.  This is true in spite
of the fact that <integer> is a full-fledged class and integers are
objects.  We don't take the Java shortcut, choosing instead to maintain
the consistency of our object model.

  Second point:  if this is your entire program, the compiler can deduce
that attempt-the-impossible will generate a type error.  It can understand
the type of z, it can understand that <list> and <integer> are disjoint,
and it can understand that there is only one method in the add-two-integers
generic function.  Harlequin Dylan will not refuse to compile the program
given above, but it will generate a serious warning when you compile it.
(Note: you'll still be able to run the program.  It may be that there are
other parts of the program that work fine, and that a type error in this
section shouldn't prevent you from testing the rest.)

  This type analysis is not rocket science.  Implementing it can be
more or less difficult, depending on how far you want to push things,
and what range of the language semantics you want to statically analyze.
But fundamentally, it is seems patently obvious that you can write
statically typed programs in Dylan.  If you disagree, we must have
different definitions of static typing, and perhaps you could let me
know what yours is.

  On the other hand, if you agree, perhaps you could forward this message
to those other news groups where people apparently don't understand
how Dylan works!

  -Andrew

p.s. give my regards to Thads if you talk to him.

--

                                            http://www.folly.org/~alms
This is our garden, although we have no grass.
-Bahrije Baftiu, Kosavar refugee in Macedonia



Tue, 08 Jan 2002 03:00:00 GMT  
 Dylan type-safety


Quote:
>  This type analysis is not rocket science.  Implementing it can be
>more or less difficult, depending on how far you want to push things,
>and what range of the language semantics you want to statically analyze.
>But fundamentally, it is seems patently obvious that you can write
>statically typed programs in Dylan.  If you disagree, we must have
>different definitions of static typing, and perhaps you could let me
>know what yours is.

One more point.  The example I gave does not define any classes.
It uses the built in classes <integer> and <list>, both of which
are sealed.  However, exactly the same analysis can be performed
on user-defined classes, provided that the proper sealing declarations
are used to prevent arbitrary extension of the classes and generic
functions involved.  The default, btw, is that these items be sealed,
so the default tends to enable more static type analysis.

--

                                            http://www.folly.org/~alms
This is our garden, although we have no grass.
-Bahrije Baftiu, Kosavar refugee in Macedonia



Tue, 08 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Quote:

> A discussion has come up in some other newsgroups (comp.lang.object a few
> weeks ago, comp.lang.eiffel yesterday) about whether Dylan has strong static
> type-checking.  My impression, as a relative newbie, is that it doesn't:
> even if you scrupulously declare the types of all your variables and
> methods, you can easily write code that causes run-time type errors with no
> warning from the compiler, and with no indication in the code that you're
> doing anything dangerous.

> Of course, many people are perfectly happy with a dynamically-typed language
> such as Smalltalk, and if Dylan sees itself as another language in that
> category, I have no objection.  But Dylan programmers do seem to identify it
> as a strongly-typed language -- or rather, as an optionally strongly-typed
> language, in which you can prevent run-time type errors by following a
> certain coding discipline.  I'm not convinced that is the case.

A certain coding discipline, together with a cetain
quality-of-implementation of the compilers, I think.

Which we probably don't yet have :-)

Quote:
> Here's a sample of some code that causes the kind of problem I'm talking
> about:

>   define abstract class <bird> (<object>) end;
>   define class <sparrow> (<bird>) end;
>   define class <penguin> (<bird>) end;

>   define generic fly (b :: <bird>) => ();

>   define method fly (s :: <sparrow>) => ()
>     format-out("Sparrow flying!");
>   end method fly;

>   // don't define fly (p :: <penguin>) -- penguins can't fly!

>   define method get-bird() => (bird :: <bird>)
>     make(<penguin>);
>   end method get-bird;

>   define function do-it()
>     let bird = get-bird();  // compiler doesn't know it's a penguin
>     fly(bird);              // causes run-time dispatch failure
>   end function do-it;

> When I compile this sample with HD, in "production" mode, I don't get any
> warnings.  But it causes a run-time dispatch failure.

What do you get in Harlequin?

I think it's interesting that what you get in Gwydion is:


Expected an instance of {the class <sparrow>}, but got {an instance of
<penguin>}
Aborted (core dumped)

This is interesting because it shows that the compiler knew quite a bit
about the situation.  In fact, here is the C code generated for do-it():

/* do-it{} */
descriptor_t * birdsZbirdsZdo_it_METH(descriptor_t *orig_sp)
{
    heapptr_t L_bird; /* bird */
    descriptor_t L_temp;

    /* #line {Class <unknown-source-location>} */

    #line 23 "./birds.dylan"
    /* get-bird{} */
    L_bird = birdsZbirdsZget_bird_METH(orig_sp);

    #line 365 "./condition.dylan"
    if ((birdsZbirdsZCLS_sparrow.heapptr == SLOT(L_bird, heapptr_t, 0))) {

        #line 24 "./birds.dylan"
        /* fly{<sparrow>} */
        birdsZbirdsZfly_METH(orig_sp, L_bird);
        return orig_sp + 0;
    }
    else {
        /* #line {Class <unknown-source-location>} */

        #line 368 "./condition.dylan"
        L_temp.heapptr = L_bird;
        L_temp.dataword.l = 0;
        /* type-error{<object>, <type>} */
        dylanZdylan_visceraZtype_error_METH(orig_sp, L_temp,
birdsZbirdsZCLS_sparrow.heapptr);
        not_reached();
    }

Quote:
}

It would seem to be quite possible to have d2c issue a warning at compile
time that there could be a runtime error at this line -- after all it just
generated one in the code!

It would also be quite possible for d2c to issue an error or a warning
when it analyses the generic function for fly() and finds that there is no
applicable method for <penguin>.

d2c does neither of these things at the moment, but if it was desired it's
just a SMOP.

Quote:
> Basically, the <penguin> class fails to live up to its contract.

The problem is that declaring...

   define generic fly (b :: <bird>) => ();

... doesn't appear according to anything I can find in the DRM to be a
contract that all subclasses of <bird> will be able to respond to fly().
I agree that it would be very desirable to have this property, but:

a) Had fly() been an open generic (generics are sealed by default) it
would be impossible to ensure this at compile time because other libraries
could add fly(<penguin>).  It would also be impossible to ensure this at
link time, because methods could be added or removed from the generic
function at runtime.  However, given that the generic function is sealed,
the compiler could certainly check this, if it was part of the language.

b) a program that doesn't define fly(<penguin>) may be correct if it
happens to never call fly() on a <penguin>.  This is, of course,
impossible to prove at compile time.

c) a program that doesn't define fly(<penguin>) may still be correct even
if it calls fly() on a <penguin> because the program might trap and deal
with the "no applicable method" exception.

d) there would be an inconsistency in that a generic function that is not
declared explicity is implicitly the same as if it had been declared
taking parameters of type <object>.  It would be unreasonable to require
that every subclass of <object> should be able to respond to a call of
such a generic function.  We thus would need to make <object> an
exception.  Which seems sucky.

I'd sure like to see Dylan have (optionally) the sort of type-safety that
you want.

What I think I could support either:

1) a compiler switch that optionally causes the compiler to check that any
generic function for which at least one required parameter is declared to
be of a class other than <object> must have an applicable method for every
subclass of that class.  Where possible (sealed class and either sealed
generic or sealed domain) this is checked at compile time, otherwise it is
checked immediately at program startup, before main() is run.

Actually, due to add-method() and remove-method() this may not be possible
at program startup, but it could be redone at the first execution of the
generic method after add-method() or remove-method() are used.  Or, we
could just not do it at all for open generics.

I'm not sure whether this counts as a change to the language defnition or
not :-) but I think I'll put in on my wish-list for d2c.

OR

2) a new pair of keywords in the declaration of a generic method.  Perhaps
"covering" could be one of them, but I'm not sure what the opposite should
be.

Clearly this *is* a language change, and would need veeeery careful
consideration.

Quote:
> Another way to describe the problem is that Dylan's types define
> implementations but not interfaces.

I'm not sure that is true.  An abstract class such as <table> pretty
clearly defines an interface rather than an implementation.

What Dylan doesn't do is guarantee that all aspects of the interface are
implemented.

Objective-C's "protocol"s and Java's "interface"s are better in that regard.

Since Dylan already has full multiple inheritence (unlike Obj-C and Java),
we have no use for a separate "protocol" concept, but it might be useful
to be able to specify the "covering" attribute for every method on a
particular (abstract?) class.  Hmmm ... maybe "protocol" and "adhoc" could
be the opposites, and could apply to either a class or to a generic
function?

Experts?

-- Bruce



Wed, 09 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Quote:

> Here's a sample of some code that causes the kind of problem I'm talking
> about:

Umm.  As an afterthought to my previous message, I guess it goes without
saying that this is a clear design/programming error in a type-safe
program, and that what *should* have happened is to have <flightless> and
<flightfull> subclasses of <bird> AND/OR have a <flying-thing> mixin
class.

In a program not intended to be fully type-safe, it's OK just hwo it is
:-)  It would be nice if we could support both styles.

-- Bruce



Wed, 09 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Quote:



>> Of course, many people are perfectly happy with a dynamically-typed
language
>> such as Smalltalk, and if Dylan sees itself as another language in that
>> category, I have no objection.  But Dylan programmers do seem to identify
it
>> as a strongly-typed language -- or rather, as an optionally
strongly-typed
>> language, in which you can prevent run-time type errors by following a
>> certain coding discipline.  I'm not convinced that is the case.

>A certain coding discipline, together with a cetain
>quality-of-implementation of the compilers, I think.

>Which we probably don't yet have :-)

Well, from what you wrote later in the same message, it seems that more than
these two things are required -- a change to the language definition would
be required to allow programmers to request the kind of static type-checking
available in many OO languages.  Since (as you've clarified for me) a
generic function declaration doesn't specify a contract that all concrete
classes must satisfy, there's really no way for the compiler to decide
whether a program is type-safe or not.  More specifically, any algorithm
that a compiler might use to ensure type-safety would also reject a large
number of perfectly valid programs, and would make it impossible to use
familiar OO programming techniques like abstract superclasses.

A true static type system must be flexible enough to allow the programmer to
express his/her intentions clearly, so that the compiler can verify that
those intentions are fulfilled.  Dylan's type system allows programmers to
express _some_ intentions, and compilers may point out _some_ violations of
those intentions at compile time.  The language extensions you proposed
(such as a "covering" keyword) would improve the expressiveness somewhat.
They might improve it enough for me to consider Dylan a true
statically-typed language.

For a language like Dylan, I would consider the following set of
capabilities as an ultimate goal:

1) You can write code with few (or no) type annotations, and the code will
be type-checked at runtime.

2) You can add type annotations in various ways to express your intentions
(or "contracts") more fully.  If you do so, the runtime system will issue an
error when you when you violate your stated intentions.  The compiler will
warn you of some violations but perhaps not all.

3) You can instruct the compiler to warn you more aggressively about
potential violations.  In this mode, any program that gets past the compiler
without warnings is guaranteed to run without runtime type errors.

4) Since the above mode is awfully restrictive, there should be some
language constructs you can use to circumvent it in specific places.  These
would be the equivalent of casts in Java: constructs that are known to be
dangerous and are used when you specifically need dynamic type-checking
instead of static type-checking.  The compiler wouldn't warn about these
constructs.  The constructs must be identifiable locally, without doing
whole-program analysis -- that is, it should be simple to write a tool that
would point out all the locations of these constructs in your code.

5) If a program runs correctly using dynamic type-checking, it should be
possible to rewrite it to use static type-checking without too much trouble,
perhaps using the known dangerous constructs in a few places.  The basic
paradigms of Dylan programming should be expressible within the static type
system.  When a program moves outside of those paradigms for some reason, it
can use the dangerous constructs as needed.

I would say that today's Dylan satisfies 1 and 2 but not 3 and 4.  5 is
clearly more subjective than the others, but I think it should be used as a
goal when designing the language features needed by 3 and 4.  For example, I
would say that Java (without generics) fails to satisfy 5, because you need
to use casts to implement common paradigms like collection classes.  Today's
Dylan _could_ be made to satisfy 3 by simply changing the compiler
implementations, but you'd be throwing out the baby with the bathwater:
you'd make it impossible to write complex programs.  In other words, if you
tried to satisfy 3 by changing the compiler only, you'd be violating 5.  The
only way to satisfy 3 and 5 together is to change the language definition.

I'm curious to see whether the Dylan language will evolve in this direction
over the next few years.  I'm also curious about how much work it would take
to accomplish this.  I believe that Cecil's type system satisfies all 5 of
the goals, but it's designed from the ground up specifically for that
purpose, and it also relies on whole-program analysis which may not be
feasible in a dynamic language like Dylan.  It would be great if Dylan's
type system can be upgraded smoothly to meet the goals.  (Even if it can't,
I'd still of course recommend Dylan to anybody interested in a
high-performance dynamically-typed language!)



Sat, 12 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Quote:

> A true static type system must be flexible enough to allow the programmer to
> express his/her intentions clearly, so that the compiler can verify that
> those intentions are fulfilled.  Dylan's type system allows programmers to
> express _some_ intentions, and compilers may point out _some_ violations of
> those intentions at compile time.  The language extensions you proposed
> (such as a "covering" keyword) would improve the expressiveness somewhat.
> They might improve it enough for me to consider Dylan a true
> statically-typed language.

Thinking about it some more, it might be reasonable for the compiler to
consider...

- an explicitly declared sealed generic function, with
- specialisers that are sealed classes

... to be a contract to supply implementations of that generic function
for all subclasses.  The same would apply to an open generic function that
has been declared to have a "sealed domain" on specialisers that are
sealed classes.

What either of these situations means is that:
- no new subclasses can be defined in this branch of the class tree,
either at runtime or in another library
- no methods that would affect the dispatch of this generic function on
this branch of the class tree can be defined, either at runtime or in
another library.

In these cases the compiler *can* statically check that there are no
potential runtime errors -- in fact d2c already does, in order to figure
out whether or not to generate a conditional call to no-applicable-method
in the generated C code -- and can issue at least a warning if not an
outright error.

I'll see if I can figure out how to add this warning to d2c. (I'm just
starting to poke around in the guts if it, so it may take a while -- I've
been confining myself to the runtime system so far).

Quote:
> 4) Since the above mode is awfully restrictive, there should be some
> language constructs you can use to circumvent it in specific places.

In this case, doesn't it suffice that the programmer can just implement a
default method on the superclass?  That kills the possibility of "no
applicable method" right there ...

-- Bruce



Sun, 13 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Quote:

> For a language like Dylan, I would consider the following set of
> capabilities as an ultimate goal:

> 1) You can write code with few (or no) type annotations, and the code will
> be type-checked at runtime.

This is a core part of Dylan. Leave the type off and this happens automatically.

Quote:
> 2) You can add type annotations in various ways to express your intentions
> (or "contracts") more fully.  If you do so, the runtime system will issue an
> error when you when you violate your stated intentions.  The compiler will
> warn you of some violations but perhaps not all.

You don't need such annotations with a language with a class system featuring
multiple inheritance and inherently polymorphic function calls.

Quote:
> 3) You can instruct the compiler to warn you more aggressively about
> potential violations.  In this mode, any program that gets past the compiler
> without warnings is guaranteed to run without runtime type errors.

I don't think this is there entirely yet, but in a mixed type safe/unsafe system
it is easy to see the limitations of such a system (they are probably provable
with simple maths or logic). This is a compiler requirement, not a language
requirement.

Quote:
> 4) Since the above mode is awfully restrictive, there should be some
> language constructs you can use to circumvent it in specific places.  These
> would be the equivalent of casts in Java: constructs that are known to be
> dangerous and are used when you specifically need dynamic type-checking
> instead of static type-checking.  The compiler wouldn't warn about these
> constructs.  The constructs must be identifiable locally, without doing
> whole-program analysis -- that is, it should be simple to write a tool that
> would point out all the locations of these constructs in your code.

This, likewise, is there already: you can cast and re-cast classes. You can
write your own type-coercers, too, which is something Java doesn't seem to have
thought of ( I work programming Java 4.5 days a week ).

Quote:
> 5) If a program runs correctly using dynamic type-checking, it should be
> possible to rewrite it to use static type-checking without too much trouble,
> perhaps using the known dangerous constructs in a few places.  The basic
> paradigms of Dylan programming should be expressible within the static type
> system.  When a program moves outside of those paradigms for some reason, it
> can use the dangerous constructs as needed.

Dylan is designed for you to be able to rapidly get going with dynamic slots,
then home in on more type safe definitions as you decide what you want.

Quote:
> I would say that today's Dylan satisfies 1 and 2 but not 3 and 4.

I am sorry, but this is incorrect. 3 is down to the compiler, not the language,
but Dylan has enough compile-time info for this to be possible. And 4 is a core
part of the language.

Please read the Dylan article in Develop, available at
http://www.mactech.com/articles/develop/issue_21/21strassman.html
It shows a project starting with typeless slots moving to stronger
type-checking, and use of classes to enforce contracts.

One of the things that attracted me to Dylan was the ability to work type-safe
or dynamic in the same language. In the same function, even. Dylan is as
type-safe as you make it, and has a far stronger and more dynamic ( the two are
not opposing ) grasp of type than many langauges.

Updating Patrick Beard's Mac Toolbox code, I am finding practical examples of a
powerfully flexible type system of a level undreamt of in C++ or Java.

- Rob.



Sun, 13 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Quote:


>> 2) You can add type annotations in various ways to express your
intentions
>> (or "contracts") more fully.  If you do so, the runtime system will issue
an
>> error when you when you violate your stated intentions.  The compiler
will
>> warn you of some violations but perhaps not all.

>You don't need such annotations with a language with a class system
featuring
>multiple inheritance and inherently polymorphic function calls.

I'm not sure what you're saying here -- do you consider all forms of static
type-checking worthless?  We could discuss that issue at great length I'm
sure.  For the purpose of this thread, I'm just trying to figure out whether
Dylan _has_ static type-checking of various sorts, not whether or not static
type-checking is important.

Quote:
>> 3) You can instruct the compiler to warn you more aggressively about
>> potential violations.  In this mode, any program that gets past the
compiler
>> without warnings is guaranteed to run without runtime type errors.

>I don't think this is there entirely yet, but in a mixed type safe/unsafe
system
>it is easy to see the limitations of such a system (they are probably
provable
>with simple maths or logic).

Well, I agree that any static type system will probably have limitations --
see 4 below.  Are those the kinds of limitations you're talking about?
Again, I guess I'm not sure what you're saying.

Quote:
>This is a compiler requirement, not a language
>requirement.

It's both.  The language has to have enough mechanism in it to let you
express your typing concepts statically, and then the compiler has to
enforce them statically.  Sure, you could make a Smalltalk compiler ensure
type-safety by simply rejecting every program you give it, but what would
that accomplish?  The language needs to allow you to annotate your code so
that the compiler can decide effectively what code to accept and what code
to reject.  That's the essence of static typing, in my opinion.

Quote:
>> 4) Since the above mode is awfully restrictive, there should be some
>> language constructs you can use to circumvent it in specific places.
These
>> would be the equivalent of casts in Java: constructs that are known to be
>> dangerous and are used when you specifically need dynamic type-checking
>> instead of static type-checking.  The compiler wouldn't warn about these
>> constructs.  The constructs must be identifiable locally, without doing
>> whole-program analysis -- that is, it should be simple to write a tool
that
>> would point out all the locations of these constructs in your code.

>This, likewise, is there already: you can cast and re-cast classes. You can
>write your own type-coercers, too, which is something Java doesn't seem to
have
>thought of ( I work programming Java 4.5 days a week ).

I'm sorry if you hate your job.  Flaws in Java's type system is another
topic that we could discuss at great length :-), but I never intended this
thread as a comparison between Dylan and Java.  Anyway, if Dylan does
already have a mechanism for indicating intentional static type violations,
that would certainly come in handy if static type-safety is ever added to
the language.

Quote:
>> 5) If a program runs correctly using dynamic type-checking, it should be
>> possible to rewrite it to use static type-checking without too much
trouble,
>> perhaps using the known dangerous constructs in a few places.  The basic
>> paradigms of Dylan programming should be expressible within the static
type
>> system.  When a program moves outside of those paradigms for some reason,
it
>> can use the dangerous constructs as needed.

>Dylan is designed for you to be able to rapidly get going with dynamic
slots,
>then home in on more type safe definitions as you decide what you want.

Of course I know that this was the goal of Dylan's design.  I'm trying to
figure out how well it meets this goal.  To that end, I've tried to express
the goal in more thorough, explicit terms.  If we go back to the sort of
vague, propagandistic language you're using here, I don't think we'll have a
productive discussion.

Quote:
>> I would say that today's Dylan satisfies 1 and 2 but not 3 and 4.

>I am sorry, but this is incorrect. 3 is down to the compiler, not the
language,
>but Dylan has enough compile-time info for this to be possible. And 4 is a
core
>part of the language.

Well, we may have to continue this discussion after Bruce has had a go at
improving type enforcement in the compiler.  I'm skeptical that Dylan can be
made to satisfy all 5 of my goals well without some fundamental changes to
the language, but I'll keep my mind open.

At the very least, some changes in the intuitive semantics of the language
will be required.  For instance, according to Bruce, declaring a generic
function with a <bird> argument does not amount to a contract that all
concrete subclasses of <bird> must provide an implementing method.  At
least, that's not how generic function declarations have been seen
historically.  Maybe we could change our view of the meaning of a g.f.d.,
and say that it does express such a contract in some cases.  That's not a
change to the language definition, but it's a change in point of view that
might take some existing Dylan programmers by surprise.  It would be nice if
this kind of change (plus changes to the compiler implementations) is all
that's required to make Dylan statically type-safe.

Quote:
>Please read the Dylan article in Develop, available at
>http://www.mactech.com/articles/develop/issue_21/21strassman.html
>It shows a project starting with typeless slots moving to stronger
>type-checking, and use of classes to enforce contracts.

A nice introduction to the way Dylan works.  Since I've already scanned the
DRM and am halfway through Feinberg, I'm not sure what you expected me to
learn from it, though.  It certainly doesn't address anything similar to the
abstract superclass problem I've been discussing in this thread.

Quote:
>Dylan is as
>type-safe as you make it

I disagree.  Using today's language definition, interpretation of the
definition, and compilers, some very simple errors are not caught at
compile-time.  Again, if Bruce is successful in the changes he's trying to
make, then we can continue this discussion.


Sun, 13 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Quote:

> Well, we may have to continue this discussion after Bruce has had a go at
> improving type enforcement in the compiler.

Uhhh.  *One* of the compilers.  Gwydion Dylan's "d2c", which is the only
open-source Dylan compiler.  It's most unlikely that you could get static
type checking in Gwydion Dylan's "Mindy" interpreter.  And neither
Harlequin's nor Apple's source code is available to private hackers like
me.

Quote:
> At the very least, some changes in the intuitive semantics of the language
> will be required.  For instance, according to Bruce, declaring a generic
> function with a <bird> argument does not amount to a contract that all
> concrete subclasses of <bird> must provide an implementing method.

I asked Andrew Shalit (who as far as I know is the ultimate authority on
what the Dylan designers intended) about this and I've appended parts of
his reply to this message.  My stuff is prefixed by "> >", Andrew's by ">"
or "> >>" (from previous comp.lang.dylan post of his).

Executive summary as I understand it:

1) a Dylan compiler may strenuously warn the programmer about possible
runtime errors

2) a Dylan compiler may have an option (could even be the default?) to
refuse to link & run the program if there are serious warnings

3) if the user wants to run it anyway, then they should be able to.

I think there's room to keep everyone happy here, *without* changing the
language definition.

-- Bruce

Quote:
> >Is the compiler *allowed* to flag an error merely based on the fact that
> >there is no fly(<penguin> and that since fly() is sealed and <bird> is
> >sealed one cannot be added by libraries or at runtime?  Would a compiler
> >which refused to compile the above library -- even if you ripped out
> >get-bird() and do-it() -- be non-conforming to the Dylan definition?

> A few points here:

>   1) I think you'd be stupid to refuse to compile this, unless your
>      compiler did so much static optimisation that it no longer had
>      the capability of compiling programs with dynamic dispatch.  Then
>      it might be ok, although the compiler would still be non-conforming,
>      because...
>   2) Dylan specifies the runtime behavior of these type errors.  That
>      implies that type errors are within the correct semantics of the
>      language.  They are logical errors, not semantic errors.  They
>      shouldn't prevent programs from compiling or running.  That said,
>   3) You could certainly choose to issue a compile-time warning, ring
>      all sorts of bells, and send smoke out the floppy disk drive.  Sure,
>      let the programmer know there is a potential runtime error.  But
>      give the programmer the option of saying, "I know, I don't care,
>      and cool it with the smoke because my office mate has asthma."

> >It seems to me that declaring something like " define generic fly (b ::
> ><bird>) => ();" really is showing an intention to implement fly() for all
> >subclasses of <bird> and that if you don't then it's either because you've
> >forgotten, or because you made a big mistake in your class hierachy.  If
> >you've got other intentions then surely you're going to have made either or
> >both of fly() or <bird> open?

> I disagree.  It might be a sign of a poorly designed program.  But then,
> I think trying to make it impossible to write poorly designed programs
> is beyond the scope of the Dylan effort (or any language design effort,
> for that matter).  And it might not even be a poorly designed program.
> It might just be a compromise involving a very complex class hierarchy.

[...]

Quote:
> >>Harlequin Dylan will not refuse to compile the program
> >>given above, but it will generate a serious warning when you compile it.
> >>(Note: you'll still be able to run the program.  It may be that there are
> >>other parts of the program that work fine, and that a type error in this
> >>section shouldn't prevent you from testing the rest.)

> >A good point, but there are arguments for refusing to run as well.  Perhaps
> >an optional "treat warnings as errors" flag?

> Harlequin Dylan has a flag specifying whether serious warnings should stop
> the build cycle before linking.

[...]

- Show quoted text -

Quote:
> OK, last point.  In spite of all my disagreements, I really do agree with
> your basic point that Dylan should do more compile-time type checking and
> method selection checking.  Here's how I would summarize.

>  1. Dylan compilers should attempt to find places where runtime errors
>     will occur or might occur.  When it finds such places, it should flag
>     them, but not prevent compilation from completing.
>  2. If the Dylan compiler can prove that there is no applicable method
>     for a given function call, it should flag this as a serious warning.
>     All programmers will want to know this.
>  3. On the other hand, there is the more ambiguous case where the compiler
>     simply doesn't know whether there will be an applicable method.  This
>     might be because (a) it doesn't know the types of the arguments with
>     sufficient specificity or (b) because the generic function is open, or
>     (c) some combination of a and b.  Most correct programs written to
>     date have many such situations, and it's perfectly acceptable Dylan style
>     to write such programs.

> I think it would be a very interesting experiment to have a compiler mode
> which flagged all cases of (3).  The first time you ran a program through
> it, you'd probably have so many warnings you wouldn't know where to start
> looking.  But eventually you'd be able to whittle them down, and you'd
> undoubtedly find some bugs.  I doubt you'd be able to get rid of all of
> them, though.

> This experiment might also provide some insight into ways in which to
> evolve the Dylan language in the future.

> Thanks for the question.  It's an interesting topic that I've thought about
> and talked with people at Harlequin about previously.  I'd love to see
> some progress on it.



Mon, 14 Jan 2002 03:00:00 GMT  
 Dylan type-safety

Hi guys,

Quote:
> Executive summary as I understand it:

> 1) a Dylan compiler may strenuously warn the programmer about
> possible runtime errors

> 2) a Dylan compiler may have an option (could even be the default?)
> to refuse to link & run the program if there are serious warnings

> 3) if the user wants to run it anyway, then they should be able to.

> I think there's room to keep everyone happy here, *without* changing
> the language definition.

This is a really interesting discussion. I agree with Harry's general
opinion, and I also like his list of five rules. I believe that there
are parts of Dylan that make it impossible to write a completely
static program, such that the warnings issued are as accurate as those
available for the equivalent C program. I would like to evolve Dylan
to fix any such problems that this group can find, so that it really
is possible to write a completely static Dylan program.

IMO, one of the best intentions of Dylan is that it is a statically
compiled language except when the programmer explicitly requests for
some aspects of it to be dynamic. This means that by default Dylan
programs should be efficient with accurate compile-time warnings, and
the cost of dynamic programming can be carefully introduced as
necessary. I think there are a few areas in the current design that
fall short of this lofty goal.

Here's an example that has been discussed a lot at Harlequin, I'd like
to hear some more opinions. The Dylan language specification states
that a generic function can list a set of keywords, but that any
method is allowed to add new keywords. This has the unfortunate side
effect that the compiler can never determine the valid set of keywords
for an open generic, unless the particular domain in question is
sealed.

So, with the following code:

  define abstract class <foo> (<object>)
  end class <foo>;

  define open generic foo
      (foo :: <foo>, #key x :: <integer>, y :: <integer>) => ();

  define function bar
      (f :: <foo>) => ()
    foo(f, z: 20)
  end function bar;

the compiler cannot issue any warnings about the keyword z: because
there is no way to know if that keyword is actually accepted by the
applicable method.

If you consider how many important generic functions are declared
open, a large percentage of Dylan code passes through Harlequin Dylan
without any warnings for incorrect keyword arguments. This means that
bugs in obscure parts of the code are not found at compile-time, and
so only get found by very thorough QA, or worse still are first
discovered by customers.

IMO there needs to be a language change to allow a generic to declare
exactly the set of allowable keywords, that way the compiler can issue
warnings. IMO this should be the default, based on the 'static by
default' principle, so creating a generic that allows methods to
handle extra keywords would need to take an extra argument. Something
like:

  define open generic make
      (class :: <class>, #key, #other-keys)
   => (object :: <object>)

The distinction between #other-keys and #all-keys would be that it is
an error to pass unacceptable keywords to a function that takes
#other-keys, but it isn't for one that takes #all-keys (the extra
keywords are just ignored).

My contention would be that #other-keys really isn't needed very
often, almost every generic function that I can think of takes a rigid
set of keywords. It is unfortunate that making this rare situation the
default disallows the compiler from enforcing the validity of keyword
arguments at compile-time.

Well, that was pretty long, it's just one example of several places in
Dylan that don't properly scale to a static programming style. I
believe with some careful thought we could redesign the langauge to
fix these issues, and that this would make an already great language
even better.

Cheers,

Andy

P.S. I would like to make clear that I'm not attacking dynamic
programming, in fact I love it. I also would like to strongly endorse
Andrew Shalit's point that a program with potential runtime errors
should be allowed to be built and run, at the very least this feature
is of great benefit when writing test suites:

  check-condition("Verify integer overflow",
                  <integer-overflow>,
                  $maximum-integer + 1);

----------

Harlequin Inc.



Mon, 14 Jan 2002 03:00:00 GMT  
 Dylan type-safety


Quote:
>> OK, last point.  In spite of all my disagreements, I really do agree with
>> your basic point that Dylan should do more compile-time type checking and
>> method selection checking.  Here's how I would summarize.

>>  1. Dylan compilers should attempt to find places where runtime errors
>>     will occur or might occur.  When it finds such places, it should flag
>>     them, but not prevent compilation from completing.
>>  2. If the Dylan compiler can prove that there is no applicable method
>>     for a given function call, it should flag this as a serious warning.
>>     All programmers will want to know this.
>>  3. On the other hand, there is the more ambiguous case where the compiler
>>     simply doesn't know whether there will be an applicable method.  This
>>     might be because (a) it doesn't know the types of the arguments with
>>     sufficient specificity or (b) because the generic function is open, or
>>     (c) some combination of a and b.  Most correct programs written to
>>     date have many such situations, and it's perfectly acceptable Dylan style
>>     to write such programs.

>> I think it would be a very interesting experiment to have a compiler mode
>> which flagged all cases of (3).  The first time you ran a program through
>> it, you'd probably have so many warnings you wouldn't know where to start
>> looking.  But eventually you'd be able to whittle them down, and you'd
>> undoubtedly find some bugs.  I doubt you'd be able to get rid of all of
>> them, though.

To clarify:  I don't think you could get rid of all warnings of type (3)
in an existing Dylan program of any size, because Dylan programmers to
date do not program with that kind of type checking in mind.  (They
use lists and other non-limited collections, etc.)

On the other hand, I do think it would be possible to write a Dylan
program from scratch which had no warnings of type 1, 2, or 3.  This
would require that you write in a subset of Dylan, but it would still
be a very powerful subset.  By supporting this kind of warning mechanism,
we would also gain insights in how the language would need to be changed
to extend this type safe subset.

  -Andrew

p.s. to Harry: if you've only made it half way through the DRM, skip
ahead and read the chapter on sealing.  That should make a lot of
this clearer.  That's where you lock things down, and really support
static compilation.

--

                                            http://www.folly.org/~alms
This is our garden, although we have no grass.
-Bahrije Baftiu, Kosavar refugee in Macedonia



Mon, 14 Jan 2002 03:00:00 GMT  
 Dylan type-safety


Quote:
>>>  3. On the other hand, there is the more ambiguous case where the compiler
>>>     simply doesn't know whether there will be an applicable method.  This
>>>     might be because (a) it doesn't know the types of the arguments with
>>>     sufficient specificity or (b) because the generic function is open, or
>>>     (c) some combination of a and b.  Most correct programs written to
>>>     date have many such situations, and it's perfectly acceptable Dylan
>>>     style to write such programs.

>>> I think it would be a very interesting experiment to have a compiler mode
>>> which flagged all cases of (3).  The first time you ran a program through
>>> it, you'd probably have so many warnings you wouldn't know where to start
>>> looking.  But eventually you'd be able to whittle them down, and you'd
>>> undoubtedly find some bugs.  I doubt you'd be able to get rid of all of
>>> them, though.

>To clarify:  I don't think you could get rid of all warnings of type (3)
>in an existing Dylan program of any size...

                      ^^^^^^^^^^^^^^^^^^^

Should have written "of any substantial size" (i.e. large).

--

                                            http://www.folly.org/~alms
This is our garden, although we have no grass.
-Bahrije Baftiu, Kosavar refugee in Macedonia



Mon, 14 Jan 2002 03:00:00 GMT  
 
 [ 16 post ]  Go to page: [1] [2]

 Relevant Pages 

1. Language Design (Re: Dylan type-safety )

2. Hi all - new to smalltalk [type services and type-safety]

3. Type restrictions / type safety in Smalltalk?

4. Eiffel Type-Safety Reference

5. breaking Eiffel's type safety?

6. Realising type-safety

7. Realising type-safety

8. Eiffel type safety.

9. type safety in LISP

10. Using type declarations in safety checks

11. An Attempt to Formalise Dylan's Type System (Part 2)

12. An Attempt to Formalise Dylan's Type System (Part 1)

 

 
Powered by phpBB® Forum Software