[28019] in Perl-Users-Digest
Perl-Users Digest, Issue: 9383 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Mon Jun 26 09:10:14 2006
Date: Mon, 26 Jun 2006 06:10:07 -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 Mon, 26 Jun 2006 Volume: 10 Number: 9383
Today's topics:
Re: What is Expressiveness in a Computer Language <ketil+news@ii.uib.no>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Re: What is Expressiveness in a Computer Language <ketil+news@ii.uib.no>
Re: What is Expressiveness in a Computer Language <ketil+news@ii.uib.no>
Re: What is Expressiveness in a Computer Language <ketil+news@ii.uib.no>
Re: What is Expressiveness in a Computer Language <rossberg@ps.uni-sb.de>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Mon, 26 Jun 2006 10:00:28 +0200
From: Ketil Malde <ketil+news@ii.uib.no>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <eg8xnk1h43.fsf@polarvier.ii.uib.no>
"Rob Thorpe" <robert.thorpe@antenova.com> writes:
>> I think statements like this are confusing, because there are
>> different interpretations of what a "value" is.
> But I mean the value as the semantics of the program itself sees it.
> Which mostly means the datum in memory.
I don't agree with that. Generally, a language specifies a virtual
machine and doesn't need to concern itself with things like "memory"
at all. Although langauges like C tries to, look at all the undefined
behavior you get when you make assumptions about memory layout etc.
Memory representation is just an artifact of a particular
implementation of the language for a particular architecture.
-k
--
If I haven't seen further, it is by standing in the footprints of giants
------------------------------
Date: Mon, 26 Jun 2006 01:58:51 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f0941a792c24922989708@news.altopia.net>
Anton van Straaten <anton@appsolutions.com> wrote:
> 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.
Let me be clear, then. I am far less agreeable than you that this
couldn't be called a type system. One of my goals here is to try to
understand, if we are going to work out what can and can't be called a
type system in human thought, how we can possible draw a boundary
between kinds of logic and say that one of them is a type system while
the other is not. I haven't seen much of a convincing way to do it.
The only things that I can see rejecting out of hand are the empirical
things; confidence gained through testing or observation of the program
in a debugger. Everything else seems to qualify, and that's the
problem.
So let's go ahead and agree about everything up until...
[...]
> As an initial next step, we could simply rely on the good old universal
> type everywhere else in the program - it ought to be possible to make
> the program well-typed in that case, it would just mean that the
> provable properties would be nowhere near as pervasive as with a
> traditional statically-typed program.
It would, in fact, mean that interesting provable properties would only
be provable if data can't flow outside of those individual small bits
where the programmer reasoned with types. Of course that's not true, or
the programmer wouldn't have written the rest of the program in the
first place. If we define the universal type as a variant type
(basically, tagged or something like it, so that the type can be tested
at runtime) then certain statements become provable, of the form "either
X or some error condition is raised because a value is inappropriate".
That is indeed a very useful property; but wouldn't it be easier to
simply prove it by appealing to the language semantics that say that "if
not X, the operation raises an exception," or to the existence of
assertions within the function that verify X, or some other such thing
(which must exist, or the statement wouldn't be true)?
> But the point is we would now
> have put our types into a formal context.
Yes, but somewhat vacuously so...
> The point about inherent informality is just that if you fully formalize
> a static type system for a dynamic language, such that entire programs
> can be statically typed, you're likely to end up with a static type
> system with the same disadvantages that the dynamic language was trying
> to avoid.
Okay, so you've forced the admission that you have a static type system
that isn't checked and doesn't prove anything interesting. If you
extended the static type system to cover the whole program, then you'd
have a statically typed language that lacks an implementation of the
type checker.
I don't see what we lose in generality by saying that the language lacks
a static type system, since it isn't checked, and doesn't prove anything
anyway. The remaining statement is that the programmer may use static
types to reason about the code. But, once again, the problem here is
that I don't see any meaning to that. It would basically mean the same
thing as that the programmer may use logic to reason about code. That
isn't particularly surprising to me. I suppose this is why I'm
searching for what is meant by saying that programmers reason about
types, and am having that conversation in several places throughout this
thread... because otherwise, it doesn't make sense to point out that
programmers reason with types.
> Well, I'm trying to use the term "latent type", as a way to avoid the
> ambiguity of "type" alone, to distinguish it from "static type", and to
> get away from the obvious problems with "dynamic type".
I replied to your saying something to Marshall about the "type systems
(in the static sense) of dynamically-typed languages." That's what my
comments are addressing. If you somehow meant something other than the
static sense, then I suppose this was all a big misunderstanding.
> But I'm much less interested in the term itself than in the issues
> surrounding dealing with "real" types in dynamically-checked programs -
> if someone had a better term, I'd be all in favor of it.
I will only repeat again that in static type systems, the "type" becomes
a degenerate concept when it is removed from the type system. It is
only the type system that makes something a type. Therefore, if you
want "real" types, then my first intuition is that you should avoid
looking in the static types of programming languages. At best, they
happen to coincide frequently with "real" types, but that's only a
pragmatic issue if it means anything at all.
> So when well-typed program fragments are considered as part of a larger
> untyped program, you're suggesting that this so radically changes the
> picture, that we can no longer distinguish the types we identified as
> being anything beyond programmer reasoning in general?
Is this so awfully surprising, when the type system itself is just
programmer reasoning? When there ceases to be anything that's provable
about the program, there also ceases to be anything meaningful about the
type system. You still have the reasoning, and that's all you ever had.
You haven't really lost anything, except a name for it. Since I doubt
the name had much meaning at all (as explained above), I don't count
that as a great loss. If you do, though, then this simple demonstrates
that you didn't really mean "type systems (in the static sense)".
> > 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.
>
> Not *all* research literature. There's literature on various notions of
> dynamic type.
I haven't seen it, but I'll take your word that some of it exists. I
wouldn't tend to read research literature on dynamic types, so that
could explain the discrepancy.
> > 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.
>
> For now, you're probably stuck with "static type".
That's fine. I replied to your attempting to apply "static type" in a
sense where it doesn't make sense.
> In CS, we don't have the luxury
> of using the classic mathematician's excuse when confronted with
> inconvenient philosophical issues, of claiming that type theory is just
> a formal symbolic game, with no meaning outside the formalism.
As it turns out, my whole purpose here is to address the idea that type
theory for programming languages is limited to some subset of problems
which people happen to think of as type problems. If type theorists
fourty years ago had limited themselves to considering what people
thought of as types back then, we'd be in a considerably worse position
today with regard to the expressive power of types in commonly used
programming languages. Hence, your implication that insisting on a
formal rather than intuitive definition is opposed to the real-world
usefulness of the field is actually rather ironic. The danger lies in
assuming that unsolved problems are unsolvable, and therefore defining
them out of the discussion until the very idea that someone would solve
that problem with these techniques starts to seem strange.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: Mon, 26 Jun 2006 11:48:40 +0200
From: Ketil Malde <ketil+news@ii.uib.no>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <eg4py81c3r.fsf@polarvier.ii.uib.no>
Chris Smith <cdsmith@twu.net> writes:
> I've since abandoned any attempt to be picky about use of the word
> "type". That was a mistake on my part. I still think it's legitimate
> to object to statements of the form "statically typed languages X, but
> dynamically typed languages Y", in which it is implied that Y is
> distinct from X. When I used the word "type" above, I was adopting the
> working definition of a type from the dynamic sense.
Umm...what *is* the definition of a "dynamic type"? In this thread
it's been argued from tags and memory representation to (almost?)
arbitrary predicates.
> That is, I'm considering whether statically typed languages may be
> considered to also have dynamic types, and it's pretty clear to me
> that they do.
Well, if you equate tags with dynamic types:
data Universal = Str String | Int Integer | Real Double
| List [Universal] ...
A pattern match failure can then be seen as a dynamic type error.
Another question is how to treat a system (and I think C++'s RTTI
qualifies, and probably related languages like Java) where static type
information is available at runtime. Does this fit with the term
"dynamic typing" with "typing" in the same sense as "static typing"?
-k
--
If I haven't seen further, it is by standing in the footprints of giants
------------------------------
Date: Mon, 26 Jun 2006 12:13:58 +0200
From: Ketil Malde <ketil+news@ii.uib.no>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <egy7vkz0k9.fsf@polarvier.ii.uib.no>
Chris Smith <cdsmith@twu.net> writes:
> Joachim Durchholz <jo@durchholz.org> wrote:
>> Assume a language that
>> a) defines that a program is "type-correct" iff HM inference establishes
>> that there are no type errors
>> b) compiles a type-incorrect program anyway, with an establishes
>> rigorous semantics for such programs (e.g. by throwing exceptions as
>> appropriate).
> So the compiler now attempts to prove theorems about the program, but
> once it has done so it uses the results merely to optimize its runtime
> behavior and then throws the results away.
Hmm... here's my compiler front end (for Haskell or other languages
that ..er.. define 'undefined'):
while(type error) {
replace an incorrectly typed function with 'undefined'
}
Wouldn't the resulting program still be statically typed?
In practice I prefer to (and do) define troublesome functions as
'undefined' manually during development.
-k
--
If I haven't seen further, it is by standing in the footprints of giants
------------------------------
Date: Mon, 26 Jun 2006 12:42:43 +0200
From: Ketil Malde <ketil+news@ii.uib.no>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <egodwgyz8c.fsf@polarvier.ii.uib.no>
Anton van Straaten <anton@appsolutions.com> writes:
> But a program as seen by the programmer has types: the programmer
> performs (static) type inference when reasoning about the program, and
> debugs those inferences when debugging the program, finally ending up
> with a program which has a perfectly good type scheme.
I'd be tempted to go further, and say that the programmer performs
(informally, incompletely, and probably incorrectly ) a proof of
correctness, and that type correctness is just a part of general
correctness.
-k
--
If I haven't seen further, it is by standing in the footprints of giants
------------------------------
Date: Mon, 26 Jun 2006 13:35:40 +0200
From: Andreas Rossberg <rossberg@ps.uni-sb.de>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7ogqc$99fn4$1@hades.rz.uni-saarland.de>
Gabriel Dos Reis wrote:
> rossberg@ps.uni-sb.de writes:
>
> | think that it is too relevant for the discussion at hand. Moreover,
> | Harper talks about a relative concept of "C-safety".
>
> Then, I believe you missed the entire point.
I think the part of my reply you snipped addressed it well enough.
Anyway, I can't believe that we actually need to argue about the fact
that - for any *useful* and *practical* notion of safety - C is *not* a
safe language. I refrain from continuing the discussion along this line,
because *that* is *really* silly.
- Andreas
------------------------------
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 9383
***************************************
