Re: What is Expressiveness in a Computer Language
Darren New schrieb: > Andreas Rossberg wrote: > > AFAICT, ADT describes a type whose values can only be accessed by a > > certain fixed set of operations. > > No. AFAIU, an ADT defines the type based on the operations. The stack > holding the integers 1 and 2 is the value (push(2, push(1, empty(. > There's no "internal" representation. The values and operations are > defined by preconditions and postconditions. Are you sure that you aren't confusing *abstract* with *algebraic* data types? In my book, abstract types usually have an internal representation, and that can even be stateful. I don't remember having encountered definitions of ADT as restrictive as you describe it. > Both a stack and a queue could be written in most languages as "values > that can only be accessed by a fixed set of operations" having the same > possible internal representations and the same function signatures. > They're far from the same type, because they're not abstract. Different abstract types can have the same signature. That does not make them the same type. The types are distinguished by their identity. Likewise, two classes can have the same set of methods, without being the same class (at least in languages that have nominal typing, which includes almost all typed OOPLs). > I'm pretty sure in Pascal you could say > > Type Apple = Integer; Orange = Integer; > and then vars of type apple and orange were not interchangable. No, the following compiles perfectly fine (using GNU Pascal): program bla; type apple = integer; orange = integer; var a : apple; o : orange; begin a := o end. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz wrote: > > > A type is the encoding of these properties. A type > > varying over time is an inherent contradiction (or another abuse of the > > term "type"). > > No. It's just a matter of definition, essentially. > E.g. in Smalltalk and Lisp, it does make sense to talk of the "type" of > a name or a value, even if that type may change over time. OK, now we are simply back full circle to Chris Smith's original complaint that started this whole subthread, namely (roughly) that long-established terms like "type" or "typing" should *not* be stretched in ways like this, because that is technically inaccurate and prone to misinterpretation. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Anton van Straaten wrote: > > Languages with latent type systems typically don't include type > declarations in the source code of programs. The "static" type scheme > of a given program in such a language is thus latent, in the English > dictionary sense of the word, of something that is present but > undeveloped. Terms in the program may be considered as having static > types, and it is possible to infer those types, but it isn't necessarily > easy to do so automatically, and there are usually many possible static > type schemes that can be assigned to a given program. > > Programmers infer and reason about these latent types while they're > writing or reading programs. Latent types become manifest when a > programmer reasons about them, or documents them e.g. in comments. I very much agree with the observation that every programmer performs "latent typing" in his head (although Pascal Constanza's seems to have the opposite opinion). But I also think that "latently typed language" is not a meaningful characterisation. And for the very same reason! Since any programming activity involves latent typing - naturally, even in assembler! - it cannot be attributed to any language in particular, and is hence useless to distinguish between them. (Even untyped lambda calculus would not be a counter-example. If you really were to program in it, you certainly would think along lines like "this function takes two chuch numerals and produces a third one".) I hear you when you define latently typed languages as those that support the programmer's latently typed thinking by providing dynamic tag checks. But in the very same post (and others) you also explain in length why these tags are far from being actual types. This seems a bit contradictory to me. As Chris Smith points out, these dynamic checks are basically a necessaity for a well-defined operational semantics. You need them whenever you have different syntactic classes of values, but lack a type system to preclude interference. They are just an encoding for differentiating these syntactic classes. Their connection to types is rather coincidential. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > > But it differs from latently typed languages like python, perl or lisp. > In such a language there is no information about the type the variable > stores. The programmer cannot write code to test it, and so can't > write functions that issue errors if given arguments of the wrong type. > The programmer must use his or her memory to substitute for that > facility. As far as I can see this is a significant distinction and > warrants a further category for latently typed languages. Take one of these languages. You have a variable that is supposed to store functions from int to int. Can you test that a given function meets this requirement? You see, IMO the difference is marginal. From my point of view, the fact that you can do such tests *in some very trivial cases* in the languages you mention is an artefact, nothing fundamental. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe write: > > > > Take one of these languages. You have a variable that is supposed to > > store functions from int to int. Can you test that a given function > > meets this requirement? > > The answer is no for python and perl AFAIK. Also no for lisp _aux > naturelle_ (you can do it by modifying lisp though of-course, I believe > you can make it entirely statically typed if you want). > > But the analogous criticism could be made of statically typed > languages. > Can I make a type in C that can only have values between 1 and 10? > How about a variable that can only hold odd numbers, or, to make it > more difficult, say fibonacci numbers? Fair point. However, there are in fact static type systems powerful enough to express all of this and more (whether they are convenient enough in practice is a different matter). On the other hand, AFAICS, it is principally impossible to express the above property on functions with tags or any other purely dynamic mechanism. > The cases can be far from trivial. In lisp a type specifier can mean > something like "argument must be a 10x10 matrix with top corner element > larger than 35" You can also, for example, easily make predicates that > tell if a value is odd, or a fibonacci number. Now, these are yet another beast. They are not tags, they are user-defined predicates. I would not call them types either, but that's an equally pointless battle. :-) - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > > > > This means that there's a sense in which the language that the > > programmer programs in is not the same language that has a formal > > semantic definition. As I mentioned in another post, programmers are > > essentially mentally programming in a richer language - a language which > > has informal (static) types - but the code they write down elides this > > type information, or else puts it in comments. > > > > [...] > > > > In this context, the term "latently-typed language" refers to the > > language that a programmer experiences, not to the subset of that > > language which is all that we're typically able to formally define. That language is not a subset, if at all, it's the other way round, but I'd say they are rather incomparable. That is, they are different languages. > That is starting to get a bit too mystical for my tastes. I have to agree. \sarcasm One step further, and somebody starts calling C a "latently memory-safe language", because a real programmer "knows" that his code is in a safe subset... And where he is wrong, dynamic memory page protection checks will guide him. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz write: > > Another observation: type safeness is more of a spectrum than a clearcut > distinction. Even ML and Pascal have ways to circumvent the type system, No. I'm not sure about Pascal, but (Standard) ML surely has none. Same with Haskell as defined by its spec. OCaml has a couple of clearly marked unsafe library functions, but no unsafe feature in the language semantics itself. > and even C is typesafe unless you use unsafe constructs. Tautology. Every language is "safe unless you use unsafe constructs". (Unfortunately, you can hardly write interesting programs in any safe subset of C.) > IOW from a type-theoretic point of view, there is no real difference > between their typesafe and not typesafe languages in the "statically > typed" column; the difference is in the amount of unsafe construct usage > in practial programs. Huh? There is a huge, fundamental difference: namely whether a type system is sound or not. A soundness proof is obligatory for any serious type theory, and failure to establish it simply is a bug in the theory. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Gabriel Dos Reis wrote: > | > | (Unfortunately, you can hardly write interesting programs in any safe > | subset of C.) > > Fortunately, some people do, as living job. I don't think so. Maybe the question is what a "safe subset" consists of. In my book, it excludes all features that are potentially unsafe. So in particular, C-style pointers are out, because they can easily dangle, be uninitialisied, whatever. Can you write a realistic C program without using pointers? - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Gabriel Dos Reis wrote: > [EMAIL PROTECTED] writes: > > | Gabriel Dos Reis wrote: > | > | > | > | (Unfortunately, you can hardly write interesting programs in any safe > | > | subset of C.) > | > > | > Fortunately, some people do, as living job. > | > | I don't think so. Maybe the question is what a "safe subset" consists > | of. In my book, it excludes all features that are potentially unsafe. > > if you equate "unsafe" with "potentially unsafe", then you have > changed gear and redefined things on the fly, and things that could > be given sense before ceases to have meaning. I decline following > such an uncertain, extreme, path. An unsafe *feature* is one that can potentially exhibit unsafe behaviour. How else would you define it, if I may ask? A safe *program* may or may not use unsafe features, but that is not the point when we talk about safe *language subsets*. > I would suggest you give more thoughts to the claims made in > > http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html Thanks, I am aware of it. Taking into account the hypothetical nature of the argument, and all the caveats listed with respect to C, I do not think that it is too relevant for the discussion at hand. Moreover, Harper talks about a relative concept of "C-safety". I assume that everybody here understands that by "safe" in this discussion we mean something else (in particular, memory safety). Or are you trying to suggest that we should indeed consider C safe for the purpose of this discussion? - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Scott David Daniels wrote: > [EMAIL PROTECTED] wrote: > > Huh? There is a huge, fundamental difference: namely whether a type > > system is sound or not. A soundness proof is obligatory for any serious > > type theory, and failure to establish it simply is a bug in the theory. > > So you claim Java and Objective C are "simply bugs in the theory." You're misquoting me. What I said is that lack of soundness of a particular type theory (i.e. a language plus type system) is a bug in that theory. But anyway, Java in fact is frequently characterised as having a bogus type system (e.g. with respect to array subtyping). Of course, in a hybrid language like Java with its dynamic checks it can be argued either way. Naturally, the type system of Objective-C is as broken as the one of plain C. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz wrote: > > > but (Standard) ML surely has none. > > NLFFI? > > > Same with Haskell as defined by its spec. > > Um... I'm not 100% sure, but I dimly (mis?)remember having read that > UnsafePerformIO also offered some ways to circumvent the type system. Neither NLFFI nor unsafePerformIO are official part of the respective languages. Besides, foreign function interfaces are outside a language by definition, and can hardly be taken as an argument - don't blame language A that unsafety arises when you subvert it by interfacing with unsafe language B on a lower level. > >> and even C is typesafe unless you use unsafe constructs. > > > > Tautology. Every language is "safe unless you use unsafe constructs". > > No tautology - the unsafe constructs aren't just typewise unsafe ;-p > > That's exactly why I replaced Luca Cardelli's "safe/unsafe" > "typesafe/not typesafe". There was no definition to the original terms > attached, and this discussion is about typing anyway. The Cardelli paper I was referring to discusses it in detail. And if you look up the context of my posting: it was exactly whether safety is to be equated with type safety. > >> IOW from a type-theoretic point of view, there is no real difference > >> between their typesafe and not typesafe languages in the "statically > >> typed" column; the difference is in the amount of unsafe construct usage > >> in practial programs. > > > > Huh? There is a huge, fundamental difference: namely whether a type > > system is sound or not. > > I think you're overstating the case. > > In type theory, of course, there's no such things as an "almost typesafe > language" - it's typesafe or it isn't. Right, and you were claiming to argue from a type-theoretic POV. [snipped the rest] - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language [correction]
Joe Marshall wrote: > Andreas Rossberg wrote: > > > > Which is why this actually is a very bad example to chose for dynamic > > typing advocacy... ;-) > > Actually, this seems a *good* example. The problem seems to be that > you end up throwing the baby out with the bathwater: your static type > system stops catching the errors you want once you make it powerful > enough to express certain programs. That is not the case: you can still express these programs, you just need to do an indirection through a datatype. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > Andreas Rossberg wrote: > > > > 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. > > So for array a, you would claim that "a[5]" is an alias for > (a part of) "a"? That seems to stretch the idea of aliasing > to me. Not at all, I'd say. In my book, aliasing occurs whenever you have two different "lvalues" that denote the same mutable cell. I think it would be rather artificial to restrict the definition to lvalues that happen to be variables or dereferenced pointers. So of course, a[i] aliases a[j] when i=j, which in fact is a well-known problem in some array or matrix routines (e.g. copying array slices must always consider overlapping slices as special cases). > > 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. > > Hmmm. Can you elaborate just a bit? Logic variables immediately become aliases when you unify them. Afterwards, after you bind one, you also bind the other - or fail, because both got already bound the other way round. Unfortunately, unification also is a deep operation, that is, aliasing can be induced into variables deeply nested into some terms that happen to get unified, possibly without you being aware of any of this (the unification, nor the variable containment). To avoid accidental aliasing you essentially must keep track of all potential unifications performed by any given predicate (including transitively, by its subgoals), which totally runs square to all concerns of modularity and abstraction. I've never been much of a logic programmer myself, but our language group has a dedicated LP and CP background, and people here have developed very strong opinions about the adequateness of unrestricted logic variables and particularly unification in practice. I remember somebody calling Prolog "the worst imperative language ever invented". - Andreas -- http://mail.python.org/mailman/listinfo/python-list
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
