Re: What is a type error? [correction]
Darren New wrote:
> David Hopwood wrote:
>
[...]
>> 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.
Yes, you're right, I did misunderstand this.
> 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.
I agree.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error? [correction]
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'.
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).
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error? [correction]
David Hopwood wrote:
> Darren New wrote:
>
>>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.)
>
> Right, but this is a disadvantage of their typestate algorithm. It is why
> the example in Figure 2 of
> <http://www.cs.ubc.ca/local/reading/proceedings/spe91-95/spe/vol25/issue4/spe950wk.pdf>
> fails to check, even though it "obviously" initializes all variables.
>
> Consider the equivalent Java program:
I mixed up Figures 1 and 2. Here is the Java program that Figure 2 should
be compared to:
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.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Darren New wrote:
> 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.)
Right, but this is a disadvantage of their typestate algorithm. It is why
the example in Figure 2 of
<http://www.cs.ubc.ca/local/reading/proceedings/spe91-95/spe/vol25/issue4/spe950wk.pdf>
fails to check, even though it "obviously" initializes all variables.
Consider the equivalent Java program:
public class LoopInitTest {
public static void main(String[] args) {
boolean b;
int i;
while (true) {
b = true;
if (b) {
v = 1;
}
v = v + 1;
}
}
}
As it happens, javac rejects this:
LoopInitTest.java:12: variable v might not have been initialized
v = v + 1;
^
but for a different and more trivial reason than the Hermes algorithm.
Change "if (b) { v = 1; }" to just "v = 1;", and the Java version will be
accepted by its definite assignment analysis (which is a dataflow analysis),
but the equivalent Hermes program still would not.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > David Hopwood <[EMAIL PROTECTED]> wrote: > >>This is true, but note that postconditions also need to be efficient >>if we are going to execute them. > > If checked by execution, yes. In which case, I am trying to get my head > around how it's any more true to say that functional languages are > compilable postconditions than to say the same of imperative languages. A postcondition must, by definition [*], be a (pure) assertion about the values that relevant variables will take after the execution of a subprogram. If a subprogram is intended to have side effects, then its postcondition can describe the results of the side effects, but must not reexecute them. [*] E.g. see <http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf>, although the term "postcondition" was introduced later than this paper. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > Joachim Durchholz <[EMAIL PROTECTED]> wrote: > >>OTOH, isn't that the grail that many people have been searching for: >>programming by simply declaring the results that they want to see? > > Possibly. > >>No, FPLs are actually just that: compilable postconditions. > > This seems to me a bit misleading. Perhaps someone will explain why I > should stop thinking this way; but currently I classify statements like > this in the "well, sort of" slot of my mind. If functional programming > were really just compilable postconditions, then functional programmers > would be able to skip a good bit of stuff that they really can't. For > example, time and space complexity of code is still entirely relevant > for functional programming. I can't simply write: > > (define fib > (lambda (x) (if (< x 2) 1 (+ (fib (- x 1)) (fib (- x 2)) > > and expect the compiler to create an efficient algorithm for me. This is true, but note that postconditions also need to be efficient if we are going to execute them. That is, the difference you've pointed out is not a difference between executable postconditions and functional programs. Both the inefficient functional definition of 'fib' and an efficient one are executable postconditions. In order to prove that the efficient implementation is as correct as the inefficient one, we need to prove that, treated as postconditions, the former implies the latter. (In this case a single deterministic result is required, so the former will be equivalent to the latter.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > David Hopwood wrote: >>Marshall wrote: >> >>>Wouldn't it be possible to do them at compile time? (Although >>>this raises decidability issues.) >> >>It is certainly possible to prove statically that some assertions cannot fail. >> >>The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2/docs.html) >>tool for JML (http://www.cs.iastate.edu/~leavens/JML/) is one system that does >>this -- although some limitations and usability problems are described in >><http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/papers/CASSIS2004.pdf>. > > I look forward to reading this. I read a paper on JML a while ago and > found it quite interesting. > >>>Mightn't it also be possible to >>>leave it up to the programmer whether a given contract >>>was compile-time or runtime? >> >>That would be possible, but IMHO a better option would be for an IDE to give >>an indication (by highlighting, for example), which contracts are dynamically >>checked and which are static. >> >>This property is, after all, not something that the program should depend on. >>It is determined by how good the static checker currently is, and we want to >>be >>able to improve checkers (and perhaps even allow them to regress slightly in >>order to simplify them .. or improve their performance .. > ) without changing programs. > > Hmmm. I have heard that argument before and I'm conflicted. > > I can think of more reasons than just runtime safety for which I'd > want proofs. Termination for example, in highly critical code; > not something for which a runtime check will suffice. It is true that some properties cannot be verified directly by a runtime check, but that does not mean that runtime checks are not indirectly useful in verifying them. For example, we can check at runtime that a loop variant is strictly decreasing with each iteration. Then, given that each iteration of the loop body terminates, it is guaranteed that the loop terminates, *either* because the runtime check fails, or because the variant goes to zero. In general, we can verify significantly more program properties using a combination of runtime checks and static proof, than we can using static proof alone. That may seem like quite an obvious statement, but the consequence is that any particular property is, in general, not verified purely statically or purely at runtime. I am not opposed to being able to annotate an assertion to say that it should be statically provable and that a runtime check should not be used. However, - such annotations should be very lightweight and visually undistracting, relative to the assertion itself; - a programmer should not interpret such an annotation on a particular assertion to mean that its static validity is not reliant on runtime checks elsewhere; - if the class of assertions that are statically provable changes, then a tool should be provided which can *automatically* add or remove these annotations (with programmer approval when they are removed). I'd like to make a couple more comments about when it is sufficient to detect errors and when it is necessary to prevent them: - If a language supports transactions, then this increases the proportion of cases in which it is sufficient to detect errors in imperative code. When state changes are encapsulated in a transaction, it is much easier to recover if an error is detected, because invariants that were true of objects used by the transaction when it started will be automatically reestablished. (Purely functional code does not need this.) - Almost all safety-critical systems have a recovery or safe shutdown behaviour which should be triggered when an error is detected in the rest of the program. The part of the program that implements this behaviour definitely needs to be statically correct, but it is usually only a small amount of code. Safety-critical systems that must either prevent errors or continue functioning in their presence (aircraft control systems, for example) are in a separate category that demand *much* greater verification effort. Even for these systems, though, it is still useful to detect errors in cases where they cannot be prevented. When multiple independent implementations of a subsystem are used to check each other, this error detection can be used as an input to the decision of which implementation is failing and which should take over. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
[Way off-topic] Re: What is a type error?
Joachim Durchholz wrote: > A concrete example: the > first thing that Windows does when accepting userland data structures > is... to copy them; this were unnecessary if the structures were immutable. It is necessary also because the userland structures are in a different privilege domain, and the memory backing them is potentially mapped by other processes, or accessible by other threads of this process, that can be running in parallel while the current thread is in the kernel. Also, it tends to be easier and more secure to treat userland structures as if they were in a different address space (even if for a particular OS, the kernel would be able to access user mode addresses directly). The kernel cannot trust that pointers in userland structures are valid, for instance. So, in order to avoid a copy when accepting a userland structure: - when servicing a kernel call for a given process, the OS must use kernel-mode page table mappings that are a superset of the user-mode mappings for that process at the point of the call. - the memory backing the structure must be immutable in all processes that could map it, and the kernel must trust the means by which it is made immutable. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Marshall wrote: > Joachim Durchholz wrote: [...] >>Preconditions/postconditions can express anything you want, and they are >>an absolutely natural extensions of what's commonly called a type >>(actually the more powerful type systems have quite a broad overlap with >>assertions). >>I'd essentially want to have an assertion language, with primitives for >>type expressions. > > Now, I'm not fully up to speed on DBC. The contract specifications, > these are specified statically, but checked dynamically, is that > right? In other words, we can consider contracts in light of > inheritance, but the actual verification and checking happens > at runtime, yes? For DBC as implemented in Eiffel, yes. > Wouldn't it be possible to do them at compile time? (Although > this raises decidability issues.) It is certainly possible to prove statically that some assertions cannot fail. The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2/docs.html) tool for JML (http://www.cs.iastate.edu/~leavens/JML/) is one system that does this -- although some limitations and usability problems are described in <http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/papers/CASSIS2004.pdf>. > Mightn't it also be possible to > leave it up to the programmer whether a given contract > was compile-time or runtime? That would be possible, but IMHO a better option would be for an IDE to give an indication (by highlighting, for example), which contracts are dynamically checked and which are static. This property is, after all, not something that the program should depend on. It is determined by how good the static checker currently is, and we want to be able to improve checkers (and perhaps even allow them to regress slightly in order to simplify them) without changing programs. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
George Neuner wrote: > On Tue, 11 Jul 2006 14:59:46 GMT, David Hopwood > <[EMAIL PROTECTED]> wrote: > >>What matters is that, over the range >>of typical programs written in the language, the value of the increased >>confidence in program correctness outweighs the effort involved in both >>adding annotations, and understanding whether any remaining run-time checks >>are guaranteed to succeed. > > Agreed, but ... > >>Look at it this way: suppose that I *need* to verify that a program has >>no range errors. Doing that entirely manually would be extremely tedious. >>If the compiler can do, say, 90% of the work, and point out the places that >>need to be verified manually, then that would be both less tedious, and >>less error-prone. > > 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. That's a good point. I don't think it would be an exaggeration to say that the some of the most commonly used compilers are riddled with bugs. gcc is a particularly bad offender, and at the moment seems to be introducing bugs with each new version at a faster rate than they can be fixed. Sun's javac also used to be poor in this respect, although I haven't used recent versions of it. 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. > I'm a fan of static typing but the major problem I have with complex > inferencing (in general) is the black box aspect of it. That is, when > the compiler rejects my code, is it really because a) I was stupid, b) > the types are too complex, or c) the compiler itself has a bug. Rejecting code incorrectly is much less of a problem than accepting it incorrectly. *If* all compiler bugs were false rejections, I would say that this would not be too much of an issue. Unfortunately there are plenty of bugs that result in silently generating bad code. But I don't think you can avoid that by using a language with a simpler type system. The quality of a compiler depends much more on the competence and attitudes of the language implementation developers, than it does on the language itself. [Although, choosing a language with a more quality-conscious compiler development team doesn't necessarily help if it is compiling to C, since then you still have to deal with C compiler bugs, but on autogenerated code :-(.] > It's certainly true that the vast majority of my problems are because > I'm stupid, but I've run into actual compiler bugs far too often for my > liking (high performance coding has a tendency to uncover them). Yes. Cryptographic algorithms, and autogenerated code also tend to do that. > I think I understand how to implement HM inferencing ... I haven't > actually done it yet, but I've studied it and I'm working on a toy > language that will eventually use it. But HM itself is a toy compared > to an inferencing system that could realistically handle some of the > problems that were discussed in this and Xah's "expressiveness" thread > (my own beef is with *static* checking of range narrowing assignments > which I still don't believe can be done regardless of Chris Smith's > assertions to the contrary). > > It seems to me that the code complexity of such a super-duper > inferencing system would make its bug free implementation quite > difficult and I personally would be less inclined to trust a compiler > that used it than one having a less capable (but easier to implement) > system. I don't think that the complexity of such a system would need to be any greater than that of the optimization frameworks used by many compilers. IIUC, what Chris Smith is suggesting is essentially equivalent to doing type inference on the SSA form of the program. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > David Hopwood <[EMAIL PROTECTED]> wrote: > >>Maybe I'm not understanding what you mean by "complete". Of course any >>type system of this expressive power will be incomplete (whether or not >>it can express conditions 3 to 5), in the sense that it cannot prove all >>true assertions about the types of expressions. > > Ah. I meant complete enough to accomplish the goal in this subthread, > which was to ensure that the compiler knows when a particular int > variable is guaranteed to be greater than 18, and when it is not. I don't think that placing too much emphasis on any individual example is the right way of thinking about this. What matters is that, over the range of typical programs written in the language, the value of the increased confidence in program correctness outweighs the effort involved in both adding annotations, and understanding whether any remaining run-time checks are guaranteed to succeed. Look at it this way: suppose that I *need* to verify that a program has no range errors. Doing that entirely manually would be extremely tedious. If the compiler can do, say, 90% of the work, and point out the places that need to be verified manually, then that would be both less tedious, and less error-prone. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Jürgen Exner wrote: > David Hopwood wrote: > [...] > > There is no such error message listed in 'perldoc perldiag'. > Please quote the actual text of your error message and include the program > that produced this error. > Then people here in CLPM may be able to assist you. Yes, I'm well aware that most of this thread has been off-topic for c.l.p.m, but it is no less off-topic for the other groups (except possibly c.l.functional), and I can't trim the Newsgroups line down to nothing. Don't you have a newsreader that can mark whole threads that you don't want to read? -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > David Hopwood <[EMAIL PROTECTED]> wrote: > >>1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather >>than types. > > One of us is missing the other's meaning here. If 3 to 5 were expressed > as assertions rather than types, then the type system would become > incomplete, requiring frequent runtime-checked type ascriptions to > prevent it from becoming impossible to write software. That's not my > idea of a usable language. Maybe I'm not understanding what you mean by "complete". Of course any type system of this expressive power will be incomplete (whether or not it can express conditions 3 to 5), in the sense that it cannot prove all true assertions about the types of expressions. So yes, some assertions would need to be checked at runtime (others could be proven to always hold by a theorem prover). Why is this a problem? The goal is not to check everything at compile time; the goal is just to support writing correct programs. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote: > At the same time, though, maybe I do want > the compiler to infer that tax cannot be negative (or maybe it can; I'm > not an accountant; I know my tax has never been negative), [...] Tax can be negative, e.g. when a business is claiming back VAT (sales tax) on its purchases, but the things it is selling have lower-rated or zero VAT (or it is making a loss). > Note that even without encapsulation, the kind of typing information > we're looking at can be very non-trivial in an imperative language. For > example, I may need to express a method signature that is kind of like > this: > > 1. The first parameter is an int, which is either between 4 and 8, or > between 11 and 17. > > 2. The second parameter is a pointer to an object, whose 'foo' field is > an int between 0 and 5, and whose 'bar' field is a pointer to another > object with three fields 'a', 'b', and 'c', each of which has the full > range of an unconstrained IEEE double precision floating point number. > > 3. After the method returns, it will be known that if this object > previously had its 'baz' field in the range m .. n, it is now in the > range (m - 5) .. (n + 1). > > 4. After the method returns, it will be known that the object reached by > following the 'bar' field of the second parameter will be modified so > that the first two of its floating point numbers are guaranteed to be of > the opposite sign as they were before, and that if they were infinity, > they are now finite. > > 5. After the method returns, the object referred to by the global > variable 'zab' has 0 as the value of its 'c' field. > > Just expressing all of that in a method signature looks interesting > enough. If we start adding abstraction to the type constraints on > objects to support encapsulation (as I think you'd have to do), then > things get even more interesting. 1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather than types. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Chris Smith wrote:
> I <[EMAIL PROTECTED]> wrote:
>
>>Incidentally, I'm not saying that such a feature would be a good idea.
I don't think it would be a bad idea. Silently giving incorrect results
on arithmetic overflow, as C-family languages do, is certainly a bad idea.
A type system that supported range type arithmetic as you've described would
have considerable advantages, especially in areas such as safety-critical
software. It would be a possible improvement to Ada, which UUIC currently
has a more restrictive range typing system that cannot infer different
ranges for a variable at different points in the program.
I find that regardless of programming language, relatively few of my
integer variables are dimensionless -- most are associated with some
specific unit. Currently, I find variable naming conventions helpful in
documenting this, but the result is probably more verbose than it would
be to drop this information from the names, and instead use more
precise types that indicate the unit and the range.
When prototyping, you could alias all of these to bignum types (with
range [0..+infinity) or (-infinity..+infinity)) to avoid needing to deal
with any type errors, and then constrain them where necessary later.
>>It generally isn't provided in languages specifically because it gets to
>>be a big pain to maintain all of the type specifications for this kind
>>of stuff.
It would take a little more work to write a program, but it would be no
more difficult to read (easier if you're also trying to verify its correctness).
Ease of reading programs is more important than writing.
> There are other good reasons, too, as it turns out. I don't want to
> overstate the "possible" until it starts to sound like "easy, even if
> it's a pain". This kind of stuff is rarely done in mainstream
> programming languages because it has serious negative consequences.
>
> For example, I wrote that example using variables of type int. If we
> were to suppose that we were actually working with variables of type
> Person, then things get a little more complicated. We would need a few
> (infinite classes of) derived subtypes of Person that further constrain
> the possible values for state. For example, we'd need types like:
>
> Person{age:{18..29}}
>
> But this starts to look bad, because we used to have this nice property
> called encapsulation.
I think you're assuming that 'age' would have to refer to a concrete field.
If it refers to a type parameter, something like:
class Person{age:Age} is
Age getAge()
end
then I don't see how this breaks encapsulation.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: languages with full unicode support
Joachim Durchholz wrote: > Chris Uppal schrieb: >> Joachim Durchholz wrote: >> >>>> This is implementation-defined in C. A compiler is allowed to accept >>>> variable names with alphabetic Unicode characters outside of ASCII. >>> >>> Hmm... that could would be nonportable, so C support for Unicode is >>> half-baked at best. >> >> Since the interpretation of characters which are yet to be added to >> Unicode is undefined (will they be digits, "letters", operators, symbol, >> punctuation ?), there doesn't seem to be any sane way that a >> language could allow an unrestricted choice of Unicode in identifiers. > > I don't think this is a problem in practice. E.g. if a language uses the > usual definition for identifiers (first letter, then letters/digits), > you end up with a language that changes its definition on the whims of > the Unicode consortium, but that's less of a problem than one might > think at first. It is not a problem at all. See the stability policies in <http://www.unicode.org/reports/tr31/tr31-2.html>. > Actually I'm not sure that Unicode is important for long-lived code. > Code tends to not survive very long unless it's written in English, in > which case anything outside of strings is in 7-bit ASCII. So the > majority of code won't ever be affected by Unicode problems - Unicode is > more a way of lowering entry barriers. Unicode in identifiers has certainly been less important than some thought it would be -- and not at all important for open source projects, for example, which essentially have to use English to get the widest possible participation. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Anton van Straaten wrote: > Chris Smith wrote: > >> What makes static type systems interesting is not the fact that these >> logical processes of reasoning exist; it is the fact that they are >> formalized with definite axioms and rules of inference, performed >> entirely on the program before execution, and designed to be entirely >> evaluatable in finite time bounds according to some procedure or set >> of rules, so that a type system may be checked and the same conclusion >> reached regardless of who (or what) is doing the checking. All that, >> and they still reach interesting conclusions about programs. > > There's only one issue mentioned there that needs to be negotiated > w.r.t. latent types: the requirement that they are "performed entirely > on the program before execution". More below. > >> If informal reasoning about types doesn't meet these criteria (and it >> doesn't), then it simply doesn't make sense to call it a type system >> (I'm using the static terminology here). It may make sense to discuss >> some of the ways that programmer reasoning resembles types, if indeed >> there are resemblances beyond just that they use the same basic rules >> of logic. It may even make sense to try to identify a subset of >> programmer reasoning that even more resembles... or perhaps even is... >> a type system. It still doesn't make sense to call programmer >> reasoning in general a type system. > > I'm not trying to call programmer reasoning in general a type system. > I'd certainly agree that a programmer muddling his way through the > development of a program, perhaps using a debugger to find all his > problems empirically, may not be reasoning about anything that's > sufficiently close to types to call them that. But "latent" means what > it implies: someone who is more aware of types can do better at > developing the latent types. So these "latent types" may in some cases not exist (in any sense), unless and until someone other than the original programmer decides how the program could have been written in a typed language? I don't get it. > As a starting point, let's assume we're dealing with a disciplined > programmer who (following the instructions found in books such as the > one at htdp.org) reasons about types, writes them in his comments, and > perhaps includes assertions (or contracts in the sense of "Contracts for > Higher Order Functions[1]), to help check his types at runtime (and I'm > talking about real type-checking, not just tag checking). > > When such a programmer writes a type signature as a comment associated > with a function definition, in many cases he's making a claim that's > provable in principle about the inputs and outputs of that function. This is talking about a development practice, not a property of the language. It may (for the sake of argument) make sense to assign a term such as latent typing to this development practice, but not to call the language "latently-typed". -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Andreas Rossberg wrote:
> 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
What I meant was, in the case of eval in an untyped ("dynamically typed")
language.
The approach you've just outlined is an implementation of staged compilation
in a typed language.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Costanza wrote: > David Hopwood wrote: >> Pascal Costanza wrote: >>> David Hopwood wrote: >>>> Marshall wrote: >>>> >>>>> The real question is, are there some programs that we >>>>> can't write *at all* in a statically typed language, because >>>>> they'll *never* be typable? >>>> >>>> In a statically typed language that has a "dynamic" type, all >>>> dynamically typed programs are straightforwardly expressible. >>> >>> What about programs where the types change at runtime? >> >> Staged compilation is perfectly compatible with static typing. >> Static typing only requires that it be possible to prove absence >> of some category of type errors when the types are known; it >> does not require that all types are known before the first-stage >> program is run. > > Can you change the types of the program that is already running, or are > the levels strictly separated? In most staged compilation systems this is intentionally not permitted. But this is not a type system issue. You can't change the types in a running program because you can't change the program, period. And you can't do that because most designers of these systems consider directly self-modifying code to be a bad idea (I agree with them). Note that prohibiting directly self-modifying code does not prevent a program from specifying another program to *replace* it. >> There are, however, staged compilation systems that guarantee that >> the generated program will be typeable if the first-stage program >> is. > > ...and I guess that this reduces again the kinds of things you can express. Yes. If you don't want that, use a system that does not impose this restriction/guarantee. >> (It's clear that to compare the expressiveness of statically and >> dynamically typed languages, the languages must be comparable in >> other respects than their type system. Staged compilation is the >> equivalent feature to 'eval'.) > > If it is equivalent to eval (i.e., executed at runtime), and the static > type checker that is part of eval yields a type error, then you still > get a type error at runtime! You can choose to use a system in which this is impossible because only typeable programs can be generated, or one in which non-typeable programs can be generated. In the latter case, type errors are detected at the earliest possible opportunity, as soon as the program code is known and before any of that code has been executed. (In the case of eval, OTOH, the erroneous code may cause visible side effects before any run-time error occurs.) I don't know what else you could ask for. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Java identifiers (was: languages with full unicode support)
ry charfinal interface static void class finally long strictfp volatile const float nativesuperwhile Identifier::= IdentifierChars butnot (Keyword | "true" | "false" | "null") IdentifierChars ::= JavaLetter | IdentifierChars JavaLetterOrDigit JavaLetter::= Lu | Ll | Lt | Lm | Lo | Nl | Sc | Pc JavaLetterOrDigit ::= JavaLetter | Nd | Mn | Mc | U+..0008 | U+000E..001B | U+007F..009F | Cf where the two-letter terminals refer to General Categories in Unicode 4.0.0 (exactly). Note that the so-called "ignorable" characters (for which isIdentifierIgnorable(codePoint) returns true) are not ignorable; they are treated like any other identifier character. This quote from the API spec: # The following Unicode characters are ignorable in a Java identifier [...] should be ignored (no pun intended). It is contradicted by: # Two identifiers are the same only if they are identical, that is, have the # same Unicode character for each letter or digit. in the language spec. Unicode does have a concept of ignorable characters in identifiers, which is probably where this documentation bug crept in. The inclusion of U+ and various control characters in the set of valid identifier characters is also a dubious decision, IMHO. Note that I am not defending in any way the complexity of this definition; there's clearly no excuse for it (or for the "ignorable" documentation bug). The language spec should have been defined directly in terms of the Unicode General Categories, and then the API in terms of the language spec. They way it is done now is completely backwards. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Paul Rubin wrote: > David Hopwood <[EMAIL PROTECTED]> writes: > >>Note that I'm not claiming that you can check any desirable property of >>a program (that would contradict Rice's Theorem), only that you can >>express any dynamically typed program in a statically typed language -- >>with static checks where possible and dynamic checks where necessary. > > It starts to look like sufficiently powerful static type systems are > confusing enough, that programming with them is at least as bug-prone > as imperative programming in dynamically typed languages. The static > type checker can spot type mismatches at compile time, but the > types themselves are easier and easier to get wrong. My assertion above does not depend on having a "sufficiently powerful static type system" to express a given dynamically typed program. It is true for static type systems that are not particularly complicated, and suffice to express all dynamically typed programs. I disagree with your implication that in general, static type systems for practical languages are getting too confusing, but that's a separate issue. (Obviously one can find type systems in research proposals that are too confusing as they stand.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: languages with full unicode support
Tim Roberts wrote: > "Xah Lee" <[EMAIL PROTECTED]> wrote: > >>Languages with Full Unicode Support >> >>As far as i know, Java and JavaScript are languages with full, complete >>unicode support. That is, they allow names to be defined using unicode. >>(the JavaScript engine used by FireFox support this) >> >>As far as i know, here's few other lang's status: >> >>C ? No. > > This is implementation-defined in C. A compiler is allowed to accept > variable names with alphabetic Unicode characters outside of ASCII. It is not implementation-defined in C99 whether Unicode characters are accepted; only how they are encoded directly in the source multibyte character set. Characters escaped using \u or \U00HH (H is a hex digit), and that are in the sets of characters defined by Unicode for identifiers, are required to be supported, and should be mangled in some consistent way by a platform's linker. There are Unicode text editors which encode/decode \u and \U on the fly, so you can treat this essentially like a Unicode transformation format (it would have been nicer to require support for UTF-8, but never mind). C99 6.4.2.1: # 3 Each universal character name in an identifier shall designate a character # whose encoding in ISO/IEC 10646 falls into one of the ranges specified in # annex D. 59) The initial character shall not be a universal character name # designating a digit. An implementation may allow multibyte characters that # are not part of the basic source character set to appear in identifiers; # which characters and their correspondence to universal character names is # implementation-defined. # # 59) On systems in which linkers cannot accept extended characters, an encoding # of the universal character name may be used in forming valid external # identifiers. For example, some otherwise unused character or sequence of # characters may be used to encode the \u in a universal character name. # Extended characters may produce a long external identifier. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joe Marshall wrote: > David Hopwood wrote: >>Joe Marshall wrote: >> >>>(defun blackhole (argument) >>> (declare (ignore argument)) >>> #'blackhole) >> >>This is typeable in any system with universally quantified types (including >>most practical systems with parametric polymorphism); it has type >>"forall a . a -> #'blackhole". > > The #' is just a namespace operator. The function accepts a single > argument and returns the function itself. You need a type that is a > fixed point (in addition to the universally quantified argument). Yes, see the correction in my follow-up. >>>>The real question is, are there some programs that we >>>>can't write *at all* in a statically typed language, because >>>>they'll *never* be typable? >>> >>>Certainly! As soon as you can reflect on the type system you can >>>construct programs that type-check iff they fail to type-check. >> >>A program that causes the type checker not to terminate (which is the >>effect of trying to construct such a thing in the type-reflective systems >>I know about) is hardly useful. >> >>In any case, I think the question implied the condition: "and that you >>can write in a language with no static type checking." > > Presumably the remainder of the program does something interesting! > > The point is that there exists (by construction) programs that can > never be statically checked. I don't think you've shown that. I would like to see a more explicit construction of a dynamically typed [*] program with a given specification, where it is not possible to write a statically typed program that meets the same specification using the same algorithms. AFAIK, it is *always* possible to construct such a statically typed program in a type system that supports typerec or gradual typing. The informal construction you give above doesn't contradict that, because it depends on reflecting on a [static] type system, and in a dynamically typed program there is no type system to reflect on. [*] Let's put aside disagreements about terminology for the time being, although I still don't like the term "dynamically typed". > The next question is whether such > programs are `interesting'. Certainly a program that is simply > designed to contradict the type checker is of limited entertainment > value, I don't know, it would probably have more entertainment value than most executive toys :-) > but there should be programs that are independently non > checkable against a sufficiently powerful type system. Why? Note that I'm not claiming that you can check any desirable property of a program (that would contradict Rice's Theorem), only that you can express any dynamically typed program in a statically typed language -- with static checks where possible and dynamic checks where necessary. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language [correction]
David Hopwood wrote:
> Joe Marshall wrote:
>
>>(defun blackhole (argument)
>> (declare (ignore argument))
>> #'blackhole)
>
> This is typeable in any system with universally quantified types (including
> most practical systems with parametric polymorphism); it has type
> "forall a . a -> #'blackhole".
Ignore this answer; I misinterpreted the code.
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.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Costanza wrote: > David Hopwood wrote: >> Marshall wrote: >> >>> The real question is, are there some programs that we >>> can't write *at all* in a statically typed language, because >>> they'll *never* be typable? >> >> In a statically typed language that has a "dynamic" type, all >> dynamically typed programs are straightforwardly expressible. > > What about programs where the types change at runtime? Staged compilation is perfectly compatible with static typing. Static typing only requires that it be possible to prove absence of some category of type errors when the types are known; it does not require that all types are known before the first-stage program is run. There are, however, staged compilation systems that guarantee that the generated program will be typeable if the first-stage program is. (It's clear that to compare the expressiveness of statically and dynamically typed languages, the languages must be comparable in other respects than their type system. Staged compilation is the equivalent feature to 'eval'.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joe Marshall wrote: > It isn't clear to me which programs we would have to give up, either. > I don't have much experience in sophisticated typed languages. It is > rather easy to find programs that baffle an unsophisticated typed > language (C, C++, Java, etc.). > > Looking back in comp.lang.lisp, I see these examples: > > (defun noisy-apply (f arglist) > (format t "I am now about to apply ~s to ~s" f arglist) > (apply f arglist)) 'noisy-apply' is typeable using either of these systems: <http://www.cs.jhu.edu/~pari/papers/fool2004/first-class_FOOL2004.pdf> <http://www.coli.uni-saarland.de/publikationen/softcopies/Muller:1998:TIF.pdf> (it should be easy to see the similarity to a message forwarder). > (defun blackhole (argument) > (declare (ignore argument)) > #'blackhole) This is typeable in any system with universally quantified types (including most practical systems with parametric polymorphism); it has type "forall a . a -> #'blackhole". >>The real question is, are there some programs that we >>can't write *at all* in a statically typed language, because >>they'll *never* be typable? > > Certainly! As soon as you can reflect on the type system you can > construct programs that type-check iff they fail to type-check. A program that causes the type checker not to terminate (which is the effect of trying to construct such a thing in the type-reflective systems I know about) is hardly useful. In any case, I think the question implied the condition: "and that you can write in a language with no static type checking." [...] >>>If you allow Turing Complete type systems, then I would say no--every >>>bug can be reforumlated as a type error. If you require your type >>>system to be less powerful, then some bugs must escape it. >> >>I don't think so. Even with a Turing complete type system, a program's >>runtime behavior is still something different from its static behavior. >>(This is the other side of the "types are not tags" issue--not only >>is it the case that there are things static types can do that tags >>can't, it is also the case that there are things tags can do that >>static types can't.) > > I agree. The point of static checking is to *not* run the program. If > the type system gets too complicated, it may be a de-facto interpreter. The following LtU post: <http://lambda-the-ultimate.org/node/1085> argues that types should be expressed in the same language that is being typed. I am not altogether convinced, but I can see the writer's point. There do exist practical languages in which types can be defined as arbitrary predicates or coercion functions, for example E (www.erights.org). E implementations currently perform type checking only at runtime, however, although it was intended to allow static analysis for types that could be expressed in a conventional static type system. I think the delay in implementing this has more to do with the E developers' focus on other (security and concurrency) issues, rather than an inherent difficulty. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language [correction]
David Hopwood wrote:
> Marshall wrote:
>>David Hopwood wrote:
>>>Marshall wrote:
>>>
>>>>The real question is, are there some programs that we
>>>>can't write *at all* in a statically typed language, because
>>>>they'll *never* be typable?
>>>
>>>In a statically typed language that has a "dynamic" type, all
>>>dynamically typed programs are straightforwardly expressible.
Correction: as the paper on gradual typing referenced below points
out in section 5, something like the "typerec" construct of
<http://citeseer.ist.psu.edu/harper95compiling.html> would be
needed, in order for a system with a "dynamic" type to be equivalent
in expressiveness to dynamic typing or gradual typing.
("typerec" can be used to implement "dynamic"; it is more general.)
>>So, how does this "dynamic" type work?
>
> <http://citeseer.ist.psu.edu/abadi89dynamic.html>
>
>>It can't simply be the "any" type, because that type has no/few
>>functions defined on it.
>
> It isn't. From the abstract of the above paper:
>
> [...] even in statically typed languages, there is often the need to
> deal with data whose type cannot be determined at compile time. To handle
> such situations safely, we propose to add a type Dynamic whose values are
> pairs of a value v and a type tag T where v has the type denoted by T.
> Instances of Dynamic are built with an explicit tagging construct and
> inspected with a type safe typecase construct.
>
> "Gradual typing" as described in
> <http://www.cs.rice.edu/~jgs3847/pubs/pubs/2006/siek06:_gradual.pdf> is
> another alternative. The difference between gradual typing and a
> "dynamic" type
This should be: the difference between gradual typing and a system with
"typerec"...
> is one of convenience rather than expressiveness --
> gradual typing does not require explicit tagging and typecase constructs.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > David Hopwood wrote: >>Marshall wrote: >>>David Hopwood wrote: >>>>Marshall wrote: >>>> >>>>>The real question is, are there some programs that we >>>>>can't write *at all* in a statically typed language, because >>>>>they'll *never* be typable? >>>> >>>>In a statically typed language that has a "dynamic" type, all >>>>dynamically typed programs are straightforwardly expressible. >>> >>>So, how does this "dynamic" type work? >> >><http://citeseer.ist.psu.edu/abadi89dynamic.html> >> >>>It can't simply be the "any" type, because that type has no/few >>>functions defined on it. >> >>It isn't. From the abstract of the above paper: >> >> [...] even in statically typed languages, there is often the need to >> deal with data whose type cannot be determined at compile time. To handle >> such situations safely, we propose to add a type Dynamic whose values are >> pairs of a value v and a type tag T where v has the type denoted by T. >> Instances of Dynamic are built with an explicit tagging construct and >> inspected with a type safe typecase construct. > > Well, all this says is that the type "dynamic" is a way to explicitly > indicate the inclusion of rtti. But that doesn't address my objection; > if a typesafe typecase construct is required, it's not like using > a dynamic language. They don't require typecase to inspect values > before one can, say, invoke a function. I was answering the question posed above: "are there some programs that we can't write *at all* in a statically typed language...?" >>"Gradual typing" as described in >><http://www.cs.rice.edu/~jgs3847/pubs/pubs/2006/siek06:_gradual.pdf> is >>another alternative. The difference between gradual typing and a >>"dynamic" type is one of convenience rather than expressiveness -- >>gradual typing does not require explicit tagging and typecase constructs. > > Perhaps this is the one I should read; it sounds closer to what I'm > talking about. Right; convenience is obviously important, as well as expressiveness. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > David Hopwood wrote: >>Marshall wrote: >> >>>The real question is, are there some programs that we >>>can't write *at all* in a statically typed language, because >>>they'll *never* be typable? >> >>In a statically typed language that has a "dynamic" type, all >>dynamically typed programs are straightforwardly expressible. > > So, how does this "dynamic" type work? <http://citeseer.ist.psu.edu/abadi89dynamic.html> > It can't simply be the "any" type, because that type has no/few > functions defined on it. It isn't. From the abstract of the above paper: [...] even in statically typed languages, there is often the need to deal with data whose type cannot be determined at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T. Instances of Dynamic are built with an explicit tagging construct and inspected with a type safe typecase construct. "Gradual typing" as described in <http://www.cs.rice.edu/~jgs3847/pubs/pubs/2006/siek06:_gradual.pdf> is another alternative. The difference between gradual typing and a "dynamic" type is one of convenience rather than expressiveness -- gradual typing does not require explicit tagging and typecase constructs. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > The real question is, are there some programs that we > can't write *at all* in a statically typed language, because > they'll *never* be typable? In a statically typed language that has a "dynamic" type, all dynamically typed programs are straightforwardly expressible. In a statically typed, Turing-complete language that does not have a "dynamic" type, it is always *possible* to express a dynamically typed program, but this may require a global transformation of the program or use of an interpreter -- i.e. the "Felleisen expressiveness" of the language is reduced. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Pascal Costanza wrote:
> David Hopwood wrote:
>> Pascal Costanza wrote:
>>> Chris Smith wrote:
>>>
>>>> While this effort to salvage the term "type error" in dynamic
>>>> languages is interesting, I fear it will fail. Either we'll all have
>>>> to admit that "type" in the dynamic sense is a psychological concept
>>>> with no precise technical definition (as was at least hinted by
>>>> Anton's post earlier, whether intentionally or not) or someone is
>>>> going to have to propose a technical meaning that makes sense,
>>>> independently of what is meant by "type" in a static system.
>>>
>>> What about this: You get a type error when the program attempts to
>>> invoke an operation on values that are not appropriate for this
>>> operation.
>>>
>>> Examples: adding numbers to strings; determining the string-length of a
>>> number; applying a function on the wrong number of parameters; applying
>>> a non-function; accessing an array with out-of-bound indexes; etc.
>>
>> This makes essentially all run-time errors (including assertion failures,
>> etc.) "type errors". It is neither consistent with, nor any improvement
>> on, the existing vaguely defined usage.
>
> Nope. This is again a matter of getting the levels right.
>
> Consider division by zero: appropriate arguments for division are
> numbers, including the zero. The dynamic type check will typically not
> check whether the second argument is zero, but will count on the fact
> that the processor will raise an exception one level deeper.
That is an implementation detail. I don't see its relevance to the above
argument at all.
> This is maybe better understandable in user-level code. Consider the
> following class definition:
>
> class Person {
> String name;
> int age;
>
> void buyPorn() {
>if (< this.age 18) throw new AgeRestrictionException();
>...
> }
> }
>
> The message p.buyPorn() is a perfectly valid message send and will pass
> both static and dynamic type tests (given p is of type Person in the
> static case). However, you will still get a runtime error.
Your definition above was "You get a type error when the program attempts
to invoke an operation on values that are not appropriate for this operation."
this.age, when less than 18, is a value that is inappropriate for the buyPorn()
operation, and so this satisfies your definition of a type error. My point was
that it's difficult to see any kind of program error that would *not* satisfy
this definition.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
Re: Termination and type systems
Dirk Thierbach wrote: > David Hopwood <[EMAIL PROTECTED]> wrote: >>Marshall wrote: >>>David Hopwood wrote: > >>>>A type system that required an annotation on all subprograms that >>>>do not provably terminate, OTOH, would not impact expressiveness >>>>at all, and would be very useful. > >>>Interesting. I have always imagined doing this by allowing an >>>annotation on all subprograms that *do* provably terminate. > > Maybe the paper "Linear types and non-size-increasing polynomial time > computation" by Martin Hofmann is interesting in this respect. <http://citeseer.ist.psu.edu/hofmann98linear.html> > From the abstract: > > We propose a linear type system with recursion operators for inductive > datatypes which ensures that all definable functions are polynomial > time computable. The system improves upon previous such systems in > that recursive definitions can be arbitrarily nested; in particular, > no predicativity or modality restrictions are made. > > It does not only ensure termination, but termination in polynomial time, > so you can use those types to carry information about this as well. That's interesting, but linear typing imposes some quite severe restrictions on programming style. From the example of 'h' on page 2, it's clear that the reason for the linearity restriction is just to ensure polynomial-time termination, and is not needed if we only want to prove termination. >>If the annotation marks not-provably-terminating subprograms, then it >>calls attention to those subprograms. This is what we want, since it is >>less safe/correct to use a nonterminating subprogram than a terminating >>one (in some contexts). > > That would be certainly nice, but it may be almost impossible to do in > practice. It's already hard enough to guarantee termination with the > extra information present in the type annotation. If this information > is not present, then the language has to be probably restricted so > severely to ensure termination that it is more or less useless. I think you're overestimating the difficulty of the problem. The fact that *in general* it can be arbitrarily hard to prove termination, can obscure the fact that for large parts of a typical program, proving termination is usually trivial. I just did a manual termination analysis for a 11,000-line multithreaded C program; it's part of a control system for some printer hardware. This program has: - 212 functions that trivially terminate. By this I mean that the function only contains loops that have easily recognized integer loop variants, and only calls other functions that are known to trivially terminate, without use of recursion. A compiler could easily prove these functions terminating without need for any annotations. - 8 functions that implement non-terminating event loops. - 23 functions that intentionally block. All of these should terminate (because of timeouts, or because another thread should do something that releases the block), but this cannot be easily proven with the kind of analysis we're considering here. - 3 functions that read from a stdio stream into a fixed-length buffer. This is guaranteed to terminate when reading a normal file, but not when reading from a pipe. In fact the code never reads from a pipe, but that is not locally provable. - 2 functions that iterate over a linked list of network adaptors returned by the Win32 GetAdaptorsInfo API. (This structure could be recognized as finite if we were calling a standard library abstraction over the OS API, but we are relying on Windows not to return a cyclic list.) - 1 function that iterates over files in a directory. (Ditto.) - 2 functions that iterate over a queue, implemented as a linked list. The queue is finite, but this is not locally provable. Possibly an artifact of the lack of abstraction from using C, where the loop is not easily recognizable as an iteration over a finite data structure. - 1 function with a loop that terminates for a non-trivial reason that involves some integer arithmetic, and is probably not expressible in a type system. The code aready had a comment informally justifying why the loop terminates, and noting a constraint needed to avoid an arithmetic overflow. (Bignum arithmetic would avoid the need for that constraint.) - 2 functions implementing a simple parsing loop, which terminates because the position of the current token is guaranteed to advance -- but this probably would not be provable given how the loop is currently written. A straightforward change (to make the 'next token' function return the number of characters to advance, asserted to be > 0, instead of a pointer to the next token)
Re: What is Expressiveness in a Computer Language [off-topic]
Matthias Blume wrote: > I agree with Bob Harper about safety being language-specific and all > that. But, with all due respect, I think his characterization of C is > not accurate. [...] > AFAIC, C is C-unsafe by Bob's reasoning. Agreed. > Of course, C can be made safe quite easily: > > Define a state "undefined" that is considered "safe" and add a > transition to "undefined" wherever necessary. I wouldn't say that was "quite easy" at all. C99 4 #2: # If a "shall" or "shall not" requirement that appears outside of a constraint # is violated, the behavior is undefined. Undefined behavior is otherwise # indicated in this International Standard by the words "undefined behavior" # *or by the omission of any explicit definition of behavior*. [...] In other words, to fix C to be a safe language (compatible with Standard C89 or C99), you first have to resolve all the ambiguities in the standard where the behaviour is *implicitly* undefined. There are a lot of them. -- David Hopwood <[EMAIL PROTECTED]> -- 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." Java's type system was unsound for much of its life. I think that supports the point that it's inadequate to simply "wish and hope" for soundness, and that a proof should be insisted on. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: Saying "latently-typed language" is making a category mistake
Matthias Blume wrote: > David Hopwood <[EMAIL PROTECTED]> writes: >>Patricia Shanahan wrote: >>>Vesa Karvonen wrote: >>>... >>> >>>>An example of a form of informal reasoning that (practically) every >>>>programmer does daily is termination analysis. [...] >>>>Given a program, it may be possible to formally >>>>prove that it terminates. >>> >>>To make the halting problem decidable one would have to do one of two >>>things: Depend on memory size limits, or have a language that really is >>>less expressive, at a very deep level, than any of the languages >>>mentioned in the newsgroups header for this message. >> >>I don't think Vesa was talking about trying to solve the halting problem. >> >>A type system that required termination would indeed significantly restrict >>language expressiveness -- mainly because many interactive processes are >>*intended* not to terminate. > > Most interactive processes are written in such a way that they > (effectively) consist of an infinitely repeated application of some > function f that maps the current state and the input to the new state > and the output. > >f : state * input -> state * output > > This function f itself has to terminate, i.e., if t has to be > guaranteed that after any given input, there will eventually be an > output. In most interactive systems the requirements are in fact much > stricter: the output should come "soon" after the input has been > received. > > I am pretty confident that the f for most (if not all) existing > interactive systems could be coded in a language that enforces > termination. Only the loop that repeatedly applies f would have to be > coded in a less restrictive language. This is absolutely consistent with what I said. While f could be coded in a system that *required* termination, the outer loop could not. As I mentioned in a follow-up, event loop languages such as E enforce this program structure, which would almost or entirely eliminate the need for annotations in a type system that proves termination of some subprograms. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
David Hopwood wrote: > Chris F Clark wrote: > >>I'm particularly interested if something unsound (and perhaps >>ambiguous) could be called a type system. > > Yes, but not a useful one. The situation is the same as with unsound > formal systems; they still satisfy the definition of a formal system. I meant "inconsistent formal systems". -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris F Clark wrote: > Chris Smith <[EMAIL PROTECTED]> writes: > >>Unfortunately, I have to again reject this idea. There is no such >>restriction on type theory. Rather, the word type is defined by type >>theorists to mean the things that they talk about. > > Do you reject that there could be something more general than what a > type theorist discusses? Or do you reject calling such things a type? > > Let you write: > >>because we could say that anything that checks types is a type system, >>and then worry about verifying that it's a sound type system without >>worrying about whether it's a subset of the perfect type system. > > I'm particularly interested if something unsound (and perhaps > ambiguous) could be called a type system. Yes, but not a useful one. The situation is the same as with unsound formal systems; they still satisfy the definition of a formal system. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Joachim Durchholz wrote: > Andreas Rossberg schrieb: > >> 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. > > Here's a matrix how most people that I know would fill in with terminology: > > | Statically | Not | > | typed| statically | > | | typed | >-+--+-+ >typesafe | "strongly| Dynamically | > | typed" | typed | > | (ML, Pascal) | (Lisp) | Pascal, in most of its implementations, isn't [memory] safe; it's in the same box as C. >-+--+-+ >not | (no common | "untyped" | >typesafe | terminology) | | > | (C) | (Assembly) | >-+--+-+ I have to say that I prefer the labels used by Cardelli. > (Terms in quotes are challenged on a regular basis, or rarely if ever > applied.) > > With the above terminology, it becomes clear that the opposite if > "(statically) typed" isn't "statically untyped", but "not statically > typed". "Statically typed" and "dynamically typed" aren't even > opposites, they just don't overlap. > > Another observation: type safeness is more of a spectrum than a clearcut > distinction. Even ML and Pascal have ways to circumvent the type system, Standard ML doesn't (with just the standard basis; no external libraries, and assuming that file I/O cannot be used to corrupt the language implementation). > and even C is typesafe unless you use unsafe constructs. > 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. It is quite possible to design languages that have absolutely no unsafe constructs, and are still useful. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > Joe Marshall wrote: > >>Marshall wrote: > >>>2) I want to run my program, even though it is broken, and I >>>want to run right up to a broken part and trap there, so I can >>>use the runtime facilities of the language to inspect what's >>>going on. >> >>I do this quite often. Sometimes I'll develop `in the debugger'. I'll >>change some piece of code and run the program until it traps. Then, >>without exiting the debugger, I'll fix the immediate problem and >>restart the program at the point it trapped. This technique takes a >>bit of practice, but if you are working on something that's complex and >>has a lot of state, it saves a lot of time because you don't have to >>reconstruct the state every time you make a change. The problem with this is that from that point on, what you're running is neither the old nor the new program, since its state may have been influenced by the bug before you corrected it. I find it far simpler to just restart the program after correcting anything. If this is too difficult, I change the design to make it less difficult. > Wow, interesting. > > (I say the following only to point out differing strategies of > development, not to say one or the other is right or bad or > whatever.) > > I occasionally find myself doing the above, and when I do, > I take it as a sign that I've screwed up. I find that process > excruciating, and I do everything I can to avoid it. Over the > years, I've gotten more and more adept at trying to turn > as many bugs as possible into type errors, so I don't have > to run the debugger. > > Now, there might be an argument to be made that if I had > been using a dynamic language, the process wouldn't be > so bad, and I woudn't dislike it so much. But mabe: > > As a strawman: suppose there are two broad categories > of mental strategies for thinking about bugs, and people > fall naturally into one way or the other, the way there > are morning people and night people. One group is > drawn to the static analysis, one group hates it. > One group hates working in the debugger, one group > is able to use that tool very effectively and elegantly. > > Anyway, it's a thought. I don't buy this -- or at least, I am not in either group. A good debugger is invaluable regardless of your attitude to type systems. Recently I was debugging two programs written to do similar things in the same statically typed language (C), but where a debugger could not be used for one of the programs. It took maybe 5 times longer to find and fix each bug without the debugger, and I found it a much more frustrating experience. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
David Hopwood wrote: > Anton van Straaten wrote: > >>I'm suggesting that if a language classifies and tags values in a way >>that supports the programmer in static reasoning about the behavior of >>terms, that calling it "untyped" does not capture the entire picture, >>even if it's technically accurate in a restricted sense (i.e. in the >>sense that terms don't have static types that are known within the >>language). >> >>Let me come at this from another direction: what do you call the >>classifications into number, string, vector etc. that a language like >>Scheme does? And when someone writes a program which includes the >>following lines, how would you characterize the contents of the comment: >> >>; third : integer -> integer >>(define (third n) (quotient n 3)) > > I would call it an informal type annotation. But the very fact that > it has to be expressed as a comment, and is not checked, What I meant to say here is "and is not used in any way by the language implementation," > means that > the *language* is not typed (even though Scheme is dynamically tagged, > and even though dynamic tagging provides *partial* support for a > programming style that uses this kind of informal annotation). -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Anton van Straaten wrote: > David Hopwood wrote: > >> I can accept that dynamic tagging provides some support for latent typing >> performed "in the programmer's head". But that still does not mean that >> dynamic tagging is the same thing as latent typing > > No, I'm not saying it is, although I am saying that the former supports > the latter. But since the relevant feature that the languages in question possess is dynamic tagging, it is more precise and accurate to use that term to describe them. Also, dynamic tagging is only a minor help in this respect, as evidenced by the fact that explicit tag tests are quite rarely used by most programs, if I'm not mistaken. IMHO, the support does not go far enough for it to be considered a defining characteristic of these languages. When tag tests are used implicitly by other language features such as pattern matching and dynamic dispatch, they are used for purposes that are equally applicable to statically typed and non-(statically-typed) languages. >> or that languages >> that use dynamic tagging are "latently typed". This simply is not a >> property of the language (as you've already conceded). > > Right. I see at least two issues here: one is that as a matter of > shorthand, compressing "language which supports latent typing" to > "latently-typed language" ought to be fine, as long as the term's > meaning is understood. If, for the sake of argument, "language which supports latent typing" is to be compressed to "latently-typed language", then statically typed languages must be considered also latently typed. After all, statically typed languages support expression and verification of the "types in the programmer's head" at least as well as non-(statically-typed) languages do. In particular, most recent statically typed OO languages use dynamic tagging and are memory safe. And they support comments ;-) This is not, quite obviously, what most people mean when they say that a particular *language* is "latently typed". They almost always mean that the language is dynamically tagged, *not* statically typed, and memory safe. That is how this term is used in R5RS, for example. > But beyond that, there's an issue here about the definition of "the > language". When programming in a latently-typed language, a lot of > action goes on outside the language - reasoning about static properties > of programs that are not captured by the semantics of the language. This is true of programming in any language. > 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. If you consider stuff that might be in the programmer's head as part of the program, where do you stop? When I maintain a program written by someone I've never met, I have no idea what was in that programmer's head. All I have is comments, which may be (and frequently are, unfortunately) inaccurate. (Actually, it's worse than that -- if I come back to a program 5 years later, I probably have little idea what was in my head at the time I wrote it.) > We have to accept, then, that the formal semantic definitions of > dynamically-checked languages are incomplete in some important ways. > Referring to those semantic definitions as "the language", as though > that's all there is to the language in a broader sense, is misleading. Bah, humbug. The language is just the language. > 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. I'm with Marshall -- this is way too mystical for me. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: Saying "latently-typed language" is making a category mistake
Pascal Costanza wrote: > Vesa Karvonen wrote: > >> I think that we're finally getting to the bottom of things. While >> reading your reponses something became very clear to me: latent-typing and >> latent-types are not a property of languages. Latent-typing, also known as >> informal reasoning, is something that all programmers do as a normal part >> of programming. To say that a language is latently-typed is to make a >> category mistake, because latent-typing is not a property of languages. > > I disagree with you and agree with Anton. Here, it is helpful to > understand the history of Scheme a bit: parts of its design are a > reaction to what Schemers perceived as having failed in Common Lisp (and > other previous Lisp dialects). > > One particularly illuminating example is the treatment of nil in Common > Lisp. That value is a very strange beast in Common Lisp because it > stands for several concepts at the same time: most importantly the empty > list and the boolean false value. Its type is also "interesting": it is > both a list and a symbol at the same time. It is also "interesting" that > its quoted value is equivalent to the value nil itself. This means that > the following two forms are equivalent: > > (if nil 42 4711) > (if 'nil 42 4711) > > Both forms evaluate to 4711. > > It's also the case that taking the car or cdr (first or rest) of nil > doesn't give you an error, but simply returns nil as well. > > The advantage of this design is that it allows you to express a lot of > code in a very compact way. See > http://www.apl.jhu.edu/~hall/lisp/Scheme-Ballad.text for a nice > illustration. > > The disadvantage is that it is mostly impossible to have a typed view of > nil, at least one that clearly disambiguates all the cases. There are > also other examples where Common Lisp conflates different types, and > sometimes only for special cases. [1] > > Now compare this with the Scheme specification, especially this section: > http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs-Z-H-6.html#%25_sec_3.2 > > This clearly deviates strongly from Common Lisp (and other Lisp > dialects). The emphasis here is on a clear separation of all the types > specified in the Scheme standard, without any exception. This is exactly > what makes it straightforward in Scheme to have a latently typed view of > programs, in the sense that Anton describes. So latent typing is a > property that can at least be enabled / supported by a programming > language, so it is reasonable to talk about this as a property of some > dynamically typed languages. If anything, I think that this example supports my and Vesa's point. The example demonstrates that languages *that are not distinguished in whether they are called latently typed* support informal reasoning about types to varying degrees. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Termination and type systems
Marshall wrote: > David Hopwood wrote: > >>A type system that required an annotation on all subprograms that do not >>provably terminate, OTOH, would not impact expressiveness at all, and would >>be very useful. > > Interesting. I have always imagined doing this by allowing an > annotation on all subprograms that *do* provably terminate. If > you go the other way, you have to annotate every function that > uses general recursion (or iteration if you swing that way) and that > seems like it might be burdensome. Not at all. Almost all subprograms provably terminate (with a fairly easy proof), even if they use general recursion or iteration. If it were not the case that almost all functions provably terminate, then the whole idea would be hopeless. If a subprogram F calls G, then in order to prove that F terminates, we probably have to prove that G terminates. Consider a program where only half of all subprograms are annotated as provably terminating. In that case, we would be faced with very many cases where the proof cannot be discharged, because an annotated subprogram calls an unannotated one. If, on the other hand, more than, say, 95% of subprograms provably terminate, then it is much more likely that we (or the inference mechanism) can easily discharge any particular proof involving more than one subprogram. So provably terminating should be the default, and other cases should be annotated. In some languages, annotations may never or almost never be needed, because they are implied by other characteristics. For example, the concurrency model used in the language E (www.erights.org) is such that there are implicit top-level event loops which do not terminate as long as the associated "vat" exists, but handling a message is always required to terminate. > Further, it imposes the > annotation requirement even where the programer might not > care about it, which the reverse does not do. If the annotation marks not-provably-terminating subprograms, then it calls attention to those subprograms. This is what we want, since it is less safe/correct to use a nonterminating subprogram than a terminating one (in some contexts). There could perhaps be a case for distinguishing annotations for "intended not to terminate", and "intended to terminate, but we couldn't prove it". I do not know how well such a type system would work in practice; it may be that typical programs would involve too many non-trivial proofs. This is something that would have to be tried out in a research language. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: Saying "latently-typed language" is making a category mistake
Patricia Shanahan wrote: > Vesa Karvonen wrote: > ... > >> An example of a form of informal reasoning that (practically) every >> programmer does daily is termination analysis. There are type systems >> that guarantee termination, but I think that is fair to say that it is >> not yet understood how to make a practical general purpose language, whose >> type system would guarantee termination (or at least I'm not aware of >> such a language). It should also be clear that termination analysis need >> not be done informally. Given a program, it may be possible to formally >> prove that it terminates. > > To make the halting problem decidable one would have to do one of two > things: Depend on memory size limits, or have a language that really is > less expressive, at a very deep level, than any of the languages > mentioned in the newsgroups header for this message. I don't think Vesa was talking about trying to solve the halting problem. A type system that required termination would indeed significantly restrict language expressiveness -- mainly because many interactive processes are *intended* not to terminate. A type system that required an annotation on all subprograms that do not provably terminate, OTOH, would not impact expressiveness at all, and would be very useful. Such a type system could work by treating some dependent type parameters as variants which must strictly decrease in a recursive call or loop. For example, consider a recursive quicksort implementation. The type of the 'sort' routine would take an array of length (dependent type parameter) n. Since it only performs recursive calls to itself with parameter strictly less than n, it is not difficult to prove automatically that the quicksort terminates. The programmer would probably just have to give hints in some cases as to which parameters are to be treated as variants; the rest can be inferred. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Anton van Straaten wrote: > I'm suggesting that if a language classifies and tags values in a way > that supports the programmer in static reasoning about the behavior of > terms, that calling it "untyped" does not capture the entire picture, > even if it's technically accurate in a restricted sense (i.e. in the > sense that terms don't have static types that are known within the > language). > > Let me come at this from another direction: what do you call the > classifications into number, string, vector etc. that a language like > Scheme does? And when someone writes a program which includes the > following lines, how would you characterize the contents of the comment: > > ; third : integer -> integer > (define (third n) (quotient n 3)) I would call it an informal type annotation. But the very fact that it has to be expressed as a comment, and is not checked, means that the *language* is not typed (even though Scheme is dynamically tagged, and even though dynamic tagging provides *partial* support for a programming style that uses this kind of informal annotation). -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris Uppal wrote: > David Hopwood wrote: > >>>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. >> >>A common term for languages which have defined behaviour at run-time is >>"memory safe". For example, "Smalltalk is untyped and memory safe." >>That's not too objectionable, is it? > > I find it too weak, as if to say: "well, ok, it can't actually corrupt memory > as such, but the program logic is still apt go all over the shop"... Well, it might ;-) (In case anyone thinks I am being pejorative toward not-statically-typed languages here, I would say that the program logic can *also* "go all over the shop" in a statically typed, memory safe language. To avoid this, you need at least a language that is "secure" in the sense used in capability systems, which is a stronger property than memory safety.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Dr.Ruud wrote: > Marshall schreef: >>Rob Thorpe: > >>>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? >> >>Well, of course you can't in *C*; you can barely zip you pants with C. >>But I believe you can do the above in C++, can't you? > > You can write self-modifying code in C, so I don't see how you can not > do that in C. ;) Strictly speaking, you can't write self-modifying code in Standard C. -- David Hopwood <[EMAIL PROTECTED]> -- 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: >> >>>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. > > Consider a langauge something like BCPL or a fancy assembler, but with > not quite a 1:1 mapping with machine langauge. > > It differs in one key regard: it has a variable declaration command. > This command allows the programmer to allocate a block of memory to a > variable. If the programmer attempts to index a variable outside the > block of memory allocated to it an error will occur. Similarly if the > programmer attempts to copy a larger block into a smaller block an > error would occur. > > Such a language would be truly untyped and "safe", that is safe > according to many peoples use of the word including, I think, yours. > > 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. So the hypothetical language, unlike Python, Perl and Lisp, is not dynamically *tagged*. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Anton van Straaten wrote: > [EMAIL PROTECTED] wrote: > >> I very much agree with the observation that every programmer performs >> "latent typing" in his head [...] >> 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".) > > Vesa raised a similar objection in his post 'Saying "latently typed > language" is making a category mistake'. I've made some relevant > responses to that post. > > I agree that there's a valid point in the sense that latent types are > not a property of the semantics of the languages they're associated with. > > But to take your example, I've had the pleasure of programming a little > in untyped lambda calculus. I can tell you that not having tags is > quite problematic. You certainly do perform latent typing in your head, > but without tags, the language doesn't provide any built-in support for > it. You're on your own. I can accept that dynamic tagging provides some support for latent typing performed "in the programmer's head". But that still does not mean that dynamic tagging is the same thing as latent typing, or that languages that use dynamic tagging are "latently typed". This simply is not a property of the language (as you've already conceded). -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Anton van Straaten wrote: > Andreas Rossberg wrote: >> Rob Warnock wrote: >> >>> 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. >> [...] > > That text goes back at least 20 years, to R3RS in 1986, and possibly > earlier, so part of what it represents is simply changing use of > terminology, combined with an attempt to put Scheme in context relative > to multiple languages and terminology usages. The fact that we're still > discussing this now, and haven't settled on terminology acceptable to > all sides, illustrates the problem. > > The Scheme report doesn't actually say anything about how latent types > relate to static types, in the way that I've recently characterized the > relationship here. However, I thought this was a good place to explain > how I got to where I am on this subject. > > There's been a lot of work done on soft type inference in Scheme, and > other kinds of type analysis. The Scheme report talks about latent > types as meaning "types are associated with values". While this might > cause some teeth-grinding amongst type theorists, it's meaningful enough > when you look at simple cases: cases where the type of a term is an > exact match for the type tags of the values that flow through that term. > > When you get to more complex cases, though, most type inferencers for > Scheme assign traditional static-style types to terms. If you think > about this in conjunction with the term "latent types", it's an obvious > connection to make that what the inferencer is doing is recovering types > that are latent in the source. But these types are not part of the Scheme language. If you combine Scheme with a type inferencer, you get a new language that is not R*RS Scheme, and *that* language is typed. Note that different inferencers will give different type assignments. They may be similar, but they may also be quite dissimilar in some cases. This casts considerable doubt on the assertion that the inferencer is "recovering types latent in the source". -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is a type error?
Pascal Costanza wrote: > Chris Smith wrote: > >> While this effort to salvage the term "type error" in dynamic >> languages is interesting, I fear it will fail. Either we'll all have >> to admit that "type" in the dynamic sense is a psychological concept >> with no precise technical definition (as was at least hinted by >> Anton's post earlier, whether intentionally or not) or someone is >> going to have to propose a technical meaning that makes sense, >> independently of what is meant by "type" in a static system. > > What about this: You get a type error when the program attempts to > invoke an operation on values that are not appropriate for this operation. > > Examples: adding numbers to strings; determining the string-length of a > number; applying a function on the wrong number of parameters; applying > a non-function; accessing an array with out-of-bound indexes; etc. This makes essentially all run-time errors (including assertion failures, etc.) "type errors". It is neither consistent with, nor any improvement on, the existing vaguely defined usage. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Travails of the JVM type system (was: What is Expressiveness in a Computer Language)
Chris Uppal wrote: > Maybe you are thinking that I mean that /because/ the JVM does verification, > etc, at "runtime" the system is hybrid ? > > Anyway that is /not/ what I mean. I'm (for these purposes) completely > uninterested in the static checking done by the Java to bytecode translator, > javac. I'm interested in what happens to the high-level, statically typed, > OO, > language called "java bytecode" when the JVM sees it. That language has a > strict static type system which the JVM is required to check. That's a > /static/ check in my book -- it happens before the purportedly correct code is > accepted, rather than while that code is running. > > I am also completely uninterested (for these immediate purposes) in the run > time checking that the JVM does (the stuff that results in > NoSuchMethodException, and the like). In the wider context of the thread, I > do > want to call that kind of thing (dynamic) type checking -- but those checks > are > not why I call the JVMs type system hybrid either. > > Oh well, having got that far, I may as well take another stab at "hybrid". > Since the JVM is running a static type system without access to the whole text > of the program, there are some things that it is expected to check which it > can't. So it records preconditions on classes which might subsequently be > loaded. It does, but interestingly, it wasn't originally intended to. It was intended to be possible to check each classfile based only on that class' explicit dependencies, without having to record constraints on the loading of future classes. However, the designers made various mistakes with the design of ClassLoaders which resulted in the original JVM type system being unsound, and hence insecure. The problem is described in <http://www.cis.upenn.edu/~bcpierce/courses/629/papers/Saraswat-javabug.html> (which spells my name wrong, I just noticed). The constraint-based approach, proposed by Liang and Bracha in <http://www.cs.purdue.edu/homes/jv/smc/pubs/liang-oopsla98.pdf>, was adopted in order to fix this. There were other, simpler, solutions (for example, restricting ClassLoader delegation to a strict tree structure), but the responsible people at Sun felt that they were insufficiently expressive. I thought, and still think, that they were mistaken. It is important for the type system to be no more complicated than necessary if there is to be any confidence in the security of implementations. In any case, as shown by <http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=4670071>, current JVM implementations do *not* reliably support the patterns of ClassLoader delegation that were intended to be enabled by Liang and Bracha's approach. [This "bug" (it should be classed as an RFE) is, inexplicably given how few programs are affected by it, the most voted-for bug in Sun's tracking system. I get the impression that most of the commentators don't understand how horribly complicated it would be to fix. Anyway, it hasn't been fixed for 4 years.] -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Andreas Rossberg wrote: > 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. 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. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Bourguignon wrote: > But it's always possible at run-time that new functions and new > function calls be generated such as: > > (let ((x "two")) > (eval `(defmethod g ((self ,(type-of x))) t)) > (eval `(defmethod h ((x ,(type-of x)) (y string)) >(,(intern (format nil "DO-SOMETHING-WITH-A-~A" (type-of x))) x) >(do-something-with-a-string y))) > (funcall (compile nil `(let ((x ,x)) (lambda () (f x "Hi!")) > > Will you execute the whole type-inference on the whole program "black > box" everytime you define a new function? Will you recompile all the > "black box" functions to take into account the new type the arguments > can be now? Yes, why not? > This wouldn't be too efficient. It's rare, so it doesn't need to be efficient. 'eval' is inherently inefficient, anyway. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Bourguignon wrote: > Pascal Costanza <[EMAIL PROTECTED]> writes: >>Andreas Rossberg wrote: >>>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?? >> >>Basically, yes. >> >>Note that this is a simplistic example. Consider, instead, sending a >>message to an object, or calling a generic function, without ensuring >>that there will be applicable methods for all possible cases. When I >>get a "message not understood" exception, I can then decide whether >>that kind of object shouldn't be a receiver in the first place, or >>else whether I should define an appropriate method. I don't want to be >>forced to decide this upfront, because either I don't want to be >>bothered, or maybe I simply can't because I don't understand the >>domain well enough yet, or maybe I want to keep a hook to be able to >>update the program appropriately while it is running. > > Moreover, a good proportion of the program and a good number of > algorithms don't even need to know the type of the objects they > manipulate. > > 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. But this is true also in a statically typed language with parametric polymorphism. [...] > Why should adding a few functions or methods, and providing input > values of a new type be rejected from a statically checked point of > view by a compiled program that would be mostly bit-for-bit the same > with or without this new type? It usually wouldn't be -- adding methods in a typical statically typed OO language is unlikely to cause type errors (unless there is a naming conflict, in some cases). Nor would adding new types or new functions. (*Using* new methods without declaring them would cause an error, yes.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > David Hopwood wrote: > >>As far as I can tell, the people who advocate using "typed" and "untyped" >>in this way are people who just want to be able to discuss all languages in >>a unified terminological framework, and many of them are specifically not >>advocates of statically typed languages. > > Its easy to create a reasonable framework. My earlier posts show simple > ways of looking at it that could be further refined, I'm sure there are > others who have already done this. > > The real objection to this was that latently/dynamically typed > languages have a place in it. You seem to very keen to attribute motives to people that are not apparent from what they have said. > 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. A common term for languages which have defined behaviour at run-time is "memory safe". For example, "Smalltalk is untyped and memory safe." That's not too objectionable, is it? (It is actually more common for statically typed languages to fail to be memory safe; consider C and C++, for example.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > Chris Smith wrote: >>Marshall <[EMAIL PROTECTED]> wrote: >> >>>I think what this highlights is the fact that our existing terminology >>>is not up to the task of representing all the possible design >>>choices we could make. Some parts of dynamic vs. static >>>a mutually exclusive; some parts are orthogonal. >> >>Really? I can see that in a strong enough static type system, many >>dynamic typing features would become unobservable and therefore would be >>pragmatically excluded from any probable implementations... but I don't >>see any other kind of mutual exclusion between the two. > > Well, it strikes me that some of what the dynamic camp likes > is the actual *absence* of declared types, or the necessity > of having them. So why aren't they happy with something like, say, Alice ML, which is statically typed, but has a "dynamic" type and type inference? I mean this as a serious question. > At the very least, requiring types vs. not requiring > types is mutually exclusive. Right, but it's pretty well established that languages that don't require type *declarations* can still be statically typed. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > Vesa Karvonen wrote: > >>In comp.lang.functional Anton van Straaten <[EMAIL PROTECTED]> wrote: >> >>>Let me add another complex subtlety, then: the above description misses >>>an important point, which is that *automated* type checking is not the >>>whole story. I.e. that compile time/runtime distinction is a kind of >>>red herring. >> >>I agree. I think that instead of "statically typed" we should say >>"typed" and instead of "(dynamically|latently) typed" we should say >>"untyped". [...] >>>It's certainly close enough to say that the *language* is untyped. >> >>Indeed. Either a language has a type system and is typed or has no >>type system and is untyped. I see very little room for confusion >>here. In my experience, the people who confuse these things are >>people from the dynamic/latent camp who wish to see types everywhere >>because they confuse typing with safety or having well-defined >>semantics. > > No. It's because the things that we call latent types we use for the > same purpose that programmers of static typed languages use static > types for. > > Statically typed programmers ensure that the value of some expression > is of some type by having the compiler check it. Programmers of > latently typed languages check, if they think it's important, by asking > what the type of the result is. > > The objection here is that advocates of statically typed language seem > to be claiming the "type" as their own word, and asking that others use > their definitions of typing, which are really specific to their > subjects of interest. As far as I can tell, the people who advocate using "typed" and "untyped" in this way are people who just want to be able to discuss all languages in a unified terminological framework, and many of them are specifically not advocates of statically typed languages. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
What is a type error?
Chris Uppal wrote: > David Hopwood wrote: > >> When people talk about "types" being associated with values in a "latently >> typed" >> or "dynamically typed" language, they really mean *tag*, not type. > > I don't think that's true. Maybe /some/ people do confuse the two, but I am > certainly a counter-example ;-) > > The tag (if any) is part of the runtime machinery (or, if not, then I don't > understand what you mean by the word), and while that is certainly a > reasonably > approximation to the type of the object/value, it is only an approximation, > and -- what's more -- is only an approximation to the type as yielded by one > specific (albeit abstract, maybe even hypothetical) type system. Yes. I should perhaps have mentioned that people sometimes mean "protocol" rather than "tag" or "type" (a protocol being the set of messages that an object can respond to, roughly speaking). > If I send #someMessage to a proxy object which has not had its referent set > (and assuming the default value, presumably some variant of nil, does not > understand #someMessage), then that's just as much a type error as sending > #someMessage to a variable holding a nil value. It's an error, certainly. People usually call it a type error. But does that terminology actually make sense? Typical programming languages have many kinds of semantic error that can occur at run-time: null references, array index out of bounds, assertion failures, failed casts, "message not understood", ArrayStoreExceptions in Java, arithmetic overflow, divide by zero, etc. Conventionally, some of these errors are called "type errors" and some are not. But there seems to be little rhyme or reason to this categorization, as far as I can see. If in a particular language, both array index bounds errors and "message not understood" can occur at run-time, then there's no objective reason to call one a type error and the other not. Both *could* potentially be caught by a type-based analysis in some cases, and both *are not* caught by such an analysis in that language. A more consistent terminology would reserve "type error" for errors that occur when a typechecking/inference algorithm fails, or when an explicit type coercion or typecheck fails. According to this view, the only instances where a run-time error should be called a "type error" are: - a failed cast, or no match for any branch of a 'typecase' construct. Here the construct that fails is a coercion of a value to a specific type, or a check that it conforms to that type, and so the term "type error" makes sense. - cases where a typechecking/inference algorithm fails at run-time (e.g. in a language with staged compilation, or dynamic loading with link-time typechecking). In other cases, just say "run-time error". > If I then assign the referent > of the proxy to some object which does understand #someMessage, then it is not > a type error to send #someMessage to the proxy. So the type has changed, but > nothing in the tag system of the language implementation has changed. In the terminology I'm suggesting, the object has no type in this language (assuming we're talking about a Smalltalk-like language without any type system extensions). So there is no type error, and no inconsistency. Objects in this language do have protocols, so this situation can be described as a change to the object's protocol, which changes whether a given message causes a protocol error. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Marshall wrote: > Torben Ægidius Mogensen wrote: > >>That's not true. ML has variables in the mathematical sense of >>variables -- symbols that can be associated with different values at >>different times. What it doesn't have is mutable variables (though it >>can get the effect of those by having variables be immutable >>references to mutable memory locations). > > 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. But one that is at least two hundred years old [*], and so unlikely to be fixed now. In any case, the intent of this usage (in both mathematics and programming) is that different *instances* of a variable can be associated with different values. [*] introduced by Leibniz, according to <http://members.aol.com/jeff570/v.html>, but that was presumably in Latin. The first use of "variable" as a noun recorded by the OED in written English is in 1816. -- David Hopwood <[EMAIL PROTECTED]> -- 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[*]. That can be handled readily (if not perfectly) in the informal > internal type system(s) which programmers run in their heads (pace the very > sensible post by Anton van Straaten today in this thread -- several branches > away), but cannot be handled by a type system based on sets-of-values (and is > also a counter-example to the idea that "the" dynamic type of an object/value > can be identified with its tag). > > ([*] if the set of operations in which it can legitimately partake changes. > That can happen explicitly in Smalltalk (using DNU proxies for instance if the > proxied object changes, or even using #becomeA:), but can happen anyway in > less > "free" languages -- the State Pattern for instance, or even (arguably) in the > difference between an empty list and a non-empty list). Dynamic changes in object behaviour are not incompatible with type systems based on sets of values (e.g. semantic subtyping). There are some tricky issues in making such a system work, and I'm not aware of any implemented language that does it currently, but in principle it's quite feasible. For a type system that can handle dynamic proxying, see <http://www.doc.ic.ac.uk/~scd/FOOL11/FCM.pdf>. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Rob Thorpe wrote: > Matthias Blume wrote: >>"Rob Thorpe" <[EMAIL PROTECTED]> writes: >> >>>I think we're discussing this at cross-purposes. In a language like C >>>or another statically typed language there is no information passed >>>with values indicating their type. >> >>You seem to be confusing "does not have a type" with "no type >>information is passed at runtime". >> >>>Have a look in a C compiler if you don't believe me. >> >>Believe me, I have. > > In a C compiler the compiler has no idea what the values are in the program. > It knows only their type in that it knows the type of the variable they > are contained within. > Would you agree with that? No. In any language, it may be possible to statically infer that the value of an expression will belong to a set of values smaller than that allowed by the expression's type in that language's type system. For example, all constants have a known value, but most constants have a type which allows more than one value. (This is an essential point, not just nitpicking.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
genea wrote: > [...] NOW that being said, I think > that the reason I like Haskell, a very strongly typed language, is that > because of it's type system, the language is able to do things like > lazy evaluation, [...] Lazy evaluation does not depend on, nor is it particularly helped by static typing (assuming that's what you mean by "strongly typed" here). An example of a non-statically-typed language that supports lazy evaluation is Oz. (Lazy functions are explicitly declared in Oz, as opposed to Haskell's implicit lazy evaluation, but that's not because of the difference in type systems.) -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Costanza wrote: > Rob Thorpe wrote: >> Pascal Costanza wrote: >>> Matthias Blume wrote: >>>> Pascal Costanza <[EMAIL PROTECTED]> writes: >>>> >>>>> (slot-value p 'address) is an attempt to access the field 'address in >>>>> the object p. In many languages, the notation for this is p.address. >>>>> >>>>> Although the class definition for person doesn't mention the field >>>>> address, the call to (eval (read)) allows the user to change the >>>>> definition of the class person and update its existing >>>>> instances. Therefore at runtime, the call to (slot-value p 'adress) >>>>> has a chance to succeed. >>>> >>>> I am quite comfortable with the thought that this sort of evil would >>>> get rejected by a statically typed language. :-) >>> >>> This sort of feature is clearly not meant for you. ;-P >> >> To be fair though that kind of thing would only really be used while >> debugging a program. >> Its no different than adding a new member to a class while in the >> debugger. >> >> There are other places where you might add a slot to an object at >> runtime, but they would be done in tidier ways. > > Yes, but the question remains how a static type system can deal with > this kind of updates. It's not difficult in principle: - for each class [*], define a function which converts an 'old' value of that class to a 'new' value (the ability to do this is necessary anyway to support some kinds of upgrade). A default conversion function may be autogenerated if the class definition has changed only in minor ways. - typecheck the new program and the conversion functions, using the old type definitions for the argument of each conversion function, and the new type definitions for its result. - have the debugger apply the conversions to all values, and then resume the program. [*] or nearest equivalent in a non-OO language. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Pascal Costanza wrote: > Chris Smith wrote: > >> Knowing that it'll cause a lot of strenuous objection, I'll >> nevertheless interject my plea not to abuse the word "type" with a >> phrase like "dynamically typed". If anyone considers "untyped" to be >> perjorative, as some people apparently do, then I'll note that another >> common term is "type-free," which is marketing-approved but doesn't >> carry the misleading connotations of "dynamically typed." We are >> quickly losing any rational meaning whatsoever to the word "type," and >> that's quite a shame. > > The words "untyped" or "type-free" only make sense in a purely > statically typed setting. In a dynamically typed setting, they are > meaningless, in the sense that there are _of course_ types that the > runtime system respects. > > Types can be represented at runtime via type tags. You could insist on > using the term "dynamically tagged languages", but this wouldn't change > a lot. Exactly _because_ it doesn't make sense in a statically typed > setting, the term "dynamically typed language" is good enough to > communicate what we are talking about - i.e. not (static) typing. Oh, but it *does* make sense to talk about dynamic tagging in a statically typed language. That's part of what makes the term "dynamically typed" harmful: it implies a dichotomy between "dynamically typed" and "statically typed" languages, when in fact dynamic tagging and static typing are (mostly) independent features. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: What is Expressiveness in a Computer Language
Chris Smith wrote: > Chris Uppal <[EMAIL PROTECTED]> wrote: > >>>I'm unsure whether to consider explicitly stored array lengths, which >>>are present in most statically typed languages, to be part of a "type" >>>in this sense or not. >> >>If I understand your position correctly, wouldn't you be pretty much forced to >>reject the idea of the length of a Java array being part of its type ? > > I've since abandoned any attempt to be picky about use of the word "type". I think you should stick to your guns on that point. When people talk about "types" being associated with values in a "latently typed" or "dynamically typed" language, they really mean *tag*, not type. It is remarkable how much of the fuzzy thinking that often occurs in the discussion of type systems can be dispelled by insistence on this point (although much of the benefit can be obtained just by using this terminology in your own mind and translating what other people are saying to it). It's a good example of the weak Sapir-Whorf hypothesis, I think. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: A critic of Guido's blog on Python's lambda
M Jared Finder wrote: > Alex Martelli wrote: >> Stefan Nobis <[EMAIL PROTECTED]> wrote: >>> [EMAIL PROTECTED] (Alex Martelli) writes: >>> >>>> if anonymous functions are available, they're used in even more >>>> cases where naming would help >>> >>> Yes, you're right. But don't stop here. What about expressions? Many >>> people write very complex expression, that are hard to understand. A >>> good language should forbid these abuse and don't allow expressions >>> with more than 2 or maybe 3 operators! >> >> That would _complicate_ the language (by adding a rule). I repeat what >> I've already stated repeatedly: a good criterion for deciding which good >> practices a language should enforce and which ones it should just >> facilitate is _language simplicity_. If the enforcement is done by >> adding rules or constructs it's probably not worth it; if the >> "enforcements" is done by NOT adding extra constructs it's a double win >> (keep the language simpler AND push good practices). > > Your reasoning, taken to the extreme, implies that an assembly language, > by virtue of having the fewest constructs, is the best designed language > ever. Assembly languages don't have the fewest constructs; kernel languages such as Core ML or Kernel-Oz do. In any case, I didn't read Alex's point as being that simplicity was the only criterion on which to make decisions about what practices a language should enforce or facilitate; just "a good criterion". However, IMHO anonymous lambdas do not significantly increase the complexity of the language or of programs, and they can definitely simplify programs in functional languages, or languages that use them for control constructs. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: A critic of Guido's blog on Python's lambda
Ken Tilton wrote: > [...] The upshot of what [Guido] wrote is that it would be really hard to make > semantically meaningful indentation work with lambda. Haskell manages it. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
Re: A Lambda Logo Tour
Xah Lee wrote: > PS if you know any new lambda logo, please let me know. Thanks. ^ Oops, no, that would be an old lambda logo... -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
