> On Mon, 06 Mar 2000 11:18:41 -0800, Erann Gat wrote:
>
> > 2. Issues with dynamic vs. lexical bindings, including beginner's
> > confusion, and the fact that there is no portable way to write code that
> > is guaranteed to produce a lexical binding.
>
> Sure there is: create an uninterned symbol for your guaranteed-lexical
> variable. If you really think this is worthwhile, you could write
> code like
>
> (let ((#1=#:foo 42))
> (lambda () (format t "~&;; The value of FOO is ~D" #1#)))
>
> or you could write a "lexical-let" macro that makes gensyms for all
> the bindings and code-walks the body doing the replacements.
And it then occurred to me that code walking isn't necessary -- you
can use SYMBOL-MACROLET to do the code walking for you. So here is
LLET, lexical-let, a macro that guarantees lexical bindings:
(defmacro llet (bindings &body body)
(let* ( (vars (mapcar 'first bindings))
(vals (mapcar 'second bindings))
(gensyms (mapcar (lambda (v) (gensym (symbol-name (first v))))
bindings)) )
`(let ,(mapcar 'list gensyms vals)
(symbol-macrolet ,(mapcar 'list vars gensyms)
,@body))))
> Personally, I wouldn't bother unless I saw some evidence that this is
> actually a problem "in real life".
As I wrote to Paul, I work for NASA and I am trying to convince people
to use Lisp on spacecraft, which are multimillion-dollar assets. Managers
want to see safety guarantees, not just empirical evidence. Just because
something hasn't been a problem in the past doesn't mean it won't be a
problem in the future. And in the space biz, the first glitch could also
be your last.
Erann Gat
g...@jpl.nasa.gov
> And it then occurred to me that code walking isn't necessary -- you
> can use SYMBOL-MACROLET to do the code walking for you. So here is
> LLET, lexical-let, a macro that guarantees lexical bindings:
>
> (defmacro llet (bindings &body body)
> (let* ( (vars (mapcar 'first bindings))
> (vals (mapcar 'second bindings))
> (gensyms (mapcar (lambda (v) (gensym (symbol-name (first v))))
> bindings)) )
> `(let ,(mapcar 'list gensyms vals)
> (symbol-macrolet ,(mapcar 'list vars gensyms)
> ,@body))))
Turns out this doesn't work. It's an error to use SYMBOL-MACROLET on
a symbol that has been declared SPECIAL. Damn! :-(
Well, it kind of works. It *does* guarantee lexical bindings, which is
the really important thing (IMO). But it would be nice to be able to do
the following as well:
(defvar *x* 1)
(defun foo () *x*)
(llet ( (*x* 2) ) (list *x* (foo))) --> (2 1)
But this generates an error.
? (llet ( (*x* 2) ) (list *x* (foo)))
> Error: While compiling an anonymous function :
> SPECIAL declaration applies to symbol macro *X*
> Type Command-. to abort.
See the RestartsŠ menu item for further choices.
1 >
Erann Gat
g...@jpl.nasa.gov
Hi,
This is a serious question, and not meant to trigger a flame-fest, so
maybe it's best answered and asked (sorry) be email. Here goes...
While I like Lisp a lot, it strikes me that a statically typed language
might be preferable in extreme reliability situations (I'm thinking of
ML, for example). Is that an issue in your experience, and how do you
defend Lisp against that criticism?
(In my very limited opinion I get the impression that static checking
has improved a lot recently (but it may be that this is decade old work
that has stalled) and that a statically typed language with flexibility
approaching that of Lisp might be possible - that's a separate issue
since you are dealing with existing languages, but is teh background to
my question).
Cheers,
Andrew
Sent via Deja.com http://www.deja.com/
Before you buy.
> While I like Lisp a lot, it strikes me that a statically typed language
> might be preferable in extreme reliability situations (I'm thinking of
> ML, for example).
I'm puzzled by this. If I understand correctly you are saying that
statically typed languages are more reliable. First, in what way are
statically typed languges more reliable? Second, lisp *can* be typed and
for `extreme reliability situation' you may want to do this. (This touches
on Paul Graham's `lisp is really two languages' argument [1]).
Best Regards,
:) will
[1] As in 'Lisp is really two languages: a language for writing fast
programs and a language for writing programs fast.' p. 213 `ANSI Common
Lisp', P.Graham.
OK...
1. You snipped all my defensive comments about not being an expert on
this.
2. I said *might* be preferrable.
3. Part of safety might be that you are *forced* by the language to
statically type. I have no idea if it is easy or even possible to do
static checks on Lisp code that prove that it is statically typed.
4. Other languages might provide features that help you write
statically typed programs. Again, I have no idea whether it is easy or
even possible to have type inference in Lisp compile time.
5. My not knowing or understanding something doesn't preculde me from
asking for information on it.
> As I wrote to Paul, I work for NASA and I am trying to convince people
> to use Lisp on spacecraft, which are multimillion-dollar assets. Managers
> want to see safety guarantees, not just empirical evidence. Just because
> something hasn't been a problem in the past doesn't mean it won't be a
> problem in the future. And in the space biz, the first glitch could also
> be your last.
I think that your LLET form gives this kind of guarantee. As you
pointed out in a followup, it doesn't work to try and do a
SYMBOL-MACROLET that would shadow a special variable. But the
standard makes it clear that an error is signalled this is so (not
just that `it is an error'). It doesn't say, but I assume this would
be a compile-time error (and this would be easy to check in an
implementation). So you can be pretty sure that if the code
compiles, that binding is lexical. Could you ask for more?
Incidentally, I'd be rather surprised if you can win the
dynamic-typing battle but then lose on special variables in
safety-critical lisp!
--tim
> I'm puzzled by this. If I understand correctly you are saying that
> statically typed languages are more reliable. First, in what way are
> statically typed languges more reliable? Second, lisp *can* be typed and
> for `extreme reliability situation' you may want to do this. (This touches
> on Paul Graham's `lisp is really two languages' argument [1]).
Statically typed programs are considered more reliable because you (or
the compiler) can prove more properties about them, so you may get
more guarantees of the form `if this compiles, it will run' from the
system. You typically need compiler support to do this (or
code-walker support I suppose) -- just because you can say:
(defun foo (x)
(declare (type integer x))
(car x))
Does not mean that the compiler will check that declaration for you
(and some won't). Of course, you could write a type-checker for CL
programs but that would be a fair lot of work.
Of course, like many things in CS, it is not completely clear what
this reliability translates to in practice. There are undoubtedly
`studies that show...' but they are likely based on statistically
insignificant samples. (Either for the pro-static or
anti-static-typing camps.)
Both camps will also happily point you at the Ariane disaster as an
indication that the other is wrong.
--tim
> Both camps will also happily point you at the Ariane disaster as an
> indication that the other is wrong.
I think this is becoming a fundamental law in software engineering and
programming language development: Everybody uses the Ariane disaster.
Maybe ESA should have trademarked "Ariane 5 Disaster" and "Ariane 5
Report", and they could have recouped the money lost, probably x times
over... ;)
Regs, Pierre.
--
Pierre Mai <pm...@acm.org> PGP and GPG keys at your nearest Keyserver
"One smaller motivation which, in part, stems from altruism is Microsoft-
bashing." [Microsoft memo, see http://www.opensource.org/halloween1.html]
What I wrote was not intended as a flame. If you read it as such I
apologise :( Also, please do not think that I am an expert because I'm
not.
Andrew Cooke wrote:
> 1. You snipped all my defensive comments about not being an expert
>on this.
True. But you must have thought something along these lines otherwise
you wouldn't have posted ;)
> 3. Part of safety might be that you are *forced* by the language to
> statically type.
Why do you think this? This is the nub of what I was asking. As a
follow up to this: why are you concerned with static (as opposed to
dynamic) type checking?
>I have no idea if it is easy or even possible to do static checks on
>Lisp code that prove that it is statically typed.
But, if you can do this type of checking in C or pascal, say, why can't
you do this in lisp? Maybe the question is how hard it is to do
this.
>5. My not knowing or understanding something doesn't preculde me from
>asking for information on it.
No, that is true. If you thought that was what I was doing then there
is a problem with they way I expressed myself. If this is so, I am
sorry,
Best Regards,
:) will
Tim wrote:
> Statically typed programs are considered more reliable because you
> (or the compiler) can prove more properties about them, so you may
> get more guarantees...from the system.
and
> ...it is not completely clear what this reliability translates to in
> practice. There are undoubtedly `studies that show...' but they are
> likely based on statistically insignificant samples. (Either for the
> pro-static or anti-static-typing camps.)
This is what I was trying to say in my usual fuddled fashion. As far as
I know (which is not saying that much) the case for static vs dynamic
vs no type checking is moot. And as you say, these guarantees are in
the well maybe camp[1].
> Does not mean that the compiler will check that declaration for you
>(and some won't).
And yes, you got me here. I made the assumption that the compiler would
honour type declarations. Which, of course, it does not have to.
However, I would be unhappy if a compiler didn't at least try do this.
>Of course, you could write a type-checker for CL programs but that
>would be a fair lot of work.
You forsaw my follow up post. This internet telepathy is great ;)
Best Regards,
:) will
[1] As usual I look forward to being corrected on this ;)
Sorry - I'm getting a bit frazzled by various conversation on the
internet.
Thanks for the info.
Andrew
Because I program in Java and a (the one> ;-) advantage over Lisp is
that it catches some mistakes that dynamic testing doesn't. I know that
one can have tests etc, but it seems that the earlier one catches errors
the better. The original post was about software which is effectively
run once (outside testing) and must work - I was thinking that the
extreme emphasis on perfect code must favour anything that detects
errors.
> >I have no idea if it is easy or even possible to do static checks on
> >Lisp code that prove that it is statically typed.
>
> But, if you can do this type of checking in C or pascal, say, why
can't
> you do this in lisp? Maybe the question is how hard it is to do
> this.
Because Lisp is much more dynamic (eg Macros) (there was a post on this
group today about a package to allow manipulation of program fragments
in ML - I haven't looked, but it would show the difference between doing
something like that in a statically typed language and a in Lisp).
My experience in ML is limited, so the following could be simply my lack
of experience in the language, but...
Not only does it allow for more automated checking, but you are
programming in an environment wher you are constantly reminded of what
is what. My programming moved from my usual slap it together and it'll
work style to writing something approaching a logical argument in code.
Obviously, this mainly means I can't code for toffee (it was also my
first meeting with functional programming), but I could see how it would
bring code closer to a specification.
Hmmm. Maybe I'll give it another try :-)
Andrew
PS If anyone is interested, I gather than OCaml is the cutting edge of
ML these days. I used SMLNJ which seems to be the "standard".
> Why do you think this? This is the nub of what I was asking. As a
> follow up to this: why are you concerned with static (as opposed to
> dynamic) type checking?
Because static type checking catches (some) errors at compile time,
whereas dynamic checking will catch them only at runtime. If there's
no reasonable way of dealing with the runtime error (or if the people
writing the code didn't bother to deal with it), and the system is
safety-critical or just inaccessible (on Mars, say), then a runtime
type error may be a very bad thing to get.
(Incidentally, in this context, `type' often means much more than
`representational type' -- it can be very useful to know that
something is an (integer 0 8) say).
> But, if you can do this type of checking in C or pascal, say, why can't
> you do this in lisp? Maybe the question is how hard it is to do
> this.
You can do it, but you need compiler support, or a code-walker and the
ability to write your own type-checker at least.
--tim
it's a contentious issue because there's no relevant research to support
the static-typing crowd, yet they have an "intuitive edge" that is very
hard both to defend formally and to attack informally. it's like arguing
against adults needing milk. (we don't. really.)
| While I like Lisp a lot, it strikes me that a statically typed language
| might be preferable in extreme reliability situations (I'm thinking of
| ML, for example). Is that an issue in your experience, and how do you
| defend Lisp against that criticism?
in my current setting, which is somewhat more down to earth than NASA's
lofty projects despite dealing with financial news distribution, handling
errors _gracefully_ has virtually defined the success of the project,
which is expanding and providing new services at increasing speed. the
reason explicitly cited has been that the old system that mine replaced
died completely and randomly when a component died, while mine stops in a
state that is usually continuable right away and never fatal. running a
production system under Emacs under screen may seem rather odd to the old
batch-oriented school, but what it means is that I can connect to the
Emacs process controlling Allegro CL and examine the system state, talk
to background debugging streams, and fix whatever goes wrong if the
system hiccups in any way, which it has so far done only with really
weird input from the outside world.
to obtain this level of gracefulness in one of the usual statically typed
languages would have required _massive_ amounts of code, simply because
you can't combine the dynamism with static typing without recompiling,
since _only_ the compiler is privy to the type information.
conversely, if you need all the type information hanging around at
run-time, anyway, why not make _full_ use of it? sadly, the static
typing crowd believes this is inefficient because they never had to make
it perform optimally, using their static typing the proof that it is so
much easier to do it compile-time, but that only proves they never spent
the effort to make it fast at run-time.
incidentally, my main gripe with static typing is when it is explicit.
implicit static typing (like type inference) has a bunch of specific
advantages over both dynamic and explicitly typed languages, but in
general fall short in terms of dynamism on one hand and the programmer's
ability to predict what the system is doing on the other.
| (In my very limited opinion I get the impression that static checking has
| improved a lot recently (but it may be that this is decade old work that
| has stalled) and that a statically typed language with flexibility
| approaching that of Lisp might be possible - that's a separate issue
| since you are dealing with existing languages, but is teh background to
| my question).
I think it's important to differentiate not on the basis of what the
compiler can do with the type information, but what something other than
the compiler can do with the type information. this is largely, but not
fully, orthogonal to whether the language is statically or dynamically
typed. debuggers for most languages maintain type information (mainly in
order to access the memory they use, of course), but you can't use it if
you aren't the debugger. in some development environments, you get help
calling functions and using variables, but what's the big difference
between a lookup system only available in some program after compilation
and manual pages in external documentation? the dynamism of _current_
information is missing in all of these systems.
I don't think it's possible to make a statically typed language as
dynamic as Common Lisp environments are simply because the work involved
in making a statically typed language able to handle the dynamism will
involve _very_ intelligent recompilation strategies, mounds of debugging
information that people will want to discard, and introspection will have
to be added to these languages in environment-specific ways.
#:Erik
Tim Bradshaw wrote:
> * Will Deakin wrote:
> >> 3. Part of safety might be that you are *forced* by the language to
> >> statically type.
>
> > Why do you think this? This is the nub of what I was asking. As a
> > follow up to this: why are you concerned with static (as opposed to
> > dynamic) type checking?
>
> Because static type checking catches (some) errors at compile time,
> whereas dynamic checking will catch them only at runtime.
More to the point: in ML all possible program paths are type checked.
If testing cannot be guaranteed to cover all possible program paths,
this may be an important point.
OTOH, I seem to have very few problems with types in lisp. But this
does not mean no one will, or it might not be super-critical for some
applicaitons ( such as spacecraft programming ).
It seems possible ( to me ) to write some lisp macros to produce a typed
version of the language, eg:
(def-typed-fun square( (x float) )(* x x))
(def-typed-var (*max-users* fixnum) 100)
the second case would require creating a setf-function for setting
*max-users* to assure any setf was type checked. Might even want
to make the *real* variable name scoped so it could not be set
accidentally somehow. This also leads to issues if normal lisp code
was calling some of the type-checked functions. Wrappers would
have to be used in both directions.
dave
> While I like Lisp a lot, it strikes me that a statically typed language
> might be preferable in extreme reliability situations (I'm thinking of
> ML, for example). Is that an issue in your experience, and how do you
> defend Lisp against that criticism?
No one is seriously pushing for ML in space as far as I know so the
issue hasn't come up. But if someone did the most effective argument
against it would be that there are no commercial vendors for ML and
Haskell, and it's even harder to find ML and Haskell programmers than
Lisp programmers.
There are two technical arguments that I use against people who make
the static-typing argument for C++.
The first is that static typing cannot eliminate all type errors because
the problem is undecidable. (Run-time math errors are type errors.)
Since you can't eliminate all type errors, you need a mechanism for
handling them at run time regardless of whether you are doing static
typing or not. Since you need this mechanism anyway, the incremental
benefit of having compile time checks is fairly small. In other words,
having static typing is worse than not having static typing because it
provides the *illusion* of safety but not the reality.
The third argument is that it's not hard to add static type checking
to Lisp if it is determined that the benefit is worthwhile.
Erann Gat
g...@jpl.nasa.gov
before you reinvent the wheel, please investigate the THE special form
and how it behaves in interpreted and compiled code under various
optimization settings. you might be _very_ surprised.
few Common Lisp programmers seem to know about the THE form, however.
#:Erik
Having had significant experience with both static and dynamic typing, the
primary benefit of static typing, in my not so humble opinion, is the checking
of interface conformance.
That is, during building a system out of components/modules/subsystems
whatever, when piecing together the parts, having things not compile unless
things "fit" is a major major help. I.e. Things like not being able to call a
function unless you supply all and only all of the required parameters and of
the right type.
Static type checking simply prevents whole classes of errors right away. The
compiler is performing certain classes of error checks immediately as opposed
to the user finding them during testing or out in the field.
Static typing does not prevent all errors by any means, and you still need
mechanisms to handle run-time failures. That does not mean, however, that the
benefits are insigificant. Just think of it as an additional tool one can use
to prevent errors.
That many statically typed languages ditch the type information during
run-time is not an argument against static typing. There is nothing to prevent
a language system from keeping type information around to be used by whoever
needs it.
That a dynamically typed system is often fundamentally more powerful than a
statically typed system is not an argument against static typing. Both styles
can co-exist, as in Common Lisp.
The point about static typing is that the programmer is specifying more
precisely how an abstraction can be used. The language environment then
verifies this usage. For many abstractions, the point is to *restrict* the
usage to a precise set, and not be flexible about it.
My approach is to do a statically typed style by default, and then to change
to a dynamic style only if the problem domain calls for it.
E.g. This is preferrable (apologies for any syntax errors):
(defun (doit (integer to-me))
(process to-me))
over this:
(defun (doit to-me)
(cond ((integerp to-me) (process to-me))
(error "unexpected type")))
that is, until it is shown to be necessary to handle multiple type
possibilities. The former is a more precise contract of what the function is
supposed to do. A client cannot even *express* (this kind of) incorrect usage,
since the static typing prevents it.
Of course, both are vastly preferrable to this:
(defun (doit to-me) ;; had better be an integer, by God!
(process to-me))
--
Cheers, The Rhythm is around me,
The Rhythm has control.
Ray Blaak The Rhythm is inside me,
bl...@infomatch.com The Rhythm has my soul.
Erik Naggum wrote:
> * David Hanley <d...@ncgr.org>
> | It seems possible (to me) to write some lisp macros to produce a typed
> | version of the language...
>
> before you reinvent the wheel, please investigate the THE special form
> and how it behaves in interpreted and compiled code under various
> optimization settings. you might be _very_ surprised.
I do know about the "the" form, but:
1) I don't beleive it's doing static checking. A compile error will
not be signaled if the types could be proved at compile time to
be mismatched.
2) The standard explicitly states that the results if
the "real" types do not match the "the" type is undefined.
http://www.xanalys.com/software_tools/reference/HyperSpec/Body/speope_the.html
dave
(DECLAIM (FTYPE (FUNCTION ( {formal-types}* ) return-type)
function-name))
e.g
---
(declaim (ftype (function (integer) t)
doit))
I hope that helps and that
Tunc
On Wed, 8 Mar 2000, Robert Monfera wrote:
>
Ray Blaak wrote:
>
> > That is, during building a system out of components/modules/subsystems
> > whatever, when piecing together the parts, having things not compile
> > unless things "fit" is a major major help.
>
> I agree in that interfaces are the critical parts for type checking,
> because the developer of the module is responsible for balancing
> performance and robustness inside a module, but he can never take it
> granted how the module will be used. This is unfortunately true for
> run-time errors too, and I think that error checking at the interface
> level and static typing are orthogonal.
>
> > E.g. This is preferrable (apologies for any syntax errors):
> >
> > (defun (doit (integer to-me))
> > (process to-me))
>
> What's wrong with
>
> (defmethod doit ((integer to-me))
> (process to-me))
>
> It does what you expect, run-time.
>
> > over this:
> >
> > (defun (doit to-me)
> > (cond ((integerp to-me) (process to-me))
> > (error "unexpected type")))
>
> You could use ASSERT or even better, CHECK-TYPE. They're quite a bit
> nicer.
>
> Robert
>
>
huh? through the high number of people who reinvent it in various ways,
and the low number of people who point out that they are reinventing
existing functionality whenever this happens. isn't this quite obvious?
#:Erik
> few Common Lisp programmers seem to know about the THE form, however.
How can you tell?
(knows-p (the seasoned programmer) (the form 'the-form)) -> T
Robert
> (defmethod doit ((integer to-me))
> (process to-me))
Sorry for the typo, I just took code reuse literally :-)
(defmethod doit ((to-me integer))
(process to-me))
>> E.g. This is preferrable (apologies for any syntax errors):
>>
>> (defun (doit (integer to-me))
>> (process to-me))
> What's wrong with
> (defmethod doit ((integer to-me))
> (process to-me))
> It does what you expect, run-time.
But not at compile time, which is the point. However, you can do
(declaim (ftype (function (integer) t) doit))
after which some implementations (CMUCL) will issue compile-time
warnings if it can tell the argument isn't an integer.
--
Succumb to natural tendencies. Be hateful and boring.
(setq reply-to
(concatenate 'string "Paul Foley " "<mycroft" '(#\@) "actrix.gen.nz>"))
This is different from run-time dispatch, for example, the compiler may
completely ignore it. Even if an implementation makes use of this
declaration, it's mostly used for optimizations. Paul Foley just
hinted that CMUCL compares such declarations with inferred types, but
it's neither guaranteed by the standard nor is a widespread feature
among implementations.
Robert
> In article <gat-060300...@milo.jpl.nasa.gov>,
> g...@jpl.nasa.gov (Erann Gat) wrote:
> > As I wrote to Paul, I work for NASA and I am trying to convince people
> > to use Lisp on spacecraft, which are multimillion-dollar assets.
> Managers
> > want to see safety guarantees, not just empirical evidence. Just
> because
> > something hasn't been a problem in the past doesn't mean it won't be a
> > problem in the future. And in the space biz, the first glitch could
> also
> > be your last.
>
> Hi,
>
> This is a serious question, and not meant to trigger a flame-fest, so
> maybe it's best answered and asked (sorry) be email. Here goes...
>
> While I like Lisp a lot, it strikes me that a statically typed language
> might be preferable in extreme reliability situations (I'm thinking of
> ML, for example). Is that an issue in your experience, and how do you
> defend Lisp against that criticism?
Lisp is easy to type statically, and the fact that it doesn't have to
always be typed has significant advantages.
There's a legitimate issue in there, in that typing isn't mandatory in
Lisp.
The one thing I would add to Lisp's type system are abstract types,
meaning types that are defined by supporting certain operations. You
can kind of kluuge them in Lisp with:
(satisfies
(compute-applicable-methods generic-function args... ))
but that's unneccessarily complex and indirect.
--
Tom Breton, http://world.std.com/~tob
Not using "gh" since 1997. http://world.std.com/~tob/ugh-free.html
Rethink some Lisp features, http://world.std.com/~tob/rethink-lisp/index.html
I agree with all of this. Its just that I'm not convinced that static
typing (or dynamic typing) is a silver bullet But what I was thinking
about at this point is probably straying into `worse is better'
territory. Having a language (and possibly an OS) that enables you to
deal which runtime errors if you want rather that going into core-dump
kernel-panic or whatever is probably a win. Putting it another way, I
would prefer BNFL to use lisp and UNIX for their control software,
rather than C++/MFC under windows 98, say ;)
> (Incidentally, in this context, `type' often means much more than
> `representational type' -- it can be very useful to know that
> something is an (integer 0 8) say).
Which, if this is honoured, is a real bonus,
Cheers,
:) will
Andrew Cooke wrote:
> it seems that the earlier one catches errors the better.
This isn't always true.
One advantage of run-time errors (compared to compile-time errors) is that
there's a lot more context available to show you where you went wrong. You
don't just get a message from the compiler telling you in abstract terms why
your program is impossible. Instead, you get a fully worked-out example,
presented on a silver platter by your debugger.
For most typos and simple thinkos this may not be very important; but for
real bugs, it can be invaluable. I've spent hours staring at type mismatch
error messages from ML compilers only to find bugs that would've taken me
a few minutes to find with a decent debugger.
Arthur Lemmens
Although it's neither standard nor common, if one cared about static
typing, one could quite reasonably write a separate static type-checker
for CL that made use of such global (and local) declarations, as well
as a lot of type-inference information on the built-in functions. In
principle, this shouldn't be much harder than writing a type-checker
for one of the modern polymorphic functional languages, modulo:
- List/Cons types: We probably need better type specifiers to note in
a statically recognizable way that lists contain only elements of
type X. Without this, you can't do much type inference on list
operations (like first, etc.), and so the need for local type
declarations increases.
- Once dynamism sets in, users will have to make guarantees via local
declarations somewhere, or type-checking will break down:
(let ((x (read stream)))
;; This will propagate as Type t and cause all subsequent type
;; inference to fail => yield t. So you'll have to narrow the
;; type at some point, not do degenerate into a mass of erroneous
;; warnings/errors.
(+ x 1) ; Will raise error, since t is not a subtype of number
(cons x nil) ; Will raise no error, but TI will yield a type of
; (cons t null) which will probably get you into
; trouble later on...
(etypecase x
(number (+ x 1)) ; These work, and produce mildly
(string (cons x nil)))) ; meaningful inferred types...
- All the hairier features of CL reading and evaluation will mean that
you'll probably have to take a compiler front-end embedded in the CL
implementation of your choice as a front-end to your type-checker.
- Probably quite a number of things I've missed.
All in all you could probably do worse than starting with CMUCL's type
stuff (probably in the guise of SBCL), and modify it's behaviour in a
number of places:
- Turn around the type-checking logic in a number of places, so that
simple intersection of types doesn't suffice: Arguments must be
subtypes of the declared type.
Currently the following will compile without warnings in CMUCL
(declaim (ftype (function ((or cons number) (or cons number))
number) myfun3))
(defun myfun3 (x y)
(+ x y))
(Although with high speed settings it will produce efficiency
notes). This should raise a warning/type-error.
- Probably improve some of the type inferrence and type recognition
code in some places, a number of other things...
You might also want to take a look at Henry G. Baker's Paper "The
Nimble Type Inferencer for Common Lisp-84", which is available at
ftp://ftp.netcom.com/pub/hb/hbaker/TInference.html
All in all, I'd say if some student is looking for something to do
with both theoretical and practical contents, and a connection to CL,
then implementing something like this should make for a nice project,
possibly worth a nice degree of some sort...
> I agree with all of this. Its just that I'm not convinced that static
> typing (or dynamic typing) is a silver bullet
In case it wasn't clear from my posts in this thread: neither do I.
>> (Incidentally, in this context, `type' often means much more than
>> `representational type' -- it can be very useful to know that
>> something is an (integer 0 8) say).
> Which, if this is honoured, is a real bonus,
CMUCL can make use of info like this. For instance if you have two
suitably small fixnums a,b then it can prove that a + b is a fixnum
too. Likewise for things like SQRT (I think).
--tim
> One advantage of run-time errors (compared to compile-time errors) is that
> there's a lot more context available to show you where you went wrong. You
> don't just get a message from the compiler telling you in abstract terms why
> your program is impossible. Instead, you get a fully worked-out example,
> presented on a silver platter by your debugger.
But there are situations where run-time errors are just too expensive
to have.
Ariane looks like a place where they'd decided this, but probably they
were wrong. (The argument put forward seems to be that having error
handlers in there (which Ada has, of course) would have made the code
slower so they'd miss their real-time budget. I think this is
implausible, but I don't know.)
But things like nuclear power plant control systems are definitely cases
where you might worry about this -- *certainly* you don't want to end
up sitting in the debugger in some time-critical part of the code.
There, now I've mentioned nuclear power *and* spacecraft in one
message about type checking! I believe this is sufficient to invoke
the C.L.L version of Godwin's law. Actually I shall also just
randomly say that Lisp is dead thus ensuring that I invoke it.
--tim
> - List/Cons types: We probably need better type specifiers to note in
> a statically recognizable way that lists contain only elements of
> type X. Without this, you can't do much type inference on list
> operations (like first, etc.), and so the need for local type
> declarations increases.
I was thinking about this the other day. Once the cons specifier
can take optional car and cdr type arguments, the specific list types
become:
(deftype list (&optional (typ nil typ-p))
(if typ-p
`(or (cons ,typ) null)
`(or cons null)))
(deftype proper-list (typ) `(or null (cons ,typ (proper-list ,typ))))
Note that Series already understands specifiers like (list fixnum).
--
Fernando D. Mato Mira
Real-Time SW Eng & Networking
Advanced Systems Engineering Division
CSEM
Jaquet-Droz 1 email: matomira AT acm DOT org
CH-2007 Neuchatel tel: +41 (32) 720-5157
Switzerland FAX: +41 (32) 720-5720
www.csem.ch www.vrai.com ligwww.epfl.ch/matomira.html
> (deftype list (&optional (typ nil typ-p))
> (if typ-p
> `(or (cons ,typ) null)
> `(or cons null)))
I forgot to recurse:
(deftype list (&optional (typ nil typ-p))
(if typ-p
`(or null (cons ,typ (or (not list) (list ,typ))))
`(or cons null)))
> One advantage of run-time errors (compared to compile-time errors) is that
> there's a lot more context available to show you where you went wrong. You
> don't just get a message from the compiler telling you in abstract terms why
> your program is impossible. Instead, you get a fully worked-out example,
> presented on a silver platter by your debugger.
>
> For most typos and simple thinkos this may not be very important; but for
> real bugs, it can be invaluable. I've spent hours staring at type mismatch
> error messages from ML compilers only to find bugs that would've taken me
> a few minutes to find with a decent debugger.
I think that tracking down such bugs in ML would be much easier if
compilers showed the type derivation that led to the mismatch.
(Maybe some do; the ones I've seen don't.)
Andras
> "Fernando D. Mato Mira" wrote:
>
> > (deftype list (&optional (typ nil typ-p))
> > (if typ-p
> > `(or (cons ,typ) null)
> > `(or cons null)))
>
> I forgot to recurse:
>
> (deftype list (&optional (typ nil typ-p))
> (if typ-p
> `(or null (cons ,typ (or (not list) (list ,typ))))
> `(or cons null)))
And there's the rub: In CL cons is a compound type specifier that can
take car and cdr type specs. BUT you aren't allowed to define
recursive type specifiers with deftype. See postings a couple of
years ago about this issue.
Since I agree that introducing recursive type specifiers into CL is a
bit problematic (deftype is like defmacro, but without the result
being evaluated, so you'd have to do lazy expansion), introducing an
atomic list type specifier might be the way to go.
As has been said in other posts, one fundamental thing about static
type-checking is that it is always a tradeoff. You cannot
automatically accept all `correct' programs and reject all
in-`correct' ones, and at the same time give a sensible,
uncontroversial meaning to `correct'. As an example, division by zero
is usually not considered a type error by static typing supporters
(rather it's considered a run-time exception), and quite some ML code
I've seen compiles with warnings about non-exhaustive case analyses.
Static type-checking is relative to your type-system and your
definition of type-correctness. It can give you useful information at
compile time. At the same time the restrictions of your type system
can prevent you from doing pretty sensible things, like dynamically
changing and extending a complex running piece of software in ML:
there's the static typing slogan `if it compiles it's correct'; by
modus tollens this becomes something like `it won't compile unless the
compiler thinks it's correct'.
So what are the advantages (+) and disadvantages (-) of compile-time
type-checking (in a broad sense) as compared to runtime checks? In
addition to the ones that have been mentionned in other followups I am
aware of the following.
+ You don't have to test a counterexample before you know that you got
something wrong
+ You don't have to invent the counterexample in the first place
- There are properties you cannot check at compile-time unless you are
prepared to allow interactive theorem proving as part of the
compilation process (e.g. `the resulting tree is balanced', or some
such)
+ You might not be prepared to check these properties at runtime
either (for efficiency reasons, say)
+ Some important properties are not meaningfully expressible as
runtime checks (`this function terminates')
- It is difficult to design a type system for lisp that allows at
least a significant amount of `normal' programs to be checked
automatically
Does this make sense? Any comments?
Cheers,
Axel
> And there's the rub: In CL cons is a compound type specifier that can
> take car and cdr type specs.
Gee. That's "new". I missed that one.
> BUT you aren't allowed to define
> recursive type specifiers with deftype.
Yeah. I know that, but then I also write stuff like (declare
(wihout-full-continuations)) ;->
> See postings a couple of
> years ago about this issue.
>
> Since I agree that introducing recursive type specifiers into CL is a
> bit problematic (deftype is like defmacro, but without the result
> being evaluated, so you'd have to do lazy expansion), introducing an
> atomic list type specifier might be the way to go.
If I like Lisp, it's because I want one language that can do all and more nice
things any other can [And even some not so nice, like volatile char *reg,
what!]
Actually, the problem with Ariane, as I understand it, was that they took code
for the Ariane 4, reasoned (incorrectly) that it could run without changes or
testing on Ariane 5, and simply used it.
A situation that was impossible for Ariane 4 happened on Ariane 5,
inappropriate error handler invoked, and the rocket blew up.
The problem had nothing to do with the language used, or error handling
mechanisms per se. The problem was the use of software being used in an
environment it was not designed for.
> A situation that was impossible for Ariane 4 happened on Ariane 5,
> inappropriate error handler invoked, and the rocket blew up.
I think the problem was that there wasn't an overflow handler
reasonably close to where the overflow happened -- it just trapped out
to some default handler which then dumped debugging output down the
wire and broke other stuff. They'd reasoned that `this can't happen'
for ariane 4 and this left out the sanity checks
> The problem had nothing to do with the language used, or error handling
> mechanisms per se. The problem was the use of software being used in an
> environment it was not designed for.
I agree with that of course. But if they had written the thing more
defensively (`even though this can never overflow I'll deal with the
case that it might', just in case someone reuses my code in some
different context without checking) they might have survived even so,
although I have heard the claim that this extra protection might have
meant they'd miss real-time deadlines.
But yes, of course it was an organisational foulup more than anything.
Ariane is like inconsistency in formal systems, you can use it to prove
whatever you like!
--tim
| Actually, the problem with Ariane, as I understand it, was that they
| took code for the Ariane 4, reasoned (incorrectly) that it could run
| without changes or testing on Ariane 5, and simply used it.
|
| A situation that was impossible for Ariane 4 happened on Ariane 5,
| inappropriate error handler invoked, and the rocket blew up.
It is not clear to me from what I have read if it was really
impossible on Ariane 4, or merely very unlikely. Apparently, part of
the problem was the greater acceleration of the Ariane 5. A
conversion from a 64 bit floating point number to a 16 bit signed
integer overflowed, the overflow was not trapped, and the resulting
error code was interpreted as flight data.
<http://sspg1.bnsc.rl.ac.uk/Share/ISTP/ariane5rep.htm>
| The problem had nothing to do with the language used, or error handling
| mechanisms per se. The problem was the use of software being used in an
| environment it was not designed for.
"Lack of attention to the strict preconditions below, especially the
last term in each, was the direct cause of the destruction of the
Ariane 5 and its payload [...]"
<http://www.cs.wits.ac.za/~bob/ariane5.htm>
(Risks Digest is a good source of information on this kind of thing.)
--
* Harald Hanche-Olsen <URL:http://www.math.ntnu.no/~hanche/>
- "There arises from a bad and unapt formation of words
a wonderful obstruction to the mind." - Francis Bacon
This has been discussed endlessly on comp.lang.ada several times since the
accident. With the Ariane 4, this particular condition could not possibly
occur except in the event of some sort of hardware failure, in which case
error handling was pointless and a computer shutdown (passing control to the
backup (the French usage of the term seems to be confusingly different from
the American)) was considered to be the best action to take. If the backup
did the same thing, it really didn't matter with the Ariane 4 because that
meant something was catastrophically and irretrievably wrong with the
rocket.
What I don't understand is why the Inertial Reference Systems (that choked
on the out-of-range data) were even operating at all after launch. They
served no purpose then, but it was considered a "don't care" situation. That
was one of the two stupid design decisions that caused the accident. The
other one was taking that subsystem from Ariane 4 and just sticking it in
Ariane 5 without any kind of review.
> | The problem had nothing to do with the language used, or error handling
> | mechanisms per se. The problem was the use of software being used in an
> | environment it was not designed for.
>
> "Lack of attention to the strict preconditions below, especially the
> last term in each, was the direct cause of the destruction of the
> Ariane 5 and its payload [...]"
>
> <http://www.cs.wits.ac.za/~bob/ariane5.htm>
Yes, the programmers produced _exactly_ what was specified for the Ariane 4.
It's not their fault (nor Ada's) that the specs were somewhat stupid for
Ariane 4 and totally stupid for the Ariane 5 which came along years later.
From things I've read, it's all something all too typical with the
apparently incredibly bureaucratic ESA. It does seem that NASA is also
increasingly suffering from the chronic bureaucratic bloat that eventually
seems to afflict almost every governmental agency.
Larry
Yes, this seems to be a compiler problem, not a language problem. The early
Ada compilers were wretched in this regard (as well as many others) which
helped cast a pall over the language from which it still hasn't really
recovered. As far as static vs. dynamic typing goes, I can't really add
anything useful since my experience with Lisp and dynamic typing goes back
only 4 months (I'm now working my way through Norvig's book, which certainly
lives up to it's recommendations here), but except for trivial programs, I
greatly prefer strong static typing (Ada 95) over weak static typing (C, and
to a lesser extent C++). That is, _if_ the compiler gives good warnings and
error messages. If it doesn't, you're not much better off. I found that when
I used Ada, I rarely ever _used_ a debugger, whereas with C/C++, it's almost
essential to have a good one at hand.
Forth (which I really liked and used a lot back when I had a Z-80 CP/M
machine, but is too low level where it's standardized and incredibly
fragmented where it's not (much worse than Lisp ever was, IMHO)) has no type
checking at all and what would be considered primitive debugging tools in
other languages. Using small word definitions and bottom-up interactive
programming made sophisticated debuggers superfluous. This seems to apply to
Lisp, too.
One question I have that really relates to this newsgroup is: does using
lots of smaller definitions have a negative performance impact on Lisp? I
know it does with other languages, but after learning and using Forth
(second language I learned after Basic), I came to have a real abhorrence of
long function definitions that stretch over several pages. Is there any
consensus of opinion on this question?
Larry
> And there's the rub: In CL cons is a compound type specifier that can
> take car and cdr type specs. BUT you aren't allowed to define
> recursive type specifiers with deftype. See postings a couple of
> years ago about this issue.
Discussion on this issue occured more recently than a couple years
ago. I remember Lispworks being the only Lisp able to make use of CONS
compound type specifiers.
Christopher
> Although it's neither standard nor common, if one cared about static
> typing, one could quite reasonably write a separate static type-checker
> for CL that made use of such global (and local) declarations, as well
> as a lot of type-inference information on the built-in functions.
This has been done for Scheme by some people at Rice. They call it
soft typing. Basically, the type inference engine tries to prove the
correctness of as much of the program as it can and it inserts code to
check at run time where it can't. IIRC, you can get a front end for
DrScheme that will indicate where checks were inserted so you can get
to a fully statically checked program by inserting your own checks.
One of the papers describing this is at
http://www.cs.rice.edu/CS/PLT/Publications/toplas97-wc.ps.gz
I don't see any large problems in doing the same for CL although
encoding the effects of all standard functions would be a large job.
--
Lieven Marchand <m...@bewoner.dma.be>
If there are aliens, they play Go. -- Lasker
>
> One question I have that really relates to this newsgroup is: does using
> lots of smaller definitions have a negative performance impact on Lisp?
>
Quick answer: Not really. Don't worry about it.
Long answer: It might, depending upon how often the function runs,
how much `overhead' is involved in the function calling sequence, how
much `overhead' is involved in inlining it (by introducing more
variables into the function's caller, you might cause the compiler
to `spill' regist