[28012] in Perl-Users-Digest
Perl-Users Digest, Issue: 9376 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Sun Jun 25 14:10:13 2006
Date: Sun, 25 Jun 2006 11:10:06 -0700 (PDT)
From: Perl-Users Digest <Perl-Users-Request@ruby.OCE.ORST.EDU>
To: Perl-Users@ruby.OCE.ORST.EDU (Perl-Users Digest)
Perl-Users Digest Sun, 25 Jun 2006 Volume: 10 Number: 9376
Today's topics:
Re: What is Expressiveness in a Computer Language <jo@durchholz.org>
Re: What is Expressiveness in a Computer Language <vesa.karvonen@cs.helsinki.fi>
Re: What is Expressiveness in a Computer Language rossberg@ps.uni-sb.de
Re: What is Expressiveness in a Computer Language <pc@p-cos.net>
Re: What is Expressiveness in a Computer Language <david.nospam.hopwood@blueyonder.co.uk>
Re: What is Expressiveness in a Computer Language <david.nospam.hopwood@blueyonder.co.uk>
Re: What is Expressiveness in a Computer Language <david.nospam.hopwood@blueyonder.co.uk>
Re: What is Expressiveness in a Computer Language <gdr@integrable-solutions.net>
Re: What is Expressiveness in a Computer Language rossberg@ps.uni-sb.de
Re: What is Expressiveness in a Computer Language <cfc@shell01.TheWorld.com>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Re: What is Expressiveness in a Computer Language <gdr@integrable-solutions.net>
Re: What is Expressiveness in a Computer Language <scott.daniels@acm.org>
Re: What is Expressiveness in a Computer Language <marshall.spight@gmail.com>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Re: What is Expressiveness in a Computer Language <jurgenex@hotmail.com>
Re: What is Expressiveness in a Computer Language <jo@durchholz.org>
Re: What is Expressiveness in a Computer Language rossberg@ps.uni-sb.de
Re: What is Expressiveness in a Computer Language <jo@durchholz.org>
Re: What is Expressiveness in a Computer Language rossberg@ps.uni-sb.de
Re: What is Expressiveness in a Computer Language <jo@durchholz.org>
Re: What is Expressiveness in a Computer Language <jo@durchholz.org>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Sun, 25 Jun 2006 15:21:56 +0200
From: Joachim Durchholz <jo@durchholz.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7m2l5$35g$1@online.de>
Andreas Rossberg schrieb:
>
> Luca Cardelli has given the most convincing one in his seminal tutorial
> "Type Systems", where he identifies "typed" and "safe" as two orthogonal
> dimensions and gives the following matrix:
>
> | typed | untyped
> -------+-------+----------
> safe | ML | Lisp
> unsafe | C | Assembler
>
> Now, jargon "dynamically typed" is simply untyped safe, while "weakly
> typed" is typed unsafe.
Here's a matrix how most people that I know would fill in with terminology:
| Statically | Not |
| typed | statically |
| | typed |
---------+--------------+-------------+
typesafe | "strongly | Dynamically |
| typed" | typed |
| (ML, Pascal) | (Lisp) |
---------+--------------+-------------+
not | (no common | "untyped" |
typesafe | terminology) | |
| (C) | (Assembly) |
---------+--------------+-------------+
(Terms in quotes are challenged on a regular basis, or rarely if ever
applied.)
With the above terminology, it becomes clear that the opposite if
"(statically) typed" isn't "statically untyped", but "not statically
typed". "Statically typed" and "dynamically typed" aren't even
opposites, they just don't overlap.
Another observation: type safeness is more of a spectrum than a clearcut
distinction. Even ML and Pascal have ways to circumvent the type system,
and even C is typesafe unless you use unsafe constructs.
IOW from a type-theoretic point of view, there is no real difference
between their typesafe and not typesafe languages in the "statically
typed" column; the difference is in the amount of unsafe construct usage
in practial programs.
Regards,
Jo
------------------------------
Date: 25 Jun 2006 13:57:30 GMT
From: Vesa Karvonen <vesa.karvonen@cs.helsinki.fi>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7m4oa$mm0$1@oravannahka.helsinki.fi>
In comp.lang.functional Joachim Durchholz <jo@durchholz.org> wrote:
> [...] Even ML and Pascal have ways to circumvent the type system, [...]
Show me a Standard ML program that circumvents the type system.
-Vesa Karvonen
------------------------------
Date: 25 Jun 2006 07:10:28 -0700
From: rossberg@ps.uni-sb.de
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151244628.566060.40500@p79g2000cwp.googlegroups.com>
Joachim Durchholz write:
>
> Another observation: type safeness is more of a spectrum than a clearcut
> distinction. Even ML and Pascal have ways to circumvent the type system,
No. I'm not sure about Pascal, but (Standard) ML surely has none. Same
with Haskell as defined by its spec. OCaml has a couple of clearly
marked unsafe library functions, but no unsafe feature in the language
semantics itself.
> and even C is typesafe unless you use unsafe constructs.
Tautology. Every language is "safe unless you use unsafe constructs".
(Unfortunately, you can hardly write interesting programs in any safe
subset of C.)
> IOW from a type-theoretic point of view, there is no real difference
> between their typesafe and not typesafe languages in the "statically
> typed" column; the difference is in the amount of unsafe construct usage
> in practial programs.
Huh? There is a huge, fundamental difference: namely whether a type
system is sound or not. A soundness proof is obligatory for any serious
type theory, and failure to establish it simply is a bug in the theory.
- Andreas
------------------------------
Date: Sun, 25 Jun 2006 16:14:14 +0200
From: Pascal Costanza <pc@p-cos.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <4g7k1mF1ma4ghU1@individual.net>
Joachim Durchholz wrote:
> Andreas Rossberg schrieb:
>>
>> Luca Cardelli has given the most convincing one in his seminal
>> tutorial "Type Systems", where he identifies "typed" and "safe" as two
>> orthogonal dimensions and gives the following matrix:
>>
>> | typed | untyped
>> -------+-------+----------
>> safe | ML | Lisp
>> unsafe | C | Assembler
>>
>> Now, jargon "dynamically typed" is simply untyped safe, while "weakly
>> typed" is typed unsafe.
>
> Here's a matrix how most people that I know would fill in with terminology:
>
> | Statically | Not |
> | typed | statically |
> | | typed |
> ---------+--------------+-------------+
> typesafe | "strongly | Dynamically |
> | typed" | typed |
> | (ML, Pascal) | (Lisp) |
> ---------+--------------+-------------+
> not | (no common | "untyped" |
> typesafe | terminology) | |
> | (C) | (Assembly) |
> ---------+--------------+-------------+
>
> (Terms in quotes are challenged on a regular basis, or rarely if ever
> applied.)
>
> With the above terminology, it becomes clear that the opposite if
> "(statically) typed" isn't "statically untyped", but "not statically
> typed". "Statically typed" and "dynamically typed" aren't even
> opposites, they just don't overlap.
>
> Another observation: type safeness is more of a spectrum than a clearcut
> distinction. Even ML and Pascal have ways to circumvent the type system,
> and even C is typesafe unless you use unsafe constructs.
> IOW from a type-theoretic point of view, there is no real difference
> between their typesafe and not typesafe languages in the "statically
> typed" column; the difference is in the amount of unsafe construct usage
> in practial programs.
It's also relevant how straightforward it is to distinguish between safe
and unsafe code, how explicit you have to be when you use unsafe code,
how likely it is that you accidentally use unsafe code without being
aware of it, what the generally accepted conventions in a language
community are, etc. pp.
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
------------------------------
Date: Sun, 25 Jun 2006 15:22:32 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <YSxng.477416$xt.143460@fe3.news.blueyonder.co.uk>
Joachim Durchholz wrote:
> Andreas Rossberg schrieb:
>
>> Luca Cardelli has given the most convincing one in his seminal
>> tutorial "Type Systems", where he identifies "typed" and "safe" as two
>> orthogonal dimensions and gives the following matrix:
>>
>> | typed | untyped
>> -------+-------+----------
>> safe | ML | Lisp
>> unsafe | C | Assembler
>>
>> Now, jargon "dynamically typed" is simply untyped safe, while "weakly
>> typed" is typed unsafe.
>
> Here's a matrix how most people that I know would fill in with terminology:
>
> | Statically | Not |
> | typed | statically |
> | | typed |
> ---------+--------------+-------------+
> typesafe | "strongly | Dynamically |
> | typed" | typed |
> | (ML, Pascal) | (Lisp) |
Pascal, in most of its implementations, isn't [memory] safe; it's in the same
box as C.
> ---------+--------------+-------------+
> not | (no common | "untyped" |
> typesafe | terminology) | |
> | (C) | (Assembly) |
> ---------+--------------+-------------+
I have to say that I prefer the labels used by Cardelli.
> (Terms in quotes are challenged on a regular basis, or rarely if ever
> applied.)
>
> With the above terminology, it becomes clear that the opposite if
> "(statically) typed" isn't "statically untyped", but "not statically
> typed". "Statically typed" and "dynamically typed" aren't even
> opposites, they just don't overlap.
>
> Another observation: type safeness is more of a spectrum than a clearcut
> distinction. Even ML and Pascal have ways to circumvent the type system,
Standard ML doesn't (with just the standard basis; no external libraries,
and assuming that file I/O cannot be used to corrupt the language
implementation).
> and even C is typesafe unless you use unsafe constructs.
> IOW from a type-theoretic point of view, there is no real difference
> between their typesafe and not typesafe languages in the "statically
> typed" column; the difference is in the amount of unsafe construct usage
> in practial programs.
It is quite possible to design languages that have absolutely no unsafe
constructs, and are still useful.
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: Sun, 25 Jun 2006 15:31:50 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <G%xng.477395$tc.466834@fe2.news.blueyonder.co.uk>
Chris F Clark wrote:
> Chris Smith <cdsmith@twu.net> writes:
>
>>Unfortunately, I have to again reject this idea. There is no such
>>restriction on type theory. Rather, the word type is defined by type
>>theorists to mean the things that they talk about.
>
> Do you reject that there could be something more general than what a
> type theorist discusses? Or do you reject calling such things a type?
>
> Let you write:
>
>>because we could say that anything that checks types is a type system,
>>and then worry about verifying that it's a sound type system without
>>worrying about whether it's a subset of the perfect type system.
>
> I'm particularly interested if something unsound (and perhaps
> ambiguous) could be called a type system.
Yes, but not a useful one. The situation is the same as with unsound
formal systems; they still satisfy the definition of a formal system.
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: Sun, 25 Jun 2006 15:34:12 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <U1yng.477449$tc.249586@fe2.news.blueyonder.co.uk>
David Hopwood wrote:
> Chris F Clark wrote:
>
>>I'm particularly interested if something unsound (and perhaps
>>ambiguous) could be called a type system.
>
> Yes, but not a useful one. The situation is the same as with unsound
> formal systems; they still satisfy the definition of a formal system.
I meant "inconsistent formal systems".
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: 25 Jun 2006 18:54:03 +0200
From: Gabriel Dos Reis <gdr@integrable-solutions.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <m34py9dvmc.fsf@uniton.integrable-solutions.net>
rossberg@ps.uni-sb.de writes:
[...]
| > and even C is typesafe unless you use unsafe constructs.
|
| Tautology. Every language is "safe unless you use unsafe constructs".
| (Unfortunately, you can hardly write interesting programs in any safe
| subset of C.)
Fortunately, some people do, as living job.
I must confess I'm sympathetic to Bob Harper's view expressed in
http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html
-- Gaby
------------------------------
Date: 25 Jun 2006 09:17:06 -0700
From: rossberg@ps.uni-sb.de
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151252226.104247.62960@b68g2000cwa.googlegroups.com>
Gabriel Dos Reis wrote:
> |
> | (Unfortunately, you can hardly write interesting programs in any safe
> | subset of C.)
>
> Fortunately, some people do, as living job.
I don't think so. Maybe the question is what a "safe subset" consists
of. In my book, it excludes all features that are potentially unsafe.
So in particular, C-style pointers are out, because they can easily
dangle, be uninitialisied, whatever. Can you write a realistic C
program without using pointers?
- Andreas
------------------------------
Date: 25 Jun 2006 12:22:44 -0400
From: Chris F Clark <cfc@shell01.TheWorld.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <sdd8xnl2oiz.fsf@shell01.TheWorld.com>
Chris F Clark (I) wrote:
> I'm particularly interested if something unsound (and perhaps
> ambiguous) could be called a type system. I definitely consider such
> things type systems.
"Marshall" <marshall.spight@gmail.com> wrote:
> I don't understand. You are saying you prefer to investigate the
> unsound over the sound?
...
> Again, I cannot understand this. In a technical realm, vagueness
> is the opposite of understanding.
At the risk of injecting too much irrelevant philosophy into the
discussion, I will with great trepdiation reply.
First in the abstrtact: No, understanding is approximating. The world
is inherently vague. We make false symbolic models of the world which
are consistent, but at some level they do not reflect reality, because
reality isn't consistent. Only by abtracting away the inherent
infinite amout of subtlety present in the real universe can we come to
comprehensible models. Those models can be consistent, but they are
not the universe. The models in their consistency, prove things which
are not true about the real universe.
Now in the concrete: In my work productivity is ultimately important.
Therefore, we live by the 80-20 rule in numerous variations. One of
ths things we do to achieve productivity is simplify things. In fact,
we are more interested in an unsound simplification that is right 80%
of the time, but takes only 20% of the effort to compute, than a
completely sound (100% right) model which takes 100% of the time to
compute (which is 5 times as long). We are playing the probabilities.
It's not that we don't respect the sound underpining, the model which
is consistent and establishes certain truths. However, what we want
is the rule of thumb which is far simpler and approximates the sound
model with reasonable accuracy. In particular, we accept two types of
unsoundness in the model. One, we accept a model which gives wrong
answers which are detectable. We code tests to catch those cases, and
use a different model to get the right answer. Two, we accept a model
which gets the right answer only when over-provisioned. for example,
if we know a loop will occassionaly not converge in the n-steps that
it theoretically should, we will run the loop for n+m steps until the
approximation also converges--even if that requires allocating m extra
copies of some small element than are theoretically necessary. A
small waste of a small resource, is ok if it saves a waste of a more
critical resource--the most critical resource of all being our project
timeliness.
We do the same things in our abstract reasoning (including our type
model). The problems we are solving are too large for us to
understand. Therefore, we make simplifications, simplifications we
know are inaccurate and potentially unsound. Our algorithm then
solves the simplified model, which we think covers the main portion of
the problem. It also attempts to detect when it has encountered a
problem that is outside of the simplified region, on the edge so to
speak. Now, in general, we can figure out how to handle certain edge
cases, and we do it. However, some times the edge of one part of the
algorithm intereacts with an edge of another part of the algorithm and
we get a "corner case". Because our model is too simple and the
reasoning it allows is thus unsound, the algorithm will occassionally
compute the wrong results for some of those corners. We use the same
techniques for dealing with them. Dynamic tagging is one way of
catching when we have gotten the wrong answer in our type
simplification.
Marshall's last point:
> I flipped a coin to see who would win the election; it came
> up "Bush". Therefore I *knew* who was going to win the
> election before it happened. See the probem?
Flipping one coin to determine an election is not playing the
probabilities correctly. You need a plausible explanation for why the
coin should predict the right answer and a track record of it being
correct. If you had a coin that had correctly predicted the previous
42 presidencies and you had an explanation why the coin was right,
then it would be credible and I would be willing to wager that it
could also predict that the coin could tell us who the 44th president
would be. One flip and no explanation is not sufficient. (And to the
abstract point, to me that is all knowledge is, some convincing amount
of examples and a plausible explanation--anyone who thinks they have
more is appealing to a "knowledge" of the universe that I don't
accept.)
I do not want incredible unsound reasoning, just reasoning that is
marginal, within a margin of safety that I can control. Everyone that
I have know of has as far as I can tell made simplifying assumptions
to make the world tractable. Very rarely do we deal with the world
completely formally. Look at where that got Russell and Whitehead.
I'm just trying to be "honest" about that fact and find ways to
compensate for my own failures.
-Chris
------------------------------
Date: Sun, 25 Jun 2006 10:32:59 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f0868a2e5fe99229896fb@news.altopia.net>
Joachim Durchholz <jo@durchholz.org> wrote:
> Sorry, I have to insist that it's not me who's stretching terms here.
>
> All textbook definitions that I have seen define a type as the
> set/operations/axioms triple I mentioned above.
> No mention of immutability, at least not in the definitions.
The immutability comes from the fact (perhaps implicit in these
textbooks, or perhaps they are not really texts on formal type theory)
that types are assigned to expressions, and the program is not likely to
change as it executes. Even such oddities as "self-modifying code" are
generally formally modeled as a single program, which reduces to other
programs as it evaluates just like everything else. The original
program doesn't change in the formal model.
Hence the common (and, I think, meaningless) distinction that has been
made here: that static type systems assign types to expressions
(sometimes I hear variables, which is limiting and not really correct),
while dynamic type systems do so to values. However, that falls apart
when you understand what formal type systems mean by types. What they
mean, roughly, is "that label which we attach to an expressions
according to fixed rules to help facilitate our proofs". Since dynamic
type systems don't do such proofs, I'm having trouble understanding what
could possibly be meant by assigning types to values, unless we redefine
type. That's what I've been trying to do. So far I've had only limited
success, although there is definite potential in one post by Chris Uppal
and another by Chris Clark (or maybe I'm just partial to other people
named Chris).
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: 25 Jun 2006 19:47:32 +0200
From: Gabriel Dos Reis <gdr@integrable-solutions.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <m3mzc1cekr.fsf@uniton.integrable-solutions.net>
rossberg@ps.uni-sb.de writes:
| Gabriel Dos Reis wrote:
| > |
| > | (Unfortunately, you can hardly write interesting programs in any safe
| > | subset of C.)
| >
| > Fortunately, some people do, as living job.
|
| I don't think so. Maybe the question is what a "safe subset" consists
| of. In my book, it excludes all features that are potentially unsafe.
if you equate "unsafe" with "potentially unsafe", then you have
changed gear and redefined things on the fly, and things that could
be given sense before ceases to have meaning. I decline following
such an uncertain, extreme, path.
| So in particular, C-style pointers are out, because they can easily
| dangle, be uninitialisied, whatever.
sorry, the specific claim I was responding to is not whether *you* can
easily misuse C constructs. I would refrain from generalizing your
inability to write interesting correct programs in C, to a quality of
the language itself. Rather, the claim I was responding to is this:
(Unfortunately, you can hardly write interesting programs in any safe
subset of C.)
I would suggest you give more thoughts to the claims made in
http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html
-- Gaby
------------------------------
Date: Sun, 25 Jun 2006 09:53:53 -0700
From: Scott David Daniels <scott.daniels@acm.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <449eba8d$1@nntp0.pdx.net>
rossberg@ps.uni-sb.de wrote:
> Huh? There is a huge, fundamental difference: namely whether a type
> system is sound or not. A soundness proof is obligatory for any serious
> type theory, and failure to establish it simply is a bug in the theory.
So you claim Java and Objective C are "simply bugs in the theory."
--Scott David Daniels
scott.daniels@acm.org
------------------------------
Date: 25 Jun 2006 10:15:49 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151255749.436492.70680@m73g2000cwd.googlegroups.com>
Joachim Durchholz wrote:
> Anton van Straaten schrieb:
> >> It seems we have languages:
> >> with or without static analysis
> >> with or without runtime type information (RTTI or "tags")
> >> with or without (runtime) safety
> >> with or without explicit type annotations
> >> with or without type inference
> >>
> >> Wow. And I don't think that's a complete list, either.
> >
> > Yup.
>
> What else?
> (Genuinely curious.)
I left off a big one: nominal vs. structural
Also: has subtyping polymorphism or not, has parametric polymorphism or
not.
Marshall
------------------------------
Date: Sun, 25 Jun 2006 11:18:15 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f087344223ab0ab9896fc@news.altopia.net>
Anton van Straaten <anton@appsolutions.com> wrote:
> The problem is that there are no useful sound definitions for the type
> systems (in the static sense) of dynamically-typed languages. Yet, we
> work with type-like static properties in those languages all the time,
> as I've been describing.
I honestly don't find it very compelling that there are similarities
between the kinds of reasoning that goes on in static type systems
versus those used by programmers in dynamically typed languages.
Rather, of course there are similarities. It would be shocking if there
were not similarities. These similarities, though, have nothing to with
the core nature of types.
Basically, there are ways to reason about programs being correct.
Static type systems describe their reasoning (which is always axiomatic
in nature) by assigning "types" to expressions. Programmers in
dynamically typed languages still care about the correctness of their
programs, though, and they find ways to reason about their programs as
well. That reasoning is not completely axiomatic, but we spend an
entire lifetime applying this basic logical system, and it makes sense
that programmers would try to reason from premises to conclusions in
ways similar to a type system. Sometimes they may even ape other type
systems with which they are familiar; but even a programmer who has
never worked in a typed language would apply the same kind of logic as
is used by type systems, because it's a form of logic with which
basically all human beings are familiar and have practiced since the age
of three (disclaimer: I am not a child psychologist).
On the other hand, programmers don't restrict themselves to that kind of
pure axiomatic logic (regardless of whether the language they are
working in is typed). The also reason inductively -- in the informal
sense -- and are satisfied with the resulting high probabilities. They
generally apply intuitions about a problem statement that is almost
surely not written clearly enough to be understood by a machine. And so
forth.
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. 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.
In the same post here, you simultaneously suppose that there's something
inherently informal about the type reasoning in dynamic languages; and
then talk about the type system "in the static sense" of a dynamic
language. How is this possibly consistent?
> We know that we can easily take dynamically-typed program fragments and
> assign them type schemes, and we can make sure that the type schemes
> that we use in all our program fragments use the same type system.
Again, it would be surprising if this were not true. If programmers do,
in fact, tend to reason correctly about their programs, then one would
expect that there are formal proofs that could be found that they are
right. That doesn't make their programming in any way like a formal
proof. I tend to think that a large number of true statements are
provable, and that programmers are good enough to make a large number of
statements true. Hence, I'd expect that it would be possible to find a
large number of true, provable statements in any code, regardless of
language.
> So we actually have quite a bit of evidence about the presence of static
> types in dynamically-typed programs.
No. What we have is quite a bit of evidence about properties remaining
true in dynamically typed programs, which could have been verified by
static typing.
> We're currently discussing something that so far has only been captured
> fairly informally. If we restrict ourselves to only what we can say
> about it formally, then the conversation was over before it began.
I agree with that statement. However, I think the conversation
regarding static typing is also over when you decide that the answer is
to weaken static typing until the word applies to informal reasoning.
If the goal isn't to reach a formal understanding, then the word "static
type" shouldn't be used; and when that is the goal, it still shouldn't
be applied to process that aren't formalized until they manage to become
formalized.
Hopefully, this isn't perceived as too picky. I've already conceded
that we can use "type" in a way that's incompatible with all existing
research literature. I would, however, like to retain some word with
actually has that meaning. Otherwise, we are just going to be
linguistically prevented from discussing it.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: Sun, 25 Jun 2006 17:19:27 GMT
From: "Jürgen Exner" <jurgenex@hotmail.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <zAzng.8068$Wl.2943@trnddc01>
Scott David Daniels wrote:
> rossberg@ps.uni-sb.de wrote:
>> Huh? There is a huge, fundamental difference: namely whether a type
>> system is sound or not. A soundness proof is obligatory for any
>> serious type theory, and failure to establish it simply is a bug in
>> the theory.
>
> So you claim Java and Objective C are "simply bugs in the theory."
They are certainly off topic in CLPM.
jue
------------------------------
Date: Sun, 25 Jun 2006 19:33:02 +0200
From: Joachim Durchholz <jo@durchholz.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7mhbv$52g$1@online.de>
Chris Smith schrieb:
> Joachim Durchholz <jo@durchholz.org> wrote:
>> Sorry, I have to insist that it's not me who's stretching terms here.
>>
>> All textbook definitions that I have seen define a type as the
>> set/operations/axioms triple I mentioned above.
>> No mention of immutability, at least not in the definitions.
>
> The immutability comes from the fact (perhaps implicit in these
> textbooks, or perhaps they are not really texts on formal type theory)
> that types are assigned to expressions,
That doesn't *define* what's a type or what isn't!
If it's impossible to assign types to all expressions of a program in a
language, that does mean that there's no useful type theory for the
program, but it most definitely does not mean that there are no types in
the program.
I can still sensibly talk about sets of values, sets of allowable
operations over each value, and about relationships between inputs and
outputs of these operations.
So programs have types, even if they don't have a static type system.
Q.E.D.
Regards,
Jo
------------------------------
Date: 25 Jun 2006 10:44:40 -0700
From: rossberg@ps.uni-sb.de
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151257480.183097.165640@b68g2000cwa.googlegroups.com>
Gabriel Dos Reis wrote:
> rossberg@ps.uni-sb.de writes:
>
> | Gabriel Dos Reis wrote:
> | > |
> | > | (Unfortunately, you can hardly write interesting programs in any safe
> | > | subset of C.)
> | >
> | > Fortunately, some people do, as living job.
> |
> | I don't think so. Maybe the question is what a "safe subset" consists
> | of. In my book, it excludes all features that are potentially unsafe.
>
> if you equate "unsafe" with "potentially unsafe", then you have
> changed gear and redefined things on the fly, and things that could
> be given sense before ceases to have meaning. I decline following
> such an uncertain, extreme, path.
An unsafe *feature* is one that can potentially exhibit unsafe
behaviour. How else would you define it, if I may ask?
A safe *program* may or may not use unsafe features, but that is not
the point when we talk about safe *language subsets*.
> I would suggest you give more thoughts to the claims made in
>
> http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html
Thanks, I am aware of it. Taking into account the hypothetical nature
of the argument, and all the caveats listed with respect to C, I do not
think that it is too relevant for the discussion at hand. Moreover,
Harper talks about a relative concept of "C-safety". I assume that
everybody here understands that by "safe" in this discussion we mean
something else (in particular, memory safety).
Or are you trying to suggest that we should indeed consider C safe for
the purpose of this discussion?
- Andreas
------------------------------
Date: Sun, 25 Jun 2006 19:52:30 +0200
From: Joachim Durchholz <jo@durchholz.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7migg$7em$1@online.de>
rossberg@ps.uni-sb.de schrieb:
> Joachim Durchholz write:
>> Another observation: type safeness is more of a spectrum than a clearcut
>> distinction. Even ML and Pascal have ways to circumvent the type system,
>
> No. I'm not sure about Pascal,
You'd have to use an untagged union type.
It's the standard maneuver in Pascal to get unchecked bitwise
reinterpretation.
Since it's an undefined behavior, you're essentially on your own, but in
practice, any compilers that implemented a different semantics were
hammered with bug reports until they complied with the standard - in
this case, an unwritten (and very unofficial) one, but a rather
effective one.
> but (Standard) ML surely has none.
NLFFI?
> Same with Haskell as defined by its spec.
Um... I'm not 100% sure, but I dimly (mis?)remember having read that
UnsafePerformIO also offered some ways to circumvent the type system.
(Not that this would be an important point anyway.)
> OCaml has a couple of clearly
> marked unsafe library functions, but no unsafe feature in the language
> semantics itself.
If there's a library with not-typesafe semantics, then at least that
language implementation is not 100% typesafe.
If all implementations of a language are not 100% typesafe, then I
cannot consider the language itself 100% typesafe.
Still, even Pascal is quite a lot "more typesafe" than, say, C.
>> and even C is typesafe unless you use unsafe constructs.
>
> Tautology. Every language is "safe unless you use unsafe constructs".
No tautology - the unsafe constructs aren't just typewise unsafe ;-p
That's exactly why I replaced Luca Cardelli's "safe/unsafe"
"typesafe/not typesafe". There was no definition to the original terms
attached, and this discussion is about typing anyway.
> (Unfortunately, you can hardly write interesting programs in any safe
> subset of C.)
Now that's a bold claim that I'd like to see substantiated.
>> IOW from a type-theoretic point of view, there is no real difference
>> between their typesafe and not typesafe languages in the "statically
>> typed" column; the difference is in the amount of unsafe construct usage
>> in practial programs.
>
> Huh? There is a huge, fundamental difference: namely whether a type
> system is sound or not.
I think you're overstating the case.
In type theory, of course, there's no such things as an "almost typesafe
language" - it's typesafe or it isn't.
In practice, I find no implementation where type mismatches cannot
occur, if only when interfacing with the external world (except if you
cheat by treating everything external as a byte sequence, which is like
saying that all languages have at least a universal ANY type and are
hence statically-typed).
And in those languages that do have type holes, these holes may be more
or less relevant - and it's a *very* broad spectrum here.
And from that perspective, if ML indeed has no type hole at all, then
it's certainly an interesting extremal point, but I still have a
relevant spectrum down to assembly language.
Regards,
Jo
------------------------------
Date: 25 Jun 2006 10:52:13 -0700
From: rossberg@ps.uni-sb.de
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151257933.443578.245450@r2g2000cwb.googlegroups.com>
Scott David Daniels wrote:
> rossberg@ps.uni-sb.de wrote:
> > Huh? There is a huge, fundamental difference: namely whether a type
> > system is sound or not. A soundness proof is obligatory for any serious
> > type theory, and failure to establish it simply is a bug in the theory.
>
> So you claim Java and Objective C are "simply bugs in the theory."
You're misquoting me. What I said is that lack of soundness of a
particular type theory (i.e. a language plus type system) is a bug in
that theory.
But anyway, Java in fact is frequently characterised as having a bogus
type system (e.g. with respect to array subtyping). Of course, in a
hybrid language like Java with its dynamic checks it can be argued
either way.
Naturally, the type system of Objective-C is as broken as the one of
plain C.
- Andreas
------------------------------
Date: Sun, 25 Jun 2006 19:58:27 +0200
From: Joachim Durchholz <jo@durchholz.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7mirk$7s1$1@online.de>
rossberg@ps.uni-sb.de schrieb:
> Gabriel Dos Reis wrote:
>> |
>> | (Unfortunately, you can hardly write interesting programs in any safe
>> | subset of C.)
>>
>> Fortunately, some people do, as living job.
>
> I don't think so. Maybe the question is what a "safe subset" consists
> of. In my book, it excludes all features that are potentially unsafe.
Unless you define "safe", *any* program is unsafe.
Somebody could read the program listing, which could trigger a traumatic
childhood experiece.
(Yes, I'm being silly. But the point is very serious. Even with less
silly examples, whether a language or subset is "safe" entirely depends
on what you define to be "safe", and these definitions tend to vary
vastly across language communities.)
Regards,
Jo
------------------------------
Date: Sun, 25 Jun 2006 20:00:09 +0200
From: Joachim Durchholz <jo@durchholz.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7miuq$7s1$2@online.de>
Pascal Costanza schrieb:
>> Another observation: type safeness is more of a spectrum than a
>> clearcut distinction. Even ML and Pascal have ways to circumvent the
>> type system, and even C is typesafe unless you use unsafe constructs.
>> IOW from a type-theoretic point of view, there is no real difference
>> between their typesafe and not typesafe languages in the "statically
>> typed" column; the difference is in the amount of unsafe construct
>> usage in practial programs.
>
> It's also relevant how straightforward it is to distinguish between safe
> and unsafe code, how explicit you have to be when you use unsafe code,
> how likely it is that you accidentally use unsafe code without being
> aware of it, what the generally accepted conventions in a language
> community are, etc. pp.
Fully agreed.
------------------------------
Date: 6 Apr 2001 21:33:47 GMT (Last modified)
From: Perl-Users-Request@ruby.oce.orst.edu (Perl-Users-Digest Admin)
Subject: Digest Administrivia (Last modified: 6 Apr 01)
Message-Id: <null>
Administrivia:
#The Perl-Users Digest is a retransmission of the USENET newsgroup
#comp.lang.perl.misc. For subscription or unsubscription requests, send
#the single line:
#
# subscribe perl-users
#or:
# unsubscribe perl-users
#
#to almanac@ruby.oce.orst.edu.
NOTE: due to the current flood of worm email banging on ruby, the smtp
server on ruby has been shut off until further notice.
To submit articles to comp.lang.perl.announce, send your article to
clpa@perl.com.
#To request back copies (available for a week or so), send your request
#to almanac@ruby.oce.orst.edu with the command "send perl-users x.y",
#where x is the volume number and y is the issue number.
#For other requests pertaining to the digest, send mail to
#perl-users-request@ruby.oce.orst.edu. Do not waste your time or mine
#sending perl questions to the -request address, I don't have time to
#answer them even if I did know the answer.
------------------------------
End of Perl-Users Digest V10 Issue 9376
***************************************
