Author |
Message |
Harry Chomsk #1 / 16
|
 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 |
|
 |
Gregory T. Sulliv #2 / 16
|
 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 |
|
 |
Harry Chomsk #3 / 16
|
 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 |
|
 |
Andrew LM Shali #4 / 16
|
 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 |
|
 |
Andrew LM Shali #5 / 16
|
 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 |
|
 |
Bruce Hou #6 / 16
|
 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 |
|
 |
Bruce Hou #7 / 16
|
 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 |
|
 |
Harry Chomsk #8 / 16
|
 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 |
|
 |
Bruce Hou #9 / 16
|
 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 |
|
 |
Rob Myer #10 / 16
|
 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 |
|
 |
Harry Chomsk #11 / 16
|
 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 |
|
 |
Bruce Hou #12 / 16
|
 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.
[...] 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 |
|
 |
Andy Armstron #13 / 16
|
 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 |
|
 |
Andrew LM Shali #14 / 16
|
 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 |
|
 |
Andrew LM Shali #15 / 16
|
 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 |
|
|
Page 1 of 2
|
[ 16 post ] |
|
Go to page:
[1]
[2] |
|