Re^5: "strong typing" is potentially ambiguous

I assert that Perl's type system is overall stronger than C's or Java's, even if it's limited in the number of types it has.

Ah, here's where we part company. C and Java have many types (unlimited in fact, go ahead make your own structs, unions, etc.). And they also do their type checking at compile time. Sure, if you want you can subvert the type system in a way that you couldn't with an ML or Haskell, but its much harder to do it accidently. Fewer types is synonymous with having fewer proofs of the programs behavior. I like perl as much as the next guy (heck, counting just now, I've got 6 books on my bookshelf with "perl" in the title), but all else being equal (i.e. same quality programmers, etc.), if I had to choose between being hooked up to a heart/lung machine running Java, and one running Perl, I'd pick Java. I wonder what they really use? If we knew the answer we'd probably all shudder. Now the question becomes, if I was going to design the heart/lung machine I'd be using on myself, what language would I use? I'd probably want to create some sort of very minimal strongly-typed hybrid lisp/haskell, in which I'd proven the compiler correct with some sort of computer algebra system.

If you want more typing theory discussion than you can shake a stick at, I'd recommend some of these threads...

Why type systems are interesting
Why type systems are interesting - part II
Why type systems are interesting - part III: latent types

-- All code is 100% tested and functional unless otherwise noted.

Comment on Re^5: "strong typing" is potentially ambiguous

Replies are listed 'Best First'.
Re^6: "strong typing" is potentially ambiguous by hardburn (Abbot) on Dec 15, 2004 at 14:23 UTC
Sure, if you want you can subvert the type system in a way that you couldn't with an ML or Haskell, but its much harder to do it accidently. If you can subvert the system, then it's not strong. It's pretty much impossible to subvert Perl's type system, except using operations that are valid in any programming language (as I demonstrated eariler in the thread). The fact that Perl has a limited number of types is irrelevent to any argument over its strength. You could say that C/Java/etc. has a more useful type system. However, because of its lack of strength, I don't think Pascal-derived type systems are useful for showing program correctness. They are only good for providing hints to the compiler. Which is really all they were designed for. I lurk on Lambda, and have read parts of the flame war^H^H^H^H threads you mention. There's a lot of material there to go through. "There is no shame in being self-taught, only in not trying to learn in the first place." -- Atrus, Myst: The Book of D'ni.	[reply]
Re^7: "strong typing" is potentially ambiguous by jdporter (Paladin) on Dec 15, 2004 at 15:22 UTC
If you can subvert the system, then it's not strong. Please go back and read MJD on Strong Typing again. As he says, there is no universally agreed-upon definition of "strong typing". One of the several de facto definitions he cites is the one you're reflecting, above. But there are others. Given that, it would be wise (IMHO) to stop trying to argue whether/how Perl's type system is "strong". Thanks. (Update: "more typing goodness from MJD", as sleepingsquirrel put it.)	[reply]
Re^8: "strong typing" is potentially ambiguous by hardburn (Abbot) on Dec 15, 2004 at 15:47 UTC
There is a good definition of what a type system is. As I noted earilier in the thread, a type system limits the operations you can perform on a given peice of data (this definition is a bit informal, but will do for now). Further, type systems come out of formal logic, and predate CS. From that, the definition of "strong type system" comes quite naturally. If you can perform operations that the type system should have forbid, it's a weak type system. Otherwise, it's strong. "There is no shame in being self-taught, only in not trying to learn in the first place." -- Atrus, Myst: The Book of D'ni.	[reply]
Re^9: "strong typing" is potentially ambiguous by jdporter (Paladin) on Dec 15, 2004 at 16:25 UTC
Re^10: "strong typing" is potentially ambiguous by hardburn (Abbot) on Dec 15, 2004 at 16:28 UTC
Re^7: "strong typing" is potentially ambiguous by sleepingsquirrel (Chaplain) on Dec 15, 2004 at 18:05 UTC
I don't think Pascal-derived type systems are useful for showing program correctness. They are only good for providing hints to the compiler. Well, some people are doing some very interesting research into proof carrying code in java... A Proof-Carrying Code Architecture for Java An Overview of Proof-Carrying Code -- All code is 100% tested and functional unless otherwise noted.	[reply]