Darren New wrote:
David Hopwood wrote:
[...]
Apparently, Hermes (at least the version of it described in that paper)
essentially forgets that is_last has been initialized at the top of the
loop, and so when it does the merge, it is merging 'not necessarily
initialized' with 'initialized
trivial reason than the Hermes algorithm.
Change if (b) { v = 1; } to just v = 1;, and the Java version will be
accepted by its definite assignment analysis (which is a dataflow analysis),
but the equivalent Hermes program still would not.
--
David Hopwood [EMAIL PROTECTED]
--
http
David Hopwood wrote:
Darren New wrote:
From what I can determine, the authors seem to imply that typestate is
dataflow analysis modified in (at least) two ways:
1) When control flow joins, the new typestate is the intersection of
typestates coming into the join, where as dataflow analysis
Darren New wrote:
David Hopwood wrote:
public class LoopInitTest {
public static String getString() { return foo; }
public static void main(String[] args) {
String line = getString();
boolean is_last = false;
while (!is_last
it is
made immutable.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
Wouldn't it be possible to do them at compile time? (Although
this raises decidability issues.)
It is certainly possible to prove statically that some assertions cannot fail.
The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2
will be equivalent to the latter.)
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Chris Smith wrote:
David Hopwood [EMAIL PROTECTED] wrote:
This is true, but note that postconditions also need to be efficient
if we are going to execute them.
If checked by execution, yes. In which case, I am trying to get my head
around how it's any more true to say that functional
is, after all, not something that the program should depend on.
It is determined by how good the static checker currently is, and we want to be
able to improve checkers (and perhaps even allow them to regress slightly in
order to simplify them) without changing programs.
--
David Hopwood [EMAIL
Chris Smith wrote:
David Hopwood [EMAIL PROTECTED] wrote:
Maybe I'm not understanding what you mean by complete. Of course any
type system of this expressive power will be incomplete (whether or not
it can express conditions 3 to 5), in the sense that it cannot prove all
true assertions about
George Neuner wrote:
On Tue, 11 Jul 2006 14:59:46 GMT, David Hopwood
[EMAIL PROTECTED] wrote:
What matters is that, over the range
of typical programs written in the language, the value of the increased
confidence in program correctness outweighs the effort involved in both
adding annotations
' would have to refer to a concrete field.
If it refers to a type parameter, something like:
class Person{age:Age} is
Age getAge()
end
then I don't see how this breaks encapsulation.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
have to do), then
things get even more interesting.
1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Chris Smith wrote:
David Hopwood [EMAIL PROTECTED] wrote:
1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.
One of us is missing the other's meaning here. If 3 to 5 were expressed
as assertions rather than types, then the type system would become
Jürgen Exner wrote:
David Hopwood wrote:
[...]
There is no such error message listed in 'perldoc perldiag'.
Please quote the actual text of your error message and include the program
that produced this error.
Then people here in CLPM may be able to assist you.
Yes, I'm well aware
to use English to get the widest possible participation.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
. For example, some otherwise unused character or sequence of
# characters may be used to encode the \u in a universal character name.
# Extended characters may produce a long external identifier.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Paul Rubin wrote:
David Hopwood [EMAIL PROTECTED] writes:
Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where
of the Unicode General
Categories,
and then the API in terms of the language spec. They way it is done now is
completely backwards.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Pascal Costanza wrote:
David Hopwood wrote:
Pascal Costanza wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has
Andreas Rossberg wrote:
David Hopwood wrote:
(In the case of eval, OTOH,
the erroneous code may cause visible side effects before any run-time
error occurs.)
Not necessarily. You can replace the primitive eval by compile, which
delivers a function encapsulating the program, so you can
.
In a statically typed, Turing-complete language that does not have a
dynamic type, it is always *possible* to express a dynamically typed
program, but this may require a global transformation of the program
or use of an interpreter -- i.e. the Felleisen expressiveness of the
language is reduced.
--
David
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed programs
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
David Hopwood wrote:
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed
it was intended to allow static analysis for types that could be
expressed in a conventional static type system. I think the delay in
implementing this has more to do with the E developers' focus on other
(security and concurrency) issues, rather than an inherent difficulty.
--
David Hopwood [EMAIL
Pascal Costanza wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed programs
David Hopwood wrote:
Joe Marshall wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
forall a . a - #'blackhole
Joe Marshall wrote:
David Hopwood wrote:
Joe Marshall wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
forall
the behaviour is *implicitly* undefined. There are a lot of them.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Dirk Thierbach wrote:
David Hopwood [EMAIL PROTECTED] wrote:
Marshall wrote:
David Hopwood wrote:
A type system that required an annotation on all subprograms that
do not provably terminate, OTOH, would not impact expressiveness
at all, and would be very useful.
Interesting. I have always
Pascal Costanza wrote:
David Hopwood wrote:
Pascal Costanza wrote:
Chris Smith wrote:
While this effort to salvage the term type error in dynamic
languages is interesting, I fear it will fail. Either we'll all have
to admit that type in the dynamic sense is a psychological concept
in practial programs.
It is quite possible to design languages that have absolutely no unsafe
constructs, and are still useful.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
of the perfect type system.
I'm particularly interested if something unsound (and perhaps
ambiguous) could be called a type system.
Yes, but not a useful one. The situation is the same as with unsound
formal systems; they still satisfy the definition of a formal system.
--
David Hopwood
David Hopwood wrote:
Chris F Clark wrote:
I'm particularly interested if something unsound (and perhaps
ambiguous) could be called a type system.
Yes, but not a useful one. The situation is the same as with unsound
formal systems; they still satisfy the definition of a formal system.
I
Matthias Blume wrote:
David Hopwood [EMAIL PROTECTED] writes:
Patricia Shanahan wrote:
Vesa Karvonen wrote:
...
An example of a form of informal reasoning that (practically) every
programmer does daily is termination analysis. [...]
Given a program, it may be possible to formally
prove
and Objective C are simply bugs in the theory.
Java's type system was unsound for much of its life. I think that supports
the point that it's inadequate to simply wish and hope for soundness,
and that a proof should be insisted on.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman
typing, or that languages
that use dynamic tagging are latently typed. This simply is not a
property of the language (as you've already conceded).
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
*tagged*.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
.
But I believe you can do the above in C++, can't you?
You can write self-modifying code in C, so I don't see how you can not
do that in C. ;)
Strictly speaking, you can't write self-modifying code in Standard C.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python
Chris Uppal wrote:
David Hopwood wrote:
But some of the advocates of statically
typed languages wish to lump these languages together with assembly
language a untyped in an attempt to label them as unsafe.
A common term for languages which have defined behaviour at run-time is
memory safe
* is not typed (even though Scheme is dynamically tagged,
and even though dynamic tagging provides *partial* support for a
programming style that uses this kind of informal annotation).
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
as to which parameters are to be
treated as variants; the rest can be inferred.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Marshall wrote:
David Hopwood wrote:
A type system that required an annotation on all subprograms that do not
provably terminate, OTOH, would not impact expressiveness at all, and would
be very useful.
Interesting. I have always imagined doing this by allowing an
annotation on all
latently typed*
support informal reasoning about types to varying degrees.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Anton van Straaten wrote:
David Hopwood wrote:
I can accept that dynamic tagging provides some support for latent typing
performed in the programmer's head. But that still does not mean that
dynamic tagging is the same thing as latent typing
No, I'm not saying it is, although I am saying
David Hopwood wrote:
Anton van Straaten wrote:
I'm suggesting that if a language classifies and tags values in a way
that supports the programmer in static reasoning about the behavior of
terms, that calling it untyped does not capture the entire picture,
even if it's technically accurate
could not be used for one of the programs. It took maybe 5 times
longer to find and fix each bug without the debugger, and I found it
a much more frustrating experience.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
be classed as an RFE) is, inexplicably given how few
programs are affected by it, the most voted-for bug in Sun's tracking system.
I get the impression that most of the commentators don't understand how
horribly complicated it would be to fix. Anyway, it hasn't been fixed for
4 years.]
--
David
-time errors (including assertion failures,
etc.) type errors. It is neither consistent with, nor any improvement
on, the existing vaguely defined usage.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
considerable doubt on the assertion that the inferencer is
recovering types latent in the source.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Rob Thorpe wrote:
David Hopwood wrote:
As far as I can tell, the people who advocate using typed and untyped
in this way are people who just want to be able to discuss all languages in
a unified terminological framework, and many of them are specifically not
advocates of statically typed
them would cause an error, yes.)
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
to take into account the new type the arguments
can be now?
Yes, why not?
This wouldn't be too efficient.
It's rare, so it doesn't need to be efficient. 'eval' is inherently
inefficient, anyway.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
or something similar to describe
abstract types in a types-as-sets metaphor.
Set theory has no difficulty with this. It's common, for example, to see
the set of strings representing propositions used in treatments of
formal systems.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org
have a
type which allows more than one value.
(This is an essential point, not just nitpicking.)
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
.
For a type system that can handle dynamic proxying, see
http://www.doc.ic.ac.uk/~scd/FOOL11/FCM.pdf.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
in Latin. The first use of variable as a noun
recorded by the OED in written English is in 1816.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Chris Uppal wrote:
David Hopwood wrote:
When people talk about types being associated with values in a latently
typed
or dynamically typed language, they really mean *tag*, not type.
I don't think that's true. Maybe /some/ people do confuse the two, but I am
certainly a counter-example
to their
subjects of interest.
As far as I can tell, the people who advocate using typed and untyped
in this way are people who just want to be able to discuss all languages in
a unified terminological framework, and many of them are specifically not
advocates of statically typed languages.
--
David
.
At the very least, requiring types vs. not requiring
types is mutually exclusive.
Right, but it's pretty well established that languages that don't
require type *declarations* can still be statically typed.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
and translating what other people are saying to it). It's a good example of
the weak Sapir-Whorf hypothesis, I think.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
.
That's part of what makes the term dynamically typed harmful: it implies
a dichotomy between dynamically typed and statically typed languages,
when in fact dynamic tagging and static typing are (mostly) independent
features.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman
and the conversion functions, using the old
type definitions for the argument of each conversion function, and the
new type definitions for its result.
- have the debugger apply the conversions to all values, and then resume
the program.
[*] or nearest equivalent in a non-OO language.
--
David
.)
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
of the language or of programs, and they can definitely simplify programs in
functional languages, or languages that use them for control constructs.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Ken Tilton wrote:
[...] The upshot of what [Guido] wrote is that it would be really hard to make
semantically meaningful indentation work with lambda.
Haskell manages it.
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Xah Lee wrote:
PS if you know any new lambda logo, please let me know. Thanks.
^
Oops, no, that would be an old lambda logo...
--
David Hopwood [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
68 matches
Mail list logo
