[27991] in Perl-Users-Digest
Perl-Users Digest, Issue: 9355 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Fri Jun 23 09:15:16 2006
Date: Fri, 23 Jun 2006 06:15:09 -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 Fri, 23 Jun 2006 Volume: 10 Number: 9355
Today's topics:
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 <pc@p-cos.net>
Re: What is Expressiveness in a Computer Language <piet@cs.uu.nl>
Re: What is Expressiveness in a Computer Language <pc@p-cos.net>
Re: What is Expressiveness in a Computer Language <chris.uppal@metagnostic.REMOVE-THIS.org>
Re: What is Expressiveness in a Computer Language <chris.uppal@metagnostic.REMOVE-THIS.org>
Re: What is Expressiveness in a Computer Language <chris.uppal@metagnostic.REMOVE-THIS.org>
Re: What is Expressiveness in a Computer Language <anton@appsolutions.com>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Fri, 23 Jun 2006 12:02:36 +0200
From: Andreas Rossberg <rossberg@ps.uni-sb.de>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7ge7s$90ukl$2@hades.rz.uni-saarland.de>
David Hopwood wrote:
>>
>>"Values" refers to the concrete values existent in the semantics of a
>>programming language. This set is usually infinite, but basically fixed.
>>To describe the set of "values" of an abstract type you would need
>>"fresh" values that did not exist before (otherwise the abstract type
>>would be equivalent to some already existent type). So you'd need at
>>least a theory for name generation or something similar to describe
>>abstract types in a types-as-sets metaphor.
>
> Set theory has no difficulty with this. It's common, for example, to see
> "the set of strings representing propositions" used in treatments of
> formal systems.
Oh, I was not saying that this particular aspect cannot be described in
set theory (that was a different argument, about different issues). Just
that you cannot naively equate types with a set of underlying values,
which is what is usually meant by the types-are-sets metaphor - to
capture something like type abstraction you need to do more. (Even then
it might be arguable if it really describes the same thing.)
- Andreas
------------------------------
Date: Fri, 23 Jun 2006 13:41:47 +0200
From: Pascal Costanza <pc@p-cos.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <449BD37B.10904@p-cos.net>
Marshall wrote:
> I am sceptical of the idea that when programming in a dynamically
> typed language one doesn't have to think about both models as well.
> I don't have a good model of the mental process of working
> in a dynamically typed language, but how could that be the case?
> (I'm not asking rhetorically.) Do you then run your program over
> and over, mechanically correcting the code each time you discover
> a type error? In other words, if you're not thinking of the type model,
> are you using the runtime behavior of the program as an assistant,
> the way I use the static analysis of the program as an assistant?
Yes.
> I don't accept the idea about pairing the appropriateness of each
> system according to whether one is doing exploratory programming.
> I do exploratory programming all the time, and I use the static type
> system as an aide in doing so. Rather I think this is just another
> manifestation of the differences in the mental processes between
> static typed programmers and dynamic type programmers, which
> we are beginning to glimpse but which is still mostly unknown.
Probably.
> Oh, and I also want to say that of all the cross-posted mega threads
> on static vs. dynamic typing, this is the best one ever. Most info;
> least flames. Yay us!
Yay! :)
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
------------------------------
Date: Fri, 23 Jun 2006 13:46:47 +0200
From: Pascal Costanza <pc@p-cos.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <4g22l7F1j8p4mU1@individual.net>
Marshall wrote:
> Pascal Costanza wrote:
>> Consider a simple expression like 'a + b': In a dynamically typed
>> language, all I need to have in mind is that the program will attempt to
>> add two numbers. In a statically typed language, I additionally need to
>> know that there must a guarantee that a and b will always hold numbers.
>
> I still don't really see the difference.
>
> I would not expect that the dynamic programmer will be
> thinking that this code will have two numbers most of the
> time but sometimes not, and fail. I would expect that in both
> static and dynamic, the thought is that that code is adding
> two numbers, with the difference being the static context
> gives one a proof that this is so.
There is a third option: it may be that at the point where I am writing
this code, I simply don't bother yet whether a and b will always be
numbers. In case something other than numbers pop up, I can then make a
decision how to proceed from there.
> In this simple example,
> the static case is better, but this is not free, and the cost
> of the static case is evident elsewhere, but maybe not
> illuminated by this example.
Yes, maybe the example is not the best one. This kind of example,
however, occurs quite often when programming in an object-oriented
style, where you don't know yet what objects will and will not respond
to a message / generic function. Even in the example above, it could be
that you can give an appropriate definition for + for objects other than
numbers.
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
------------------------------
Date: Fri, 23 Jun 2006 13:37:25 +0200
From: Piet van Oostrum <piet@cs.uu.nl>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <m2mzc4drwq.fsf@ordesa.cs.uu.nl>
>>>>> "Marshall" <marshall.spight@gmail.com> (M) wrote:
>M> Torben Ęgidius Mogensen wrote:
>>>
>>> That's not true. ML has variables in the mathematical sense of
>>> variables -- symbols that can be associated with different values at
>>> different times. What it doesn't have is mutable variables (though it
>>> can get the effect of those by having variables be immutable
>>> references to mutable memory locations).
>M> While we're on the topic of terminology, here's a pet peeve of
>M> mine: "immutable variable."
>M> immutable = can't change
>M> vary-able = can change
>M> Clearly a contradiction in terms.
I would say that immutable = 'can't *be* changed' rather than 'can't
change'. But I am not a native English speaker.
Compare with this: the distance of the Earth to Mars is variable (it
varies), but it is also immutable (we can't change it).
--
Piet van Oostrum <piet@cs.uu.nl>
URL: http://www.cs.uu.nl/~piet [PGP 8DAE142BE17999C4]
Private email: piet@vanoostrum.org
------------------------------
Date: Fri, 23 Jun 2006 14:01:51 +0200
From: Pascal Costanza <pc@p-cos.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <4g23hgF1l4434U1@individual.net>
Marshall wrote:
> Joe Marshall wrote:
>> That's the important point: I want to run broken code.
>
> I want to make sure I understand. I can think of several things
> you might mean by this. It could be:
> 1) I want to run my program, even though I know parts of it
> are broken, because I think there are parts that are not broken
> and I want to try them out.
> 2) I want to run my program, even though it is broken, and I
> want to run right up to a broken part and trap there, so I can
> use the runtime facilities of the language to inspect what's
> going on.
>
>
>> I want to run
>> as much of the working fragments as I can, and I want a `safety net' to
>> prevent me from performing undefined operations, but I want the safety
>> net to catch me at the *last* possible moment.
>
> This statement is interesting, because the conventional wisdom (at
> least as I'm used to hearing it) is that it is best to catch bugs
> at the *first* possible moment. But I think maybe we're talking
> about different continua here. The last last last possible moment
> is after the software has shipped to the customer, and I'm pretty
> sure that's not what you mean. I think maybe you mean something
> more like 2) above.
Nowadays, we have more options wrt what it means to "ship" code. It
could be that your program simply runs as a (web) service to which you
have access even after the customer has started to use the program. See
http://www.paulgraham.com/road.html for a good essay on this idea.
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
------------------------------
Date: Fri, 23 Jun 2006 11:55:04 +0100
From: "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <449bde5e$1$663$bed64819@news.gradwell.net>
Andreas Rossberg wrote:
> Chris Uppal wrote:
> >
> > > > It's worth noting, too, that (in some sense) the type of an object
> > > > can change over time[*].
> > >
> > > No. Since a type expresses invariants, this is precisely what may
> > > *not* happen. If certain properties of an object may change then the
> > > type of
> > > the object has to reflect that possibility. Otherwise you cannot
> > > legitimately call it a type.
> >
> > Well, it seems to me that you are /assuming/ a notion of what kinds of
> > logic can be called type (theories), and I don't share your
> > assumptions. No offence intended.
>
> OK, but can you point me to any literature on type theory that makes a
> different assumption?
'Fraid not. (I'm not a type theorist -- for all I know there may be lots, but
my suspicion is that they are rare at best.)
But perhaps I shouldn't have used the word theory at all. What I mean is that
there is one or more logic of type (informal or not -- probably informal) with
respect to which the object in question has changed it categorisation. If no
existing type /theory/ (as devised by type theorists) can handle that case,
then that is a deficiency in the set of existing theories -- we need newer and
better ones.
But, as a sort of half-way, semi-formal, example: consider the type environment
in a Java runtime. The JVM does formal type-checking of classfiles as it loads
them. In most ways that checking is static -- it's treating the bytecode as
program text and doing a static analysis on it before allowing it to run (and
rejecting what it can't prove to be acceptable by its criteria). However, it
isn't /entirely/ static because the collection of classes varies at runtime in
a (potentially) highly dynamic way. So it can't really examine the "whole"
text of the program -- indeed there is no such thing. So it ends up with a
hybrid static/dynamic type system -- it records any assumptions it had to make
in order to find a proof of the acceptability of the new code, and if (sometime
in the future) another class is proposed which violates those assumptions, then
that second class is rejected.
> > I see no reason,
> > even in practise, why a static analysis should not be able to see that
> > the set of acceptable operations (for some definition of acceptable)
> > for some object/value/variable can be different at different times in
> > the execution.
>
> Neither do I. But what is wrong with a mutable reference-to-union type,
> as I suggested? It expresses this perfectly well.
Maybe I misunderstood what you meant by union type. I took it to mean that the
type analysis didn't "know" which of the two types was applicable, and so would
reject both (or maybe accept both ?). E..g if at instant A some object, obj,
was in a state where it to responds to #aMessage, but not #anotherMessage; and
at instant B it is in a state where it responds to #anotherMessage but not
#aMessage. In my (internal and informal) type logic, make the following
judgements:
In code which will be executed at instant A
obj aMessage. "type correct"
obj anotherMessage. "type incorrect"
In code which will be executed at instant B
obj aMessage. "type incorrect"
obj anotherMessage. "type correct"
I don't see how a logic with no temporal element can arrive at all four those
judgements, whatever it means by a union type.
-- chris
------------------------------
Date: Fri, 23 Jun 2006 13:11:53 +0100
From: "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <449bde5f$1$663$bed64819@news.gradwell.net>
Anton van Straaten wrote:
> In that case, you could say that the conceptual type is different than
> the inferred static type. But most of the time, the human is reasoning
> about pretty much the same types as the static types that Haskell
> infers. Things would get a bit confusing otherwise.
Or any mechanised or formalised type system, for any language. If a system
doesn't match pretty closely with at least part of the latent type systems (in
your sense) used by the programmers, then that type system is useless.
(I gather that it took, or maybe is still taking, theorists a while to get to
grips with the infromal type logics which were obvious to working OO
programmers.)
-- chris
------------------------------
Date: Fri, 23 Jun 2006 13:21:46 +0100
From: "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <449bde5f$2$663$bed64819@news.gradwell.net>
David Hopwood wrote:
> > But some of the advocates of statically
> > typed languages wish to lump these languages together with assembly
> > language a "untyped" in an attempt to label them as unsafe.
>
> A common term for languages which have defined behaviour at run-time is
> "memory safe". For example, "Smalltalk is untyped and memory safe."
> That's not too objectionable, is it?
I find it too weak, as if to say: "well, ok, it can't actually corrupt memory
as such, but the program logic is still apt go all over the shop"...
-- chris
------------------------------
Date: Fri, 23 Jun 2006 12:37:31 GMT
From: Anton van Straaten <anton@appsolutions.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <fgRmg.155793$F_3.69979@newssvr29.news.prodigy.net>
rossberg@ps.uni-sb.de wrote:
> I very much agree with the observation that every programmer performs
> "latent typing" in his head
Great!
> (although Pascal Constanza's seems to have
> the opposite opinion).
I'll have to catch up on that.
> But I also think that "latently typed language" is not a meaningful
> characterisation. And for the very same reason! Since any programming
> activity involves latent typing - naturally, even in assembler! - it
> cannot be attributed to any language in particular, and is hence
> useless to distinguish between them. (Even untyped lambda calculus
> would not be a counter-example. If you really were to program in it,
> you certainly would think along lines like "this function takes two
> chuch numerals and produces a third one".)
Vesa raised a similar objection in his post 'Saying "latently typed
language" is making a category mistake'. I've made some relevant
responses to that post.
I agree that there's a valid point in the sense that latent types are
not a property of the semantics of the languages they're associated with.
But to take your example, I've had the pleasure of programming a little
in untyped lambda calculus. I can tell you that not having tags is
quite problematic. You certainly do perform latent typing in your head,
but without tags, the language doesn't provide any built-in support for
it. You're on your own.
I'd characterize this as being similar to other situations in which a
language has explicit support for some programming style (e.g. FP or
OO), vs. not having such support, so that you have to take steps to fake
it. The style may be possible to some degree in either case, but it's
much easier if the language has explicit support for it.
Dynamically-typed languages provide support for latent typing. Untyped
lambda calculus and assembler don't provide such support, built-in.
However, I certainly don't want to add to confusion about things like
this. I'm open to other ways to describe these things. Part of where
"latently-typed language" comes from is as an alternative to
"dynamically-typed language" -- an alternative with connotations that
I'm suggesting should be more compatible with type theory.
> I hear you when you define latently typed languages as those that
> support the programmer's latently typed thinking by providing dynamic
> tag checks. But in the very same post (and others) you also explain in
> length why these tags are far from being actual types. This seems a bit
> contradictory to me.
I don't see it as contradictory. Tags are a mechanism. An individual
tag is not a type. But together, tags help check types. More below:
> As Chris Smith points out, these dynamic checks are basically a
> necessaity for a well-defined operational semantics. You need them
> whenever you have different syntactic classes of values, but lack a
> type system to preclude interference. They are just an encoding for
> differentiating these syntactic classes. Their connection to types is
> rather coincidential.
Oooh, I think I'd want to examine that "coincidence" very closely. For
example, *why* do we have different syntactic classes of values in the
first place? I'd say that we have them precisely to support type-like
reasoning about programs, even in the absence of a formal static type
system.
If you're going to talk about "syntactic classes of values" in the
context of latent types, you need to consider how they relate to latent
types. Syntactic classes of values relate to latent types in a very
similar way to that in which static types do.
One difference is that since latent types are not automatically
statically checked, checks have to happen in some other way. That's
what checks of tags are for.
Chris Smith's observation was made in a kind of deliberate void: one in
which the existence of anything like latent types is discounted, on the
grounds that they're informal. If you're willing to acknowledge the
idea of latent types, then you can reinterpret the meaning of tags in
the context of latent types. In that context, tags are part of the
mechanism which checks latent types.
Anton
------------------------------
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 9355
***************************************
