Re: What is Expressiveness in a Computer Language
Chris F Clark wrote: > > A static > type system eliminates some set of tags on values by syntactic > analysis of annotations (types) written with or as part of the program > and detects some of the disallowed compuatations (staticly) at compile > time. Explicit annotations are not a necessary ingredient of a type system, nor is "eliminating tags" very relevant to its function. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > > No, that isn't what I said. What I said was: > "A language is latently typed if a value has a property - called it's > type - attached to it, and given it's type it can only represent values > defined by a certain class." "it [= a value] [...] can [...] represent values"? > Easy, any statically typed language is not latently typed. Values have > no type associated with them, instead variables have types. A (static) type system assigns types to (all) *expressions*. This includes values as well as variables. Don't confuse type assignment with type annotation (which many mainstream languages enforce for, but also only allow for, variable declarations). - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: >> >>>No, that isn't what I said. What I said was: >>>"A language is latently typed if a value has a property - called it's >>>type - attached to it, and given it's type it can only represent values >>>defined by a certain class." >> >>"it [= a value] [...] can [...] represent values"? > > ??? I just quoted, in condensed form, what you said above: namely, that a value represents values - which I find a strange and circular definition. >>A (static) type system assigns types to (all) *expressions*. > > That's right most of the time yes, I probably should have said > expressions. Though I can think of static typed languages where the > resulting type of an expression depends on the type of the variable it > is being assigned to. Yes, but that's no contradiction. A type system does not necessarily assign *unique* types to individual expressions (consider overloading, subtyping, polymorphism, etc). > Well I haven't programmed in any statically typed language where values > have types themselves. They all have - the whole purpose of a type system is to ensure that any expression of type T always evaluates to a value of type T. So when you look at type systems formally then you certainly have to assign types to values, otherwise you couldn't prove any useful property about those systems (esp. soundness). - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
David Squire wrote: > Andreas Rossberg wrote: > >> Rob Thorpe wrote: >> >>>> >>>>> No, that isn't what I said. What I said was: >>>>> "A language is latently typed if a value has a property - called it's >>>>> type - attached to it, and given it's type it can only represent >>>>> values >>>>> defined by a certain class." >>>> >>>> >>>> "it [= a value] [...] can [...] represent values"? >>> >>> >>> ??? >> >> I just quoted, in condensed form, what you said above: namely, that a >> value represents values - which I find a strange and circular definition. > > But you left out the most significant part: "given it's type it can only > represent values *defined by a certain class*" (my emphasis). That qualification does not remove the circularity from the definition. > In C-ish notation: > > unsigned int x; > > means that x can only represent elements that are integers elements of > the set (class) of values [0, MAX_INT]. Negative numbers and non-integer > numbers are excluded, as are all sorts of other things. I don't see how that example is relevant, since the above definition does not mention variables. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: >Andreas Rossberg wrote: >>Rob Thorpe wrote: >> >>>>>"A language is latently typed if a value has a property - called it's >>>>>type - attached to it, and given it's type it can only represent values >>>>>defined by a certain class." >>>> >>>>"it [= a value] [...] can [...] represent values"? >>> >>>??? >> >>I just quoted, in condensed form, what you said above: namely, that a >>value represents values - which I find a strange and circular definition. > > Yes, but the point is, as the other poster mentioned: values defined by > a class. I'm sorry, but I still think that the definition makes little sense. Obviously, a value simply *is* a value, it does not "represent" one, or several ones, regardless how you qualify that statement. >>>Well I haven't programmed in any statically typed language where values >>>have types themselves. >> >>They all have - the whole purpose of a type system is to ensure that any >>expression of type T always evaluates to a value of type T. > > But it only gaurantees this because the variables themselves have a > type, No, variables are insignificant in this context. You can consider a language without variables at all (such languages exist, and they can even be Turing-complete) and still have evaluation, values, and a non-trivial type system. > But the value itself has no type You mean that the type of the value is not represented at runtime? True, but that's simply because the type system is static. It's not the same as saying it has no type. > in a C program for example I can take > the value from some variable and recast it in any way I feel and the > language cannot correct any errors I make because their is no > information in the variable to indicate what type it is. Nothing in the C spec precludes an implementation from doing just that. The problem with C rather is that its semantics is totally underspecified. In any case, C is about the worst example to use when discussing type systems. For starters, it is totally unsound - which is what your example exploits. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
David Hopwood wrote: > > Oh, but it *does* make sense to talk about dynamic tagging in a statically > typed language. It even makes perfect sense to talk about dynamic typing in a statically typed language - but keeping the terminology straight, this rather refers to something like described in the well-known paper of the same title (and its numerous follow-ups): Martin Abadi, Luca Cardelli, Benjamin Pierce, Gordon Plotkin Dynamic typing in a statically-typed language. Proc. 16th Symposium on Principles of Programming Languages, 1989 / TOPLAS 13(2), 1991 Note how this is totally different from simple tagging, because it deals with real types at runtime. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > > I think this should make it clear. If I have a "xyz" in lisp I know it > is a string. > If I have "xyz" in an untyped language like assembler it may be > anything, two pointers in binary, an integer, a bitfield. There is no > data at compile time or runtime to tell what it is, the programmer has > to remember. You have to distinguish between values (at the level of language semantics) and their low-level representation (at the implementation level). In a high-level language, the latter should be completely immaterial to the semantics, and hence not interesting for the discussion. >>No, variables are insignificant in this context. You can consider a >>language without variables at all (such languages exist, and they can >>even be Turing-complete) and still have evaluation, values, and a >>non-trivial type system. > > Hmm. You're right, ML is no-where in my definition since it has no > variables. Um, it has. Mind you, it has no /mutable/ variables, but that was not even what I was talking about. >>>But the value itself has no type >> >>You mean that the type of the value is not represented at runtime? True, >>but that's simply because the type system is static. It's not the same >>as saying it has no type. > > Well, is it even represented at compile time? > The compiler doesn't know in general what values will exist at runtime, > it knows only what types variables have. Sometimes it only has partial > knowledge and sometimes the programmer deliberately overrides it. From > what knowledge it you could say it know what types values will have. Again, variables are insignificant. From the structure of an expression the type system derives the type of the resulting value. An expression may contain variables, and then the type system generally must know (or be able to derive) their types too, but that's a separate issue. Most values are anonymous. Nevertheless their types are known. > Unfortunately it's often necessary to break static type systems. Your definitely using the wrong static language then. ;-) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris Uppal wrote: > > I have never been very happy with relating type to sets of values (objects, > whatever). Indeed, this view is much too narrow. In particular, it cannot explain abstract types, which is *the* central aspect of decent type systems. There were papers observing this as early as 1970. A type system should rather be seen as a logic, stating invariants about a program. This can include operations supported by values of certain types, as well as more advanced properties, e.g. whether something can cause a side-effect, can diverge, can have a deadlock, etc. (There are also theoretic problems with the types-as-sets view, because sufficiently rich type systems can no longer be given direct models in standard set theory. For example, first-class polymorphism would run afoul the axiom of foundation.) > It's worth noting, too, that (in some sense) the type of an object can change > over time[*]. No. Since a type expresses invariants, this is precisely what may *not* happen. If certain properties of an object may change then the type of the object has to reflect that possibility. Otherwise you cannot legitimately call it a type. Taking your example of an uninitialised reference, its type is neither "reference to nil" nor "reference to object that understands message X", it is in fact the union of both (at least). And indeed, languages with slightly more advanced type systems make things like this very explicit (in ML for example you have the option type for that purpose). - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > > While we're on the topic of terminology, here's a pet peeve of > mine: "immutable variable." > > immutable = can't change > vary-able = can change > > Clearly a contradiction in terms. > > If you have a named value that cannot be updated, it makes > no sense to call it "variable" since it isn't *able* to *vary.* > Let's call it a named constant. The name of a function argument is a variable. Its denotation changes between calls. Still it cannot be mutated. Likewise, local "constants" depending on an argument are not constant. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz wrote: >> >>> It's worth noting, too, that (in some sense) the type of an object >>> can change over time[*]. >> >> No. Since a type expresses invariants, this is precisely what may >> *not* happen. > > No. A type is a set of allowable values, allowable operations, and > constraints on the operations (which are often called "invariants" but > they are invariant only as long as the type is invariant). The purpose of a type system is to derive properties that are known to hold in advance. A type is the encoding of these properties. A type varying over time is an inherent contradiction (or another abuse of the term "type"). - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Darren New wrote: > > As far as I know, LOTOS is the only > language that *actually* uses abstract data types Maybe I don't understand what you mean with ADT here, but all languages with a decent module system support ADTs in the sense it is usually understood, see ML for a primary example. Classes in most OOPLs are essentially beefed-up ADTs as well. > Indeed, the ability to declare a new type that has the exact same > underlying representation and isomorphically identical operations but > not be the same type is something I find myself often missing in > languages. It's nice to be able to say "this integer represents vertical > pixel count, and that represents horizontal pixel count, and you don't > get to add them together." Not counting C/C++, I don't know when I last worked with a typed language that does *not* have this ability... (which is slightly different from ADTs, btw) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Vesa Karvonen wrote: > >>>Indeed, the ability to declare a new type that has the exact same >>>underlying representation and isomorphically identical operations but >>>not be the same type is something I find myself often missing in >>>languages. It's nice to be able to say "this integer represents vertical >>>pixel count, and that represents horizontal pixel count, and you don't >>>get to add them together." > >>Not counting C/C++, I don't know when I last worked with a typed >>language that does *not* have this ability... (which is slightly >>different from ADTs, btw) > > Would Java count? Yes, you are right. And there certainly are more in the OO camp. But honestly, I do not remember when I last had to actively work with one of them, including Java... :-) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Darren New wrote: > >> Maybe I don't understand what you mean with ADT here, but all >> languages with a decent module system support ADTs in the sense it is >> usually understood, see ML for a primary example. > > OK. Maybe some things like ML and Haskell and such that I'm not > intimately familiar with do, now that you mention it, yes. Well, Modula and CLU already had this, albeit in restricted form. >> Classes in most OOPLs are essentially beefed-up ADTs as well. > > Err, no. There's nothing really abstract about them. And their values > are mutable. So while one can think about them as an ADT, one actually > has to write code to (for example) calculate or keep track of how many > entries are on a stack, if you want that information. Now you lost me completely. What has mutability to do with it? And the stack? AFAICT, ADT describes a type whose values can only be accessed by a certain fixed set of operations. Classes qualify for that, as long as they provide proper encapsulation. >> Not counting C/C++, I don't know when I last worked with a typed >> language that does *not* have this ability... (which is slightly >> different from ADTs, btw) > > Java? C#? Icon? Perl? (Hmmm... Pascal does, IIRC.) I guess you just work > with better languages than I do. :-) OK, I admit that I exaggerated slightly. Although currently I'm indeed able to mostly work with the more pleasant among languages. :-) (Btw, Pascal did not have it either, AFAIK) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: >Andreas Rossberg wrote: >>Chris Uppal wrote: >> >>>I have never been very happy with relating type to sets of values (objects, >>>whatever). >> >>Indeed, this view is much too narrow. In particular, it cannot explain >>abstract types, which is *the* central aspect of decent type systems. > > What prohibits us from describing an abstract type as a set of values? If you identify an abstract type with the set of underlying values then it is equivalent to the underlying representation type, i.e. there is no abstraction. >>There were papers observing this as early as 1970. > > References? This is 1973, actually, but most relevant: James Morris Types Are Not Sets. Proc. 1st ACM Symposium on Principles of Programming Languages, 1973 >>(There are also theoretic problems with the types-as-sets view, because >>sufficiently rich type systems can no longer be given direct models in >>standard set theory. For example, first-class polymorphism would run >>afoul the axiom of foundation.) > > There is no reason why we must limit ourselves to "standard set theory" > any more than we have to limit ourselves to standard type theory. > Both are progressing, and set theory seems to me to be a good > choice for a foundation. What else would you use? I'm no expert here, but Category Theory is a preferred choice in many areas of PLT. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Warnock wrote: > > Here's what the Scheme Standard has to say: > > http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs-Z-H-4.html > 1.1 Semantics > ... > Scheme has latent as opposed to manifest types. Types are assoc- > iated with values (also called objects) rather than with variables. > (Some authors refer to languages with latent types as weakly typed > or dynamically typed languages.) Other languages with latent types > are APL, Snobol, and other dialects of Lisp. Languages with manifest > types (sometimes referred to as strongly typed or statically typed > languages) include Algol 60, Pascal, and C. Maybe this is the original source of the myth that static typing is all about assigning types to variables... With all my respect to the Scheme people, I'm afraid this paragraph is pretty off, no matter where you stand. Besides the issue just mentioned it equates "manifest" with static types. I understand "manifest" to mean "explicit in code", which of course is nonsense - static typing does not require explicit types. Also, I never heard "weakly typed" used in the way they suggest - in my book, C is a weakly typed language (= typed, but grossly unsound). > To me, the word "latent" means that when handed a value of unknown type > at runtime, I can look at it or perform TYPE-OF on it or TYPECASE or > something and thereby discover its actual type at the moment[1], whereas > "manifest" means that types[2] are lexically apparent in the code. Mh, I'd say typecase is actually a form of reflection, which is yet a different issue. Moreover, there are statically typed languages with typecase (e.g. Modula-3, and several more modern ones) or related constructs (consider instanceof). - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Costanza wrote: > > Consider a simple expression like 'a + b': In a dynamically typed > language, all I need to have in mind is that the program will attempt to > add two numbers. In a statically typed language, I additionally need to > know that there must a guarantee that a and b will always hold numbers. I'm confused. Are you telling that you just write a+b in your programs without trying to ensure that a and b are in fact numbers?? - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris Uppal wrote: > >>>It's worth noting, too, that (in some sense) the type of an object can >>>change over time[*]. >> >>No. Since a type expresses invariants, this is precisely what may *not* >>happen. If certain properties of an object may change then the type of >>the object has to reflect that possibility. Otherwise you cannot >>legitimately call it a type. > > Well, it seems to me that you are /assuming/ a notion of what kinds of logic > can be called type (theories), and I don't share your assumptions. No offence > intended. OK, but can you point me to any literature on type theory that makes a different assumption? > I see no reason, > even in practise, why a static analysis should not be able to see that the set > of acceptable operations (for some definition of acceptable) for some > object/value/variable can be different at different times in the execution. Neither do I. But what is wrong with a mutable reference-to-union type, as I suggested? It expresses this perfectly well. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Bourguignon wrote: > > For example, sort doesn't need to know what type the objects it sorts > are. It only needs to be given a function that is able to compare the > objects. Sure. That's why any decent type system supports polymorphism of this sort. (And some of them can even infer which comparison function to pass for individual calls, so that the programmer does not have to bother.) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: >> >>>What prohibits us from describing an abstract type as a set of values? >> >>If you identify an abstract type with the set of underlying values then >>it is equivalent to the underlying representation type, i.e. there is no >>abstraction. > > I don't follow. Are you saying that a set cannot be described > intentionally? How is "the set of all objects that implement the > Foo interface" not sufficiently abstract? Is it possible you are > mixing in implementation concerns? "Values" refers to the concrete values existent in the semantics of a programming language. This set is usually infinite, but basically fixed. To describe the set of "values" of an abstract type you would need "fresh" values that did not exist before (otherwise the abstract type would be equivalent to some already existent type). So you'd need at least a theory for name generation or something similar to describe abstract types in a types-as-sets metaphor. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > > Its easy to create a reasonable framework. Luca Cardelli has given the most convincing one in his seminal tutorial "Type Systems", where he identifies "typed" and "safe" as two orthogonal dimensions and gives the following matrix: | typed | untyped ---+---+-- safe | ML| Lisp unsafe | C | Assembler Now, jargon "dynamically typed" is simply untyped safe, while "weakly typed" is typed unsafe. > The real objection to this was that latently/dynamically typed > languages have a place in it. But some of the advocates of statically > typed languages wish to lump these languages together with assembly > language a "untyped" in an attempt to label them as unsafe. No, see above. And I would assume that that is how most proponents of the typed/untyped dichotomy understand it. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > > What we generally (in programming) call variables are locals > and globals. If the languages supports an update operation > on those variables, then calling them variables makes sense. > But "variable" has become such a catch-all term that we call > > public static final int FOO = 7; > > a variable, even though it can never, ever vary. > > That doesn't make any sense. It does, because it is only a degenerate case. In general, you can have something like void f(int x) { const int foo = x+1; //... } Now, foo is still immutable, it is a local, but it clearly also varies. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
David Hopwood wrote: >> >>"Values" refers to the concrete values existent in the semantics of a >>programming language. This set is usually infinite, but basically fixed. >>To describe the set of "values" of an abstract type you would need >>"fresh" values that did not exist before (otherwise the abstract type >>would be equivalent to some already existent type). So you'd need at >>least a theory for name generation or something similar to describe >>abstract types in a types-as-sets metaphor. > > Set theory has no difficulty with this. It's common, for example, to see > "the set of strings representing propositions" used in treatments of > formal systems. Oh, I was not saying that this particular aspect cannot be described in set theory (that was a different argument, about different issues). Just that you cannot naively equate types with a set of underlying values, which is what is usually meant by the types-are-sets metaphor - to capture something like type abstraction you need to do more. (Even then it might be arguable if it really describes the same thing.) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris Uppal wrote: >>> >>>Well, it seems to me that you are /assuming/ a notion of what kinds of >>>logic can be called type (theories), and I don't share your >>>assumptions. No offence intended. >> >>OK, but can you point me to any literature on type theory that makes a >>different assumption? > > 'Fraid not. (I'm not a type theorist -- for all I know there may be lots, but > my suspicion is that they are rare at best.) I would suspect the same :-). And the reason is that "type" has a well-established use in theory. It is not just my "assumption", it is established practice since 80 or so years. So far, this discussion has not revealed the existence of any formal work that would provide a theory of "dynamic types" in the sense it is used to characterise "dynamically typed" languages. So what you are suggesting may be an interesting notion, but it's not what is called "type" in a technical sense. Overloading the same term for something different is not a good idea if you want to avoid confusion and misinterpretations. > But, as a sort of half-way, semi-formal, example: consider the type > environment > in a Java runtime. The JVM does formal type-checking of classfiles as it > loads > them. In most ways that checking is static -- it's treating the bytecode as > program text and doing a static analysis on it before allowing it to run (and > rejecting what it can't prove to be acceptable by its criteria). However, it > isn't /entirely/ static because the collection of classes varies at runtime in > a (potentially) highly dynamic way. So it can't really examine the "whole" > text of the program -- indeed there is no such thing. So it ends up with a > hybrid static/dynamic type system -- it records any assumptions it had to make > in order to find a proof of the acceptability of the new code, and if > (sometime > in the future) another class is proposed which violates those assumptions, > then > that second class is rejected. Incidentally, I know this scenario very well, because that's what I'm looking at in my thesis :-). All of this can easily be handled coherently with well-established type machinery and terminology. No need to bend existing concepts and language, no need to resort to "dynamic typing" in the way Java does it either. > In code which will be executed at instant A > obj aMessage."type correct" > obj anotherMessage. "type incorrect" > > In code which will be executed at instant B > obj aMessage. "type incorrect" > obj anotherMessage."type correct" > > I don't see how a logic with no temporal element can arrive at all four those > judgements, whatever it means by a union type. I didn't say that the type system cannot have temporal elements. I only said that a type itself cannot change over time. A type system states propositions about a program, a type assignment *is* a proposition. A proposition is either true or false (or undecidable), but it is so persistently, considered under the same context. So if you want a type system to capture temporal elements, then these must be part of a type itself. You can introduce types with implications like "in context A, this is T, in context B this is U". But the whole quoted part then is the type, and it is itself invariant over time. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Gabriel Dos Reis wrote: > [EMAIL PROTECTED] writes: > > | think that it is too relevant for the discussion at hand. Moreover, > | Harper talks about a relative concept of "C-safety". > > Then, I believe you missed the entire point. I think the part of my reply you snipped addressed it well enough. Anyway, I can't believe that we actually need to argue about the fact that - for any *useful* and *practical* notion of safety - C is *not* a safe language. I refrain from continuing the discussion along this line, because *that* is *really* silly. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language [correction]
David Hopwood wrote: >> >>>(defun blackhole (argument) >>> (declare (ignore argument)) >>> #'blackhole) > I believe this example requires recursive types. It can also be expressed > in a gradual typing system, but possibly only using an unknown ('?') type. > > ISTR that O'Caml at one point (before version 1.06) supported general > recursive types, although I don't know whether it would have supported > this particular example. No problem at all. It still is possible today if you really want: ~/> ocaml -rectypes Objective Caml version 3.08.3 # let rec blackhole x = blackhole;; val blackhole : 'b -> 'a as 'a = The problem is, though, that almost everything can be typed once you have unrestricted recursive types (e.g. missing arguments etc), and consequently many actual errors remain unflagged (which clearly shows that typing is not only about potential value class mismatches). Moreover, there are very few practical uses of such a feature, and they can always be coded easily with recursive datatypes. It is a pragmatic decision born from experience that you simply do *not want* to have this, even though you easily could. E.g. for OCaml, unrestricted recursive typing was removed as default because of frequent user complaints. Which is why this actually is a very bad example to chose for dynamic typing advocacy... ;-) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
David Hopwood wrote: > > (In the case of eval, OTOH, > the erroneous code may cause visible side effects before any run-time > error occurs.) Not necessarily. You can replace the primitive eval by compile, which delivers a function encapsulating the program, so you can check the type of the function before actually running it. Eval itself can easily be expressed on top of this as a polymorphic function, which does not run the program if it does not have the desired type: eval ['a] s = typecase compile s of f : (()->'a) -> f () _ -> raise TypeError - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
David Hopwood wrote: > George Neuner wrote: >> >>All of this presupposes that you have a high level of confidence in >>the compiler. I've been in software development for going in 20 years >>now and worked 10 years on high performance, high availability >>systems. In all that time I have yet to meet a compiler ... or >>significant program of any kind ... that is without bugs, noticeable >>or not. > > [...] > > One of the main reasons for this, IMHO, is that many compilers place too > much emphasis on low-level optimizations of dubious merit. For C and > Java, I've taken to compiling all non-performance-critical code without > optimizations, and that has significantly reduced the number of compiler > bugs that I see. It has very little effect on overall execution performance > (and compile times are quicker). > > I don't think that over-complex type systems are the cause of more than a > small part of the compiler bug problem. In my estimation, the frequency of > bugs in different compilers *for the same language* can vary by an order of > magnitude. Also, the use of typed intermediate languages within the compiler might actually help drastically cutting down on the more severe problem of code transformation bugs, notwithstanding the relative complexity of suitable internal type systems. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > > Okay, sure. But for the problem you describe, both imperativeness > and the presence of pointers is each necessary but not sufficient; > it is the two together that causes the problem. So it strikes > me (again, a very minor point) as inaccurate to describe this as > a problem with imperative languages per se. > > [...] > > Right. To me the response to this clear: give up pointers. Imperative > operations are too useful to give up; indeed they are a requirement > for certain problems. Pointers on the other hand add nothing except > efficiency and a lot of confusion. They should be considered an > implementation technique only, hidden behind some pointerless > computational model. Don't get yourself distracted by the low-level notion of "pointer". The problem *really* is mutability and the associated notion of identity, which explicit pointers just exhibit on a very low level. When you have a language with mutable types (e.g. mutable arrays) then objects of these types have identity, which is observable through assignment. This is regardless of whether identity is an explicit concept (like it becomes with pointers and comparison of pointer values, i.e. addresses). Consequently, you cannot possibly get rid of aliasing issues without getting rid of (unrestricted) mutability. Mutability implies object identity implies aliasing problems. On the other hand, pointers are totally a futile concept without mutability: if everything is immutable, it is useless to distinguish between an object and a pointer to it. In other words, pointers are essentially just an *aspect* of mutability in lower-level languages. On a sufficiently high level of abstraction, it does not make much sense to differentiate between both concepts - pointers are just mutable objects holding other mutable objects (immutable pointer types exist, but are only interesting if you also have pointer arithmetics - which, however, is largely equivalent to arrays, i.e. not particularly relevant either). - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > > However if the mutable types are not first class, then there > is no way to have the aliasing. Thus, if we do not have pointers > or objects or identity but retain mutability, there is no aliasing > problem. Yes, technically you are right. But this makes a pretty weak notion of mutability. All stateful data structures had to stay within their lexical scope, and could never be passed to a function. For example, this essentially precludes object-oriented programming, because you could not have objects with state (the alternative, second class objects, would be even less "objective"). Generally, second-classness is an ad-hoc restriction that can work around all kinds of problems, but rarely with satisfactory results. So I would tend to say that this is not an overly interesting point in the design space. But YMMV. >>In other words, pointers are essentially just an *aspect* of mutability >>in lower-level languages. > > Again, I disagree: it is posible to have mutability without > pointers/identity/objects. OK, if you prefer: it is an aspect of first-class mutability - which is present in almost all imperative languages I know. :-) - Andreas -- Andreas Rossberg, [EMAIL PROTECTED] -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Darren New wrote: > Andreas Rossberg wrote: > >> Yes, technically you are right. But this makes a pretty weak notion of >> mutability. All stateful data structures had to stay within their >> lexical scope, and could never be passed to a function. > > Not really. The way Hermes handles this is with destructive assignment. > Each variable holds a value, and you (almost) cannot have multiple > variables referring to the same value. OK, this is interesting. I don't know Hermes, is this sort of like a dynamically checked equivalent of linear or uniqueness typing? > If you want to assign Y to X, you use >X := Y > after which Y is considered to be uninitialized. If you want X and Y to > have the same value, you use >X := copy of Y > after which X and Y have the same value but are otherwise unrelated, and > changes to one don't affect the other. Mh, but if I understand correctly, this seems to require performing a deep copy - which is well-known to be problematic, and particularly breaks all kinds of abstractions. Not to mention the issue with uninitialized variables that I would expect occuring all over the place. So unless I'm misunderstanding something, this feels like trading one evil for an even greater one. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > > After all, what are the alternatives? Purely-functional > languages remove themselves from a large class of > problems that I consider important: data management. Maybe, but I have yet to see how second-class variables are really more adequate in dealing with it. And note that even with second-class state you can still have aliasing issues - you just need mutable arrays and pass around indices. Keys in databases are a more general form of the same problem. > I have explored the OO path to its bitter end and am > convinced it is not the way. So what is left? Uniqueness > types and logic programming, I suppose. I enjoy logic > programming but it doesn't seem quite right. But notice: > no pointers there! And it doesn't seem to suffer from the > lack. Uh, aliasing all over the place! Actually, I think that logic programming, usually based on deep unification, brings by far the worst incarnation of aliasing issues to the table. - Andreas -- Andreas Rossberg, [EMAIL PROTECTED] -- http://mail.python.org/mailman/listinfo/python-list