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 nec
Darren New wrote:
> David Hopwood wrote:
>
>> public class LoopInitTest {
>> public static String getString() { return "foo"; }
>>
>> public static void main(String[] args) {
>> String line = getString();
>> bo
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 com
zed
v = v + 1;
^
but for a different and more trivial reason than the Hermes algorithm.
Change "if (b) { v = 1; }" to just "v = 1;", and the Java version will be
accepted by its definite assignment analysis (which is a dataflow analysis),
but the equi
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 h
to prove that, treated as
postconditions, the former implies the latter.
(In this case a single deterministic result is required, so the former
will be equivalent to the latter.)
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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.
ich it is
made immutable.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
s (and perhaps even allow them to regress slightly in
order to simplify them) without changing programs.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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
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),
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 a
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
#x27;c' field.
>
> Just expressing all of that in a method signature looks interesting
> enough. If we start adding abstraction to the type constraints on
> objects to support encapsulation (as I think you'd have to do), then
> things get even more interesting.
1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
t; Person{age:{18..29}}
>
> But this starts to look bad, because we used to have this nice property
> called encapsulation.
I think you're assuming that 'age' would have to refer to a concrete field.
If it refers to a type parameter, something like:
class Person{ag
ode is
> more a way of lowering entry barriers.
Unicode in identifiers has certainly been less important than some thought
it would be -- and not at all important for open source projects, for example,
which essentially have to use English to get the widest possible participation.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
at runtime (and I'm
> talking about real type-checking, not just tag checking).
>
> When such a programmer writes a type signature as a comment associated
> with a function definition, in many cases he's making a claim that's
> provable in principle about the inputs a
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 funct
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 static
he inclusion of U+ and various control characters in the set of valid
identifier characters is also a dubious decision, IMHO.
Note that I am not defending in any way the complexity of this definition;
there's
clearly no excuse for it (or for the "ignorable" documentation bug). The
language
spec should have been defined directly in terms of the Unicode General
Categories,
and then the API in terms of the language spec. They way it is done now is
completely backwards.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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 st
extended characters, an encoding
# of the universal character name may be used in forming valid external
# identifiers. For example, some otherwise unused character or sequence of
# characters may be used to encode the \u in a universal character name.
# Extended characters may p
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
>>
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 poly
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?
>>
>&g
y at runtime, however,
although it was intended to allow static analysis for types that could be
expressed in a conventional static type system. I think the delay in
implementing this has more to do with the E developers' focus on other
(security and concurrency) issues, rather than an inherent difficulty.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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 *nev
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 lang
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 t
n expressiveness" of the
language is reduced.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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&#x
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
afe language (compatible with Standard C89
or C99), you first have to resolve all the ambiguities in the standard where
the behaviour is *implicitly* undefined. There are a lot of them.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
heory.
>
> So you claim Java and Objective C are "simply bugs in the theory."
Java's type system was unsound for much of its life. I think that supports
the point that it's inadequate to simply "wish and hope" for soundness,
and that a proof should be
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 te
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 sa
same as with unsound
formal systems; they still satisfy the definition of a formal system.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
ternal libraries,
and assuming that file I/O cannot be used to corrupt the language
implementation).
> and even C is typesafe unless you use unsafe constructs.
> IOW from a type-theoretic point of view, there is no real difference
> between their typesafe and not typesafe languages in
t;
> Anyway, it's a thought.
I don't buy this -- or at least, I am not in either group.
A good debugger is invaluable regardless of your attitude to type
systems. Recently I was debugging two programs written to do similar
things in the same statically typed language (C), but where a
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 ent
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
g
> language, so it is reasonable to talk about this as a property of some
> dynamically typed languages.
If anything, I think that this example supports my and Vesa's point.
The example demonstrates that languages
*that are not distinguished in whether they are called latently typed*
support informal reasoning about types to varying degrees.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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
rove
automatically that the quicksort terminates. The programmer would probably
just have to give hints in some cases as to which parameters are to be
treated as variants; the rest can be inferred.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
t has to be expressed as a comment, and is not checked, means that
the *language* is not typed (even though Scheme is dynamically tagged,
and even though dynamic tagging provides *partial* support for a
programming style that uses this kind of informal annotation).
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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 fo
of course you can't in *C*; you can barely zip you pants with C.
>>But I believe you can do the above in C++, can't you?
>
> You can write self-modifying code in C, so I don't see how you can not
> do that in C. ;)
Strictly speaking, you can't write self-modifying
o information about the type the variable
> stores. The programmer cannot write code to test it, and so can't
> write functions that issue errors if given arguments of the wrong type.
So the hypothetical language, unlike Python, Perl and Lisp, is not
dynamically *tagged*.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
for
> it. You're on your own.
I can accept that dynamic tagging provides some support for latent typing
performed "in the programmer's head". But that still does not mean that
dynamic tagging is the same thing as latent typing, or that languages
that use dynamic tagging are "latently typed". This simply is not a
property of the language (as you've already conceded).
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
e not part of the Scheme language. If you combine Scheme
with a type inferencer, you get a new language that is not R*RS Scheme,
and *that* language is typed.
Note that different inferencers will give different type assignments.
They may be similar, but they may also be quite dissimilar in some cases.
This casts considerable doubt on the assertion that the inferencer is
"recovering types latent in the source".
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
number of parameters; applying
> a non-function; accessing an array with out-of-bound indexes; etc.
This makes essentially all run-time errors (including assertion failures,
etc.) "type errors". It is neither consistent with, nor any improvement
on, the existing vaguely defined usage.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
ted-for bug in Sun's tracking system.
I get the impression that most of the commentators don't understand how
horribly complicated it would be to fix. Anyway, it hasn't been fixed for
4 years.]
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
fresh" values that did not exist before (otherwise the abstract type
> would be equivalent to some already existent type). So you'd need at
> least a theory for name generation or something similar to describe
> abstract types in a types-as-sets metaphor.
Set theory has no
k
> box" everytime you define a new function? Will you recompile all the
> "black box" functions to take into account the new type the arguments
> can be now?
Yes, why not?
> This wouldn't be too efficient.
It's rare, so it doesn't need to be efficient.
d point of
> view by a compiled program that would be mostly bit-for-bit the same
> with or without this new type?
It usually wouldn't be -- adding methods in a typical statically typed
OO language is unlikely to cause type errors (unless there is a naming
conflict, in some cases). Nor would adding new types or new functions.
(*Using* new methods without declaring them would cause an error, yes.)
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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
something like, say, Alice ML, which is
statically typed, but has a "dynamic" type and type inference? I mean
this as a serious question.
> At the very least, requiring types vs. not requiring
> types is mutually exclusive.
Right, but it's pretty well established th
ic to their
> subjects of interest.
As far as I can tell, the people who advocate using "typed" and "untyped"
in this way are people who just want to be able to discuss all languages in
a unified terminological framework, and many of them are specifically not
advocates of statically typed languages.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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'
lues.
[*] introduced by Leibniz, according to <http://members.aol.com/jeff570/v.html>,
but that was presumably in Latin. The first use of "variable" as a noun
recorded by the OED in written English is in 1816.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
f any implemented language that
does it currently, but in principle it's quite feasible.
For a type system that can handle dynamic proxying, see
<http://www.doc.ic.ac.uk/~scd/FOOL11/FCM.pdf>.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
of an expression will belong to a set of values smaller than that
allowed by the expression's type in that language's type system. For
example, all constants have a known value, but most constants have a
type which allows more than one value.
(This is an essential point, not just nitpicking.)
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
because of the difference in type
systems.)
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
autogenerated if the class definition has changed only in minor ways.
- typecheck the new program and the conversion functions, using the old
type definitions for the argument of each conversion function, and the
new type definitions for its result.
- have the debugger apply the conversions to all values, and then resume
the program.
[*] or nearest equivalent in a non-OO language.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
make sense in a statically typed
> setting, the term "dynamically typed language" is good enough to
> communicate what we are talking about - i.e. not (static) typing.
Oh, but it *does* make sense to talk about dynamic tagging in a statically
typed language.
That's part of what ma
n of type systems can be dispelled by insistence on this point
(although
much of the benefit can be obtained just by using this terminology in your own
mind and translating what other people are saying to it). It's a good example of
the weak Sapir-Whorf hypothesis, I think.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
27;t read Alex's point as
being that simplicity was the only criterion on which to make decisions
about what practices a language should enforce or facilitate; just
"a good criterion".
However, IMHO anonymous lambdas do not significantly increase the complexity
of the language or of programs, and they can definitely simplify programs in
functional languages, or languages that use them for control constructs.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
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
69 matches
Mail list logo
