Re: What is a type error?
Marshall wrote: > So, what exactly separates a precondition from a postcondition > from an invariant? A precondition applies to a routine/method/function and states the conditions under which a function might be called. For example, a precondition on "stack.pop" might be "not stack.empty", and "socket.read" might have a precondition of "socket.is_open", and "socket.open_a_new_connection" might have a precondition of "socket.is_closed". A postcondition applies to a routine/method/function and states (at least part of) what that routine guarantees to be true when it returns, assuming it is called with true preconditions. So "not stack.empty" would be a postcondition of "stack.push". If your postconditions are complete, they tell you what the routine does. An invariant is something that applies to an entire object instance, any time after the constructor has completed and no routine within that instance is running (i.e., you're not in the middle of a call). There should probably be something in there about destructors, too. So an invariant might be "stack.is_empty == (stack.size == 0)" or perhaps "socket.is_open implies (socket.buffer != null)" or some such. The first problem with many of these sorts of things are that in practice, there are lots of postconditions that are difficult to express in any machine-readable way. The postcondition of "socket.read" is that the buffer passed as the first argument has valid data in the first "n" bytes, where "n" is the return value from "socket.read", unless "socket.read" returned -1. What does "valid" mean there? It has to match the bytes sent by some other process, possibly on another machine, disregarding the bytes already read. You can see how this can be hard to formalize in any particularly useful way, unless you wind up modelling the whole universe, which is what most of the really formalized network description techniques do. Plus, of course, without having preconditions and postconditions for OS calls, it's difficult to do much formally with that sort of thing. You can imagine all sorts of I/O that would be difficult to describe, even for things that are all in memory: what would be the postcondition for "screen.draw_polygon"? Any set of postconditions on that routine that don't mention that a polygon is now visible on the screen would be difficult to take seriously. There are also problems with the complexity of things. Imagine a chess-playing game trying to describe the "generate moves" routine. Precondition: An input board with a valid configuration of chess pieces. Postcondition: An array of boards with possible next moves for the selected team. Heck, if you could write those as assertions, you wouldn't need the code. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Joachim Durchholz wrote: > Actually, in a functional programming language (FPL), you write just the > postconditions and let the compiler generate the code for you. Certainly. And my point is that the postcondition describing "all valid chess boards reachable from this one" is pretty much going to be as big as an implementation for generating it, yes? The postcondition will still have to contain all the rules of chess in it, for example. At best you've replaced loops with some sort of universal quanitifier with a "such that" phrase. Anyway, I expect you could prove you can't do this in the general case. Otherwise, you could just write a postcondition that asserts the output of your function is machine code that when run generates the same outputs as the input string would. I.e., you'd have a compiler that can write other compilers, generated automatically from a description of the semantics of the input stream and the semantics of the machine the code is to run on. I'm pretty sure we're not there yet, and I'm pretty sure you start running into the limits of computability if you do that. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
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. 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. (As almost an aside, the non-scalar data structures were very similar to SQL data tables.) If you declare (the equivalent to) a function, you can indicate whether the paramters matching the arguments are passed destructively, or are read-only, or are copy-in-copy-out. So you could declare a function, for example, that you pass a table into, and if it's marked as a read-only parameter, the compiler ensures the callee does not modify the table and the compiler generates code to pass a pointer. One could also mark a variable (for example) as uninitialized on entry, intialized on return, and uninitalized on the throw of an exception, and this could be used (for example) for the read-a-line-from-a-socket routine. The only value that came close to being shared is an outgoing connection to a procedure; the equivalent of the client side of a socket. For these, you could make copies, and each copy would point to the same receiver. The receiving process could change over time, by passing its end of the socket in a message to some other process (live code upgrading, for example). Since everything could be passed as part of a message, including code, procedures, tables, and "inports" and "outports" (the ends of sockets), I don't see that it had any problems with first classness. > OK, if you prefer: it is an aspect of first-class mutability - which is > present in almost all imperative languages I know. :-) I disagree. It's entirely possible to make sophisticated imperitive languages with assignment and without aliasing. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > Unless I'm missing your point, I disagree with your disagreement. > Mutability only makes sense because of object identity (in the generic > sense; no OO going on here). Depends what you mean by "object". int x = 6; int y = 5; x = y; I'd say x was mutable, with no "identity" problems involved? Why is it problematic that variables have identity and are mutable? Certainly I can later "find" whatever value I put into x. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Andreas Rossberg wrote: > OK, this is interesting. I don't know Hermes, is this sort of like a > dynamically checked equivalent of linear or uniqueness typing? I'm not sure what linear or uniqueness typing is. It's typestate, and if I remember correctly the papers I read 10 years ago, the folks at TJWatson that invented Hermes also invented the concept of typestate. They at least claim to have coined the term. It's essentially a dataflow analysis that allows you to do the same sorts of things that "don't read variables that may not yet have been assigned to", except that you could annotate that variables change to the state of "uninitialized" after they've already been initialized. > 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. Um, no, because there are no aliases. There's only one name for any given value, so there's no "deep copy" problems. A deep copy and a shallow copy are the same thing. And there are types of values you can assign but not copy, such as callmessages (which are problematic to copy for the same reason a stack frame would be problematic to copy). I believe, internally, that there were cases where the copy was "deep" and cases where it was "shallow", depending on the surrounding code. Making a copy of a table and passing it to another process had to be a "deep" copy (given that a column could contain another table, for example). Making a copy of a table and using it for read-only purposes in the same process would likely make a shallow copy of the table. Iterating over a table and making changes during the iteration made a copy-on-write subtable, then merged it back into the original table when it was done the loop, since the high-level semantic definition of looping over a table is that you iterate over a copy of the table. The only thing close to aliases are references to some other process's input ports (i.e., multiple client-side sockets connected to a server-side socket). If you want to share data (such as a file system or program library), you put the data in a table in a process, and you hand out client-side connections to the process. Mostly, you'd define such connections as accepting a data value (for the file contents) with the parameter being undefined upon return from the call, and the file name as being read-only, for example. If you wanted to store the file, you could just pass a pointer to its data (in the implementation). If you wanted a copy of it, you would either copy it and pass the pointer, or you'd pass the pointer with a flag indicating it's copy-on-write, or you could pass the pointer and have the caller copy it at some point before returning, depending on what the caller did with it. The semantics were high-level with the intent to allow the compiler lots of leeway in implementation, not unlike SQL. > Not to mention the issue with > uninitialized variables that I would expect occuring all over the place. The typestate tracks this, and prevents you from using uninitialized variables. If you do a read (say, from a socket) and it throws an "end of data" exception, the compiler prevents you from using the buffer you just tried but failed to read. Indeed, that's the very point of it all. By doing this, you can run "untrusted" code in the same address space as trusted code, and be assured that the compiler will prevent the untrusted code from messing up the trusted code. The predecessor of Hermes (NIL) was designed to let IBM's customers write efficient networking code and emulations and such that ran in IBM's routers, without the need for expensive (in performance or money) hardware yet with the safety that they couldn't screw up IBM's code and hence cause customer service problems. > So unless I'm misunderstanding something, this feels like trading one > evil for an even greater one. In truth, it was pretty annoying. But more because you wound up having to write extensive declarations and compile the declarations before compiling the code that implements them and such. That you didn't get to use uninitialized variables was a relatively minor thing, especially given that many languages nowadays complain about uninitialized variables, dead code, etc. But for lots of types of programs, it let you do all kinds of things with a good assurance that they'd work safely and efficiently. It was really a language for writing operating systems in, when you get right down to it. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > Darren New <[EMAIL PROTECTED]> wrote: > >>I'm not sure what linear or uniqueness typing is. It's typestate, and if >>I remember correctly the papers I read 10 years ago, the folks at >>TJWatson that invented Hermes also invented the concept of typestate. >>They at least claim to have coined the term. > > Coining the term is one thing, but I feel pretty confident that the idea > was not invented in 1986 with the Hermes language, but rather far > earlier. Yes. However, the guys who invented Hermes didn't come up with it out of the blue. It was around (in NIL - Network Implementation Language) for years beforehand. I read papers about these things in graduate school, but I don't know where my photocopies are. NIL was apparently quite successful, but a niche language, designed by IBM for programming IBM routers. Hermes was an attempt years later to take the same successful formula and turn it into a general-purpose programming system, which failed (I believe) for the same reason that a general purpose operating system that can't run C programs will fail. > Perhaps they may have invented the concept of considering it > any different from other applications of types, though. From what I can determine, the authors seem to imply that typestate is dataflow analysis modified in (at least) two ways: 1) When control flow joins, the new typestate is the intersection of typestates coming into the join, where as dataflow analysis doesn't guarantee that. (They imply they think dataflow analysis is allowed to say "the variable might or might not be initialized here", while typestate would ensure the variable is uninitialized.) 2) The user has control over the typestate, so the user can (for exmaple) assert a variable is uninitialized at some point, and by doing so, make it so. How this differs from theoretical lambda types and all I couldn't say. > What is being named here is the overcoming of a limitation that > programming language designers imposed upon themselves, whether from not > understanding the theoretical research or not believing it important, I > don't know. I believe there's also a certain level of common-senseness needed to make a language even marginally popular. :-) While it's possible that there's really no difference between type and typestate at the theoretical level, I think most practical programmers would have trouble wrapping their head around that, just as programming in an entirely recursive pattern when one is used to looping can be disorienting. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Joachim Durchholz wrote: > of no assertion language that can express such temporal relationships, > and even if there is (I'm pretty sure there is), I'm rather sceptical > that programmers would be able to write correct assertions, or correctly > interpret them - temporal logic offers several traps for the unwary. FWIW, this is exactly the area to which LOTOS (Language Of Temporal Orderering Specifications) is targetted at. It's essentially based on CSP, but somewhat extended. It's pretty straightforward to learn and understand, too. Some have even added "realtime" constraints to it. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > I would propose that variables have identity, and values do not. > In part this is via the supplied definition of identity, in which, when > you change one thing, if something else changes as well, they > share identity. Maybe you gave a better definition the first time, but this one doesn't really hold up. > of equality here is too narrow; it is only necessary to show that > two things both change, not that they change in the same way.) If I change X, then Y[X] changes also. I don't think X is identical to Y or Y[X], nor is it an alias of either. I think that's where the equality comes into it. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error? [correction]
David Hopwood wrote:
>
> public class LoopInitTest {
> public static String getString() { return "foo"; }
>
> public static void main(String[] args) {
> String line = getString();
> boolean is_last = false;
>
> while (!is_last) {
> if (line.charAt(0) == 'q') {
> is_last = true;
> }
>
> // insert line into inputs (not important for analysis)
>
> if (!is_last) {
> line = getString();
> }
> }
> }
> }
>
> which compiles without error, because is_last is definitely initialized.
At what point do you think is_last or line would seem to not be
initialized? They're both set at the start of the function, and (given
that it's Java) nothing can unset them.
At the start of the while loop, it's initialized. At the end of the
while loop, it's initialized. So the merge point of the while loop has
it marked as initialized.
Now, if the "insert line into inputs" actually unset "line", then yes,
you're right, Hermes would complain about this.
Alternately, if you say
if (x) v = 1;
if (x) v += 1;
then Hermes would complain when it wouldn't need to. However, that's
more a limitation of the typestate checking algorithms than the concept
itself; that is to say, clearly the typestate checker could be made
sufficiently intelligent to track most simple versions of this problem
and not complain, by carrying around conditionals in the typestate
description.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error? [correction]
Darren New wrote: > Now, if the "insert line into inputs" actually unset "line", then yes, > you're right, Hermes would complain about this. Oh, I see. You translated from Hermes into Java, and Java doesn't have the "insert into" statement. Indeed, the line you commented out is *exactly* what's important for analysis, as it unsets line. Had it been insert copy of line into inputs then you would not have gotten any complaint from Hermes, as it would not have unset line there. In this case, it's equivalent to if (!is_line) line = getString(); if (!is_line) use line for something... except the second test is at the top of the loop instead of the bottom. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error? [correction]
David Hopwood wrote:
> Darren New wrote:
>
>>David Hopwood wrote:
>>
>>
>>>public class LoopInitTest {
>>>public static String getString() { return "foo"; }
>>>
>>>public static void main(String[] args) {
>>>String line = getString();
>>>boolean is_last = false;
>>>
>>>while (!is_last) {
>>>if (line.charAt(0) == 'q') {
>>>is_last = true;
>>>}
>>>
>>>// insert line into inputs (not important for analysis)
>>>
>>>if (!is_last) {
>>>line = getString();
>>>}
>>>}
>>>}
>>>}
>>>
>>>which compiles without error, because is_last is definitely initialized.
>>
>>At what point do you think is_last or line would seem to not be
>>initialized? They're both set at the start of the function, and (given
>>that it's Java) nothing can unset them.
>>
>>At the start of the while loop, it's initialized. At the end of the
>>while loop, it's initialized. So the merge point of the while loop has
>>it marked as initialized.
>
>
> Apparently, Hermes (at least the version of it described in that paper)
> essentially forgets that is_last has been initialized at the top of the
> loop, and so when it does the merge, it is merging 'not necessarily
> initialized'
> with 'initialized'.
No, it's not that it "forgets". It's that the "insert line into inputs"
unitializes "line". Hence, "line" is only conditionally set at the
bottom of the loop, so it's only conditionally set at the top of the loop.
> This sounds like a pretty easy thing to fix to me (and maybe it was fixed
> later, since there are other papers on Hermes' typestate checking that I
> haven't read yet).
You simply misunderstand the "insert line into inputs" semantics. Had
that line actually been commented out in the Hermes code, the loop would
have compiled without a problem.
That said, in my experience, finding this sort of typestate error
invariably led me to writing clearer code.
boolean found_ending = false;
while (!found_ending) {
string line = getString();
if (line.charAt(0) == 'q')
found_ending = true;
else
insert line into inputs;
}
It seems that's much clearer to me than the contorted version presented
as the example. If you want it to work like the Java code, where you can
still access the "line" variable after the loop, the rearrangement is
trivial and transparent as well.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz wrote: > Give a heterogenous list that would to too awkward to live in a > statically-typed language. Write a function that takes an arbitrary set of arguments and stores them into a structure allocated on the heap. > Give a case of calling nonexistent functions that's useful. See the Tcl "unknown" proc, used for interactive command expansion, dynamic loading of code on demand, etc. -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz wrote: > Give a heterogenous list that would to too awkward to live in a > statically-typed language. Printf()? -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Matthias Blume wrote: > Very good statically typed versions of printf exist. See, e.g., > Danvy's unparsing combinators. That seems to ignore the fact that the pattern is a string, which means that printf's first argument in Danvy's mechanism has to be a literal. You can't read the printf format from a configuration file (for example) to support separate languages. It doesn't look like the version of printf that can print its arguments in an order different from the order provided in the argument list is supported either; something like "%3$d" or some such. Second, what's the type of the argument that printf, sprintf, fprintf, kprintf, etc all pass to the subroutine that actually does the formatting? (Called vprintf, I think?) -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Matthias Blume wrote: > In Danvy's solution, the format argument is not a string. That's what I said, yes. >>You can't read the printf format from a configuration file >>(for example) to support separate languages. > You don't need to do that if you want to support separate languages. That's kind of irrelevant to the discussion. We're talking about collections of dynamically-typed objects, not the best mechanisms for supporting I18N. > Moreover, reading the format string from external input is a good way > of opening your program to security attacks, since ill-formed data on > external media are then able to crash you program. Still irrelevant to the point. > I am sure one could adapt Danvy's solution to support such a thing. I'm not. It's consuming arguments as it goes, from what I understood of the paper. It's translating, essentially, into a series of function calls in argument order. > Obviously, a Danvy-style solution (see, e.g., the one in SML/NJ's > library) is not necessarily structured that way. I don't see the > problem with typing, though. You asked for an example of a heterogenous list that would be awkward in a statically strongly-typed language. The arguments to printf() count, methinks. What would the second argument to apply be if the first argument is printf (since I'm reading this in the LISP group)? -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote:
> Yes, but the point is, as the other poster mentioned: values defined by
> a class.
A value can only represent one value, right? Or can a value have
multiple values?
> For example, in lisp:
> "xyz" is a string,
"xyz" cannot represent values from the class of strings. It can only
represent one value.
I think that's what the others are getting at.
>>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, the values themselves do not.
Sure they do. 23.5e3 is a "real" in Pascal, and there's no variable there.
("hello" % "there") is illegal in most languages, because the modulo
operator doesn't apply to strings. How could this be determined at
compile time if "hello" and "there" don't have types?
--
Darren New / San Diego, CA, USA (PST)
My Bath Fu is strong, as I have
studied under the Showerin' Monks.
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > The compiler > relys entirely on the types of the variables to know how to correctly > operate on the values. The values themselves have no type information > associated with them. int x = (int) (20.5 / 3); What machine code operations does the "/" there invoke? Integer division, or floating point division? How did the variables involved in the expression affect that? >>Casting in C takes values of one type to values of another type. > No it doesn't. Casting reinterprets a value of one type as a value of > another type. No it doesn't. int x = (int) 20.5; There's no point at which bits from the floating point representation appear in the variable x. int * x = (int *) 0; There's nothing that indicates all the bits of "x" are zero, and indeed in some hardware configurations they aren't. -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote:
> Darren New wrote:
>>Rob Thorpe wrote:
>>>The values themselves have no type information associated with them.
>>int x = (int) (20.5 / 3);
> In that case it knew because it could see at compile time.
Well, yes. That's the point of static typing.
> In general though it doesn't.
Sure it does. There are all kinds of formal rules about type promotions
and operator version selection.
In deed, in *general* every value has a type associated with it (at
compile time). Some values have a type associated with them due to the
declaration of the variable supplying the value, but that's far from the
general case.
Note that in
main() { char x = 'x'; foo(x); }
the value passed to "foo" is not even the same type as the declaration
of "x", so it's far from the general case that variables even determine
the values they provide to the next part of the calculation.
> If I divide x / y it only knows which to use because of types declared
> for x and y.
Yes? So? All you're saying is that the value of the expression "x" is
based on the declared type for the variable "x" in scope at that point.
That doesn't mean values don't have types. It just means that *some*
values' types are determined by the type of the variable the value is
stored in. As soon as you do anything *else* with that value, such as
passing it to an operator, a function, or a cast, the value potentially
takes on a type different from that of the variable from which it came.
> I suppose some are conversions and some reinterpretations. What I
> should have said it that there are cases where cast reinterprets.
There are cases where the cast is defined to return a value that has the
same bit pattern as its argument, to the extent the hardware can support
it. However, this is obviously limited to the values for which C
actually defines the bit patterns of its values, namely the scalar
integers.
Again, you're taking a special case and treating all the rest (which are
a majority) as aberations. For the most part, casts do *not* return the
same bit pattern as the value. For the most part
union {T1 x; T2 y;};
can be used to do transformations that
T2 y; T1 x = (T1) y;
does not. Indeed, the only bit patterns that don't change are when
casting from signed to unsigned versions of the same underlying scalar
type and back. Everything else must change, except perhaps pointers,
depending on your architecture. (I've worked on machines where char* had
more bits than long*, for example.)
(Funny that comp.lang.c isn't on this thread. ;-)
--
Darren New / San Diego, CA, USA (PST)
My Bath Fu is strong, as I have
studied under the Showerin' Monks.
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris Uppal wrote: > Personally, I would be quite happy to go there -- I dislike the idea that a > value has a specific inherent type. Interestingly, Ada defines a type as a collection of values. It works quite well, when one consistantly applies the definition. For example, it makes very clear the difference between a value of (type T) and a value of (type T or one of its subtypes). -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris Uppal wrote: > doesn't fit with my intuitions very well -- most noticeably in that the sets > are generally unbounded Errr, not in Ada. Indeed, not in any machine I know of with a limited address space. Andreas Rossberg wrote: > Indeed, this view is much too narrow. In particular, it cannot explain > abstract types, which is *the* central aspect of decent type systems. Well, it's Ada's view. I didn't say it was right for theoretical languages or anything like that. As far as I know, LOTOS is the only language that *actually* uses abstract data types - you have to use the equivalent of #include to bring in the integers, for example. Everything else uses informal rules to say how types work. But Ada's definition gives you a very nice way of talking about things like whether integers that overflow are the same type as integers that don't overflow, or whether an assignment of an integer to a positive is legal, or adding a CountOfApples to a CountOfOranges is legal, or whether passing a "Dog" object to an "Animal" function parameter makes sense in a particular context. 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." -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Matthias Blume wrote: > There are *tons* of languages that "actually" facilitate abstract data > types, and some of these languages are actually used by real people. I don't know of any others in actual use. Could you name a couple? Note that I don't consider things like usual OO languages (Eiffel, Smalltalk, etc) to have "abstract data types". -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Andreas Rossberg 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. > 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. > 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. :-) -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
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. 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. The part you can't see from outside the implementation is exactly the part that defines how it works. Granted, it's a common mistake to write that some piece of C++ code implements a stack ADT. For example, an actual ADT for a stack (and a set) is shown on http://www.cs.unc.edu/~stotts/danish/web/userman/umadt.html Note that the "axia" for the stack type completely define its operation and semantics. There is no other "implementation" involved. And in LOTOS (which uses ACT.1 or ACT.ONE (I forget which)) as its type, this is actually how you'd write the code for a stack, and then the compiler would crunch a while to figure out a corresponding implementation. I suspect "ADT" is by now so corrupted that it's useful to use a different term, such as "algebraic type" or some such. > Classes qualify for that, as long as they provide proper encapsulation. Nope. > OK, I admit that I exaggerated slightly. Although currently I'm indeed > able to mostly work with the more pleasant among languages. :-) Yah. :-) > (Btw, Pascal did not have it either, AFAIK) 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. -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
[EMAIL PROTECTED] wrote: > Are you sure that you aren't confusing *abstract* with *algebraic* data > types? I've never heard of algebraic data types. It's always been "abstract data types". Perhaps I stopped studying it, and the terminology changed when many people started to consider encapsulation as abstraction. I have any number of old textbooks and journals that refer to these as "abstract data types", including texts that show an abstract data type and then explain how to program it as an encapsulated object class. > No, the following compiles perfectly fine (using GNU Pascal): That'll teach me to rely on 15-year-old memories. :-) Maybe I'm remembering the wishful thinking from when I used Pascal. -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
John W. Kennedy wrote: > 360-family assembler, yes. 8086-family assembler, not so much. And Burroughs B-series, not at all. There was one "ADD" instruction, and it looked at the data in the addresses to determine whether to add ints or floats. :-) -- Darren New / San Diego, CA, USA (PST) My Bath Fu is strong, as I have studied under the Showerin' Monks. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Eliot Miranda wrote: > can only actually carry-out operations on objects that implement them. Execpt that every operation is implemented by every object in Smalltalk. Unless you specify otherwise, the implementation of every method is to call the receiver with doesNotUnderstand. (I don't recall whether the class of nil has a special rule for this or whether it implements doesNotUnderstand and invokes the appropriate "don't send messages to nil" method.) There are a number of Smalltalk extensions, such as multiple-inheritance, that rely on implementing doesNotUnderstand. -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > I can't see how you'd call + on a and b if you think they might > not be numbers. Now substitute "<" for "+" and see if you can make the same argument. :-) -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Eliot Miranda wrote: > classes do _not_ have to inherit from Object, I was unaware of this subtlety. Thanks! -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > point. My point was, I don't see why you'd be writing code using > operators that you thought might not be applicable to the operands. I see. I thought your point was that you might write code for which you didn't know the type of arguments. Unless you equate "type" with what smalltalk calls "protocol" (i.e., the type is the collection of operators applicable to values in the type), these are two different statements. -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Dr.Ruud wrote: > You can write self-modifying code in C, No, by violating the standards and invoking undefined behavior, you can write self-modifying code. I wouldn't say you're still "in C" any more, tho. -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > Also: has subtyping polymorphism or not, has parametric polymorphism or > not. And covariant or contravariant. -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: languages with full unicode support
Xah Lee wrote: > If you know a lang that does full unicode support, please let me know. Tcl. You may have to modify the "source" command to get it to default to something other than the system encoding, but this is trivial in Tcl. -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Gabriel Dos Reis wrote: > I would suggest you give more thoughts to the claims made in > http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html I'm not sure I understand this. Looking at "Example 2", where C is claimed to be "C-safe", he makes two points that I disagree with. First, he says Unix misimplements the operations semantics of C. It seems more like Unix simply changes the transition system such that programs which access unmapped memory are terminal. Second, he says that he hasn't seen a formal definition of C which provides precide operational semantics. However, the language standard itself specified numerous "undefined" results from operations such as accessing unallocated memory, or even pointing pointers to unallocated memory. So unless he wants to modify the C standard to indicate what should happen in such situations, I'm not sure why he thinks it's "safe" by his definition. There is no one "q" that a "p" goes to based on the language. He's confusing language with particular implementations. He seems to be saying "C is safe, oh, except for all the parts of the language that are undefined and therefore unsafe. But if you just clearly defined every part of C, it would be safe." It would also seem to be the case that one could not say that a program "p" is either terminal or not, as that would rely on input, right? gets() is "safe" as long as you don't read more than the buffer you allocated. What's the difference between "safe" and "well-defined semantics"? (Ignoring for the moment things like two threads modifying the same memory at the same time and other such hard-to-define situations?) -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz wrote: > That's actually not a design choice It's certainly a choice you can get wrong, as you say. ;-) I mean, if "without runtime safety" is a choice, I expect picking the wrong choice here can be. :-) -- Darren New / San Diego, CA, USA (PST) Native Americans used every part of the buffalo, including the wings. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote:
> // Inside this block, a has type int{17..21} and b has type
> // int{18..22}
No what happens if right here you code
b := 16;
Does that again change the type of "b"? Or is that an illegal
instruction, because "b" has the "local type" of (18..22)?
> signContract(a); // error, because a might be 17
> signContract(b); // no error, because even though the declared
> // type of b is int{14..22}, it has a local
> // type of int{18..22}.
If the former (i.e., if reassigning to "b" changes the "static type" of
b, then the term you're looking for is not type, but "typestate".
In other words, this is the same sort of test that disallows using an
unassigned variable in a value-returning expression. When
{ int a; int b; b := a; }
returns a compile-time error because "a" is uninitialized at the
assignment, that's not the "type" of a, but the typestate. Just FYI.
> Incidentally, I'm not saying that such a feature would be a good idea.
It actually works quite well if the language takes advantage of it
consistantly and allows you to designate your expected typestates and such.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > If you wish to say "typestate" to mean this, be my guest. It is also > correct to say "type". Sure. I just wasn't sure everyone here was aware of the term, is all. It makes it easier to google if you have a more specific term. > I'm not aware of a widely used language that implements stuff like this. I've only used Hermes with extensive support for this sort of thing. Hermes is process-oriented, rather than object-oriented, so it's a little easier to deal with the "encapsulation" part of the equation there. Sadly, Hermes went the way of the dodo. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > Now, I'm not fully up to speed on DBC. The contract specifications, > these are specified statically, but checked dynamically, is that > right? Yes, but there's a bunch more to it than that. The handling of exceptions, an in particular exceptions caused by failed pre/post conditions, is an integral part of the process. Plus, of course, pre/post condition checking is turned off while checking pre/post conditions. This does make sense if you think about it long enough, but it took me several months before I realized why it's necessary theoretically rather than just practically. > Wouldn't it be possible to do them at compile time? For some particularly simple ones, yes. For others, like "the chess pieces are in a position it is legal to get to from a standard opening set-up", it would be difficult. Anything to do with I/O is going to be almost impossible to write a checkable postcondition for, even at runtime. "After this call, the reader at the other end of the socket will receive the bytes in argument 2 without change." As far as I understand it, Eiffel compilers don't even make use of postconditions to optimize code or eliminate run-time checks (like null pointer testing). -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marcin 'Qrczak' Kowalczyk wrote: > The assignment might be performed in a function called there, so it's > not visible locally. In Hermes, which actually does this sort of constraint propagation, you don't have the ability[1] to munge some other routine's[2] local variables, so that becomes a non-issue. You wind up with some strange constructs, tho, like an assignment statement that copies and a different assignment statement that puts the rvalue into the variable on the left while simultaneously destroying whatever variable held the rvalue. [1] You do. Just not in a way visible to the programmer. The compiler manages to optimize out most places that different names consistantly refer to the same value. [2] There aren't subroutines. Just processes, with their own address space, to which you send and receive messages. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > Specialized > language already exist that reliably (as in, all the time) move array > bounds checking to compile time; It sounds like this means the programmer has to code up what it means to index off an array, yes? Otherwise, I can't imagine how it would work. x := read_integer_from_stdin(); write_to_stdout(myarray[x]); What does the programmer have to do to implement this semantic in the sort of language you're talking about? Surely something somewhere along the line has to "fail" (for some meaning of failure) at run-time, yes? -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. -- http://mail.python.org/mailman/listinfo/python-list
