[plt-scheme] Re: to define, or to let

From: Bill Richter (richter at math.northwestern.edu)
Date: Sat Apr 24 20:50:03 EDT 2004

   > Or a real dumb question.  Typing is a way to "pack more knowledge
   > into your software".  That's a weakness of Scheme compared to ML.

   It's a tradeoff, i.e. there are weaknesses in both directions.

Thanks, Anton.

   > But doesn't ML enforce typing?  Reaally dumb question: C enforces
   > typing, doesn't it?  If a function is declared to take integer
   > arguments, and you call it with a float, the compiler flags you,
   > right?

   Yes.  Those are static checks.  So what?  Not even C or ML can check
   everything statically.

Great!  So let's see, type-violations can be checked statically?  I
suppose so, because everything's gotta be declared/defined in the
source.  Thanks.  I guess that's pretty basic :D But order of
evaluation stuff can't be checked statically?

I thought the opposite of static is run-time.  And I certainly would
only think you can detect order of evaluation problems at run-time.
So let's say we define a new construct let@ that evaluates in any
order, so if we write, with 

(let@ ([x FOO]
       [y GOO]
       [z ZOO])

then we're proclaiming that the expressions FOO, GOO, ZOO can be
evaluated in any order [Thanks, Joe.].  I wouldn't think you could
check that without running the program.  But let's run the program.
Can we get the interpreter to hand us a run-time error?  Like division
by zero: that's a run-time error I used to get (a lot) in Fortran.

   > Let me re-ask: Aren't Robbie's contract.ss enforced by DrScheme?

   They're enforced by Robby's contract.ss.  


   Anyone else can write things to enforce their own contracts, too.
   That's the cool thing about macros.  Like BrBackwards (which is
   just a tad less comprehensive than Robby's stuff).

Ah, so contract.ss will nab all violations of the contract laws, but
your idea for BrBackwards will only nab some violations?  And it's a
macro check, not a static check?  Is it a run-time check?

   The false knowledge you're concerned about is no different than a
   piece of code that contains false knowledge about types.  The
   MzScheme compiler does not enforce that.  

But C & ML compilers do flag a type violation, right?  And Scheme
doesn't let you make assertions about type, does it?  I mean, I might
define a function on pairs, and the first thing my function should do
ask pair?, because the interpreter won't do it for me, right?  But the
interpreter doesn't declare my function to only take pairs either.

   There are also all sorts of other things that are encoded in code,
   which compilers cannot check.  Real programs have many kinds of
   bugs which can only be caught by testing.

Sure, and then some!

   All of the tools we use, like static type checks, runtime type
   checks, contract checks, code reviews, test suites, alpha testers,
   and beta testers, are designed to help us to either prove a lack of
   bugs, or detect and find bugs when we can't prove their
   non-existence.  With static checks, you're focusing on just one
   small aspect of that picture.

Sounds great, except I didn't realize I was just static.

   The fact that the compiler can't statically check order
   independence is not a valid rationale for eliminating the ability
   to assert it.  

But I bet MF would say just that, and it sounds reasonable:
"My interpreter isn't gonna let people assert things that my
interpreter (static or no) can't enforce."

   That's like saying "we hardly ever catch car thieves anyway, so
   let's just take that pesky vehicle theft law off the books so we
   aren't constantly reminded of our shortcomings".


   This is playing a game with systems, saying you don't know how to
   deal with something in the very specific way you want to deal with
   it, so you define the system so that you can't express that thing
   in it.  But Goedel is watching you, and wondering why you didn't
   pay more attention in that Foundations of Mathematics course.  

Nah, MF understands the Halting problem, and therefore, I'm hazarding,
MF wouldn't allow you to declare a function "unhalt-able."

   Your game doesn't eliminate the entire problem, it just makes it
   harder to talk about it within the system, like a dysfunctional


   Besides, skipping back a metaphor, people can use tools like LoJack
   to make car theft easier to fix.  That won't help as much after the
   law's been eliminated.  "Hey, that guy stole my car!"  "Yeah, but
   that's not against the law."  Suddenly, people are stealing cars
   left and right, and there's nothing you can do about it, other than
   obsessively follow your car's blip on the LoJack tracking screen,
   or maybe hire Vinnie from Brooklyn (buddy of mine) to get your car


   It's that moral hazard I was talking about.  

I didn't care for your moral hazard URL.  The arson biz was fine, but
I was catching a strong whiff of dumb right-wing attacks on welfare,
"Let 'em eat bootstraps!"  But let's not argue about that here.

   Make depending on eval order OK everywhere, and people will do it
   everywhere.  May as well be programming in Python.

Way too strident.  MF is really really interested in good programming
practices.  People can of course take DrScheme and write really bad
code in it, but that doesn't mean MF approves of it, right?  

So the real question is what's a good style to program mutation in.  I
haven't heard much about that, and you say HtDP is weak there.  

Can't you just take Python programs and translate them to Scheme?
Doesn't Guile do quite a lot of that?  The language can't prevent you
from lousy programming.  A good language will enable you to write good
programs, but you gotta know good programming style, and I don't.

But I really think the point is what I wrote above, that MF doesn't
want unenforceable assertions in the language.  Seems like folks,
e.g. Vinnie, could go either way on that, but his position would be
quite reasonable.  But maybe there's some way with a lot of work that
you can make these assertions enforceable, and that gets to MF's last
post, "We only have N manyears."  Maybe you & Joe can write the code!

Posted on the users mailing list.