from:"Joachim Durchholz"

Marshall schrieb:
 What about my example of SQL? Mutation, no pointers, no aliasing.
 Yet: useful.

Sorry, but SQL does have aliasing.

E.g. if you have records that have name=John, surname=Doe, the 
statements
   SELECT * FROM persons WHERE name = John
and
   SELECT * FROM persons WHERE name = Doe
are aliases of each other.

The alias is actually in the WHERE clause. And this *can* get you into 
trouble if you have something that does
   UPDATE ... WHERE name = John
and
   UPDATE ... WHERE surname = Doe
e.g. doing something with the Johns, then updating the names of all 
Does, and finally restoring the Johns (but not recognizing that changing 
the names of all Does might have changed your set of Johns).

Conceptually, this is just the same as having two different access path 
to the same memory cell. Or accessing the same global variable through a 
call-by-reference parameter and via its global name.

BTW with views, you get not just aliasing but what makes aliasing really 
dangerous. Without views, you can simply survey all the queries that you 
are working with and lexically compare table and field names to see 
whether there's aliasing. With views, the names that you see in a 
lexical scope are not enough to determine aliasing.
E.g. if you use a view that builds upon the set of Johns but aren't 
aware of that (possibly due to abstraction barriers), and you change the 
name field of all Does, then you're altering the view without a chance 
to locally catch the bug. That's just as bad as with any pointer 
aliasing problem.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 void foo() {
   int i = 0;
   int j = 0;
   j = 1;
   i = 2;
   // check value of j here. It is still 1, no matter what you filled
// in above.
   // The assignment to i cannot be made to affect the value of j.
 }
 
 Those two local primitive variables cannot be made to have the same
 identity.

Sure. To state it more clearly, they cannot be aliases.

  But you can update them, so this is an example of mutability
 without the possibility of identity.

You're being a bit sloppy with terminology here. Identity in the 
phrase above refers to two entities, in the sense of i and j cannot be 
identical.
Identity is actually a property of a single entity, namely that what 
remains constant regardless of what you do with the entity.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 By your definition, pointer and variable are synonyms. That doesn't
 seem like a good idea to me. (What if i and j end up in registers?
 I have not heard it said that registers have addresses.)

There are no registers in the JVM ;-P

More specifically, where Joe said pointer he really meant reference. 
i refers to a variable, and you really want to make sure that the first 
i refers to the same variable as the second i, so whatever is referred 
to by i is really an identity.

 Those two local primitive variables cannot be made to have the same
 identity. But you can update them, so this is an example of mutability
 without the possibility of identity.
 The identity is temporal:  You use the same variable name at two
 different times.  Do you intend for the second `i' to mean the same
 variable as the first `i'?
 
 Okay, so i and i have the same identity.

Vacuous but true.

 I suppose you could argue that the language's namespace is an
 address-space, and variable names are addresses.

Correct.

 At this point, though, you've made the concept of identity so broad
 that it is now necessarily a property of all languages that use named
 values, whether updatable or not. I think you would also have to call
 3 a void pointer by this scheme.

It's not a void pointer, it's a pointer to an integer, but you're 
correct: 3, when written in a program text, is a reference to the 
successor of the successor of the successor of zero.

If you find that silly and would like to stick with equality, then 
you're entirely correct. Natural numbers are entirely immutable by 
definition, and I'm definitely not the first one to observe that 
identity and equality are indistinguishable for immutable objects.

 Clearly there is *some* difference between a language which allows
 explicit pointers and thus aliasing and one that doesn't.

You can have aliasing without pointers; e.g. arrays are fully sufficient.
If i = j, then a [i] and a [j] are aliases of the same object.

(After I observed that, I found it no longer a surprise that array 
optimizations are what Fortran compiler teams sink most time into. The 
aliasing problems are *exactly* the same as those with pointers in C - 
though in practice, the Fortranistas have the advantage that the 
compiler will usually know that a [i] and b [j] cannot be aliases of 
each other, so while they have the same problems, the solutions give the 
Fortranistas more leverage.)

  What term would you use? First-class variables?

I think it's more a quasi-continuous spectrum.

On one side, we have alias-free toy languages (no arrays, no pointers, 
no call-by-reference, just to name the most common sources of aliasing).

SQL is slightly more dangerous: it does have aliases, but they are 
rarely a problem (mostly because views aren't a very common thing, and 
even if they are used, they aren't usually so abstract that they really 
hide the underlying dependencies).

Next are languages with arrays and call-by-reference. Pascal without 
pointers would be a candidate.
Here, aliasing occurs, and it can and does hide behind abstraction 
barriers, but it's not a serious problem unless the software becomes 
*really* large.

The end of the line are languages that use references to mutable data 
everywhere. All OO languages are a typical example of that.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 Joachim Durchholz wrote:
 It's just that I know that it's viable to give up destructive updates.
 Giving up pointers is a far more massive restriction.
 
 Oddly, I feel the opposite. While it's true there are many domains
 for which purely functional programming is a fine choice, there
 are some domains for which it is insufficient. Any kind of data
 managament, for example, requires that you be able to update
 the information.

Sure, the data itself cannot be managed non-destructively.

However, the programs that operate on the data need not do destructive 
updates internally. That way, I can have pointers inside the programs 
without giving up aliasing.
(Aliasing is really, really, really important. It's the reason why 
mathematicians can handle infinite objects - they copy just the alias, 
i.e. the name or description, instead of the object itself. It's one of 
the things that make abstraction useful.)

 Right. To me the response to this clear: give up pointers. Imperative
 operations are too useful to give up; indeed they are a requirement
 for certain problems.
 I don't know any.
 In some cases, you need an additional level of conceptual indirection -
 instead of *doing* the updates, you write a function that *describes* them.
 
 But then what do you do with that function?

I pass it to an engine that's imperative.

However, that engine doesn't need to do aliasing anymore.

In other words, I'm separating mutability and aliasing, so that they 
can't combine and explode.

  Let's say I have an
 employee database. John Smith just got hired on 1/1/2006 with
 a salary of $10,000. I need to record this fact somewhere. How
 do I do that without variables? Current-employees is a variable.
 Even if I have the space to keep all historical data, so I'm not
 deleting anything, I still have to have a variable for the latest
 version of the accumulated data. I can solve this without
 pointers, but I can't solve it without variables.

As I said elsewhere, the record has an identity even though it isn't 
explicit in SQL.
(SQL's data manipulation language is generally not considered half as 
clean as the query language; I think the core of the problemsis that 
DML combines mutability and identity.)

 I should like to learn more about these. I have some vague
 perception of the existence of linear logic, but not much
 else. However, I also already have an excellent solution
 to the pointer aliasing problem, so I'm less motivated.

Pointers are just the most obvious form of aliasing. As I said 
elsewhere, there are others: array indexing, by-reference parameters, or 
even WHERE clauses in SQL statements. In fact, anything that selects an 
updatable piece of data from a collection is an alias, and incurs the 
same problems as pointers, though they may come in different disguises.

 Actually SQL has references - they are called primary keys, but they
 are references nevertheless.
 
 I strongly object; this is quite incorrect. I grant you that from the
 50,000 foot level they appear identical, but they are not. To
 qualify as a reference, there need to be reference and dereference
 operations on the reference datatype; there is no such operation
 is SQL.
 
 Would you say the relational algebra has references?

Yes.

 Or, consider the classic prolog ancestor query. Let's say we're
 setting up as follows
 
 father(bob, joe).
 father(joe, john).
 
 Is joe a reference, here? After all, when we do the ancestor
 query for john, we'll see his father is joe and then use that to
 find joe's father. Keys in SQL are isomorphic to joe in the
 above prolog.

Agreed. They are both references ;-P

 (Some SQL dialects also offer synthetic
 ID fields that are guaranteed to remain stable over the lifetime of a
 record.
 
 Primary keys are updatable; there is nothing special about them.

Right - I was wrong with identifying keys and identities. In fact the 
identity of an SQL record cannot be directly obtained (unless via those 
ID fields).
The records still have identities. It's possible to have two WHERE 
clauses that refer to the same record, and if you update the record 
using one WHERE clause, the record returned by the other WHERE clause 
will have changed, too.

 With a repeatable read isolation level, you actually return to a
 declarative view of the database: whatever you do with it, you won't see
 it until you commit the transaction. (As soon as you commit, the
 declarative peace is over and you better watch out that your data
 doesn't become inconsistent due to aliasing.)
 
 Alas, transaction isolation levels are a performance hack.
 I cannot defend them on any logical basis. (Aside: did you mean
 serializable, rather than repeatable read?)

Possibly. There are so many isolation levels that I have to look them up 
whenever I want to get the terminology 100% correct.

 The only thing that can really be done about it is not adding it
 artificially into a program. In those cases where aliasing is part

Re: What is a type error?

Marshall schrieb:
 Joachim Durchholz wrote:
 Marshall schrieb:
 What about my example of SQL? Mutation, no pointers, no aliasing.
 Yet: useful.
 Sorry, but SQL does have aliasing.
 
 Well. I suppose we do not have an agreed upon definition
 of aliasing, so it is hard to evaluate either way. I would
 propose using the same one you used for identity:
 
 if there are two variables and modifying one also modifies
 the other, then there is aliasing between them.

I think that's an adequate example.
For a definition, I'd say it's a bit too narrow unless we use a fairly 
broad definition for variable. I.e. in a C context, I'd say that a-b 
is a variable, too, as would be foo(blah)-x.

 I avoided mentioning equality to include, for example,
 having an array i that is an alias to a subset of array j.

This would mean that there's aliasing between, say, a list of 
transaction records and the balance of the account (since modifying the 
list of transactions will change the balance, unless the object isn't 
properly encapsulated).
For purposes of this discussion, it's probably fair to say that's a 
form of aliasing, too, even though it's quite indirect.

 E.g. if you have records that have name=John, surname=Doe, the
 statements
SELECT * FROM persons WHERE name = John
 and
SELECT * FROM persons WHERE name = Doe
 are aliases of each other.

Argh... I made a most braindamaged, stupid mistake here. The second 
SELECT should have used the *surname* field, so it would be

 SELECT * FROM persons WHERE surname = Doe

Then, if there's a record that has name = John, surname = Doe, the 
two WHERE clauses have aliasing in the form of overlapping result sets.

 The alias is actually in the WHERE clause.
 
 Not by my definition, because there is only one variable here.

Sorry, my wording was sloppy.

I meant to say that 'in SQL, you identify records via clauses like WHERE 
name = John, i.e. WHERE clauses are a kind of identity'.

This is still not precise - the identity of an SQL record isn't 
explicitly accessible (except the nonstandard OID facility that some SQL 
engines offer). Nevertheless, they do have an identity, and there's a 
possibility of aliasing - if you change all Johns, you may also change a 
Doe.

 And this *can* get you into
 trouble if you have something that does
UPDATE ... WHERE name = John
 and
UPDATE ... WHERE surname = Doe
 e.g. doing something with the Johns, then updating the names of all
 Does, and finally restoring the Johns (but not recognizing that changing
 the names of all Does might have changed your set of Johns).
 
 The fact that some person might get confused about the
 semantics of what they are doing does not indicate aliasing.
 It is easy enough to do an analysis of your updates and
 understand what will happen; this same analysis is impossible
 with two arbitrary pointers, unless one has a whole-program
 trace. That strikes me as a significant difference.

Sure. I said that aliases in SQL aren't as bad as in other programs.

Once you get abstraction mixed in, the analysis becomes less 
straightforward. In the case of SQL, views are such an abstraction 
facility, and they indeed can obscure what you're doing and make the 
analysis more difficult. If it's just SQL we're talking about, you 
indeed have to look at the whole SQL to check whether there's a view 
that may be involved in the queries you're analysing, so the situation 
isn't *that* different from pointers - it's just not a problem because 
the amount of code is so tiny!

 Conceptually, this is just the same as having two different access path
 to the same memory cell. Or accessing the same global variable through a
 call-by-reference parameter and via its global name.
 
 There are similarities, but they are not the same.

What are the relevant differences? How does the semantics of a WHERE 
clause differ from that of a pointer, in terms of potential aliasing?

My line of argument would be this:
Pointers can be simulated using arrays, so it's no surprise that arrays 
can emulate all the aliasing of pointers.
Arrays can be simulated using WHERE (with SELECT and UPDATE), so I'd say 
that SQL can emulate all the aliasing of arrays, and hence that of pointers.

 BTW with views, you get not just aliasing but what makes aliasing really
 dangerous. Without views, you can simply survey all the queries that you
 are working with and lexically compare table and field names to see
 whether there's aliasing. With views, the names that you see in a
 lexical scope are not enough to determine aliasing.
 E.g. if you use a view that builds upon the set of Johns but aren't
 aware of that (possibly due to abstraction barriers), and you change the
 name field of all Does, then you're altering the view without a chance
 to locally catch the bug. That's just as bad as with any pointer
 aliasing problem.
 
 It is certainly aliasing, but I would not call it just as bad. There
 are
 elaborate declarative constraint mechanisms in place

Re: What is a type error?

Marshall schrieb:
 Joachim Durchholz wrote:
 You can have aliasing without pointers; e.g. arrays are fully sufficient.
 If i = j, then a [i] and a [j] are aliases of the same object.
 
 I am having a hard time with this very broad definition of aliasing.
 Would we also say that a[1+1] and a[2] are aliases? It seems
 to me, above, that we have only a, and with only one variable
 there can be no aliasing.

a[1] is a variable, too. You can assign values to it.

Inside function foo when called as foo(a[1]), it may even be referenced 
with yet another name and updated in isolation; foo may not even know 
it's an array element. (This is sort-of true in C, and definitely true 
in languages that don't have pointer arithmetic. If you pass a[1] to a 
call-by-reference parameter in Pascal, the callee has no way to access 
the parameter as if it were an array element.)

 A further question:
 
 given a 32 bit integer variable x, and offsets i and j (equal as in
 the above example) would you say that
 
x = (1  i)
 and
x = (1  j)
 
 are aliased expressions for setting a particular bit in x?

Yes.

 I am not being facetious; I am trying to understand the limits
 of your definition for aliasing.

Understood and appreciated.

 (After I observed that, I found it no longer a surprise that array
 optimizations are what Fortran compiler teams sink most time into. The
 aliasing problems are *exactly* the same as those with pointers in C -
 though in practice, the Fortranistas have the advantage that the
 compiler will usually know that a [i] and b [j] cannot be aliases of
 each other, so while they have the same problems, the solutions give the
 Fortranistas more leverage.)
 
 I don't understand this paragraph. On the one hand, it seems you
 are saying that C and Fortran are identically burdened with the
 troubles caused by aliasing, and then a moment later it seems
 you are saying the situation is distinctly better with Fortran.

That's exactly the situation.
Aliasing is present in both language, but in Fortran, the guarantee that 
two names aren't aliased are easier to come by.
Even more non-aliasing guarantees exist if the language has a more 
expressive type system. In most cases, if you know that two expressions 
have different types, you can infer that they cannot be aliases.

Of course, the life of compiler writers if of less importance to us; I 
added them only because the reports of Fortran compilers having aliasing 
problems due to array indexes made me aware that pointers aren't the 
only source of aliasing. That was quite a surprise to me then.

 Now with this, it appears you are agreeing that SQL has an advantage
 vis-a-vis aliasing compared to OO languages. Yes?

Sure.
I think that making an aliasing bug in SQL is just as easy as in any 
pointer-ridden language, but transactions and constraints (plus the 
considerably smaller typical size of SQL code) make it far easier to 
diagnose any such bugs.

 If so, we are agreeing on the part I care about, and the specifics of
 just what we call aliasing are not so important to me.

I'm not sure whether I'm getting the same mileage out of this, but the 
relevance of a problem is obviously a function on what one is doing on a 
day-to-day basis, so I can readily agree with that :-)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
Joachim Durchholz wrote:
Marshall schrieb:
Joachim Durchholz wrote:
Marshall schrieb:
I can see the lack of a formal model being an issue, but is the
imperative bit really all that much of an obstacle? How hard
is it really to deal with assignment? Or does the issue have
more to do with pointers, aliasing, etc.?
Actually aliasing is *the* hard issue.
Okay, sure. Nice explanation.

But one minor point: you describe this as an issue with imperative
languages. But aliasing is a problem associated with pointers,
not with assignment.
Aliasing is not a problem if the aliased data is immutable.

Okay, sure. But for the problem you describe, both imperativeness
and the presence of pointers is each necessary but not sufficient;
it is the two together that causes the problem. So it strikes
me (again, a very minor point) as inaccurate to describe this as
a problem with imperative languages per se.

Sure.
It's just that I know that it's viable to give up destructive updates.
Giving up pointers is a far more massive restriction.

Right. To me the response to this clear: give up pointers. Imperative
operations are too useful to give up; indeed they are a requirement
for certain problems.

I don't know any.
In some cases, you need an additional level of conceptual indirection -
instead of *doing* the updates, you write a function that *describes* them.

Pointers on the other hand add nothing except
efficiency and a lot of confusion. They should be considered an
implementation technique only, hidden behind some pointerless
computational model.

I recognize that this is likely to be a controversial opinion.

Indeed.

In fact modes are a way to restrict pointer aliasing.

I heartily support immutability as the default, for these and other
reasons.

OK, then we're in agreement here.

Some functional languages restrict assignment so that there can exist at
most a single reference to any mutable data structure. That way, there's
still no aliasing problems, but you can still update in place where it's
really, really necessary.

Are we speaking of uniqueness types now? I haven't read much about
them, but it certainly seems like an intriguing concept.

Yup.
It's called modes in some other languages (Mercury or Clean IIRC).

I know of no professional language that doesn't have references of some
kind.

Ah, well. I suppose I could mention prolog or mercury, but then
you used that troublesome word professional. So I will instead
mention a language which, if one goes by number of search results
on hotjobs.com for xxx progammer for different value of xxx, is
more popular than Java and twice as popular as C++. It lacks
pointers (although I understand they are beginning to creep in
in the latest version of the standard.) It also posesses a quite
sophisticated set of facilities for declarative integrity constraints.
Yet for some reason it is typically ignored by language designers.

http://hotjobs.yahoo.com/jobseeker/jobsearch/search_results.html?keywords_all=sql+programmer

Oh, right. SQL is an interesting case of getting all the problems of
pointers without having them ;-)

Actually SQL has references - they are called primary keys, but they
are references nevertheless. (Some SQL dialects also offer synthetic
ID fields that are guaranteed to remain stable over the lifetime of a
record. Seems like SQL is imperative enough that programmers want this,
else the SQL vendors wouldn't have added the feature...)
SQL also has updates.
The result: updates with undefined semantics. E.g. if you have a numeric
key field, UPDATE commands that increment the key by 1 will fail or work
depending on the (unspecified) order in which UPDATE touches the
records. You can have even more fun with updatable views.
With a repeatable read isolation level, you actually return to a
declarative view of the database: whatever you do with it, you won't see
it until you commit the transaction. (As soon as you commit, the
declarative peace is over and you better watch out that your data
doesn't become inconsistent due to aliasing.)

Aliasing isn't really related to specific programming practices. If two
accountants chat, and one talks about the hot blonde secretaire and the
other about his adorable wife, you can imagine the awkwardness that
ensues as soon as they find out they're talking about the same person!
The only thing that can really be done about it is not adding it
artificially into a program. In those cases where aliasing is part of
the modelled domain, you really have to carefully inspect all
interactions and never, never, never dream about abstracting it away.

Regards,
Jo
--
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Darren New schrieb:
 Joachim Durchholz wrote:
 Actually, in a functional programming language (FPL), you write just 
 the postconditions and let the compiler generate the code for you.
 
 Certainly. And my point is that the postcondition describing all valid 
 chess boards reachable from this one is pretty much going to be as big 
 as an implementation for generating it, yes?

Yes. It's a classical case where the postcondition and the code that 
fulfils it are essentially the same.

  The postcondition will
 still have to contain all the rules of chess in it, for example. At best 
 you've replaced loops with some sort of universal quanitifier with a 
 such that phrase.

Correct.

OTOH, isn't that the grail that many people have been searching for: 
programming by simply declaring the results that they want to see?

 Anyway, I expect you could prove you can't do this in the general case. 
 Otherwise, you could just write a postcondition that asserts the output 
 of your function is machine code that when run generates the same 
 outputs as the input string would. I.e., you'd have a compiler that can 
 write other compilers, generated automatically from a description of the 
 semantics of the input stream and the semantics of the machine the code 
 is to run on. I'm pretty sure we're not there yet, and I'm pretty sure 
 you start running into the limits of computability if you do that.

No, FPLs are actually just that: compilable postconditions.
Computability issues aren't more or less a factor than with other kinds 
of compilers: they do limit what you can do, but these limits are loose 
enough that you can do really useful stuff within them (in particular, 
express all algorithms).

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 David Hopwood wrote:
 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.
 
 Hmmm. I have heard that argument before and I'm conflicted.

I'd want several things.

A way for me to indicate what assertions must be proven statically.
Highlighting (be it compiler messages or flashing colors in an IDE) that 
marks assertions that *will* break.
And highlighting for assertions that *may* break.
In the language, a (possibly) simplicistic inference engine definition 
that gives me minimum guarantees about the things that it will be able 
to prove; if something is out of the reach of the engine, a 
straightforward way to add intermediate assertions until the inference 
succeeds.

(Plus diagnostics that tell me where the actual error may be, whether 
it's a bug in the code or an omission in the assertions. That's probably 
the hardest part of it all.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 Mutability by itself does not imply identity.

Well, the implication certainly holds from identity to mutability.
The only definition of identity that I found to hold up for all kinds of 
references (pointers, shared-memory identifiers, URLs etc.) is this:

Two pieces of data are identical if and only if:
a) they are equal
b) they stay equal after applying an arbitrary operation to one of them.

This means that for immutable objects, there's no observable difference 
between equality and identity (which I think it just fine).


For the implicaton from mutability to identity, I'm not sure whether 
talking about mutation still makes sense without some kind of identity. 
For example, you need to establish that the object after the mutation is 
still the same in some sense, and this the same concept is exactly 
identity.

  I agree that mutability
 plus identity implies aliasing problems, however.

Then we're agreeing about the most important point anyway.

 In other words, pointers are essentially just an *aspect* of mutability
 in lower-level languages.
 
 Again, I disagree: it is posible to have mutability without
 pointers/identity/objects.

I'm sceptical.
Any examples?

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 Joachim Durchholz wrote:
 Marshall schrieb:
 Now, I'm not fully up to speed on DBC. The contract specifications,
 these are specified statically, but checked dynamically, is that
 right?
 That's how it's done in Eiffel, yes.

   In other words, we can consider contracts in light of
 inheritance, but the actual verification and checking happens
 at runtime, yes?
 Sure. Though, while DbC gives rules for inheritance (actually subtypes),
 these are irrelevant to the current discussion; DbC-minus-subtyping can
 still be usefully applied.
 
 Yes, subtyping. Of course I meant to say subtyping.blush

No need to blush for that, it's perfectly OK in the Eiffel context, 
where a subclass ist always assumed to be a subtype. (This assumption 
isn't always true, which is why Eiffel has some serious holes in the 
type system. The DbC ideas are still useful though, saying subtype 
instead of subclass just makes the concept applicable outside of OO 
languages.)

 I can certainly see how DbC would be useful without subtyping.
 But would there still be a reason to separate preconditions
 from postconditions? I've never been clear on the point
 of differentiating them (beyond the fact that one's covariant
 and the other is contravariant.)

There is indeed.
The rules about covariance and contravariance are just consequences of 
the notion of having a subtype (albeit important ones when it comes to 
designing concrete interfaces).

For example, if a precondition fails, something is wrong about the 
things that the subroutine assumes about its environment, so it 
shouldn't have been called. This means the error is in the caller, not 
in the subroutine that carries the precondition.

The less important consequence is that this should be reflected in the 
error messages.

The more important consequences apply when integrating software.
If you have a well-tested library, it makes sense to switch off 
postcondition checking for the library routines, but not their 
precondition checking.
This applies not just for run-time checking: Ideally, with compile-time 
inference, all postconditions can be inferred from the function's 
preconditions and their code. The results of that inference can easily 
be stored in the precompiled libraries.
Preconditions, on the other hand, can only be verified by checking all 
places where the functions are called.

 Wouldn't it be possible to do them at compile time? (Although
 this raises decidability issues.)
 Exactly, and that's why you'd either uses a restricted assertion
 language (and essentially get something that's somewhere between a type
 system and traditional assertion); or you'd use some inference system
 and try to help it along (not a simple thing either - the components of
 such a system exist, but I'm not aware of any system that was designed
 for the average programmer).
 
 As to the average programmer, I heard this recently on
 comp.databases.theory:
 
 Don't blame me for the fact that competent programming, as I view it
 as an intellectual possibility, will be too difficult for the
 average programmer  -you must not fall into the trap of rejecting
 a surgical technique because it is beyond the capabilities of the
 barber in his shop around the corner.   -- EWD512

Given the fact that we have far more need for competently-written 
programs than for competent surgery, I don't think that we'll be able to 
follow that idea.

 Mightn't it also be possible to
 leave it up to the programmer whether a given contract
 was compile-time or runtime?
 I'd agree with that, but I'm not sure how well that would hold up in
 practice.
 
 I want to try it and see what it's like.

So do I :-)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Darren New schrieb:
 As far as I understand it, Eiffel compilers don't even make use of 
 postconditions to optimize code or eliminate run-time checks (like null 
 pointer testing).

That's correct.

I think a large part of the reasons why this isn't done is that Eiffel's 
semantics is (a) too complicated (it's an imperative language after 
all), and (b) not formalized, which makes it difficult to assess what 
optimizations are safe and what aren't.

(Reason (c) is that Eiffel compiler vendors don't have the manpower for 
this kind of work, mostly in quantity but also, to some degree, in 
quality: people with a solid language semantics background tend to be 
repelled by the language inventor's know-it-all deny-the-problems 
don't-bother-me-with-formalisms attitude. He still has moved the state 
of the art ahead - mostly by pointing out a certain class of problems in 
OO designs and explaining them lucidly, and proposing solutions that 
hold up better than average even if still fundamentally flawed.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 I can see the lack of a formal model being an issue, but is the
 imperative bit really all that much of an obstacle? How hard
 is it really to deal with assignment? Or does the issue have
 more to do with pointers, aliasing, etc.?

Actually aliasing is *the* hard issue.
Just one data point: C compiler designers spend substantial effort to 
determine which data structures cannot have aliasing to be able to apply 
optimizations.

This can bite even with runtime assertion checking.
For example, ordinarily one would think that if there's only a fixed set 
of routines that may modify some data structure A, checking the 
invariants of that structure need only be done at the exit of these 
routines.
Now assume that A has a reference to structure B, and that the 
invariants involve B in some way. (E.g. A.count = A-B.count.)
There's still no problem with that - until you have a routine that 
exports a reference to B, which gets accessed from elsewhere, say via C.
Now if I do
   C-B.count = 27
I will most likely break A's invariant. If that assignment is in some 
code that's far away from the code for A, debugging can become 
exceedingly hard: the inconsistency (i.e. A violating its invariant) can 
live for the entire runtime of the program.

So that innocent optimization don't check all the program's invariants 
after every assignment immediately breaks with assignment (unless you 
do some aliasing analysis).

In an OO language, it's even more difficult to establish that some data 
structure cannot be aliased: even if the code for A doesn't hand out a 
reference to B, there's no guarantee that some subclass of A doesn't. 
I.e. the aliasing analysis has to be repeated whenever there's a new 
subclass, which may happen at link time when you'd ordinarily don't want 
to do any serious semantic analysis anymore.

There's another way around getting destroyed invariants reported at the 
time the breakage occurs: lock any data field that goes into an 
invariant (or a postcondition, too). The rationale behind this is that 
from the perspective of assertions, an alias walks, smells and quacks 
just like concurrent access, so locking would be the appropriate answer. 
The problem here is that this means that updates can induce *very* 
expensive machinery - imagine an invariant that says A-balance is the 
sum of all the transaction-amount fields in the transaction list of A, 
it would cause all these -amount fields to be locked as soon as a 
transaction list is hooked up with the amount. OTOH one could argue that 
such a locking simply makes cost in terms of debugging time visible as 
runtime overhead, which isn't entirely a Bad Thing.


There are all other kinds of things that break in the presence of 
aliasing; this is just the one that I happen to know best :-)

Without mutation, such breakage cannot occur. Invariants are just the 
common postconditions of all the routines that may construct a structure 
of a given type.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 So, what exactly separates a precondition from a postcondition
 from an invariant? I have always imagined that one writes
 assertions on parameters and return values, and those
 assertions that only reference parameters were preconditions
 and those which also referenced return values were postconditions.
 Wouldn't that be easy enough to determine automatically?

Sure.
Actually this can be done in an even simpler fashion; e.g. in Eiffel, it 
is (forgive me if I got the details wrong, it's been several years since 
I last coded in it):

   foo (params): result_type is
   require
 -- list of assertions; these become preconditions
   do
 -- subroutine body
   ensure
 -- list of assertions; these become postconditions
   end

 And what's an invariant anyway?

In general, it's a postcondition to all routines that create or modify a 
data structure of a given type.

Eiffel does an additional check at routine entry, but that's just a 
last-ditch line of defense against invariant destruction via aliases, 
not a conceptual thing. Keep aliases under control via modes (i.e. 
unaliasable marks on local data to prevent aliases from leaving the 
scope of the data structure), or via locking, or simply by disallowing 
destructive updates, and you don't need the checks at routine entry anymore.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Marshall schrieb:
 Joachim Durchholz wrote:
 Marshall schrieb:
 I can see the lack of a formal model being an issue, but is the
 imperative bit really all that much of an obstacle? How hard
 is it really to deal with assignment? Or does the issue have
 more to do with pointers, aliasing, etc.?
 Actually aliasing is *the* hard issue.
 
 Okay, sure. Nice explanation.
 
 But one minor point: you describe this as an issue with imperative
 languages. But aliasing is a problem associated with pointers,
 not with assignment.

Aliasing is not a problem if the aliased data is immutable.

  One can have assignment, or other forms
 of destructive update, without pointers; they are not part of the
 definition of imperative.

Sure.
You can have either of destructive updates and pointers without 
incurring aliasing problems. As soon as they are combined, there's trouble.

Functional programming languages often drop assignment entirely. (This 
is less inefficient than one would think. If everything is immutable, 
you can freely share data structures and avoid some copying, and you can 
share across abstraction barriers. In programs with mutable values, 
programmers are forced to choose the lesser evil of either copying 
entire data structures or doing a cross-abstraction analysis of who 
updates what elements of what data structure. 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.)

Some functional languages restrict assignment so that there can exist at 
most a single reference to any mutable data structure. That way, there's 
still no aliasing problems, but you can still update in place where it's 
really, really necessary.

I know of no professional language that doesn't have references of some 
kind.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

Darren New schrieb:
 There are also problems with the complexity of things. Imagine a 
 chess-playing game trying to describe the generate moves routine. 
 Precondition: An input board with a valid configuration of chess pieces. 
 Postcondition: An array of boards with possible next moves for the 
 selected team.  Heck, if you could write those as assertions, you 
 wouldn't need the code.

Actually, in a functional programming language (FPL), you write just the 
postconditions and let the compiler generate the code for you.

At least that's what happens for those FPL functions that you write down 
without much thinking. You can still tweak the function to make it more 
efficient. Or you can define an interface using preconditions and 
postconditions, and write a function that fulfills these assertions 
(i.e. requires no more preconditions than the interface specifies, and 
fulfills at least the postcondition that the interface specifies); here 
we'd have a postcondition that's separate from the code, too.
I.e. in such cases, the postconditions separate the accidental and 
essential properties of a function, so they still have a role to play.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

2006-07-11 Thread Joachim Durchholz

Marshall schrieb:
 Now, I'm not fully up to speed on DBC. The contract specifications,
 these are specified statically, but checked dynamically, is that
 right?

That's how it's done in Eiffel, yes.

  In other words, we can consider contracts in light of
 inheritance, but the actual verification and checking happens
 at runtime, yes?

Sure. Though, while DbC gives rules for inheritance (actually subtypes), 
these are irrelevant to the current discussion; DbC-minus-subtyping can 
still be usefully applied.

 Wouldn't it be possible to do them at compile time? (Although
 this raises decidability issues.)

Exactly, and that's why you'd either uses a restricted assertion 
language (and essentially get something that's somewhere between a type 
system and traditional assertion); or you'd use some inference system 
and try to help it along (not a simple thing either - the components of 
such a system exist, but I'm not aware of any system that was designed 
for the average programmer).

  Mightn't it also be possible to
 leave it up to the programmer whether a given contract
 was compile-time or runtime?

I'd agree with that, but I'm not sure how well that would hold up in 
practice.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

2006-07-10 Thread Joachim Durchholz

Chris Smith schrieb:
 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.  To work around that, we'd need to
 make one of a few choices: [...] (c) invent some kind of generic
 constraint language so that constraints like this could be expressed
 without exposing field names. [...] Choice (c), though, looks a
 little daunting.

That's not too difficult.
Start with boolean expressions.
If you need to check everything statically, add enough constraints that 
they become decidable.
For the type language, you also need to add primitives for type 
checking, and if the language is stateful, you'll also want primitives 
for accessing earlier states (most notably at function entry).

 So I'll stop there.  The point is that while it is emphatically true 
 that this kind of stuff is possible, it is also very hard in Java.

No surprise: It's always very hard to retrofit an inference system to a 
language that wasn't designed for it.

This doesn't mean it can't be done. Adding genericity to Java was a 
pretty amazing feat.
(But I won't hold my breath for a constraint-style type system in Java 
anyway... *gg*)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

2006-07-10 Thread Joachim Durchholz

Chris Smith schrieb:
 I think 
 there's something fundamentally important about information hiding that 
 can't be given up.

Indeed.
Without information hiding, with N entities, you have O(N^2) possible 
interactions between them. This quickly outgrows the human capacity for 
managing the interactions.
With information hiding, you can set up a layered approach, and the 
interactions are usually down to something between O(log N) and O(N log 
N). Now that's far more manageable.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is a type error?

2006-07-10 Thread Joachim Durchholz

Marshall schrieb:
 Joachim Durchholz wrote:
 Chris Smith schrieb:
 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.  To work around that, we'd need to
 make one of a few choices: [...] (c) invent some kind of generic
 constraint language so that constraints like this could be expressed
 without exposing field names. [...] Choice (c), though, looks a
 little daunting.
 That's not too difficult.
 Start with boolean expressions.
 If you need to check everything statically, add enough constraints that
 they become decidable.
 
 I'm not sure I understand. Could you elaborate?

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.

 For the type language, you also need to add primitives for type
 checking, and if the language is stateful, you'll also want primitives
 for accessing earlier states (most notably at function entry).
 
 Again I'm not entirely clear what this means. Are you talking
 about pre/post conditions,

Yes.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: languages with full unicode support

2006-07-04 Thread Joachim Durchholz

Oliver Bandel schrieb:
 Matthias Blume wrote:
 
 Tin Gherdanarra [EMAIL PROTECTED] writes:


 Oliver Bandel wrote:

 こんいちわ Xah-Lee san ;-)

 Uhm, I'd guess that Xah is Chinese. Be careful
 with such things in real life; Koreans might
 beat you up for this. Stay alive!


 And the Japanese might beat him up, too.  For butchering their
 language. :-)
 
 OK, back to ISO-8859-1 :)  no one needs so much symbols,
 this is enough: äöüÄÖÜß :)

If you want äöüÄÖÜß, anybody else will want their local characters, too, 
and nothing below full Unicode will work.

Just for laughs, here's a list of non-ASCII Latin-based letters in 
Unicode (not verified for completeness):
   ÀÁÂÃÄÅÆàáâãäåæĀāĂăĄąǺǻǼǽ
   ÇçĆćĈĉĊċČč
   ĎďĐđ
   ÈÉÊËèéêëĒēĔĕĖėĘęĚě
   ĜĝĞğĠġĢģ
   ĤĥĦħ
   ÌÍÎÏìíîïĨĩĪīĬĭĮįİıĲĳ
   Ĵĵ
   Ķķĸ
   ĹĺĻļĽĿŀŁł
   Ðð
   ÑñŃńŅņŇňŉŊŋ
   ÒÓÔÕØòóôöõŌōŎŏÖŐőŒœǾǿ
   ŔŕŖŗŘř
   ŚśŜŝŞşŠšß
   ŢţŤťŦŧ
   ÜÙÚÛüùúûŨũŪūŭŮůŰűŲų
   Ŵŵ
   ÝýÿŶŷŸ
   Þþ
   ŹźŻżŽž
   ƒſ
ISO 8859-1 covers just a fraction of these, so Unicode would indeed be 
necessary to allow a program written in one country to compile in 
another one.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-07-04 Thread Joachim Durchholz

Andreas Rossberg schrieb:
 AFAICT, ADT describes a type whose values can only be accessed by a 
 certain fixed set of operations. Classes qualify for that, as long as 
 they provide proper encapsulation.

The first sentence is true if you associate a semantics (i.e. axioms) 
with the operations. Most OO languages don't have a place for expressing 
axioms (except via comments and handwaving), so they still don't fully 
qualify.

Regards,
jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-07-01 Thread Joachim Durchholz

Matthias Blume schrieb:
 Erlang relies on a combination of purity, concurrency, and message
 passing, where messages can carry higher-order values.
 
 Data structures are immutable, and each computational agent is a
 thread.  Most threads consist a loop that explicitly passes state
 around.  It dispatches on some input event, applies a state
 transformer (which is a pure function), produces some output event (if
 necessary), and goes back to the beginning of the loop (by
 tail-calling itself) with the new state.

Actually any Erlang process, when seen from the outside, is impure: it 
has observable state.
However, from what I hear, such state is kept to a minimum. I.e. the 
state involved is just the state that's mandated by the purpose of the 
process, not by computational bookkeeping - you won't send file 
descriptors in a message, but maybe information about the state of some 
hardware, or about a permanent log.

So to me, the approach of Erlang seems to amount to make pure 
programming so easy and efficient that aren't tempted to introduce state 
that isn't already there.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: languages with full unicode support

2006-07-01 Thread Joachim Durchholz

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.

I'd expect two kinds of changes in character categorization: additions 
and corrections. (Any other?)

Additions are relatively unproblematic. Existing code will remain valid 
and retain its semantics. The new characters will be available for new 
programs.
There's a slight technological complication: the compiler needs to be 
able to look up the newest definition. In other words, for a compiler to 
run, it needs to be able to access http://unicode.org, or the language 
infrastructure needs a way to carry around various revisions of the 
Unicode tables and select the newest one.

Corrections are technically more problematic, but then we can rely on 
the common sense of the programmers. If the Unicode consortium 
miscategorized a character as a letter, the programmers that use that 
character set will probably know it well enough to avoid its use. It 
will probably not even occur to them that that character could be a 
letter ;-)


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.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-28 Thread Joachim Durchholz

Paul Rubin schrieb:
 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.

That's where type inference comes into play. Usually you don't write the 
types, the compiler infers them for you, so you don't get them wrong.

Occasionally, you still write down the types, if only for documentation 
purposes (the general advice is: do the type annotations for external 
interfaces, but not internally).

BTW if you get a type wrong, you'll be told by the compiler, so this is 
still less evil than bugs in the code that pop up during testing (and 
*far* less evil than bugs that pop up after roll-out).
And the general consensus among FPL programmers is that you get the hang 
of it fairly quickly (one poster mentioned two to three months - this 
doesn't seem to be slower than learning to interpret synax error 
messages, so it's OK considering it's an entirely new kind of diagnostics).

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: languages with full unicode support

2006-06-28 Thread Joachim Durchholz

Tim Roberts schrieb:
 Xah Lee [EMAIL PROTECTED] wrote:
 C ? No.
 
 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.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-26 Thread Joachim Durchholz

Andrew McDonagh schrieb:
 Joachim Durchholz wrote:
 Chris Smith schrieb:
 Joachim Durchholz [EMAIL PROTECTED] wrote:
 Sorry, I have to insist that it's not me who's stretching terms here.

 All textbook definitions that I have seen define a type as the 
 set/operations/axioms triple I mentioned above.
 No mention of immutability, at least not in the definitions.

 The immutability comes from the fact (perhaps implicit in these 
 textbooks, or perhaps they are not really texts on formal type 
 theory) that types are assigned to expressions,

 That doesn't *define* what's a type or what isn't!

 If it's impossible to assign types to all expressions of a program in 
 a language, that does mean that there's no useful type theory for the 
 program, but it most definitely does not mean that there are no types 
 in the program.
 I can still sensibly talk about sets of values, sets of allowable 
 operations over each value, and about relationships between inputs and 
 outputs of these operations.

 So programs have types, even if they don't have a static type system.
 Q.E.D.
 
 Of course not.  Otherwise programs using dynamically  typed systems 
 wouldnt exist.

I don't understand.
Do you mean dynamic typing (aka runtime types)?

 I haven't read all of this thread, I wonder, is the problem to do with 
 Class being mistaken for Type? (which is usually the issue)

No, not at all. I have seen quite a lot beyond OO ;-)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-26 Thread Joachim Durchholz

Darren New schrieb:
 Marshall wrote:
 Also: has subtyping polymorphism or not, has parametric polymorphism or
 not.
 
 And covariant or contravariant.

That's actually not a design choice - if you wish to have a sound type 
system, all input parameters *must* be contravariant, all output 
parameters *must* be covariant, and all in/out parameters must be 
novariant. (Eiffel got this one wrong in almost all cases.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-26 Thread Joachim Durchholz

Anton van Straaten schrieb:
 Joachim Durchholz wrote:
  Anton van Straaten schrieb:
 There's a close connection between latent types in the sense I've 
 described, and the tagged values present at runtime.  However, as 
 type theorists will tell you, the tags used to tag values at runtime, 
 as e.g. a number or a string or a FooBar object, are not the same 
 thing as the sort of types which statically-typed languages have.

 Would that be a profound difference, or is it just that annotating a 
 value with a full type expression would cause just too much runtime 
 overhead?
 
 It's a profound difference.  The issue is that it's not just the values 
 that need to be annotated with types, it's also other program terms.

Yes - but isn't that essentially just auxiliary data from and for the 
data-flow analysis that tracks what values with what types might reach 
which functions?

  In
 addition, during a single run of a program, all it can ever normally do 
 is record the types seen on the path followed during that run, which 
 doesn't get you to static types of terms.  To figure out the static 
 types, you really need to do static analysis.

Agreed.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

George Neuner schrieb:
 The point is really that the checks that prevent these things must be
 performed at runtime and can't be prevented by any practical type
 analysis performed at compile time.  I'm not a type theorist but my
 opinion is that a static type system that could, a priori, prevent the
 problem is impossible.

No type theory is needed.
Assume that the wide index type goes into a function and the result is 
assigned to a variable fo the narrow type, and it's instantly clear that 
the problem is undecidable.
Undecidability can always be avoided by adding annotations, but of 
course that would be gross overkill in the case of index type widening.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Dimitri Maziuk schrieb:
 That is the basic argument in favour of compile time error checking,
 extended to runtime errors. I don't really care if it's the compiler
 or runtime that tells the luser your code is broken, as long as it
 makes it clear it's *his* code that's broken, not mine.

You can make runtime errors point to the appropriate code. Just apply 
programming by contract: explicitly state what preconditions a 
function is requiring of the caller, have it check the preconditions on 
entry (and, ideally, throw the execption in a way that the error is 
reported in the caller's code - not a complicated thing but would 
require changes in the exception machinery of most languages).

Any errors past that point are either a too liberal precondition (i.e. a 
bug in the precondition - but documenting wrong preconditions is still a 
massive bug, even if it's just a documentation bug), or a bug in the 
function's code.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

[EMAIL PROTECTED] schrieb:
 Joachim Durchholz wrote:
   A type is the encoding of these properties. A type
 varying over time is an inherent contradiction (or another abuse of the
 term type).
 No. It's just a matter of definition, essentially.
 E.g. in Smalltalk and Lisp, it does make sense to talk of the type of
 a name or a value, even if that type may change over time.
 
 OK, now we are simply back full circle to Chris Smith's original
 complaint that started this whole subthread, namely (roughly) that
 long-established terms like type or typing should *not* be
 stretched in ways like this, because that is technically inaccurate and
 prone to misinterpretation.

Sorry, I have to insist that it's not me who's stretching terms here.

All textbook definitions that I have seen define a type as the 
set/operations/axioms triple I mentioned above.
No mention of immutability, at least not in the definitions.

Plus, I don't see any necessity on insisting on immutability for the 
definition of type. Otherwise, you'd have to declare that Smalltalk 
objects truly don't have a type (not even an implied one), and that 
would simply make no sense: they do in fact have a type, even though it 
may occasionally change.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Chris F Clark schrieb:
 Chris F Clark schrieb:
 In that sense, a static type system is eliminating tags, because the
 information is pre-computed and not explicitly stored as a part of the
 computation.  Now, you may not view the tag as being there, but in my
 mind if there exists a way of perfoming the computation that requires
 tags, the tag was there and that tag has been eliminated.
 
 Joachim Durchholz replied:
 On a semantic level, the tag is always there - it's the type (and
 definitely part of an axiomatic definition of the language).
 Tag elimination is just an optimization.
 
 I agree the tag is always there in the abstract.  

Well - in the context of a discussion of dynamic and static typing, I'd 
think that the semantic (abstract) level is usually the best level of 
discourse.
Of course, this being the Usenet, shifting the level is common (and can 
even helpful).

 In the end, I'm trying to fit things which are too big and too
 slow into much less space and time, using types to help me reliably
 make my program smaller and faster is just one trick.  [...]
 
 However, I also know that my way of thinking about it is fringe.

Oh, I really agree that's an important application of static typing.

Essentially, which aspects of static typing is more important depends on 
where your problems lie: if it's ressource constraints, static typing 
tends to be seen as a tool to keep ressource usage down; if it's bug 
counts, static typing tends to be seen as a tool to express static 
properties.
These aspects are obviously not equally important to everybody.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Darren New schrieb:
 John W. Kennedy wrote:
 360-family assembler, yes. 8086-family assembler, not so much.
 
 And Burroughs B-series, not at all. There was one ADD instruction, and 
 it looked at the data in the addresses to determine whether to add ints 
 or floats. :-)

I heard that the Telefunken TR series had a tagged architecture.
This seems roughly equivalent to what the B-series did (does?).

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Anton van Straaten schrieb:
 Marshall wrote:
 Can you be more explicit about what latent types means?
 
 Sorry, that was a huge omission.  (What I get for posting at 3:30am.)
 
 The short answer is that I'm most directly referring to the types in 
 the programmer's head.

Ah, finally that terminology starts to make sense to me. I have been 
wondering whether there's any useful difference between latent and 
run-time typing. (I tend to avoid the term dynamic typing because 
it's overloaded with too many vague ideas.)

 there are usually many possible static 
 type schemes that can be assigned to a given program.

This seems to apply to latent types as well.

Actually the set of latent types seems to be the set of possible static 
type schemes.
Um, well, a superset of these - static type schemes tend to be slightly 
less expressive than what the programmer in his head. (Most type schemes 
cannot really express things like the range of this index variable is 
such-and-so, and the boundary to general assertions about the code is 
quite blurry anyway.)

 There's a close connection between latent types in the sense I've 
 described, and the tagged values present at runtime.  However, as type 
 theorists will tell you, the tags used to tag values at runtime, as e.g. 
 a number or a string or a FooBar object, are not the same thing as the 
 sort of types which statically-typed languages have.

Would that be a profound difference, or is it just that annotating a 
value with a full type expression would cause just too much runtime 
overhead?

In your terminology:

 So, where do tagged values fit into this?  Tags help to check types at 
 runtime, but that doesn't mean that there's a 1:1 correspondence between 
 tags and types.

Would it be possible to establish such a correspondence, would it be 
common consensus that such a system should be called tags anymore, or 
are there other, even more profound differences?

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Marshall schrieb:
 It seems we have languages:
 with or without static analysis
 with or without runtime type information (RTTI or tags)
 with or without (runtime) safety
 with or without explicit type annotations
 with or without type inference
 
 Wow. And I don't think that's a complete list, either.
 
 I would be happy to abandon strong/weak as terminology
 because I can't pin those terms down. (It's not clear what
 they would add anyway.)

Indeed.

 Programmers infer and reason about these latent types while they're
 writing or reading programs.  Latent types become manifest when a
 programmer reasons about them, or documents them e.g. in comments.
 
 Uh, oh, a new term, manifest. Should I worry about that?

I think that was OED usage of the term.

 Well, darn. It strikes me that that's just a decision the language
 designers
 made, *not* to record complete RTTI. (Is it going to be claimed that
 there is an *advantage* to having only incomplete RTTI? It is a
 serious question.)

In most cases, it's probably we don't have to invent or look up 
efficient algorithms that we can't think of right now.
One could consider this a sorry excuse or a wise decision to stick with 
available resources, both views have their merits IMHO ;-)

 But function is not a useful type.  Why not?  Because if all you know
 is that timestwo is a function, then you have no idea what an expression
 like timestwo(foo) means.  You couldn't write working programs, or
 read them, if all you knew about functions was that they were functions.
   As a type, function is incomplete.
 
 Yes, function is a parameterized type, and they've left out the
 parameter values.

Well, in JavaScript, the explicit type system as laid down in the 
run-time type information is unparameterized.
You can criticize this as unsound, or inadequate, or whatever you wish, 
and I'd like agree with that ;-), but the type of timestwo is indeed 
just function.

*Your mental model* is far more detailed, of course.

 Question: if a language *does* record complete RTTI, and the
 languages does *not* have subtyping, could we then say that
 the runtime type information *is* the same as the static type?

Only if the two actually use the same type system.

In practice, I'd say that this is what most designers intend but what 
implementors may not have gotten right ;-p

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Anton van Straaten schrieb:
 It seems we have languages:
 with or without static analysis
 with or without runtime type information (RTTI or tags)
 with or without (runtime) safety
 with or without explicit type annotations
 with or without type inference

 Wow. And I don't think that's a complete list, either.
 
 Yup.

What else?
(Genuinely curious.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

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)  |
-+--+-+
not  | (no common   | untyped   |
typesafe | terminology) | |
 | (C)  | (Assembly)  |
-+--+-+

(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, 
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.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Chris Smith schrieb:
 Joachim Durchholz [EMAIL PROTECTED] wrote:
 Sorry, I have to insist that it's not me who's stretching terms here.

 All textbook definitions that I have seen define a type as the 
 set/operations/axioms triple I mentioned above.
 No mention of immutability, at least not in the definitions.
 
 The immutability comes from the fact (perhaps implicit in these 
 textbooks, or perhaps they are not really texts on formal type theory) 
 that types are assigned to expressions,

That doesn't *define* what's a type or what isn't!

If it's impossible to assign types to all expressions of a program in a 
language, that does mean that there's no useful type theory for the 
program, but it most definitely does not mean that there are no types in 
the program.
I can still sensibly talk about sets of values, sets of allowable 
operations over each value, and about relationships between inputs and 
outputs of these operations.

So programs have types, even if they don't have a static type system.
Q.E.D.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

[EMAIL PROTECTED] schrieb:
 Joachim Durchholz write:
 Another observation: type safeness is more of a spectrum than a clearcut
 distinction. Even ML and Pascal have ways to circumvent the type system,
 
 No. I'm not sure about Pascal,

You'd have to use an untagged union type.
It's the standard maneuver in Pascal to get unchecked bitwise 
reinterpretation.
Since it's an undefined behavior, you're essentially on your own, but in 
practice, any compilers that implemented a different semantics were 
hammered with bug reports until they complied with the standard - in 
this case, an unwritten (and very unofficial) one, but a rather 
effective one.

  but (Standard) ML surely has none.

NLFFI?

  Same with Haskell as defined by its spec.

Um... I'm not 100% sure, but I dimly (mis?)remember having read that 
UnsafePerformIO also offered some ways to circumvent the type system.

(Not that this would be an important point anyway.)

  OCaml has a couple of clearly
 marked unsafe library functions, but no unsafe feature in the language
 semantics itself.

If there's a library with not-typesafe semantics, then at least that 
language implementation is not 100% typesafe.
If all implementations of a language are not 100% typesafe, then I 
cannot consider the language itself 100% typesafe.

Still, even Pascal is quite a lot more typesafe than, say, C.

 and even C is typesafe unless you use unsafe constructs.
 
 Tautology. Every language is safe unless you use unsafe constructs.

No tautology - the unsafe constructs aren't just typewise unsafe ;-p

That's exactly why I replaced Luca Cardelli's safe/unsafe 
typesafe/not typesafe. There was no definition to the original terms 
attached, and this discussion is about typing anyway.

 (Unfortunately, you can hardly write interesting programs in any safe
 subset of C.)

Now that's a bold claim that I'd like to see substantiated.

 IOW from a type-theoretic point of view, there is no real difference
 between their typesafe and not typesafe languages in the statically
 typed column; the difference is in the amount of unsafe construct usage
 in practial programs.
 
 Huh? There is a huge, fundamental difference:  namely whether a type
 system is sound or not.

I think you're overstating the case.

In type theory, of course, there's no such things as an almost typesafe 
language - it's typesafe or it isn't.

In practice, I find no implementation where type mismatches cannot 
occur, if only when interfacing with the external world (except if you 
cheat by treating everything external as a byte sequence, which is like 
saying that all languages have at least a universal ANY type and are 
hence statically-typed).
And in those languages that do have type holes, these holes may be more 
or less relevant - and it's a *very* broad spectrum here.
And from that perspective, if ML indeed has no type hole at all, then 
it's certainly an interesting extremal point, but I still have a 
relevant spectrum down to assembly language.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

[EMAIL PROTECTED] schrieb:
 Gabriel Dos Reis wrote:
 |
 | (Unfortunately, you can hardly write interesting programs in any safe
 | subset of C.)

 Fortunately, some people do, as living job.
 
 I don't think so. Maybe the question is what a safe subset consists
 of. In my book, it excludes all features that are potentially unsafe.

Unless you define safe, *any* program is unsafe.
Somebody could read the program listing, which could trigger a traumatic 
childhood experiece.
(Yes, I'm being silly. But the point is very serious. Even with less 
silly examples, whether a language or subset is safe entirely depends 
on what you define to be safe, and these definitions tend to vary 
vastly across language communities.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Pascal Costanza schrieb:
 Another observation: type safeness is more of a spectrum than a 
 clearcut distinction. Even ML and Pascal have ways to circumvent the 
 type system, 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's also relevant how straightforward it is to distinguish between safe 
 and unsafe code, how explicit you have to be when you use unsafe code, 
 how likely it is that you accidentally use unsafe code without being 
 aware of it, what the generally accepted conventions in a language 
 community are, etc. pp.

Fully agreed.
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-22 Thread Joachim Durchholz

Marshall schrieb:
 immutable = can't change
 vary-able = can change
 
 Clearly a contradiction in terms.

Not in mathematics.
The understanding there is that a variable varies - not over time, but 
according to the whim of the usage. (E.g. if a function is displayed in 
a graph, the parameter varies along the X axis. If it's used within a 
term, the parameter varies depending on how it's used. Etc.)

Similarly for computer programs.
Of course, if values are immutable, the value associated with a 
parameter name cannot vary within the same invocation - but it can still 
vary from one invocation to the next.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-22 Thread Joachim Durchholz

Andreas Rossberg schrieb:
 Joachim Durchholz wrote:

 It's worth noting, too, that (in some sense) the type of an object 
 can change over time[*].

 No. Since a type expresses invariants, this is precisely what may 
 *not* happen.

 No. A type is a set of allowable values, allowable operations, and 
 constraints on the operations (which are often called invariants but 
 they are invariant only as long as the type is invariant).
 
 The purpose of a type system is to derive properties that are known to 
 hold in advance.

That's just one of many possible purposes (a noble one, and the most 
preeminent one in FPLs I'll agree any day, but it's still *not the 
definition of a type*).

  A type is the encoding of these properties. A type
 varying over time is an inherent contradiction (or another abuse of the 
 term type).

No. It's just a matter of definition, essentially.
E.g. in Smalltalk and Lisp, it does make sense to talk of the type of 
a name or a value, even if that type may change over time.
I regard it as a highly dubious practice to have things change their 
types over their lifetime, but if there are enough other constraints, 
type constancy may indeed have to take a back seat.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-22 Thread Joachim Durchholz

Andreas Rossberg schrieb:
 (Btw, Pascal did not have it either, AFAIK)

Indeed.
Some Pascal dialects have it.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Andreas Rossberg schrieb:
 Rob Thorpe wrote:
 Hmm.  You're right, ML is no-where in my definition since it has no
 variables.
 
 Um, it has. Mind you, it has no /mutable/ variables, but that was not 
 even what I was talking about.

Indeed. A (possibly nonexhaustive) list of program entities that (can) 
have type would comprise of mutable variables, immutable variables (i.e. 
constants and parameter names), and functions resp. their results.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Matthias Blume schrieb:
 Joachim Durchholz [EMAIL PROTECTED] writes:
 
 Matthias Blume schrieb:
 Perhaps better: A language is statically typed if its definition
 includes (or ever better: is based on) a static type system, i.e., a
 static semantics with typing judgments derivable by typing rules.
 Usually typing judgmets associate program phrases (expressions) with
 types given a typing environment.
 This is defining a single term (statically typed) using three
 undefined terms (typing judgements, typing rules, typing
 environment).
 
 This was not meant to be a rigorous definition.

Rigorous or not, introducing additional undefined terms doesn't help 
with explaining a term.

 Also, I'm not going to repeat the textbook definitions for those
 three standard terms here.

These terms certainly aren't standard for Perl, Python, Java, or Lisp, 
and they aren't even standard for topics covered on comp.lang.functional 
(which includes dynamically-typed languages after all).

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Pascal Costanza schrieb:
 (It's really important to understand that the idea is to use this for 
 deployed programs - albeit hopefully in a more structured fashion - and 
 not only for debugging. The example I have given is an extreme one that 
 you would probably not use as such in a real-world setting, but it 
 shows that there is a boundary beyond which static type systems cannot 
 be used in a meaningful way anymore, at least as far as I can tell.)

As soon as the running program can be updated, the distinction between 
static (compile time) and dynamic (run time) blurs.
You can still erect a definition for such a case, but it needs to refer 
to the update process, and hence becomes language-specific. In other 
words, language-independent definitions of dynamic and static typing 
won't give any meaningful results for such languages.

I'd say it makes more sense to talk about what advantages of static vs. 
dynamic typing can be applied in such a situation.
E.g. one interesting topic would be the change in trade-offs: making 
sure that a type error cannot occur becomes much more difficult 
(particularly if the set of available types can change during an 
update), so static typing starts to lose some of its appeal; OTOH a good 
type system can give you a lot of guarantees even in such a situation, 
even if it might have to revert to the occasional run-time type check, 
so static checking still has its merits.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Chris Uppal schrieb:
 Chris Smith wrote:
 I think Marshall got this one right.  The two are accomplishing
 different things.  In one case (the dynamic case) I am safeguarding
 against negative consequences of the program behaving in certain non-
 sensical ways.  In the other (the static case) I am proving theorems
 about the impossibility of this non-sensical behavior ever happening.
 
 And so conflating the two notions of type (-checking) as a kind of category
 error ?  If so then I see what you mean, and it's a useful distinction, but am
 unconvinced that it's /so/ helpful a perspective that I would want to exclude
 other perspectives which /do/ see the two as more-or-less trivial variants on
 the same underlying idea.

It is indeed helpful.
Just think of all the unit tests that you don't have to write.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Matthias Blume schrieb:
 Joachim Durchholz [EMAIL PROTECTED] writes:
 
 Matthias Blume schrieb:
 Joachim Durchholz [EMAIL PROTECTED] writes:

 Matthias Blume schrieb:
 Perhaps better: A language is statically typed if its definition
 includes (or ever better: is based on) a static type system, i.e., a
 static semantics with typing judgments derivable by typing rules.
 Usually typing judgmets associate program phrases (expressions) with
 types given a typing environment.
 This is defining a single term (statically typed) using three
 undefined terms (typing judgements, typing rules, typing
 environment).
 This was not meant to be a rigorous definition.
 Rigorous or not, introducing additional undefined terms doesn't help
 with explaining a term.
 
 I think you missed my point.  My point was that a language is
 statically typed IF IT IS DEFINED THAT WAY, i.e., if it has a static
 type system that is PART OF THE LANGUAGE DEFINITION.  The details are
 up to each individual definition.

Well, that certainly makes more sense to me.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Pascal Costanza schrieb:
 Static type systems potentially change the semantics of a 
 language in ways that cannot be captured by dynamically typed languages 
 anymore, and vice versa.

Very true.

I also suspect that's also why adding type inference to a 
dynamically-typed language doesn't give you all the benefits of static 
typing: the added-on type system is (usually) too weak to express really 
interesting guarantees, usually because the language's semantics isn't 
tailored towards making the inference steps easy enough.

Conversely, I suspect that adding dynamic typing to statically-typed 
languages tends to miss the most interesting applications, mostly 
because all the features that can simply be done in a 
dynamically-typed language have to be retrofitted to the 
statically-typed language on a case-by-case basis.

In both cases, the language designers often don't know the facilities of 
the opposed camp well enough to really assess the trade-offs they are doing.

 There is, of course, room for research on performing static type checks 
 in a running system, for example immediately after or before a software 
 update is applied, or maybe even on separate type checking on software 
 increments such that guarantees for their composition can be derived. 
 However, I am not aware of a lot of work in that area, maybe because the 
 static typing community is too focused on compile-time issues.

I think it's mostly because it's intimidating.

The core semantics of an ideal language fits on a single sheet of paper, 
to facilitate proofs of language properties. Type checking 
dynamically-loaded code probably wouldn't fit on that sheet of paper.
(The non-core semantics is then usually a set of transformation rules 
that map the constructs that the programmer sees to constructs of the 
core language.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-20 Thread Joachim Durchholz

Torben Ægidius Mogensen schrieb:
 That's not really the difference between static and dynamic typing.
 Static typing means that there exist a typing at compile-time that
 guarantess against run-time type violations.  Dynamic typing means
 that such violations are detected at run-time. 

Agreed.

  This is orthogonal to
 strong versus weak typing, which is about whether such violations are
 detected at all.  The archetypal weakly typed language is machine code
 -- you can happily load a floating point value from memory, add it to
 a string pointer and jump to the resulting value.

I'd rather call machine code untyped.
(Strong typing and weak typing don't have a universally accepted 
definition anyway, and I'm not sure that this terminology is helpful 
anyway.)

 Anyway, type inference for statically typed langauges don't make them
 any more dynamically typed.  It just moves the burden of assigning the
 types from the programmer to the compiler.  And (for HM type systems)
 the compiler doesn't guess at a type -- it finds the unique most
 general type from which all other legal types (within the type system)
 can be found by instantiation.

Hmm... I think this distinction doesn't cover all cases.

Assume a language that
a) defines that a program is type-correct iff HM inference establishes 
that there are no type errors
b) compiles a type-incorrect program anyway, with an establishes 
rigorous semantics for such programs (e.g. by throwing exceptions as 
appropriate).
The compiler might actually refuse to compile type-incorrect programs, 
depending on compiler flags and/or declarations in the code.

Typed (strongly typed) it is, but is it statically typed or 
dynamically typed?
(Softly typed doesn't capture it well enough - if it's declarations in 
the code, then those part of the code are statically typed.)

 You miss some of the other benefits of static typing,
 though, such as a richer type system -- soft typing often lacks
 features like polymorphism (it will find a set of monomorphic
 instances rather than the most general type) and type classes.

That's not a property of soft typing per se, it's a consequence of 
tacking on type inference on a dynamically-typed language that wasn't 
designed for allowing strong type guarantees.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-20 Thread Joachim Durchholz

Matthias Blume schrieb:
 Perhaps better: A language is statically typed if its definition
 includes (or ever better: is based on) a static type system, i.e., a
 static semantics with typing judgments derivable by typing rules.
 Usually typing judgmets associate program phrases (expressions) with
 types given a typing environment.

This is defining a single term (statically typed) using three 
undefined terms (typing judgements, typing rules, typing environment).

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-20 Thread Joachim Durchholz

Chris F Clark schrieb:
 In that sense, a static type system is eliminating tags, because the
 information is pre-computed and not explicitly stored as a part of the
 computation.  Now, you may not view the tag as being there, but in my
 mind if there exists a way of perfoming the computation that requires
 tags, the tag was there and that tag has been eliminated.

On a semantic level, the tag is always there - it's the type (and 
definitely part of an axiomatic definition of the language).
Tag elimination is just an optimization.

 To put it another way, I consider the tags to be axiomatic.  Most
 computations involve some decision logic that is driven by distinct
 values that have previously been computed.  The separation of the
 values which drive the compuation one-way versus another is a tag.
 That tag can potentially be eliminated by some apriori computation.

Um... just as precomputing constants, I'd say.
Are the constants that went into a precomputed constant eliminated?
On the implementation level, yes. On the semantic/axiomatic level, no.
Or, well, maybe - since that's just an optimization, the compiler may 
have decided to no precompute the constant at all.

(Agreeing with the snipped parts.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

2006-06-17 Thread Joachim Durchholz

Raffael Cavallaro schrieb:
 On 2006-06-16 17:59:07 -0400, Joachim Durchholz [EMAIL PROTECTED] said:
 
 I think it's easier to start with a good (!) statically-typed language 
 and relax the checking, than to start with a dynamically-typed one and 
 add static checks.

 This is purely a matter of programming style. For explorative
 programming it is easier to start with dynamic typing and add static
 guarantees later rather than having to make decisions about
 representation and have stubs for everything right from the start.

Sorry for being ambiguous - I meant to talk about language evolution.

I agree that static checking could (and probably should) be slightly 
relaxed: compilers should still do all the diagnostics that current-day 
technology allows, but any problems shouldn't abort the compilation. 
It's always possible to generate code that will throw an exception as 
soon as a problematic piece of code becomes actually relevant; depending 
on the kind of run-time support, this might abort the program, abort 
just the computation, or open an interactive facility to correct and/or 
modify the program on the spot (the latter is the norm in highly dynamic 
systems like those for Lisp and Smalltalk, and I consider this actually 
useful).

I don't see static checking and explorative programming as opposites.
Of course, in practice, environments that combine these don't seem to 
exist (except maybe in experimental or little-known state).

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Raffael Cavallaro schrieb:
 On 2006-06-14 15:04:34 -0400, Joachim Durchholz [EMAIL PROTECTED] said:
 
 Um... heterogenous lists are not necessarily a sign of expressiveness. 
 The vast majority of cases can be transformed to homogenous lists 
 (though these might then contain closures or OO objects).

 As to references to nonexistent functions - heck, I never missed 
 these, not even in languages without type inference :-)

 [[snipped - doesn't seem to relate to your answer]]
 
 This is a typical static type advocate's response when told that users 
 of dynamically typed languages don't want their hands tied by a type 
 checking compiler:
 
 *I* don't find those features expressive so *you* shouldn't want them.

And this is a typical dynamic type advocate's response when told that 
static typing has different needs:

*I* don't see the usefulness of static typing so *you* shouldn't want 
it, either.

No ad hominem arguments, please. If you find my position undefendable, 
give counterexamples.
Give a heterogenous list that would to too awkward to live in a 
statically-typed language.
Give a case of calling nonexistent functions that's useful.
You'll get your point across far better that way.

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Sacha schrieb:
 
 Many lists are heterogenous, even in statically typed languages.
 For instance lisp code are lists, with several kinds of atoms and 
 sub-lists..

Lisp isn't exactly a statically-typed language :-)

 A car dealer will sell cars, trucks and equipment..
 In a statically typed language you would need to type the list on a common 
 ancestor...

Where's the problem with that?

BTW the OO way isn't the only way to set up a list from heterogenous data.
In statically-typed FPL land, lists require homogenous data types all 
right, but the list elements aren't restricted to data - they can be 
functions as well.
Now the other specialty of FPLs is that you can construct functions at 
run-time - you take a function, fill some of its parameters and leave 
others open - the result is another function. And since you'll iterate 
over the list and will do homogenous processing over it, you construct 
the function so that it will do all the processing that you'll later need.

The advantage of the FPL way over the OO way is that you can use ad-hoc 
functions. You don't need precognition to know which kinds of data 
should be lumped under a common supertype - you simply write and/or 
construct functions of a common type that will go into the list.

 What would then be the point of statical typing , as you stilll need to type 
 check each element in order to process that list ?

Both OO and FPL construction allow static type checks.

  Sure you can do this in a
 statically-typed
 language, you just need to make sure some relevant ancestor exists. In my 
 experience
 you'll end up with the base object-class more often than not, and that's 
 what i call dynamic typing.

Not quite - the common supertype is more often than not actually useful.

However, getting the type hierarchy right requires a *lot* of 
experimentation and fine-tuning. You can easily spend a year or more 
(sometimes *much* more) with that (been there, done that). Even worse, 
once the better hierarchy is available, you typically have to adapt all 
the client code that uses it (been there, done that, too).

That's the problems in OO land. FPL land doesn't have these problems - 
if the list type is just a function mapping two integers to another 
integer, reworking the data types that went into the functions of the 
list don't require those global changes.

 Give a case of calling nonexistent functions that's useful.
 
 I might want to test some other parts of my program before writing this 
 function.

That's unrelated to dynamic typing. All that's needed is an environment 
that throws an exception once such an undefined function is called, 
instead of aborting the compilation.

I'll readily admit that very few static languages offer such an 
environment. (Though, actually, C interpreters do exist.)

 Or maybe will my program compile that function depending on user input.

Hmm... do I really want this kind of power at the user's hand in the age 
of malware?

 As long as i get a warning for calling a non-existing function, everything 
 is fine.

That depends.
For software that's written to run once (or very few times), and where 
somebody who's able to correct problems is always nearby, that's a 
perfectly viable strategy.
For safety-critical software where problems must be handled within 
seconds (or an even shorter period of time), you want to statically 
ensure as many properties as you can. You'll take not just static 
typing, you also want to ascertain value ranges and dozens of other 
properties. (In Spark, an Ada subset, this is indeed done.)

Between those extremes, there's a broad spectrum.
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language

Raffael Cavallaro schrieb:
 There is a very large class of software where user inputs are 
 unpredictable and/or where input data comes from an untrusted source. In 
 these cases run-time checks are going to be needed anyway so the 
 advantages of static type checking are greatly reduced - you end up 
 doing run-time checks anyway, precisely the thing you were trying to 
 avoid by doing static analysis.

There's still a large class of errors that *can* be excluded via type 
checking.

 Ideally one wants a language with switchable typing - static where 
 possible and necessary, dynamic elsewhere.

That has been my position for a long time now.

  To a certain extent this is
 what common lisp does but it requires programmer declarations. Some 
 implementations try to move beyond this by doing type inference and 
 alerting the programmer to potential static guarantees that the 
 programmer could make that would allow the compiler to do a better job.

I think it's easier to start with a good (!) statically-typed language 
and relax the checking, than to start with a dynamically-typed one and 
add static checks.
With the right restrictions, a language can make all kinds of strong 
guarantees, and it can make it easy to construct software where static 
guarantees abound. If the mechanisms are cleverly chosen, they interfere 
just minimally with the programming process. (A classical example it 
Hindley-Milner type inference systems. Typical reports from languages 
with HM systems say that you can have it verify thousand-line programs 
without a single type annotation in the code. That's actually far better 
than you'd need - you'd *want* to document the types at least on the 
major internal interfaces after all *grin*.)
With a dynamically-typed language, programming style tends to evolve in 
directions that make it harder to give static guarantees.

 It seems to 
 me that if we set aside that class of software where safety is paramount 
 - mostly embedded software such as aircraft and medical devices - we are 
 left mostly with efficiency concerns.

Nope. Efficiency has taken a back seat. Software is getting slower 
(barely offset by increasing machine speed), and newer languages even 
don't statically typecheck everything (C++, Java). (Note that the 
impossibility to statically typecheck everything in OO languages doesn't 
mean that it's impossible to do rigorous static checking in general. 
FPLs have been quite rigorous about static checks; the only cases when 
an FPL needs to dynamically typecheck its data structures is after 
unmarshalling one from an untyped data source such as a network stream, 
a file, or an IPC interface.)

The prime factor nowadays seems to be maintainability.

And the difference here is this:
With dynamic typing, I have to rely on the discipline of the programmers 
to document interfaces.
With static typing, the compiler will infer (and possibly document) at 
least part of their semantics (namely the types).

 So static typing should be invoked for that small portion of a program 
 where efficiency is really needed and that dynamic typing should be the 
 default elswhere. This is how common lisp works - dynamic typing by 
 default with static guarantees available where one needs them.

Actually static typing seems to become more powerful at finding errors 
as the program size increases.
(Yes, that's a maintainability argument. Efficiency isn't *that* 
important; since maintenance is usually the most important single 
factor, squelching bugs even before testing is definitely helpful.)

Regards,
Jo
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language