[28008] in Perl-Users-Digest
Perl-Users Digest, Issue: 9372 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Sun Jun 25 00:05:44 2006
Date: Sat, 24 Jun 2006 21:05:03 -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 Sat, 24 Jun 2006 Volume: 10 Number: 9372
Today's topics:
Re: Hash of Arrays <tadmc@augustmail.com>
Newbie precompile/PPM question <qbert@comcast.net>
Re: Newbie precompile/PPM question <john@castleamber.com>
Re: Newbie precompile/PPM question <qbert@comcast.net>
Re: Perl core support for inside-out classes <rvtol+news@isolution.nl>
Re: Regex: Exact semantics of ^ and $ when using /m <mumia.w.18.spam+nospam.usenet@earthlink.net>
Re: Saying "latently-typed language" is making a catego <find@my.address.elsewhere>
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 <cfc@shell01.TheWorld.com>
Re: What is Expressiveness in a Computer Language <marshall.spight@gmail.com>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Sat, 24 Jun 2006 17:08:30 -0500
From: Tad McClellan <tadmc@augustmail.com>
Subject: Re: Hash of Arrays
Message-Id: <slrne9rduu.1em.tadmc@magna.augustmail.com>
Deepu <pradeep.bg@gmail.com> wrote:
> Hi James,
Huh?
> Thanks a lot for helping me on this.
Please learn the proper way of composing a followup.
Please do this very very soon.
> Peter J. Holzer wrote:
>> Tad McClellan wrote:
>> > John W. Krahn <someone@example.com> wrote:
>> >> Deepu wrote:
Errr, no "James" there...
[snip the rest of the vile TOFU]
--
Tad McClellan SGML consulting
tadmc@augustmail.com Perl programming
Fort Worth, Texas
------------------------------
Date: Sat, 24 Jun 2006 20:27:38 -0400
From: "Jockser" <qbert@comcast.net>
Subject: Newbie precompile/PPM question
Message-Id: <Dp6dndfEQPboRQDZnZ2dnUVZ_tadnZ2d@comcast.com>
Hello, I'm trying to install Template-Toolkit-2.15.
This is my first time dealling with Perl and have only done a very little
with VB, and Jscript before. I've noticed that the normail instructions for
installing it fail due to me running on a WinXP system. I think I have to
use a precompiled version of Template Tookit to get it installed via PPM but
I'm coming up short on where to down load a precompiled version.
If someone could tell me where to get a precompiled version, or how to
compile it myself, or if I'm off my rocker and just need to do something
totally different to get this thing work, that would be great.
Thanks
------------------------------
Date: 25 Jun 2006 01:55:43 GMT
From: John Bokma <john@castleamber.com>
Subject: Re: Newbie precompile/PPM question
Message-Id: <Xns97ECD4E52E787castleamber@130.133.1.4>
"Jockser" <qbert@comcast.net> wrote:
> Hello, I'm trying to install Template-Toolkit-2.15.
> This is my first time dealling with Perl and have only done a very
> little with VB, and Jscript before. I've noticed that the normail
> instructions for installing it fail due to me running on a WinXP
> system. I think I have to use a precompiled version of Template
> Tookit to get it installed via PPM but I'm coming up short on where to
> down load a precompiled version.
>
> If someone could tell me where to get a precompiled version, or how to
> compile it myself, or if I'm off my rocker and just need to do
> something totally different to get this thing work, that would be
> great.
C:\>ppm install http://theoryx5.uwinnipeg.ca/ppms/Template-Toolkit.ppd
might do the trick.
--
John Bokma Freelance software developer
&
Experienced Perl programmer: http://castleamber.com/
------------------------------
Date: Sat, 24 Jun 2006 23:57:13 -0400
From: "Jockser" <qbert@comcast.net>
Subject: Re: Newbie precompile/PPM question
Message-Id: <AK2dndxVKoYFlAPZnZ2dnUVZ_s-dnZ2d@comcast.com>
Thanks for the try John, but it seems to point back out to a URL that
doesn't have the package any more
Here is what I get.
ppm> install http://theoryx5.uwinnipeg.ca/ppms/Template-Toolkit.p
Error: Failed to download URL
http://openinteract.sourceforge.net/AppConfig.ppd: 404 Not Found
Also AppConfig is a requirement for Template Toolkit so I tried to install
it via http://theoryx5.uwinnipeg.ca/ppms/
Here is what I get with that one:
ppm> install http://theoryx5.uwinnipeg.ca/ppms/appconfig.ppd
Error: Failed to download URL
http://theoryx5.uwinnipeg.ca/ppms/appconfig.ppd: 404 Not Found
Looks like I'll have to keep hunting or figure out a way to create this PPM
some how with the normal source.
Anyone have any suggestions?
Thanks
"John Bokma" <john@castleamber.com> wrote in message
news:Xns97ECD4E52E787castleamber@130.133.1.4...
> "Jockser" <qbert@comcast.net> wrote:
>
>> Hello, I'm trying to install Template-Toolkit-2.15.
>> This is my first time dealling with Perl and have only done a very
>> little with VB, and Jscript before. I've noticed that the normail
>> instructions for installing it fail due to me running on a WinXP
>> system. I think I have to use a precompiled version of Template
>> Tookit to get it installed via PPM but I'm coming up short on where to
>> down load a precompiled version.
>>
>> If someone could tell me where to get a precompiled version, or how to
>> compile it myself, or if I'm off my rocker and just need to do
>> something totally different to get this thing work, that would be
>> great.
>
> C:\>ppm install http://theoryx5.uwinnipeg.ca/ppms/Template-Toolkit.ppd
>
> might do the trick.
>
> --
> John Bokma Freelance software developer
> &
> Experienced Perl programmer: http://castleamber.com/
------------------------------
Date: Sun, 25 Jun 2006 00:22:47 +0200
From: "Dr.Ruud" <rvtol+news@isolution.nl>
Subject: Re: Perl core support for inside-out classes
Message-Id: <e7kl22.1d0.1@news.isolution.nl>
Anno Siegel schreef:
> As of v5.10 Perl will provide support for inside-out classes in form
> of a new core module Hash::Util::FieldHash. It is already available
> in the current bleadperl.
>
> Inside-out classes store object data in hashes keyed by the object.
> That way each field of a class is realized as one lexical hash which
> may thus be called a field hash.
>
> Normal hashes have a number of disadvantages in this approach. For
> one, references are stringified when used as hash keys, but the
> stringification depends on the bless status of the reference. After
> a re-bless of an object, its data would be lost (not to mention
> overloaded stringification). This is usually corrected by calling the
> function Scalar::Util::Refaddr (or some equivalent) before a
> refrerence is used as a hash key.
>
> Another problem is that hash entries don't go away when objects go out
> of scope. This leads to an obvious memory leak. Even worse, objects
> are re-used by the perl interpreter, and if the field hashes aren't
> cleaned up, a new object may accidentally access data that had been
> used by its earlier incarnation. So an inside-out class based on
> standard hashes *must* have a DESTROY method which needs some infra-
> structure to work.
>
> A third problem is threads. When a new thread is created, the entire
> perl interpreter is cloned. That means that in the new thread all
> variables will have new reference addresses. So objects will lose
> their data across threads, unless the class has a CLONE method to
> correct that. It turns out that CLONE needs much the same infra-
> structure as garbage collection.
>
> With Hash::Util::FieldHash you can declare a new type of hash that
> takes care of these problems. The stringification of keys as their
> decimal reference address is built into these hashes. Furthermore,
> field hashes are garbage-collected and thread-safe so that a class
> built with field hashes can safely run without DESTROY and
> CLONE methods. That simplifies the construction considerably.
>
> The documentation of Hash::Util::FieldHash can be seen at
> http://www.tu-berlin.de/zrz/mitarbeiter/anno4000/clpm/FieldHash.html
>
> Inside-out classes have a fourth problem, which is serialization
> and persistence. Tools like Data::Dumper and Storable don't save,
> restore or show the data of an inside-out object, they know nothing
> about that. Hash::Util::FieldHash doesn't address this problem.
> I am planning a (non-core) module for CPAN, probably Class::Field
> (based on FieldHash) that makes inside-out classes that are
> constructed with it viewable, dumpable and restorable.
Almost as great as Argentina - Mexico. <g>
Thanks!
--
Affijn, Ruud
"Gewoon is een tijger."
------------------------------
Date: Sat, 24 Jun 2006 23:40:04 GMT
From: "Mumia W." <mumia.w.18.spam+nospam.usenet@earthlink.net>
Subject: Re: Regex: Exact semantics of ^ and $ when using /m
Message-Id: <o3kng.11650$o4.4436@newsread2.news.pas.earthlink.net>
Dr.Ruud wrote:
> Mumia W. schreef:
>
>> ^ only matches the beginning of a line when it appears at the
>> beginning of the RE, and $ only matches the end of a line when it
>> appears at the end of the RE.
>
>
> No.
>
> perl -wle '"a\nb" =~ /a$(?:\n)^b/m and print 1'
>
> perl -wle '"a\nb" =~ / a $ \n ^ b /mx and print 1'
>
> perl -wle '"a\nb" =~ / a $ \s ^ b /mx and print 1'
>
> perl -wle '"a\nb" =~ / a $ (?:[^^]) ^ b /mx and print 1'
>
> etc.
>
Hmm, it seems I was wrong about "^"; thanks.
------------------------------
Date: Sat, 24 Jun 2006 21:54:08 -0500
From: Matthias Blume <find@my.address.elsewhere>
Subject: Re: Saying "latently-typed language" is making a category mistake
Message-Id: <m2veqq6j3j.fsf@hanabi.local>
David Hopwood <david.nospam.hopwood@blueyonder.co.uk> writes:
> Patricia Shanahan wrote:
>> Vesa Karvonen wrote:
>> ...
>>
>>> An example of a form of informal reasoning that (practically) every
>>> programmer does daily is termination analysis. There are type systems
>>> that guarantee termination, but I think that is fair to say that it is
>>> not yet understood how to make a practical general purpose language, whose
>>> type system would guarantee termination (or at least I'm not aware of
>>> such a language). It should also be clear that termination analysis need
>>> not be done informally. Given a program, it may be possible to formally
>>> prove that it terminates.
>>
>> To make the halting problem decidable one would have to do one of two
>> things: Depend on memory size limits, or have a language that really is
>> less expressive, at a very deep level, than any of the languages
>> mentioned in the newsgroups header for this message.
>
> I don't think Vesa was talking about trying to solve the halting problem.
>
> A type system that required termination would indeed significantly restrict
> language expressiveness -- mainly because many interactive processes are
> *intended* not to terminate.
Most interactive processes are written in such a way that they
(effectively) consist of an infinitely repeated application of some
function f that maps the current state and the input to the new state
and the output.
f : state * input -> state * output
This function f itself has to terminate, i.e., if t has to be
guaranteed that after any given input, there will eventually be an
output. In most interactive systems the requirements are in fact much
stricter: the output should come "soon" after the input has been
received.
I am pretty confident that the f for most (if not all) existing
interactive systems could be coded in a language that enforces
termination. Only the loop that repeatedly applies f would have to be
coded in a less restrictive language.
------------------------------
Date: Sat, 24 Jun 2006 22:39:23 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <vajng.477125$xt.438414@fe3.news.blueyonder.co.uk>
Anton van Straaten wrote:
> David Hopwood wrote:
>
>> I can accept that dynamic tagging provides some support for latent typing
>> performed "in the programmer's head". But that still does not mean that
>> dynamic tagging is the same thing as latent typing
>
> No, I'm not saying it is, although I am saying that the former supports
> the latter.
But since the relevant feature that the languages in question possess is
dynamic tagging, it is more precise and accurate to use that term to
describe them.
Also, dynamic tagging is only a minor help in this respect, as evidenced
by the fact that explicit tag tests are quite rarely used by most programs,
if I'm not mistaken. IMHO, the support does not go far enough for it to be
considered a defining characteristic of these languages.
When tag tests are used implicitly by other language features such as
pattern matching and dynamic dispatch, they are used for purposes that are
equally applicable to statically typed and non-(statically-typed) languages.
>> or that languages
>> that use dynamic tagging are "latently typed". This simply is not a
>> property of the language (as you've already conceded).
>
> Right. I see at least two issues here: one is that as a matter of
> shorthand, compressing "language which supports latent typing" to
> "latently-typed language" ought to be fine, as long as the term's
> meaning is understood.
If, for the sake of argument, "language which supports latent typing" is
to be compressed to "latently-typed language", then statically typed
languages must be considered also latently typed.
After all, statically typed languages support expression and
verification of the "types in the programmer's head" at least as well
as non-(statically-typed) languages do. In particular, most recent
statically typed OO languages use dynamic tagging and are memory safe.
And they support comments ;-)
This is not, quite obviously, what most people mean when they say
that a particular *language* is "latently typed". They almost always
mean that the language is dynamically tagged, *not* statically typed,
and memory safe. That is how this term is used in R5RS, for example.
> But beyond that, there's an issue here about the definition of "the
> language". When programming in a latently-typed language, a lot of
> action goes on outside the language - reasoning about static properties
> of programs that are not captured by the semantics of the language.
This is true of programming in any language.
> This means that there's a sense in which the language that the
> programmer programs in is not the same language that has a formal
> semantic definition. As I mentioned in another post, programmers are
> essentially mentally programming in a richer language - a language which
> has informal (static) types - but the code they write down elides this
> type information, or else puts it in comments.
If you consider stuff that might be in the programmer's head as part
of the program, where do you stop? When I maintain a program written
by someone I've never met, I have no idea what was in that programmer's
head. All I have is comments, which may be (and frequently are,
unfortunately) inaccurate.
(Actually, it's worse than that -- if I come back to a program 5 years
later, I probably have little idea what was in my head at the time I
wrote it.)
> We have to accept, then, that the formal semantic definitions of
> dynamically-checked languages are incomplete in some important ways.
> Referring to those semantic definitions as "the language", as though
> that's all there is to the language in a broader sense, is misleading.
Bah, humbug. The language is just the language.
> In this context, the term "latently-typed language" refers to the
> language that a programmer experiences, not to the subset of that
> language which is all that we're typically able to formally define.
I'm with Marshall -- this is way too mystical for me.
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: Sat, 24 Jun 2006 22:50:01 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <tkjng.477126$xt.379128@fe3.news.blueyonder.co.uk>
David Hopwood wrote:
> Anton van Straaten wrote:
>
>>I'm suggesting that if a language classifies and tags values in a way
>>that supports the programmer in static reasoning about the behavior of
>>terms, that calling it "untyped" does not capture the entire picture,
>>even if it's technically accurate in a restricted sense (i.e. in the
>>sense that terms don't have static types that are known within the
>>language).
>>
>>Let me come at this from another direction: what do you call the
>>classifications into number, string, vector etc. that a language like
>>Scheme does? And when someone writes a program which includes the
>>following lines, how would you characterize the contents of the comment:
>>
>>; third : integer -> integer
>>(define (third n) (quotient n 3))
>
> I would call it an informal type annotation. But the very fact that
> it has to be expressed as a comment, and is not checked,
What I meant to say here is "and is not used in any way by the language
implementation,"
> means that
> the *language* is not typed (even though Scheme is dynamically tagged,
> and even though dynamic tagging provides *partial* support for a
> programming style that uses this kind of informal annotation).
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: Sat, 24 Jun 2006 23:06:58 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <mAjng.465989$tc.228623@fe2.news.blueyonder.co.uk>
Marshall wrote:
> Joe Marshall wrote:
>
>>Marshall wrote:
>
>>>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 do this quite often. Sometimes I'll develop `in the debugger'. I'll
>>change some piece of code and run the program until it traps. Then,
>>without exiting the debugger, I'll fix the immediate problem and
>>restart the program at the point it trapped. This technique takes a
>>bit of practice, but if you are working on something that's complex and
>>has a lot of state, it saves a lot of time because you don't have to
>>reconstruct the state every time you make a change.
The problem with this is that from that point on, what you're running
is neither the old nor the new program, since its state may have been
influenced by the bug before you corrected it.
I find it far simpler to just restart the program after correcting
anything. If this is too difficult, I change the design to make it
less difficult.
> Wow, interesting.
>
> (I say the following only to point out differing strategies of
> development, not to say one or the other is right or bad or
> whatever.)
>
> I occasionally find myself doing the above, and when I do,
> I take it as a sign that I've screwed up. I find that process
> excruciating, and I do everything I can to avoid it. Over the
> years, I've gotten more and more adept at trying to turn
> as many bugs as possible into type errors, so I don't have
> to run the debugger.
>
> Now, there might be an argument to be made that if I had
> been using a dynamic language, the process wouldn't be
> so bad, and I woudn't dislike it so much. But mabe:
>
> As a strawman: suppose there are two broad categories
> of mental strategies for thinking about bugs, and people
> fall naturally into one way or the other, the way there
> are morning people and night people. One group is
> drawn to the static analysis, one group hates it.
> One group hates working in the debugger, one group
> is able to use that tool very effectively and elegantly.
>
> Anyway, it's a thought.
I don't buy this -- or at least, I am not in either group.
A good debugger is invaluable regardless of your attitude to type
systems. Recently I was debugging two programs written to do similar
things in the same statically typed language (C), but where a debugger
could not be used for one of the programs. It took maybe 5 times
longer to find and fix each bug without the debugger, and I found it
a much more frustrating experience.
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: 24 Jun 2006 21:01:36 -0400
From: Chris F Clark <cfc@shell01.TheWorld.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <sddk676m4jz.fsf@shell01.TheWorld.com>
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. I definitely consider such
things type systems. However, I like my definitions very general and
vague. Your writing suggests the opposite preference. To me if
something works in an analogous way to how a known type system, I tend
to consider it a "type system". That probably isn't going to be at
all satisfactory to someone wanting a more rigorous definition. Of
course, to my mind, the rigorous definitions are just an attempt to
capture something that is already known informally and put it on a
more rational foundation.
> So what is the domain of a function? (Heck, what is a function?
...
> (I need a word here that implies something like a set, but I don't care
> to verify the axioms of set theory. I'm just going to use set. Hope
> that's okay.)
Yes, I meant the typical HS algebra definition of domain, which is a
set, same thing for function. More rigorous definitions can be
sustituted as necessary and appropriate.
> 1. The domain is the set of inputs to that expression which are going to
> produce a correct result.
>
> 2. The domain is the set of inputs that I expected this expression to
> work with when I wrote it.
>
> 3. The domain is the set of inputs for which the expression has a
> defined result within the language semantics.
>
> So the problem, then, more clearly stated, is that we need something
> stronger than #3 and weaker than #1, but #2 includes some psychological
> nature that is problematic to me (though, admittedly, FAR less
> problematic than the broader uses of psychology to date.)
Actually, I like 2 quite well. There is some set in my mind when I'm
writing a particular expression. It is likely an ill-defined set, but
I don't notice that. That set is exactly the "type". I approximate
that set and it's relationships to other sets in my program with the
typing machinery of the language I am using. That is the static (and
well-founded) type. It is however, only an approximation to the ideal
"real" type. If I could make that imaginary mental set concrete (and
well-defined), that would be exactly my concept of type.
Now, that overplays the conceptual power in my mind. My mental image
is influenced by my knowledge of the semantics of the language and
also any implementations I may have used. Thus, I will weaken 2 to be
closer to 3, because I don't expect a perfectly ideal type system,
just an approximation. To the extent that I am aware of gotchas in
the language or a relavent implementation, I amy write extra code to
try and limit things to model 1. Note that in my fallible mind, 1 and
2 are identical. In my hubris, I expect that the extra checks I have
made have restricted my inputs to where model 3 and 1 coincide.
Expanding that a little. I expect the language to catch type errors
where I violate model 3. To the extent model 3 differs from model 1
and my code hasn't added extra checks to catch it, I have bugs
resulting from undetected type errors or perhaps modelling errors. To
me they are type errors, because I expect that there is a typing
system that captures 1 for the program I am writing, even though I
know that that is not generally true.
As I reflect on this more, I really do like 2 in the sense that I
believe there is some abstract Platonic set that is an ideal type
(like 1) and that is what the type system is approximating. to the
sense that languages approximate either 1 or 2, those facilites are
type facilities of a language. That puts me very close to your
(rejected) definition of type as the well-defined semantics of the
language. Except I think of types as the sets of values that the
language provides, so it isn't the entire semantics of the language,
just that part which divides values into discrete sets which are
approriate to different operations (and detect inaapropriate values).
-Chris
------------------------------
Date: 24 Jun 2006 18:33:16 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151199196.870389.81960@p79g2000cwp.googlegroups.com>
Chris F Clark wrote:
>
> I'm particularly interested if something unsound (and perhaps
> ambiguous) could be called a type system. I definitely consider such
> things type systems.
I don't understand. You are saying you prefer to investigate the
unsound over the sound?
> However, I like my definitions very general and
> vague. Your writing suggests the opposite preference.
Again, I cannot understand this. In a technical realm, vagueness
is the opposite of understanding. To me, it sounds like you are
saying that you prefer not to understand the field you work in.
> To me if
> something works in an analogous way to how a known type system, I tend
> to consider it a "type system". That probably isn't going to be at
> all satisfactory to someone wanting a more rigorous definition.
Analogies are one thing; definitions are another.
> Of
> course, to my mind, the rigorous definitions are just an attempt to
> capture something that is already known informally and put it on a
> more rational foundation.
If something is informal and non-rational, it cannot be said to
be "known." At best, it could be called "suspected." Even if you
think something which turns out to be true, we could not say
that you "knew" it unless your reasons for your thoughts were
valid.
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?
Marshall
------------------------------
Date: Sat, 24 Jun 2006 21:15:28 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f07adba87e360d29896f8@news.altopia.net>
Chris F Clark <cfc@shell01.TheWorld.com> wrote:
> 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?
I think that the correspondence partly in the wrong direction to
describe it that way. If someone were to stand up and say "every
possible but of reasoning about program correctness or behavior is type
reasoning", then I'd be happy to say that formal type systems are a
subset of that kind of reasoning. However, that's quite the statement
to ask of anyone. So far, everyone has wanted to say that there are
some kinds of reasoning that are type reasoning and some that are not.
If that is the case, then a formal type system is in that sense more
general than this intuitive notion of type, since formal type systems
are not limited to verifying any specific category of statements about
program behavior (except, perhaps that they are intended to verify
guarantees, not possibilities; I don't believe it would fit all
definitions of formal types to try to verify that it is possible for a
program to terminate, for example).
What I can't agree to is that what you propose is actually more general.
It is more general in some ways, and more limited in others. As such,
the best you can say is that is analogous to formal types in some ways,
but certainly not that it's a generalization of them.
> 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, although this is sort of a pedantic question in the first place, I
believe that an unsound type system would still generally be called a
type system in formal type theory. However, I have to qualify that with
a clarification of what is meant by unsound. We mean that it DOES
assign types to expressions, but that those types are either not
sufficient to prove what we want about program behavior, or they are not
consistent so that a program that was well typed may reduce to poorly
typed program during its execution. Obviously, such type systems don't
prove anything at all, but they probably still count as type systems.
(I'll point out briefly that a typical, but not required, approach to
type theory is to define program semantics so that the evaluator lacks
even the rules to continue evaluating programs that are poorly typed or
that don't have the property of interest. Hence, you'll see statements
like one earlier in this thread that part of type-soundness is a
guarantee that the evaluation or semantics doesn't get stuck. I
actually think this is an unfortunate confusion of the model with the
thing being modeled, and the actual requirement of interest is that the
typing relation is defined so that all well-typed terms have the
interesting property which we are trying to prove. It is irrelevant
whether the definition of the language semantics happens to contain
rules that generalize to ill-typed programs or not.)
I suspect, though, that you mean something else by unsound. I don't
know what you mean, or whether it could be considered formally a type
system.
> > 1. The domain is the set of inputs to that expression which are going to
> > produce a correct result.
> >
> > 2. The domain is the set of inputs that I expected this expression to
> > work with when I wrote it.
> >
> > 3. The domain is the set of inputs for which the expression has a
> > defined result within the language semantics.
> Actually, I like 2 quite well. There is some set in my mind when I'm
> writing a particular expression. It is likely an ill-defined set, but
> I don't notice that. That set is exactly the "type".
I don't actually mind #2 when we're talking about types that exist in
the programmer's mind. I suspect that it may get some complaint along
the lines that in the presence of type polymorphism, programmers don't
need to be (perhaps rarely are) thinking of any specific set of values
when they write code. I would agree with that statement, but point out
that I can define at least my informal kind of set by saying, for
instance, "the set of all inputs on which X operations make sense".
I believe there is more of a concrete difference between #1 and #2 than
you may realize. If we restrict types to considering the domain of
functions without regard to the context in which they are called, then
there are plenty of inputs on which this function does its own job quite
well, but a global analysis tool may be able to conclude that if that
input has been passed in, then this program already beyond the
possibility of producing a correct result. #1 would, therefore, be a
more global form of analysis than #2, rather than being merely a
question of whether you are fallible or not.
> Expanding that a little. I expect the language to catch type errors
> where I violate model 3.
So would I. (Actually, that's another pesky question; if the language
"catches" it, did the error even occur, or did the expression just gain
a defined result such that domain #3 is indistinguishable from the set
of all possible inputs. I tend to agree with Chris Uppal, I suppose,
that the latter is really the case, so that dynamic type systems in
languages, if they are sound, prevent concept #3 from ever being in
question. But, of course, you don't think about it that way, which
distinguishes 2 from 3.)
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
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 9372
***************************************
