669  25292 
David Hopwood wrote: Joe Marshall wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
"forall a . a -> #'blackhole".
Ignore this answer; I misinterpreted the code.
I believe this example requires recursive types. It can also be expressed
in a gradual typing system, but possibly only using an unknown ('?') type.
ISTR that O'Caml at one point (before version 1.06) supported general
recursive types, although I don't know whether it would have supported
this particular example.
--
David Hopwood <da******************@blueyonder.co.uk>
Joe Marshall wrote: David Hopwood wrote:Joe Marshall wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
"forall a . a -> #'blackhole".
The #' is just a namespace operator. The function accepts a single
argument and returns the function itself. You need a type that is a
fixed point (in addition to the universally quantified argument).
Yes, see the correction in my follow-up.
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
Certainly! As soon as you can reflect on the type system you can
construct programs that type-check iff they fail to type-check.
A program that causes the type checker not to terminate (which is the
effect of trying to construct such a thing in the type-reflective systems
I know about) is hardly useful.
In any case, I think the question implied the condition: "and that you
can write in a language with no static type checking."
Presumably the remainder of the program does something interesting!
The point is that there exists (by construction) programs that can
never be statically checked.
I don't think you've shown that. I would like to see a more explicit
construction of a dynamically typed[*] program with a given specification,
where it is not possible to write a statically typed program that meets
the same specification using the same algorithms.
AFAIK, it is *always* possible to construct such a statically typed
program in a type system that supports typerec or gradual typing. The
informal construction you give above doesn't contradict that, because
it depends on reflecting on a [static] type system, and in a dynamically
typed program there is no type system to reflect on.
[*] Let's put aside disagreements about terminology for the time being,
although I still don't like the term "dynamically typed".
The next question is whether such
programs are `interesting'. Certainly a program that is simply
designed to contradict the type checker is of limited entertainment
value,
I don't know, it would probably have more entertainment value than most
executive toys :-)
but there should be programs that are independently non
checkable against a sufficiently powerful type system.
Why?
Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where possible and dynamic checks where necessary.
--
David Hopwood <da******************@blueyonder.co.uk>
David Hopwood <da******************@blueyonder.co.uk> writes: Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where possible and dynamic checks where necessary.
It starts to look like sufficiently powerful static type systems are
confusing enough, that programming with them is at least as bug-prone
as imperative programming in dynamically typed languages. The static
type checker can spot type mismatches at compile time, but the
types themselves are easier and easier to get wrong.
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
David Hopwood wrote: (defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
I believe this example requires recursive types. It can also be expressed
in a gradual typing system, but possibly only using an unknown ('?') type.
ISTR that O'Caml at one point (before version 1.06) supported general
recursive types, although I don't know whether it would have supported
this particular example.
No problem at all. It still is possible today if you really want:
~/> ocaml -rectypes
Objective Caml version 3.08.3
# let rec blackhole x = blackhole;;
val blackhole : 'b -> 'a as 'a = <fun>
The problem is, though, that almost everything can be typed once you
have unrestricted recursive types (e.g. missing arguments etc), and
consequently many actual errors remain unflagged (which clearly shows
that typing is not only about potential value class mismatches).
Moreover, there are very few practical uses of such a feature, and they
can always be coded easily with recursive datatypes.
It is a pragmatic decision born from experience that you simply do *not
want* to have this, even though you easily could. E.g. for OCaml,
unrestricted recursive typing was removed as default because of frequent
user complaints.
Which is why this actually is a very bad example to chose for dynamic
typing advocacy... ;-)
- Andreas
Paul Rubin wrote: David Hopwood <da******************@blueyonder.co.uk> writes:
Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where possible and dynamic checks where necessary.
It starts to look like sufficiently powerful static type systems are
confusing enough, that programming with them is at least as bug-prone
as imperative programming in dynamically typed languages. The static
type checker can spot type mismatches at compile time, but the
types themselves are easier and easier to get wrong.
My assertion above does not depend on having a "sufficiently powerful static
type system" to express a given dynamically typed program. It is true for
static type systems that are not particularly complicated, and suffice to
express all dynamically typed programs.
I disagree with your implication that in general, static type systems for
practical languages are getting too confusing, but that's a separate issue.
(Obviously one can find type systems in research proposals that are too
confusing as they stand.)
--
David Hopwood <da******************@blueyonder.co.uk>
David Hopwood wrote: Pascal Costanza wrote: David Hopwood wrote: Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a "dynamic" type, all
dynamically typed programs are straightforwardly expressible. What about programs where the types change at runtime?
Staged compilation is perfectly compatible with static typing.
Static typing only requires that it be possible to prove absence
of some category of type errors when the types are known; it
does not require that all types are known before the first-stage
program is run.
Can you change the types of the program that is already running, or are
the levels strictly separated?
There are, however, staged compilation systems that guarantee that
the generated program will be typeable if the first-stage program
is.
....and I guess that this reduces again the kinds of things you can express.
(It's clear that to compare the expressiveness of statically and
dynamically typed languages, the languages must be comparable in
other respects than their type system. Staged compilation is the
equivalent feature to 'eval'.)
If it is equivalent to eval (i.e., executed at runtime), and the static
type checker that is part of eval yields a type error, then you still
get a type error at runtime!
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006 http://lisp-ecoop06.bknr.net/
Pascal Costanza wrote: David Hopwood wrote: Pascal Costanza wrote: David Hopwood wrote:
Marshall wrote:
> The real question is, are there some programs that we
> can't write *at all* in a statically typed language, because
> they'll *never* be typable?
In a statically typed language that has a "dynamic" type, all
dynamically typed programs are straightforwardly expressible.
What about programs where the types change at runtime?
Staged compilation is perfectly compatible with static typing.
Static typing only requires that it be possible to prove absence
of some category of type errors when the types are known; it
does not require that all types are known before the first-stage
program is run.
Can you change the types of the program that is already running, or are
the levels strictly separated?
In most staged compilation systems this is intentionally not permitted.
But this is not a type system issue. You can't change the types in a
running program because you can't change the program, period. And you
can't do that because most designers of these systems consider directly
self-modifying code to be a bad idea (I agree with them).
Note that prohibiting directly self-modifying code does not prevent a
program from specifying another program to *replace* it. There are, however, staged compilation systems that guarantee that
the generated program will be typeable if the first-stage program
is.
...and I guess that this reduces again the kinds of things you can express.
Yes. If you don't want that, use a system that does not impose this
restriction/guarantee. (It's clear that to compare the expressiveness of statically and
dynamically typed languages, the languages must be comparable in
other respects than their type system. Staged compilation is the
equivalent feature to 'eval'.)
If it is equivalent to eval (i.e., executed at runtime), and the static
type checker that is part of eval yields a type error, then you still
get a type error at runtime!
You can choose to use a system in which this is impossible because only
typeable programs can be generated, or one in which non-typeable programs
can be generated. In the latter case, type errors are detected at the
earliest possible opportunity, as soon as the program code is known and
before any of that code has been executed. (In the case of eval, OTOH,
the erroneous code may cause visible side effects before any run-time
error occurs.)
I don't know what else you could ask for.
--
David Hopwood <da******************@blueyonder.co.uk>
David Hopwood wrote: Pascal Costanza wrote: David Hopwood wrote: Pascal Costanza wrote:
David Hopwood wrote:
> Marshall wrote:
>
>> The real question is, are there some programs that we
>> can't write *at all* in a statically typed language, because
>> they'll *never* be typable?
> In a statically typed language that has a "dynamic" type, all
> dynamically typed programs are straightforwardly expressible.
What about programs where the types change at runtime?
Staged compilation is perfectly compatible with static typing.
Static typing only requires that it be possible to prove absence
of some category of type errors when the types are known; it
does not require that all types are known before the first-stage
program is run. Can you change the types of the program that is already running, or are
the levels strictly separated?
In most staged compilation systems this is intentionally not permitted.
But this is not a type system issue. You can't change the types in a
running program because you can't change the program, period. And you
can't do that because most designers of these systems consider directly
self-modifying code to be a bad idea (I agree with them).
Whether you consider something you cannot do with statically typed
languages a bad idea or not is irrelevant. You were asking for things
that you cannot do with statically typed languages.
There are at least systems that a lot of people rely on (the JVM, .NET)
that achieve runtime efficiency primarily by executing what is
essentially self-modifying code. These runtime optimization systems have
been researched primarily for the language Self, and also implemented in
Strongtalk, CLOS, etc., to various degrees.
Beyond that, I am convinced that the ability to update a running system
without the need to shut it down can be an important asset.
Note that prohibiting directly self-modifying code does not prevent a
program from specifying another program to *replace* it.
....and this creates problems with moving data from one version of a
program to the next.
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006 http://lisp-ecoop06.bknr.net/
Pascal Costanza <pc@p-cos.net> writes: Whether you consider something you cannot do with statically typed
languages a bad idea or not is irrelevant. You were asking for things
that you cannot do with statically typed languages.
The whole point of static type systems is to make sure that there are
things that one cannot do. So the fact that there are such things are
not an argument per se against static types.
[ ... ]
Beyond that, I am convinced that the ability to update a running
system without the need to shut it down can be an important asset.
And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed. Note that prohibiting directly self-modifying code does not prevent a
program from specifying another program to *replace* it.
...and this creates problems with moving data from one version of a
program to the next.
How does this "create" such a problem? The problem is there in either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the "replace the code" model
along with a "translate the data where necessary at the time of
replacement". Translating the data, i.e., re-establishing the
invariants expected by the updated/replaced code, seems much harder
(to me) in the case of self-modifying code. Erlang got this one
right.
David Hopwood wrote:
(In the case of eval, OTOH,
the erroneous code may cause visible side effects before any run-time
error occurs.)
Not necessarily. You can replace the primitive eval by compile, which
delivers a function encapsulating the program, so you can check the type
of the function before actually running it. Eval itself can easily be
expressed on top of this as a polymorphic function, which does not run
the program if it does not have the desired type:
eval ['a] s = typecase compile s of
f : (()->'a) -> f ()
_ -> raise TypeError
- Andreas
Matthias Blume wrote: Pascal Costanza <pc@p-cos.net> writes:
Whether you consider something you cannot do with statically typed
languages a bad idea or not is irrelevant. You were asking for things
that you cannot do with statically typed languages.
The whole point of static type systems is to make sure that there are
things that one cannot do. So the fact that there are such things are
not an argument per se against static types.
I am not arguing against static type systems. I am just responding to
the question what the things are that you cannot do in statically typed
languages.
[ ... ]
Beyond that, I am convinced that the ability to update a running
system without the need to shut it down can be an important asset.
And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed.
Maybe. The interesting question then is whether you can express the
kinds of dynamic updates that are relevant in practice. Because a static
type system always restricts what kinds of runtime behavior you can
express in your language. I am still skeptical, because changing the
types at runtime is basically changing the assumptions that the static
type checker has used to check the program's types in the first place.
For example, all the approaches that I have seen in statically typed
languages deal with adding to a running program (say, class fields and
methods, etc.), but not with changing to, or removing from it. Note that prohibiting directly self-modifying code does not prevent a
program from specifying another program to *replace* it.
...and this creates problems with moving data from one version of a
program to the next.
How does this "create" such a problem? The problem is there in either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the "replace the code" model
along with a "translate the data where necessary at the time of
replacement". Translating the data, i.e., re-establishing the
invariants expected by the updated/replaced code, seems much harder
(to me) in the case of self-modifying code. Erlang got this one
right.
....and the "translate the date where necessary" approach is essentially
triggered by a dynamic type test (if value x is of an old version of
type T, update it to reflect the new version of type T [1]). QED.
Pascal
[1] BTW, that's also the approach taken in CLOS.
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006 http://lisp-ecoop06.bknr.net/
Andreas Rossberg wrote: David Hopwood wrote:
(In the case of eval, OTOH,
the erroneous code may cause visible side effects before any run-time
error occurs.)
Not necessarily. You can replace the primitive eval by compile, which
delivers a function encapsulating the program, so you can check the type
of the function before actually running it. Eval itself can easily be
expressed on top of this as a polymorphic function, which does not run
the program if it does not have the desired type:
eval ['a] s = typecase compile s of
f : (()->'a) -> f ()
_ -> raise TypeError
What I meant was, in the case of eval in an untyped ("dynamically typed")
language.
The approach you've just outlined is an implementation of staged compilation
in a typed language.
--
David Hopwood <da******************@blueyonder.co.uk>
Matthias Blume wrote:
How does this "create" such a problem? The problem is there in either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the "replace the code" model
along with a "translate the data where necessary at the time of
replacement". Translating the data, i.e., re-establishing the
invariants expected by the updated/replaced code, seems much harder
(to me) in the case of self-modifying code. Erlang got this one
right.
Pardon my ignorance, but what is the Erlang solution to this problem?
Marshall
Pascal Costanza <pc@p-cos.net> writes: And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed.
Maybe. The interesting question then is whether you can express the
kinds of dynamic updates that are relevant in practice. Because a
static type system always restricts what kinds of runtime behavior you
can express in your language. I am still skeptical, because changing
the types at runtime is basically changing the assumptions that the
static type checker has used to check the program's types in the first
place.
That's why I find the Erlang model to be more promising.
I am extremely skeptical of code mutation at runtime which would
"change types", because to me types are approximations of program
invariants. So if you do a modification that changes the types, it is
rather likely that you did something that also changed the invariants,
and existing code relying on those invariants will now break.
For example, all the approaches that I have seen in statically typed
languages deal with adding to a running program (say, class fields and
methods, etc.), but not with changing to, or removing from it.
Of course, there are good reasons for that: removing fields or
changing their invariants requires that all /deployed/ code which
relied on their existence or their invariants must be made aware of
this change. This is a semantic problem which happens to reveal
itself as a typing problem. By making types dynamic, the problem does
not go away but is merely swept under the rug. Note that prohibiting directly self-modifying code does not prevent a
program from specifying another program to *replace* it.
...and this creates problems with moving data from one version of a
program to the next.
How does this "create" such a problem? The problem is there in
either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the "replace the code" model
along with a "translate the data where necessary at the time of
replacement". Translating the data, i.e., re-establishing the
invariants expected by the updated/replaced code, seems much harder
(to me) in the case of self-modifying code. Erlang got this one
right.
...and the "translate the date where necessary" approach is
essentially triggered by a dynamic type test (if value x is of an old
version of type T, update it to reflect the new version of type T
[1]). QED.
But this test would have to already exist in code that was deployed
/before/ the change! How did this code know what to test for, and how
did it know how to translate the data? Plus, how do you detect that
some piece of data is "of an old version of type T"? If v has type T
and T "changes" (whatever that might mean), how can you tell that v's
type is "the old T" rather than "the new T"! Are there two different
Ts around now? If so, how can you say that T has changed?
The bottom line is that even the concept of "changing types at
runtime" makes little sense. Until someone shows me a /careful/
formalization that actually works, I just can't take it very
seriously.
David Hopwood wrote: Joe Marshall wrote:
The point is that there exists (by construction) programs that can
never be statically checked.
I don't think you've shown that. I would like to see a more explicit
construction of a dynamically typed[*] program with a given specification,
where it is not possible to write a statically typed program that meets
the same specification using the same algorithms.
I think we're at cross-purposes here. It is trivial to create a static
type system that has a `universal type' and defers all the required
type narrowing to runtime. In effect, we've `turned off' the static
typing (because everything trivially type checks at compile time).
However, a sufficiently powerful type system must be incomplete or
inconsistent (by Godel). A type system proves theorems about a
program. If the type system is rich enough, then there are unprovable,
yet true theorems. That is, programs that are type-safe but do not
type check. A type system that could reflect on itself is easily
powerful enough to qualify.
AFAIK, it is *always* possible to construct such a statically typed
program in a type system that supports typerec or gradual typing. The
informal construction you give above doesn't contradict that, because
it depends on reflecting on a [static] type system, and in a dynamically
typed program there is no type system to reflect on.
A static type system is usually used for universal proofs: For all
runtime values of such and such... Dynamic checks usually provide
existential refutations: This particular value isn't a string. It may
be the case that there is no universal proof, yet no existential
refutation.
Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where possible and dynamic checks where necessary.
Sure. And I'm not saying that you cannot express these programs in a
static language, but rather that there exist programs that have
desirable properties (that run without error and produce the right
answer) but that the desirable properties cannot be statically checked.
The real question is how common these programs are, and what sort of
desirable properties are we trying to check.
"Marshall" <ma*************@gmail.com> writes: Matthias Blume wrote:
How does this "create" such a problem? The problem is there in either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the "replace the code" model
along with a "translate the data where necessary at the time of
replacement". Translating the data, i.e., re-establishing the
invariants expected by the updated/replaced code, seems much harder
(to me) in the case of self-modifying code. Erlang got this one
right.
Pardon my ignorance, but what is the Erlang solution to this problem?
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.
When a code update is necessary, a special event is sent to the
thread, passing along the new code to be executed. The old code, upon
receiving such an event, ceases to go back to its own loop entry point
(by simply not performing the self-tail-call). Instead it tail-calls
the new code with the current state.
If the new code can live with the same data structures that the old
code had, then it can directly proceed to perform real work. If new
invariants are to be established, it can first run a translation
function on the current state before resuming operation.
From what I hear from the Erlang folks that I have talked to, this
approach works extremely well in practice.
Matthias Blume wrote: Pascal Costanza <pc@p-cos.net> writes:
And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed. Maybe. The interesting question then is whether you can express the
kinds of dynamic updates that are relevant in practice. Because a
static type system always restricts what kinds of runtime behavior you
can express in your language. I am still skeptical, because changing
the types at runtime is basically changing the assumptions that the
static type checker has used to check the program's types in the first
place.
That's why I find the Erlang model to be more promising.
I am extremely skeptical of code mutation at runtime which would
"change types", because to me types are approximations of program
invariants. So if you do a modification that changes the types, it is
rather likely that you did something that also changed the invariants,
and existing code relying on those invariants will now break.
....no, it will throw exceptions that you can catch and handle, maybe
interactively.
For example, all the approaches that I have seen in statically typed
languages deal with adding to a running program (say, class fields and
methods, etc.), but not with changing to, or removing from it.
Of course, there are good reasons for that: removing fields or
changing their invariants requires that all /deployed/ code which
relied on their existence or their invariants must be made aware of
this change. This is a semantic problem which happens to reveal
itself as a typing problem. By making types dynamic, the problem does
not go away but is merely swept under the rug.
....and yet this requirement sometimes comes up.
> Note that prohibiting directly self-modifying code does not prevent a
> program from specifying another program to *replace* it.
...and this creates problems with moving data from one version of a
program to the next.
How does this "create" such a problem? The problem is there in
either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the "replace the code" model
along with a "translate the data where necessary at the time of
replacement". Translating the data, i.e., re-establishing the
invariants expected by the updated/replaced code, seems much harder
(to me) in the case of self-modifying code. Erlang got this one
right.
...and the "translate the date where necessary" approach is
essentially triggered by a dynamic type test (if value x is of an old
version of type T, update it to reflect the new version of type T
[1]). QED.
But this test would have to already exist in code that was deployed
/before/ the change! How did this code know what to test for, and how
did it know how to translate the data?
In CLOS, the test is indeed already there from the beginning. It's part
of the runtime semantics. The translation of the data is handled by
'update-instance-for-redefined-class, which is a generic function for
which you can define your own methods. So this is user-extensible and
can, for example, be provided as part of the program update.
Furthermore, slot accesses typically go through generic functions (aka
setters and getters in other languages) for which you can provide
methods that can perform useful behavior in case the corresponding slots
have gone. These methods can also be provided as part of the program update.
Note that I am not claiming that CLOS provides the perfect solution, but
it seems to work reasonably well that people use it in practice.
Plus, how do you detect that
some piece of data is "of an old version of type T"? If v has type T
and T "changes" (whatever that might mean), how can you tell that v's
type is "the old T" rather than "the new T"! Are there two different
Ts around now? If so, how can you say that T has changed?
Presumably, objects have references to their class metaobjects which
contain version information and references to more current versions of
themselves. This is not rocket science.
The bottom line is that even the concept of "changing types at
runtime" makes little sense. Until someone shows me a /careful/
formalization that actually works, I just can't take it very
seriously.
Maybe this feature just isn't made for you.
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006 http://lisp-ecoop06.bknr.net/
Andreas Rossberg wrote:
~/> ocaml -rectypes
Objective Caml version 3.08.3
# let rec blackhole x = blackhole;;
val blackhole : 'b -> 'a as 'a = <fun>
The problem is, though, that almost everything can be typed once you
have unrestricted recursive types (e.g. missing arguments etc), and
consequently many actual errors remain unflagged (which clearly shows
that typing is not only about potential value class mismatches).
Moreover, there are very few practical uses of such a feature, and they
can always be coded easily with recursive datatypes.
It is a pragmatic decision born from experience that you simply do *not
want* to have this, even though you easily could. E.g. for OCaml,
unrestricted recursive typing was removed as default because of frequent
user complaints.
Which is why this actually is a very bad example to chose for dynamic
typing advocacy... ;-)
Actually, this seems a *good* example. The problem seems to be that
you end up throwing the baby out with the bathwater: your static type
system stops catching the errors you want once you make it powerful
enough to express certain programs.
So now it seems to come down to a matter of taste: use a restricted
language and catch certain errors early or use an unrestricted language
and miss certain errors. It is interesting that the PLT people have
made this tradeoff as well. In the DrScheme system, there are
different `language levels' that provide a restricted subset of Scheme.
At the beginner level, first-class procedures are not allowed. This
is obviously restrictive, but it has the advantage that extraneous
parenthesis (a common beginner mistake) cannot be misinterpreted as the
intent to invoke a first-class procedure.
Anton van Straaten wrote: Chris Smith wrote:
What makes static type systems interesting is not the fact that these
logical processes of reasoning exist; it is the fact that they are
formalized with definite axioms and rules of inference, performed
entirely on the program before execution, and designed to be entirely
evaluatable in finite time bounds according to some procedure or set
of rules, so that a type system may be checked and the same conclusion
reached regardless of who (or what) is doing the checking. All that,
and they still reach interesting conclusions about programs.
There's only one issue mentioned there that needs to be negotiated
w.r.t. latent types: the requirement that they are "performed entirely
on the program before execution". More below.
If informal reasoning about types doesn't meet these criteria (and it
doesn't), then it simply doesn't make sense to call it a type system
(I'm using the static terminology here). It may make sense to discuss
some of the ways that programmer reasoning resembles types, if indeed
there are resemblances beyond just that they use the same basic rules
of logic. It may even make sense to try to identify a subset of
programmer reasoning that even more resembles... or perhaps even is...
a type system. It still doesn't make sense to call programmer
reasoning in general a type system.
I'm not trying to call programmer reasoning in general a type system.
I'd certainly agree that a programmer muddling his way through the
development of a program, perhaps using a debugger to find all his
problems empirically, may not be reasoning about anything that's
sufficiently close to types to call them that. But "latent" means what
it implies: someone who is more aware of types can do better at
developing the latent types.
So these "latent types" may in some cases not exist (in any sense), unless
and until someone other than the original programmer decides how the program
could have been written in a typed language?
I don't get it.
As a starting point, let's assume we're dealing with a disciplined
programmer who (following the instructions found in books such as the
one at htdp.org) reasons about types, writes them in his comments, and
perhaps includes assertions (or contracts in the sense of "Contracts for
Higher Order Functions[1]), to help check his types at runtime (and I'm
talking about real type-checking, not just tag checking).
When such a programmer writes a type signature as a comment associated
with a function definition, in many cases he's making a claim that's
provable in principle about the inputs and outputs of that function.
This is talking about a development practice, not a property of the
language. It may (for the sake of argument) make sense to assign a term
such as latent typing to this development practice, but not to call the
language "latently-typed".
--
David Hopwood <da******************@blueyonder.co.uk>
Joe Marshall wrote: Andreas Rossberg wrote:
Which is why this actually is a very bad example to chose for dynamic
typing advocacy... ;-)
Actually, this seems a *good* example. The problem seems to be that
you end up throwing the baby out with the bathwater: your static type
system stops catching the errors you want once you make it powerful
enough to express certain programs.
That is not the case: you can still express these programs, you just
need to do an indirection through a datatype.
- Andreas
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
Darren New <dn**@san.rr.com> writes: Andreas Rossberg wrote: AFAICT, ADT describes a type whose values can only be accessed by a
certain fixed set of operations.
No. AFAIU, an ADT defines the type based on the operations. The stack
holding the integers 1 and 2 is the value (push(2, push(1,
empty()))). There's no "internal" representation. The values and
operations are defined by preconditions and postconditions.
As a user of the ADT you get a specification consisting of a signature
(names the operations and defines their arity and type of each
argument) and axioms which define the behaviour of the operations.
The implementer has the task for producing an implementation (or
"model" to use alebraic specifiction terminology) that satisfies the
specification. One model that comes for free is the term model where
the operations are treated as terms and the representation of a stack
containing 2 and 1 would just be "(push(2, push(1, empty())))".
However, while that model comes for free it isn't necessarily the most
efficient model. Thus the non-free aspect of chosing a different
implementation is that technically it requires an accompanying proof
that the implementation satisfies the specification.
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
On Mon, 26 Jun 2006 11:49:51 -0600, Chris Smith <cd*****@twu.net>
wrote:
>Pascal Costanza <pc@p-cos.netwrote:
>This is maybe better understandable in user-level code. Consider the
following class definition:
class Person {
String name;
int age;
void buyPorn() {
if (< this.age 18) throw new AgeRestrictionException();
...
}
}
The message p.buyPorn() is a perfectly valid message send and will pass
both static and dynamic type tests (given p is of type Person in the
static case).
It appears you've written the code above to assume that the type system
can't cerify that age >= 18... otherwise, the if statement would not
make sense. It also looks like Java, in which the type system is indeed
not powerfule enough to do that check statically. However, it sounds as
if you're claiming that it wouldn't be possible for the type system to
do this? If so, that's not correct. If such a thing were checked at
compile-time by a static type check, then failing to actually provide
that guarantee would be a type error, and the compiler would tell you
so.
Now this is getting ridiculous. Regardless of implementation
language, Pascal's example is of a data dependent, runtime constraint.
Is the compiler to forbid a person object from aging? If not, then
how does this person object suddenly become a different type when it
becomes 18? Is this conversion to be automatic or manual?
The programmer could forget to make a manual conversion, in which case
the program's behavior is wrong. If your marvelous static type
checker does the conversion automatically, then obviously types are
not static and can be changed at runtime.
Either way you've failed to prevent a runtime problem using a purely
static analysis.
George
--
for email reply remove "/" from address
George Neuner <gneuner2/@comcast.netwrote:
Now this is getting ridiculous.
It's not at all ridiculous. The fact that it seems ridiculous is a good
reason to educate people about what static typing does (and doesn't)
mean, and specifically that it doesn't imply any constraints on the kind
of behavioral property that's being checked; but only on the way that
the check occurs.
(As a subtle point here, we're assuming that this really is an error;
i.e., it shouldn't happen in a correct program. If this is validation
against a user mistake, then that's a different matter; obviously, that
would typically be done with a conditional statement like if, and
wouldn't count as a type error in any context.)
Regardless of implementation
language, Pascal's example is of a data dependent, runtime constraint.
99% of program errors (excluding only syntax errors and the like) are
data-dependent runtime errors. Types are a way of classifying that data
until such errors become obvious at compile time.
Is the compiler to forbid a person object from aging? If not, then
how does this person object suddenly become a different type when it
becomes 18? Is this conversion to be automatic or manual?
The object doesn't have a type (this is static typing, remember?), but
expressions do. The expressions have types, and those types are
probably inferred in such a circumstance (at least, this one would even
more of a pain without type inference).
If your marvelous static type
checker does the conversion automatically, then obviously types are
not static and can be changed at runtime.
There really is no conversion, but it does infer the correct types
automatically. It does so by having more complex rules regarding how to
determine the type of an expression. Java's current type system, of
course, is considerably less powerful. In particular, Java mostly
assures that a variable name has a certain type when used as an
expression, regardless of the context of that expression. Only with
some of the Java 5 features (capture conversion, generic method type
inference, etc) did this cease to be the case. It would be necessary to
drop this entirely to make the feature above work. For example,
consider the following in a hypothetical Java language augmented with
integer type ranges:
int{17..26} a;
int{14..22} b;
...
if (a < b)
{
// Inside this block, a has type int{17..21} and b has type
// int{18..22}
signContract(a); // error, because a might be 17
signContract(b); // no error, because even though the declared
// type of b is int{14..22}, it has a local
// type of int{18..22}.
}
(By the way, I hate this example... hence I've changed buyPorn to
signContract, which at least in the U.S. also requires a minimum age of
18. Hopefully, you'll agree this doesn't change the sunstantive
content. :)
Note that when a programmer is validating input from a user, they will
probably write precisely the kind of conditional expression that allows
the compiler to deduce a sufficiently restrictive type and thus allows
the type checker to succeed. Or if they don't do so -- say, for
example, the programmer produces a fencepost error by accidentally
entering "if (age >= 17)" instead of "if (age 17)" -- then the
compiler will produce a type error as a result. If the programmer
stores the value into a variable of general type int (assuming such a
thing still exists in our augmented Java-esque language), then the
additional type information is forgotten, just like type information is
forgotten when a reference of type String is assigned to a reference of
type Object. In both cases, a runtime-checked cast will be required to
restore the lost type information.
Incidentally, I'm not saying that such a feature would be a good idea.
It generally isn't provided in languages specifically because it gets to
be a big pain to maintain all of the type specifications for this kind
of stuff. However, it is possible, and it is a static type system,
because expressions are assigned typed syntactically, rather than values
being checked for correctness at runtime.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Chris Smith wrote:
>
[...] static typing does ... doesn't imply any constraints on the kind
of behavioral property that's being checked; but only on the way that
the check occurs.
Nice post.
Marshall
I <cd*****@twu.netwrote:
Incidentally, I'm not saying that such a feature would be a good idea.
It generally isn't provided in languages specifically because it gets to
be a big pain to maintain all of the type specifications for this kind
of stuff.
There are other good reasons, too, as it turns out. I don't want to
overstate the "possible" until it starts to sound like "easy, even if
it's a pain". This kind of stuff is rarely done in mainstream
programming languages because it has serious negative consequences.
For example, I wrote that example using variables of type int. If we
were to suppose that we were actually working with variables of type
Person, then things get a little more complicated. We would need a few
(infinite classes of) derived subtypes of Person that further constrain
the possible values for state. For example, we'd need types like:
Person{age:{18..29}}
But this starts to look bad, because we used to have this nice property
called encapsulation. To work around that, we'd need to make one of a
few choices: (a) give up encapsulation, which isn't too happy; (b) rely
on type inference for this kind of stuff, and consider it okay if the
type inference system breaks encapsulation; or (c) invent some kind of
generic constraint language so that constraints like this could be
expressed without exposing field names. Choice (b) is incomplete, as
there will often be times when I need to ascribe a type to a parameter
or some such thing, and the lack of ability to express the complete type
system will be rather limiting. Choice (c), though, looks a little
daunting.
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.
Partly, that's because Java is an imperative language, but it's also
because there are fundamental design trade-offs involved between
verbosity, complexity, expressive power, locality of knowledge, etc.
that are bound to be there in all programming languages, and which make
it harder to take one design principle to its extreme and produce a
usable language as a result. I don't know that it's impossible for this
sort of thing to be done in a usable Java-like language, but in any
case, the way to accomplish it is not obvious.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Chris Smith wrote:
>
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: (a) give up encapsulation, which isn't too happy; (b) rely
on type inference for this kind of stuff, and consider it okay if the
type inference system breaks encapsulation; or (c) invent some kind of
generic constraint language so that constraints like this could be
expressed without exposing field names. Choice (b) is incomplete, as
there will often be times when I need to ascribe a type to a parameter
or some such thing, and the lack of ability to express the complete type
system will be rather limiting. Choice (c), though, looks a little
daunting.
Damn the torpedoes, give me choice c!
I've been saying for a few years now that encapsulation is only
a hack to get around the lack of a decent declarative constraint
language.
Marshall
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
Marshall <ma*************@gmail.comwrote:
Chris Smith wrote:
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: (a) give up encapsulation, which isn't too happy; (b) rely
on type inference for this kind of stuff, and consider it okay if the
type inference system breaks encapsulation; or (c) invent some kind of
generic constraint language so that constraints like this could be
expressed without exposing field names. Choice (b) is incomplete, as
there will often be times when I need to ascribe a type to a parameter
or some such thing, and the lack of ability to express the complete type
system will be rather limiting. Choice (c), though, looks a little
daunting.
Damn the torpedoes, give me choice c!
You and I both need to figure out when to go to sleep. :) Work's gonna
suck tomorrow.
I've been saying for a few years now that encapsulation is only
a hack to get around the lack of a decent declarative constraint
language.
Choice (c) was meant to preserve encapsulation, actually. I think
there's something fundamentally important about information hiding that
can't be given up. Hypothetically, say I'm writing an accounting
package and I've decided to encapsulate details of the tax code into one
module of the application. Now, it may be that the compiler can perform
sufficient type inference on my program to know that it's impossible for
my taxes to be greater than 75% of my annual income. So if my income is
stored in a variable of type decimal{0..100000}, then the return type of
getTotalTax may be of type decimal{0..75000}. Type inference could do
that.
But the point here is that I don't WANT the compiler to be able to infer
that, because it's a transient consequence of this year's tax code. I
want the compiler to make sure my code works no matter what the tax code
is. The last thing I need to to go fixing a bunch of bugs during the
time between the release of next year's tax code and the released
deadline for my tax software. At the same time, though, maybe I do want
the compiler to infer that tax cannot be negative (or maybe it can; I'm
not an accountant; I know my tax has never been negative), and that it
can't be a complex number (I'm pretty sure about that one). I call that
encapsulation, and I don't think that it's necessary for lack of
anything; but rather because that's how the problem breaks down.
----
Note that even without encapsulation, the kind of typing information
we're looking at can be very non-trivial in an imperative language. For
example, I may need to express a method signature that is kind of like
this:
1. The first parameter is an int, which is either between 4 and 8, or
between 11 and 17.
2. The second parameter is a pointer to an object, whose 'foo' field is
an int between 0 and 5, and whose 'bar' field is a pointer to another
abject with three fields 'a', 'b', and 'c', each of which has the full
range of an unconstrained IEEE double precision floating point number.
3. After the method returns, it will be known that if this object
previously had its 'baz' field in the range m .. n, it is now in the
range (m - 5) .. (n + 1).
4. After the method returns, it will be known that the object reached by
following the 'bar' field of the second parameter will be modified so
that the first two of its floating point numbers are guaranteed to be of
the opposite sign as they were before, and that if they were infinity,
they are now finite.
5. After the method returns, the object referred to by the global
variable 'zab' has 0 as the value of its 'c' field.
Just expressing all of that in a method signature looks interesting
enough. If we start adding abstraction to the type constraints on
objects to support encapsulation (as I think you'd have to do), then
things get even more interesting.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
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
Chris Smith <cd*****@twu.netwrites:
But the point here is that I don't WANT the compiler to be able to infer
that, because it's a transient consequence of this year's tax code. I
want the compiler to make sure my code works no matter what the tax code
is. The last thing I need to to go fixing a bunch of bugs during the
time between the release of next year's tax code and the released
deadline for my tax software. At the same time, though, maybe I do want
the compiler to infer that tax cannot be negative (or maybe it can; I'm
not an accountant; I know my tax has never been negative),
Yes, it can. For example in Spain. Theorically, in France IVA can
also come out negative, and you have the right to ask for
reimbursement, but I've never seen a check from French Tax
Administration...
and that it
can't be a complex number (I'm pretty sure about that one).
I wouldn't bet on it.
For example, French taxes consider "advantages in nature", so your
income has at least two dimensions, Euros and and "advantages in
nature". Thanksfully, these advantages are converted into Euros, but
you could consider it a product by (complex 0 (- some-factor))...
I call that
encapsulation, and I don't think that it's necessary for lack of
anything; but rather because that's how the problem breaks down.
--
__Pascal Bourguignon__ http://www.informatimago.com/
You never feed me.
Perhaps I'll sleep on your face.
That will sure show you.
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?
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, or are you talking about having the
constraint language itself be something other than functional?
Marshall
Chris Smith wrote:
Marshall <ma*************@gmail.comwrote:
Chris Smith wrote:
>
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: (a) give up encapsulation, which isn't too happy; (b) rely
on type inference for this kind of stuff, and consider it okay if the
type inference system breaks encapsulation; or (c) invent some kind of
generic constraint language so that constraints like this could be
expressed without exposing field names. Choice (b) is incomplete, as
there will often be times when I need to ascribe a type to a parameter
or some such thing, and the lack of ability to express the complete type
system will be rather limiting. Choice (c), though, looks a little
daunting.
Damn the torpedoes, give me choice c!
You and I both need to figure out when to go to sleep. :) Work's gonna
suck tomorrow.
It's never been a strong point. Made worse now that my daughter
is one of those up-at-the-crack-of-dawn types, and not old enough
to understand why it's not nice to jump on mommy and daddy's
bed while they're still asleep. But aren't you actually a time zone
or two east of me?
I've been saying for a few years now that encapsulation is only
a hack to get around the lack of a decent declarative constraint
language.
Choice (c) was meant to preserve encapsulation, actually. I think
there's something fundamentally important about information hiding that
can't be given up. Hypothetically, say I'm writing an accounting
package and I've decided to encapsulate details of the tax code into one
module of the application. Now, it may be that the compiler can perform
sufficient type inference on my program to know that it's impossible for
my taxes to be greater than 75% of my annual income. So if my income is
stored in a variable of type decimal{0..100000}, then the return type of
getTotalTax may be of type decimal{0..75000}. Type inference could do
that.
The fields of an object/struct/what have you are often hidden behind
a method-based interface (sometimes callled "encapsulated") only
because we can't control their values otherwise. (The "exposing
the interface" issue is a non-issue, because we're exposing some
interface or another no matter what.) The issue is controlling the
values, and that is better handled with a declarative constraint
language. The specific value in the fields aren't known until
runtime.
However for a function, the "fields" are the in and out parameters.
The specific values in the relation that the function is aren't known
until runtime either, (and then only the subset for which we actually
perform computation.)
Did that make sense?
But the point here is that I don't WANT the compiler to be able to infer
that, because it's a transient consequence of this year's tax code. I
want the compiler to make sure my code works no matter what the tax code
is. The last thing I need to to go fixing a bunch of bugs during the
time between the release of next year's tax code and the released
deadline for my tax software. At the same time, though, maybe I do want
the compiler to infer that tax cannot be negative (or maybe it can; I'm
not an accountant; I know my tax has never been negative), and that it
can't be a complex number (I'm pretty sure about that one). I call that
encapsulation, and I don't think that it's necessary for lack of
anything; but rather because that's how the problem breaks down.
There's some significant questions in my mind about how much of
a constraint language would be static and how much would be
runtime checks. Over time, I'm starting to feel like it should be
mostly runtime, and only occasionally moving into compile time
at specific programmer request. The decidability issue comes up.
Anyone else?
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.
There are certainly syntactic issues, but I believe these are amenable
to the usual approaches. The runtime/compile time question, and
decidability seem bigger issues to me.
Marshall
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
Chris Smith wrote:
// Inside this block, a has type int{17..21} and b has type
// int{18..22}
No what happens if right here you code
b := 16;
Does that again change the type of "b"? Or is that an illegal
instruction, because "b" has the "local type" of (18..22)?
signContract(a); // error, because a might be 17
signContract(b); // no error, because even though the declared
// type of b is int{14..22}, it has a local
// type of int{18..22}.
If the former (i.e., if reassigning to "b" changes the "static type" of
b, then the term you're looking for is not type, but "typestate".
In other words, this is the same sort of test that disallows using an
unassigned variable in a value-returning expression. When
{ int a; int b; b := a; }
returns a compile-time error because "a" is uninitialized at the
assignment, that's not the "type" of a, but the typestate. Just FYI.
Incidentally, I'm not saying that such a feature would be a good idea.
It actually works quite well if the language takes advantage of it
consistantly and allows you to designate your expected typestates and such.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
Marshall <ma*************@gmail.comwrote:
It's never been a strong point. Made worse now that my daughter
is one of those up-at-the-crack-of-dawn types, and not old enough
to understand why it's not nice to jump on mommy and daddy's
bed while they're still asleep. But aren't you actually a time zone
or two east of me?
Yes, I confess I'm one time zone to your east, and I was posting later
than you. So perhaps it wasn't really past your bedtime.
The fields of an object/struct/what have you are often hidden behind
a method-based interface (sometimes callled "encapsulated") only
because we can't control their values otherwise.
I believe there are actually two kinds of encapsulation. The kind of
encapsulation that best fits your statement there is the getter/setter
sort, which says: "logically, I want an object with some set of fields,
but I can't make them fields because I lose control over their values".
That part can definitely be replaced, in a suitably powerful language,
with static constraints.
The other half of encapsulation, though, is of the sort that I mentioned
in my post. I am intentionally choosing to encapsulate something
because I don't actually know how it should end up being implemented
yet, or because it changes often, or something like that. I may
encapsulate the implementation of current tax code specifically because
I know that tax code changes on a year-to-year basis, and I want to
ensure that the rest of my program works no matter how the tax code is
modified. There may be huge structural changes in the tax code, and I
only want to commit to leaving a minimal interface.
In practice, the two purposes are not cleanly separated from each other.
Most people, if asked why they write getters and setters, would respond
not only that they want to validate against assignments to the field,
but also that it helps isolate changes should they change the internal
representation of the class. A publicly visible static constraint
language that allows the programmer to change the internal
representation of a class obviously can't make reference to any field,
since it may cease to exist with a change in representation.
However for a function, the "fields" are the in and out parameters.
The specific values in the relation that the function is aren't known
until runtime either, (and then only the subset for which we actually
perform computation.)
Did that make sense?
I didn't understand that last bit.
There are certainly syntactic issues, but I believe these are amenable
to the usual approaches. The runtime/compile time question, and
decidability seem bigger issues to me.
Well, the point of static typing is to do what's possible without
reaching the point of undecidability. Runtime support for checking the
correctness of type ascriptions certainly comes in handy when you run
into those limits.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Darren New <dn**@san.rr.comwrote:
Chris Smith wrote:
// Inside this block, a has type int{17..21} and b has type
// int{18..22}
No what happens if right here you code
b := 16;
Does that again change the type of "b"? Or is that an illegal
instruction, because "b" has the "local type" of (18..22)?
It arranges that the expression "b" after that line (barring further
changes) has type int{16..16}, which would make the later call to
signContract illegal.
If the former (i.e., if reassigning to "b" changes the "static type" of
b, then the term you're looking for is not type, but "typestate".
We're back into discussion terminology, then. How fun. Yes, the word
"typestate" is used to describe this in a good bit of literature.
Nevertheless, a good number of authors -- including all of them that I'm
aware of in programming language type theory -- would agree that "type"
is a perfectly fine word.
When I said b has a type of int{18..22}, I meant that the type that will
be inferred for the expression "b" when it occurs inside this block as
an rvalue will be int{18..22}. The type of the variable didn't change,
because variables don't *have* types. Expressions (or, depending on
your terminology preference, terms) have types. An expression "b" that
occurs after your assignment is a different expression from the one that
occurs before your assignment, so it's entirely expected that in the
general case, it may have a different type.
It's also the case (and I didn't really acknowledge this before) that
the expression "b" when used as an lvalue has a different type, which is
determined according to different rules. As such, the assignment to b
was not at all influenced by the new type that was arranged for the
expression "b" as an rvalue.
(I'm using lvalue and rvalue intuitively; in practice, these would be
assigned on a case-by-case basis along the lines of actual operators or
language syntax.)
In other words, this is the same sort of test that disallows using an
unassigned variable in a value-returning expression.
Yes, it is.
When
{ int a; int b; b := a; }
returns a compile-time error because "a" is uninitialized at the
assignment, that's not the "type" of a, but the typestate. Just FYI.
If you wish to say "typestate" to mean this, be my guest. It is also
correct to say "type".
It actually works quite well if the language takes advantage of it
consistantly and allows you to designate your expected typestates and such.
I'm not aware of a widely used language that implements stuff like this.
Are you?
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Chris Smith wrote:
If you wish to say "typestate" to mean this, be my guest. It is also
correct to say "type".
Sure. I just wasn't sure everyone here was aware of the term, is all. It
makes it easier to google if you have a more specific term.
I'm not aware of a widely used language that implements stuff like this.
I've only used Hermes with extensive support for this sort of thing.
Hermes is process-oriented, rather than object-oriented, so it's a
little easier to deal with the "encapsulation" part of the equation
there. Sadly, Hermes went the way of the dodo.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
Chris Smith wrote:
I <cd*****@twu.netwrote:
>>Incidentally, I'm not saying that such a feature would be a good idea.
I don't think it would be a bad idea. Silently giving incorrect results
on arithmetic overflow, as C-family languages do, is certainly a bad idea.
A type system that supported range type arithmetic as you've described would
have considerable advantages, especially in areas such as safety-critical
software. It would be a possible improvement to Ada, which UUIC currently
has a more restrictive range typing system that cannot infer different
ranges for a variable at different points in the program.
I find that regardless of programming language, relatively few of my
integer variables are dimensionless -- most are associated with some
specific unit. Currently, I find variable naming conventions helpful in
documenting this, but the result is probably more verbose than it would
be to drop this information from the names, and instead use more
precise types that indicate the unit and the range.
When prototyping, you could alias all of these to bignum types (with
range [0..+infinity) or (-infinity..+infinity)) to avoid needing to deal
with any type errors, and then constrain them where necessary later.
>>It generally isn't provided in languages specifically because it gets to
be a big pain to maintain all of the type specifications for this kind
of stuff.
It would take a little more work to write a program, but it would be no
more difficult to read (easier if you're also trying to verify its correctness).
Ease of reading programs is more important than writing.
There are other good reasons, too, as it turns out. I don't want to
overstate the "possible" until it starts to sound like "easy, even if
it's a pain". This kind of stuff is rarely done in mainstream
programming languages because it has serious negative consequences.
For example, I wrote that example using variables of type int. If we
were to suppose that we were actually working with variables of type
Person, then things get a little more complicated. We would need a few
(infinite classes of) derived subtypes of Person that further constrain
the possible values for state. For example, we'd need types like:
Person{age:{18..29}}
But this starts to look bad, because we used to have this nice property
called encapsulation.
I think you're assuming that 'age' would have to refer to a concrete field.
If it refers to a type parameter, something like:
class Person{age:Age} is
Age getAge()
end
then I don't see how this breaks encapsulation.
--
David Hopwood <da******************@blueyonder.co.uk>
Chris Smith wrote:
At the same time, though, maybe I do want
the compiler to infer that tax cannot be negative (or maybe it can; I'm
not an accountant; I know my tax has never been negative), [...]
Tax can be negative, e.g. when a business is claiming back VAT (sales tax)
on its purchases, but the things it is selling have lower-rated or zero
VAT (or it is making a loss).
Note that even without encapsulation, the kind of typing information
we're looking at can be very non-trivial in an imperative language. For
example, I may need to express a method signature that is kind of like
this:
1. The first parameter is an int, which is either between 4 and 8, or
between 11 and 17.
2. The second parameter is a pointer to an object, whose 'foo' field is
an int between 0 and 5, and whose 'bar' field is a pointer to another
object with three fields 'a', 'b', and 'c', each of which has the full
range of an unconstrained IEEE double precision floating point number.
3. After the method returns, it will be known that if this object
previously had its 'baz' field in the range m .. n, it is now in the
range (m - 5) .. (n + 1).
4. After the method returns, it will be known that the object reached by
following the 'bar' field of the second parameter will be modified so
that the first two of its floating point numbers are guaranteed to be of
the opposite sign as they were before, and that if they were infinity,
they are now finite.
5. After the method returns, the object referred to by the global
variable 'zab' has 0 as the value of its 'c' field.
Just expressing all of that in a method signature looks interesting
enough. If we start adding abstraction to the type constraints on
objects to support encapsulation (as I think you'd have to do), then
things get even more interesting.
1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.
--
David Hopwood <da******************@blueyonder.co.uk>
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.
jue
David Hopwood <da******************@blueyonder.co.ukwrote:
1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.
One of us is missing the other's meaning here. If 3 to 5 were expressed
as assertions rather than types, then the type system would become
incomplete, requiring frequent runtime-checked type ascriptions to
prevent it from becoming impossible to write software. That's not my
idea of a usable language.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Chris Smith wrote:
David Hopwood <da******************@blueyonder.co.ukwrote:
>>1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.
One of us is missing the other's meaning here. If 3 to 5 were expressed
as assertions rather than types, then the type system would become
incomplete, requiring frequent runtime-checked type ascriptions to
prevent it from becoming impossible to write software. That's not my
idea of a usable language.
Maybe I'm not understanding what you mean by "complete". Of course any
type system of this expressive power will be incomplete (whether or not
it can express conditions 3 to 5), in the sense that it cannot prove all
true assertions about the types of expressions.
So yes, some assertions would need to be checked at runtime (others could be
proven to always hold by a theorem prover).
Why is this a problem? The goal is not to check everything at compile time;
the goal is just to support writing correct programs.
--
David Hopwood <da******************@blueyonder.co.uk>
Jrgen Exner wrote:
David Hopwood wrote:
[...]
There is no such error message listed in 'perldoc perldiag'.
Please quote the actual text of your error message and include the program
that produced this error.
Then people here in CLPM may be able to assist you.
Yes, I'm well aware that most of this thread has been off-topic for c.l.p.m,
but it is no less off-topic for the other groups (except possibly c.l.functional),
and I can't trim the Newsgroups line down to nothing.
Don't you have a newsreader that can mark whole threads that you don't want
to read?
--
David Hopwood <da******************@blueyonder.co.uk>
David Hopwood wrote:
Jrgen Exner wrote:
David Hopwood wrote:
[...]
There is no such error message listed in 'perldoc perldiag'.
Please quote the actual text of your error message and include the program
that produced this error.
Then people here in CLPM may be able to assist you.
Yes, I'm well aware that most of this thread has been off-topic for c.l.p..m,
but it is no less off-topic for the other groups (except possibly c.l.functional),
and I can't trim the Newsgroups line down to nothing.
Don't you have a newsreader that can mark whole threads that you don't want
to read?
Sure, or he could just skip over it. Or he could make a simple
request, such as "please trim comp.lang.whatever because it's
off-topic here." But he hasn't done any of these, choosing instead
to drop in with his occasional pointless snarky comments.
Marshall
David Hopwood <da******************@blueyonder.co.ukwrote:
Maybe I'm not understanding what you mean by "complete". Of course any
type system of this expressive power will be incomplete (whether or not
it can express conditions 3 to 5), in the sense that it cannot prove all
true assertions about the types of expressions.
Ah. I meant complete enough to accomplish the goal in this subthread,
which was to ensure that the compiler knows when a particular int
variable is guaranteed to be greater than 18, and when it is not.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Joachim Durchholz wrote:
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.
Now, I'm not fully up to speed on DBC. The contract specifications,
these are specified statically, but checked dynamically, is that
right? In other words, we can consider contracts in light of
inheritance, but the actual verification and checking happens
at runtime, yes?
Wouldn't it be possible to do them at compile time? (Although
this raises decidability issues.) Mightn't it also be possible to
leave it up to the programmer whether a given contract
was compile-time or runtime?
I've been wondering about this for a while.
Marshall
David Hopwood wrote:
Yes, I'm well aware that most of this thread has been off-topic for c.l.p.m,
but it is no less off-topic for the other groups (except possibly c.l.functional),
and I can't trim the Newsgroups line down to nothing.
is someone forcing your to post off-topic stuff against your will? sounds scary.
do you want us to call the police?
</F> This thread has been closed and replies have been disabled. Please start a new discussion. Similar topics
by: Brandon J. Van Every |
last post by:
What's better about Ruby than Python? I'm sure there's something. What is
it?
This is not a troll. I'm language shopping and I want people's answers. I
don't know beans about Ruby or have...
|
by: Xah Lee |
last post by:
What is Expresiveness in a Computer Language
20050207, Xah Lee.
In languages human or computer, there's a notion of expressiveness.
English for example, is very expressive in manifestation,...
|
by: Xah Lee |
last post by:
The Concepts and Confusions of Pre-fix, In-fix, Post-fix and Fully
Functional Notations
Xah Lee, 2006-03-15
Let me summarize: The LISP notation, is a functional notation, and is
not a...
|
by: CloudSolutions |
last post by:
Introduction:
For many beginners and individual users, requiring a credit card and email registration may pose a barrier when starting to use cloud servers. However, some cloud server providers now...
|
by: Faith0G |
last post by:
I am starting a new it consulting business and it's been a while since I setup a new website. Is wordpress still the best web based software for hosting a 5 page website? The webpages will be...
|
by: isladogs |
last post by:
The next Access Europe User Group meeting will be on Wednesday 3 Apr 2024 starting at 18:00 UK time (6PM UTC+1) and finishing by 19:30 (7.30PM).
In this session, we are pleased to welcome former...
|
by: taylorcarr |
last post by:
A Canon printer is a smart device known for being advanced, efficient, and reliable. It is designed for home, office, and hybrid workspace use and can also be used for a variety of purposes. However,...
|
by: ryjfgjl |
last post by:
If we have dozens or hundreds of excel to import into the database, if we use the excel import function provided by database editors such as navicat, it will be extremely tedious and time-consuming...
|
by: ryjfgjl |
last post by:
In our work, we often receive Excel tables with data in the same format. If we want to analyze these data, it can be difficult to analyze them because the data is spread across multiple Excel files...
|
by: emmanuelkatto |
last post by:
Hi All, I am Emmanuel katto from Uganda. I want to ask what challenges you've faced while migrating a website to cloud.
Please let me know.
Thanks!
Emmanuel
|
by: BarryA |
last post by:
What are the essential steps and strategies outlined in the Data Structures and Algorithms (DSA) roadmap for aspiring data scientists? How can individuals effectively utilize this roadmap to progress...
|
by: Hystou |
last post by:
There are some requirements for setting up RAID:
1. The motherboard and BIOS support RAID configuration.
2. The motherboard has 2 or more available SATA protocol SSD/HDD slots (including MSATA, M.2...
| |
