Hello.
I'm a beginner in Lisp. I'm using Allegro Common Lisp and I want to
define a function with arguments of a specific type. For example, the
typical function:
(defun df* (a b)
(declare (double-float a b))
(* a b))
should fail with (df* 2 3), but it works! How can I get a type error?
Does somebody know it?
Thank you in advance.
Antonio Garrido Tejero <········@dsic.upv.es> writes:
> Hello.
>
> I'm a beginner in Lisp. I'm using Allegro Common Lisp and I want to
> define a function with arguments of a specific type. For example, the
> typical function:
>
> (defun df* (a b)
> (declare (double-float a b))
> (* a b))
>
> should fail with (df* 2 3), but it works! How can I get a type error?
> Does somebody know it?
>
> Thank you in advance.
>
In CMUCL
==============================================================================
* (defun df* (a b)
(declare (double-float a b))
(* a b))
DF*
* (compile 'df*)
DF*
NIL
NIL
* (df* 2 3)
Invoking debugger...
... 2 is not of type DOUBLE-FLOAT
==============================================================================
You can tune this behavior.
OTOH
==============================================================================
* (defun df* (a b)
(declare (double-float a b))
(* a b))
DF*
* (df* 2 3)
6
==============================================================================
Which is what you'd expect, given that the "compilation" process done
at "interpreter" level is not the full one.
If you want something along the lines you seem expect, you should use
ML (alas with many more constraints on types)
==============================================================================
·······@copernico:~ 51> sml
Standard ML of New Jersey, Version 0.93, February 15, 1993
val it = () : unit
- fun dfstar a b : real = a * b;
val dfstar = fn : real -> real -> real
==============================================================================
However
==============================================================================
- dfstar 2 3.0;
std_in:3.1-3.12 Error: operator and operand don't agree (tycon mismatch)
operator domain: real
operand: int
in expression:
dfstar 2
-
==============================================================================
while
==============================================================================
* (defun df-g-* (a b)
(declare (double-float b))
(* a b))
DF-G-*
* (compile 'df-g-*)
DF-G-*
NIL
NIL
* (df-g-* 2 3.0d0)
6.0d0
==============================================================================
Of course I am lagging way behinf ML development and therefore things
may have changed.
Going back to CMUCL first version of df*
==============================================================================
* (defun df* (a b)
(declare (type double-float a b))
(* a b))
DF*
* (defun use-df* (x)
(df* x 4))
USE-DF*
* (compile 'df*)
DF*
NIL
NIL
* (compile 'use-df*)
In: LAMBDA (X)
(DF* X 4)
Warning: This is not a DOUBLE-FLOAT:
4
Compilation unit finished.
1 warning
USE-DF*
T
T
*
==============================================================================
Cheers
--
Marco Antoniotti ===========================================
PARADES, Via San Pantaleo 66, I-00186 Rome, ITALY
tel. +39 - 06 68 10 03 17, fax. +39 - 06 68 80 79 26
http://www.parades.rm.cnr.it/~marcoxa
Marco Antoniotti escribi�:
> In CMUCL
>
> ==============================================================================
> * (defun df* (a b)
> (declare (double-float a b))
> (* a b))
> DF*
> * (compile 'df*)
> DF*
> NIL
> NIL
> * (df* 2 3)
> Invoking debugger...
>
> ... 2 is not of type DOUBLE-FLOAT
> ==============================================================================
>
> You can tune this behavior.
Thanks to Marco Antoniotti, but it doesn't work yet.
How can I tune the behavior of Allegro Common Lisp to obtain the error "... 2 is
not of type DOUBLE-FLOAT".
Thank you
>>>>> "Antonio" == Antonio Garrido Tejero <········@dsic.upv.es> writes:
Antonio> Marco Antoniotti escribi�:
>> In CMUCL
>>
>> ==============================================================================
>> * (defun df* (a b)
>> (declare (double-float a b)) (* a b)) DF*
>> * (compile 'df*)
>> DF* NIL NIL
>> * (df* 2 3)
>> Invoking debugger...
>>
>> ... 2 is not of type DOUBLE-FLOAT
>> ==============================================================================
>>
>> You can tune this behavior.
Antonio> Thanks to Marco Antoniotti, but it doesn't work yet.
Antonio> How can I tune the behavior of Allegro Common Lisp to
Antonio> obtain the error "... 2 is not of type DOUBLE-FLOAT".
Can't you do something like:
(defun df* (a b)
(declare (double-float a b))
(check-type a double-float)
(check-type b double-float)
(* a b))
Maybe an ASSERT instead of CHECK-TYPE would work for you too:
(assert (and (typep a 'double-float) (typep b 'double-float)))
Ray
In article <··············@rtp.ericsson.se>,
Raymond Toy <···@rtp.ericsson.se> wrote:
>Can't you do something like:
>
>(defun df* (a b)
> (declare (double-float a b))
> (check-type a double-float)
> (check-type b double-float)
> (* a b))
>
>Maybe an ASSERT instead of CHECK-TYPE would work for you too:
>
>(assert (and (typep a 'double-float) (typep b 'double-float)))
The proper way to do this is:
(defun df* (a b)
(check-type a double-float)
(check-type b double-float)
(locally
(declare (double-float a b))
(* a b)))
Remember, in Common Lisp, type declarations are a promise by the programmer
that the variables will be of the specified type. They are *not* a request
that type checks be inserted. The intent is to speed up code by allowing
the compiler to make assumptions rather than performing runtime checks.
In some implementations, if you declare high SAFETY optimization, type
checks will be inserted. It might also be necessary to declare low SPEED.
But this is not required by the language spec and not portable.
--
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Burlington, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
Antonio Garrido Tejero <········@dsic.upv.es> writes:
> Marco Antoniotti escribi�:
>
> > In CMUCL
> >
> > ===========================================================================
> > * (defun df* (a b)
> > (declare (double-float a b))
> > (* a b))
> > DF*
> > * (compile 'df*)
> > DF*
> > NIL
> > NIL
> > * (df* 2 3)
> > Invoking debugger...
> >
> > ... 2 is not of type DOUBLE-FLOAT
> > ===========================================================================
> >
> > You can tune this behavior.
>
> Thanks to Marco Antoniotti, but it doesn't work yet.
>
> How can I tune the behavior of Allegro Common Lisp to obtain the error "... 2 is
> not of type DOUBLE-FLOAT".
>
You are welcome. But. I am using CMUCL, which has a very good
compiler when it comes to type checking. I do not know whether ACL has
the same behavior.
CL is not required to signal an error in that case, and the compiler
may use the information you give to generate good code. Note that
what I reported is a runtime error, not a compile time one.
In the second example I gave, I get a compiler *warning* about the
"wrong" type.
Note however that when programming with CL, typing is something you
usually worry about at a rather late stage.
So the real question to you is: why do you need to be so precise about
types? C/C++ heritage, or MLish attitude? :)
Cheers
--
Marco Antoniotti ===========================================
PARADES, Via San Pantaleo 66, I-00186 Rome, ITALY
tel. +39 - 06 68 10 03 17, fax. +39 - 06 68 80 79 26
http://www.parades.rm.cnr.it/~marcoxa
I'm somewhat surprised no one yet has suggested the THE macro.
CL-USER 5 > (the double-float 2)
Error: The value 2 does not satisfy the type specifier DOUBLE-FLOAT.
CL-USER 13 > (the double-float 2.0)
Error: The value 2.0 does not satisfy the type specifier DOUBLE-FLOAT.
CL-USER 15 > (the double-float 2.0d0)
2.0D0
AFAIK, it will cause your code to slow down because of extra type checking,
and may turn out to be harder to eliminate than type declarations that
others have suggested. OTOH, the behavior is specified by the ANSI spec
(http://www.harlequin.com/education/books/HyperSpec/Body/speope_the.html)
so at least you know what behavior to expect across implementations.
Sunil
Antonio Garrido Tejero <········@dsic.upv.es> writes:
> Marco Antoniotti escribi�:
>
> > In CMUCL
> >
> > ==============================================================================
> > * (defun df* (a b)
> > (declare (double-float a b))
> > (* a b))
> > DF*
> > * (compile 'df*)
> > DF*
> > NIL
> > NIL
> > * (df* 2 3)
> > Invoking debugger...
> >
> > ... 2 is not of type DOUBLE-FLOAT
> > ==============================================================================
> >
> > You can tune this behavior.
>
> Thanks to Marco Antoniotti, but it doesn't work yet.
>
> How can I tune the behavior of Allegro Common Lisp to obtain the error "... 2 is
> not of type DOUBLE-FLOAT".
>
> Thank you
In article <···············@whizzy.cc.gatech.edu>,
Sunil Mishra <·······@whizzy.cc.gatech.edu> wrote:
>I'm somewhat surprised no one yet has suggested the THE macro.
Because it doesn't solve the problem. THE is a way of adding a type
declaration to an expression, just as DECLARE specifies a type declaration
of a variable, but it doesn't add type checking. Some implementations
perform type checking when high safety is enabled, but it's not required by
the language.
--
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Burlington, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
Barry Margolin <······@bbnplanet.com> writes:
> Because it doesn't solve the problem. THE is a way of adding a type
> declaration to an expression, just as DECLARE specifies a type declaration
> of a variable, but it doesn't add type checking. Some implementations
> perform type checking when high safety is enabled, but it's not required by
> the language.
Heh, sorry, misinterpreted the definition the first time I read it.
Sunil
* Antonio Garrido Tejero <········@dsic.upv.es>
| I'm using Allegro Common Lisp and I want to define a function with
| arguments of a specific type.
why?
| For example, the typical function:
|
| (defun df* (a b)
| (declare (double-float a b))
| (* a b))
|
| should fail with (df* 2 3), but it works!
great, isn't it?
| How can I get a type error?
you can do
(defun fd* (a b)
(check-type a double-float)
(check-type a double-float)
(* a b))
if you think you are going to win a speed contest with your type
"checking", you aren't. is that why you want this stuff?
#:Erik
--
@1999-07-22T00:37:33Z -- pi billion seconds since the turn of the century
Antonio Garrido Tejero <········@dsic.upv.es> writes:
>
> I'm a beginner in Lisp. I'm using Allegro Common Lisp and I want to
> define a function with arguments of a specific type. For example, the
> typical function:
>
> (defun df* (a b)
> (declare (double-float a b))
> (* a b))
>
> should fail with (df* 2 3), but it works! How can I get a type error?
> Does somebody know it?
Lisp is not required to check the types, nor is the compiler required to
use the type information to improve code efficiency.
You can, however, force type checking by using the the CHECK-TYPE call
explictly:
(defun df* (a b)
(declare (double-float a b))
(check-type a double-float)
(check-type b double-float)
(* a b))
TEST:TEST-THEORY> (df* 2 3)
Error: the value of A is 2, which is not of type DOUBLE-FLOAT.
[condition type: TYPE-ERROR]
Restart actions (select using :continue):
0: supply a new value for A.
1: Return to Top Level (an "abort" restart)
[1]TEST:TEST-THEORY> :reset
TEST:TEST-THEORY> (df* 2.0 3)
Error: the value of A is 2.0, which is not of type DOUBLE-FLOAT.
[condition type: TYPE-ERROR]
Restart actions (select using :continue):
0: supply a new value for A.
1: Return to Top Level (an "abort" restart)
[1]TEST:TEST-THEORY> :reset
TEST:TEST-THEORY> (df* 2.0d0 3)
Error: the value of B is 3, which is not of type DOUBLE-FLOAT.
[condition type: TYPE-ERROR]
Restart actions (select using :continue):
0: supply a new value for B.
1: Return to Top Level (an "abort" restart)
[1]TEST:TEST-THEORY> (df* 2.0d0 3.0d0)
6.0d0
--
Thomas A. Russ, USC/Information Sciences Institute ···@isi.edu
In article <···············@sevak.isi.edu>,
Thomas A. Russ <···@sevak.isi.edu> wrote:
>You can, however, force type checking by using the the CHECK-TYPE call
>explictly:
>
>(defun df* (a b)
> (declare (double-float a b))
> (check-type a double-float)
> (check-type b double-float)
> (* a b))
This is not correct. The declaration tells the compiler that the
CHECK-TYPEs are guaranteed to succeed, so it can optimize them away! I
don't have CMUCL so I can't test it, but I suspect that its type
propagation code may actually be able to do this.
You need to put the type checks outside the scope of the declaration. As I
wrote in an earlier post, the way to code this is:
(defun df* (a b)
(check-type a double-float)
(check-type b double-float)
(locally (declare (double-float a b))
(* a b)))
--
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Burlington, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
Barry Margolin <······@bbnplanet.com> writes:
> In article <···············@sevak.isi.edu>,
> Thomas A. Russ <···@sevak.isi.edu> wrote:
> >You can, however, force type checking by using the the CHECK-TYPE call
> >explictly:
> >
> >(defun df* (a b)
> > (declare (double-float a b))
> > (check-type a double-float)
> > (check-type b double-float)
> > (* a b))
>
> This is not correct. The declaration tells the compiler that the
> CHECK-TYPEs are guaranteed to succeed, so it can optimize them away! I
> don't have CMUCL so I can't test it, but I suspect that its type
> propagation code may actually be able to do this.
>
> You need to put the type checks outside the scope of the declaration. As I
> wrote in an earlier post, the way to code this is:
>
> (defun df* (a b)
> (check-type a double-float)
> (check-type b double-float)
> (locally (declare (double-float a b))
> (* a b)))
Though, in fairness, any implementation that can tell the first can be
optimized out also probably doesn't need the second, corrected form.
Being after a check-type with no subsequent assignment should be
enough to infer the type. Some compilers may not be smart enough,
though, so you're right that this second one at least is both correct
and friendly to compilers doing less type analysis, which I'm sure means
quite a number of compilers out there.
Incidentally, no one has said it, but check-type only really guarantees
run-time checking. Earlier checking might be done, but there is no
requirement of it. So in a trival sense, the question of how you can
force an error in the original case, if you assume the error is to be
forced at compile time, is: you can't. Lisp doesn't do strong typing.
It doesn't pretend to try.
If the type-introspection stuff from CLLT2 had not been removed in
ANSI CL, you almost could have written a macro or compiler-optimizer
that did what you wanted. We didn't remove that stuff because we thought
it was a bad idea--we only removed it because it was buggy enough that
we didn't think we could fix it in the time left before the standard
was due out. It's really a shame that it had to be removed, but buggy
is worse than not present, since vendors can at least add working
versions on their own--forcing them to implement something buggy to
conform was just too much for us to want to do.
Kent M Pitman <······@world.std.com> writes:
>
> Incidentally, no one has said it, but check-type only really guarantees
> run-time checking. Earlier checking might be done, but there is no
> requirement of it. So in a trival sense, the question of how you can
> force an error in the original case, if you assume the error is to be
> forced at compile time, is: you can't. Lisp doesn't do strong typing.
> It doesn't pretend to try.
>
This leads to something I've been curious about for a while: has anyone ever
built a language using lisp parenthesized syntax but with statically-typed
semantics similar to ML? I'm not trying to get into a debate over whether
statically-typed languages are "better" than dynamically-typed ones (IMHO it
depends on a number of factors, including what stage of program development
you're in and how often the resulting code is likely to need to change). But
I find it curious that all the ML family of languages (as well as lazy
languages like Haskell and Miranda) have abandoned the lisp syntax, despite
the numerous advantages which have been described in a different thread. I
can think of no good reason why this has to be the case. Any thoughts on
this? I think it would be cool if there was a statically-typed dialect of
lisp, since I prefer having my type errors caught at compile-time. OTOH you
do lose some flexibility that way, so the ultimate solution would be a system
where you could select either typing system, perhaps on a file-by-file basis.
Mike
-------------------------------------------------------------------------
Mike Vanier ·······@bbb.caltech.edu
Department of Computation and Neural Systems, Caltech 216-76
Will optimize nonlinear functions with complex parameter spaces for food.
In article <·················@arathorn.bbb.caltech.edu>, Michael Vanier wrote:
> I think it would be cool if there was a statically-typed dialect of
> lisp, since I prefer having my type errors caught at compile-time. OTOH you
> do lose some flexibility that way, so the ultimate solution would be a system
> where you could select either typing system, perhaps on a file-by-file basis.
Would you have to lose flexibility? Your stated alternatives of (1) choosing
EITHER strongly typed OR weakly typed, or (2) choosing file-by-file, both seem
very restrictive to me.
It would seem much more in the nature of Lisp to make strong typing information
completely optional, just like ordinary Lisp type declarations are. In fact,
it could be all that we need is requirements for strong type inferencing and
compile-time type errors.
The idea would be, the compiler reports all type conflicts that it can deduce.
The more type information you add to your program (at any granularity, even
a local block within one function within one file!), the more conclusions the
compiler can draw. If it ever finds a conflict, that becomes a "strongly
typed" compiler error.
The beauty of this is that Lisp syntax is already sufficient. You could make
the test be something like if SPEED > SAFETY, then report compile-time type
errors. It might work something like:
(defun foo (a b)
(declare (type integer a b))
(+ a b) )
(defun bar ()
(foo 1.0 2) )
So that when SPEED > SAFETY, "(compile bar)" gives
Error [in call to FOO]: 1.0 is not an integer
Perhaps this has become more a request to vendors than a question about
standards or language design...
-- Don
___________________________________________________________________________
Don Geddis ······@cadabra.com Phone (650) 508-7893
http://cadabra.com Fax (650) 508-7891
Cadabra Inc. 275 Shoreline Drive, Suite 505, Redwood Shores, CA 94065
Seen on the door to a light-wave lab:
"Do not look into laser with remaining good eye."
······@Cadabra.Com (Don Geddis) writes:
> It would seem much more in the nature of Lisp to make strong typing
> information completely optional, just like ordinary Lisp type
> declarations are. In fact, it could be all that we need is
> requirements for strong type inferencing and compile-time type
> errors.
I had an extended discussion with Jonathan Rees, my officemate, about
this very issue recently. We're doing various language-design things
these days again (a control language for distributed agent technology)
and I was arguing that "optional type inferencing" was useful. He
reacted in a way that seemed to me irrational (he didn't like that
claim and I couldn't understand why). Strangely, I think he was
thinking I was being irrational and was equally baffled by my
position. It took us both quite a while exhausting a fair bit of
patience on both sides to understand the way in which we were talking
at crossed purposes. Perhaps it will help if I share what I got out of
that debate.
If I understand his position correctly, he sees strong typing as a kind
of "weak proof" of program correctness. That is, if your program
type checks, then you have a single bit of information about a certain
class of problems your program doesn't have. (Note that he and I both
agree that whether you can get anything useful out of that bit is another,
more questionable matter. But some people think they do, and surely if
you fail to get a compilation because of a problem that is quite helpful.
So we took that it was useful as a given.)
The problem happens, if I understand correctly, that if you make
type-checking optional then you effectively end up with untyped places
in the network of connections. My answer? Declare those things to be
super-general (i.e., type T) and don't inference across those links. You
can't, after all, since the halting problem can get in your way in all
but the most trivial bridges between typed data and untyped data.
You basically have to type-check at runtime because it's opaque at
compile time. Now here's the kicker: If this can happen, he doesn't get
his one bit of information that the compilation of the system means
something. You don't get an 80% bit, you get no bit. The system compiles,
but you don't know what that means. So for him, it's all or nothing.
For me, it seems to just gracefully degrade because to me, I'm not looking
to get that warm fuzzy from compilation. I just want type inferencing
to improve performance where I use it and not otherwise. I couldn't
care less about the silliness about "proving my program correct" because
I don't believe that fabrication at all. I think it's a dangerous
assumption that a program that compiles quietly is bug free and I'd
rather not entertain it.
Jonathan calls the optimization I'm wanting "heuristic" type inferencing
and says he's frustrated by type inferencing that isn't what he calls
"algorithmic". I guess these are technical terms from some literature
somewhere. I personally feel uncomfortable calling the type inferencing
I like "heuristic" in the sense that the "operation" of what I want
seems well-defined and "algorithmic". I just want things to run
correctly either way, and faster if I add more declarations. I might
bargain down to a term like "heuristic efficiency" in the sense that
the "meaning" is algorithmic, but the speed gain is admittedly something
that's going to depend on how clever the inference engine is.
Well, I didn't clear this message with him, so please understand that
all characterizations of Jonathan's position here are only just my
impressions of what he told me, and I might have goofed on something.
Don't quote him on this by quoting my words. Still, I hope this helps
clarify the multi-dimensionality of the issue.
Also, don't take my claim that he was defending type inferencing as
meaning he doesn't like untyped systems. I think, again just my impression,
that he was saying he wants system correctly labeled so he knows what he
is getting.
As for the Lisp community, I think it's good for us to look into
embracing some of these static type issues, but we should be careful
not to coopt terms they already use to mean things they don't mean by them.
"optional type inferencing" seems to me to be an invitation for someone
to claim we've made an oxymoron. I understand what is meant by that
but I think type inferencing people wouldn't. (Some modifiers do this
to terms. Like how a "wooden duck" is not a kind of duck and a
"chocolate rabbit" is not a kind of rabbit and "a car with available
anti-lock brakes" is not a car with any kind of anti-lock brakes.
So, "optional type inferencing" might be seen by some as not a kind
of type inferencing". I'm sure there must be a "used car salesman"
joke in there but I won't try...) It *might* be that "lazy type
inferencing" would be a better term since lazy already implies you
might not get it at compile time... But it might be that a whole new
term is needed to keep from trampling others names.
On the issue of names, my Lisp Pointers paper
http://world.std.com/~pitman/PS/Name.html
talks about how others have recycled our terms on us.
I'd be sad to do that to another community.
To help you think about strogly-typed Lisp issues, you might want to take a
look at Stalin. Stalin never refuses to compile a program because of typing
issues. But it gives three kinds of error messages: IS, MIGHT, and WILL. Each
error message exists in each of those three forms. When an error is detected
at run time, the IS form of the message is generated (i.e. "The argument to CAR
is not a pair"). At compile time, the MIGHT and WILL forms are generated
(i.e. "The argument to CAR might not be a pair" and "The argument to CAR will
not be a pair"). MIGHT really means `the compiler is not able to prove that
the error cannot occur' and WILL really means `the error will occur if that
program point is reached and the compiler is not able to prove that that
program point will never be reached'.
In practise, I find that WILL forms of errors almost always indicate real bugs.
There are a very few cases, mostly due to polyvariance (automatic splitting)
where a WILL message is generated for compiler-generated unreachable code that
the compiler cannot determine is unreachable. In contrast, I find that, in
practise, MIGHT forms of errors almost always are not bugs but cases where the
type inference algorithm is too weak. This means that 0-CFA is not good enough
for real programs and we need something stronger. Some mixture of polyvariance
and polymorphism can eliminate a lot of spurious MIGHT errors.
I disagree with you that type inference give only a single bit of
information. To me, it gives many bits of information, one for each call site.
When I get no message for a call site at compile time I know that that call
site cannot give a run-time error. And when I get a WILL message I know that I
have found something that I need to look into.
I agree that type-correctness is not a proof of program correctness. But
type-INcorrectness is a strong indication of program INcorrectness. And the
multiple bits of information tell you where to look.
About a year ago, I finally got Stalin to compile itself for the first
time. And I got several WILL messages. All of them turned out to be latent
bugs in portions of the code that were never exercised despite the fact that I
had been running Stalin for several years on dozens of example programs. So
type inference wasn't useless. It helped me discover and fix those latent
bugs. Which I wouldn't have otherwise discovered for a very long time. Even
though there are still other latent bugs that I won't discover for a long
time.
Jeff (http://www.neci.nj.nec.com/homepages/qobi)
Jeffrey Mark Siskind <····@research.nj.nec.com> writes:
> I disagree with you that type inference give only a single bit of
> information. To me, it gives many bits of information, one for each
> call site.
Yes, but I guess what I meant -- i.e., what I *think* Jonathan meant
(and he didn't used the "single bit" thing--I added that) was that
once you destroyed the chain of connectivity of strong typing, you don't
get any of the bits because (as he more-or-less put it): one doesn't have
good intuitions about what it means to have "mostly checked" it or where
that will lead to failure. Whereas if you have totally checked it,
you can at least know what that means--even if it might not be useful.
Anyway, I didn't mean to say that this is the only thing you can get out
of these, but rather to say that some people might think that. This is one
of the complexities of politics: understanding that not everyone has to want
the same things, and not everyone has to care about all of the things that
others care about. We're always so focused on what WE want that it becomes
incomprehensible that someone else's values might be different.
Michael Vanier <·······@bbb.caltech.edu> writes:
> Kent M Pitman <······@world.std.com> writes:
>
> >
> > Incidentally, no one has said it, but check-type only really guarantees
> > run-time checking. Earlier checking might be done, but there is no
> > requirement of it. So in a trival sense, the question of how you can
> > force an error in the original case, if you assume the error is to be
> > forced at compile time, is: you can't. Lisp doesn't do strong typing.
> > It doesn't pretend to try.
> >
>
> This leads to something I've been curious about for a while: has anyone ever
> built a language using lisp parenthesized syntax but with statically-typed
> semantics similar to ML? I'm not trying to get into a debate over whether
> statically-typed languages are "better" than dynamically-typed ones (IMHO it
> depends on a number of factors, including what stage of program development
> you're in and how often the resulting code is likely to need to change). But
> I find it curious that all the ML family of languages (as well as lazy
> languages like Haskell and Miranda) have abandoned the lisp syntax, despite
> the numerous advantages which have been described in a different thread. I
> can think of no good reason why this has to be the case. Any thoughts on
> this? I think it would be cool if there was a statically-typed dialect of
> lisp, since I prefer having my type errors caught at compile-time. OTOH you
> do lose some flexibility that way, so the ultimate solution would be a system
> where you could select either typing system, perhaps on a file-by-file basis.
>
That is a rather interesting question. I suppose the real reason lies
in the fact that "parenthesis" are "more than syntax". With
parenthesis you gain the uniform treatment (or: you loose the
separation) of code and data. I believe this would be enough to break
many proofs of various properties of various type inferencing schemes
(I am not claiming to be an expert of the field - it's just a hunch).
Cheers
--
Marco Antoniotti ===========================================
PARADES, Via San Pantaleo 66, I-00186 Rome, ITALY
tel. +39 - 06 68 10 03 17, fax. +39 - 06 68 80 79 26
http://www.parades.rm.cnr.it/~marcoxa
From: Barry Margolin
Subject: Re: strongly-typed lisp WAS: Re: How can I obtain type errors
Date:
Message-ID: <7Xw53.254$KM3.89483@burlma1-snr2>
In article <·················@arathorn.bbb.caltech.edu>,
Michael Vanier <·······@bbb.caltech.edu> wrote:
>This leads to something I've been curious about for a while: has anyone ever
>built a language using lisp parenthesized syntax but with statically-typed
>semantics similar to ML?
Symbolics had a language called LIL whose syntax was like Lisp but
semantics more like Pascal. It was used to program the FEP of their 36xx
Lisp Machines; I don't think it was ever distributed outside of Symbolics.
Lisp-like syntax was used to make it easier to implement the compiler (it
was written in Lisp, of course, so it could use READ as its lexer) and to
allow it to use Lisp-style macros.
--
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Burlington, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
From: George Neuner
Subject: Re: strongly-typed lisp WAS: Re: How can I obtain type errors
Date:
Message-ID: <37569b2c.86053798@asgard>
On 02 Jun 1999 18:28:29 -0700, Michael Vanier
<·······@bbb.caltech.edu> wrote:
>This leads to something I've been curious about for a while: has anyone ever
>built a language using lisp parenthesized syntax but with statically-typed
>semantics similar to ML?
Rick Kelsey created a statically typed dialect of Scheme, called
"Pre-Scheme". There is a working compiler and he has used it to
create the Scheme48 VM and runtime system. It is also the basis for a
verified Scheme implementation called V-LISP.
I've not seen it available on FTP, but there is information about it
at Kelsey's site:
http://www.neci.nj.nec.com/homepages/kelsey/
George Neuner
Dynamic Resolutions, Inc.
===================================================
The opinions expressed herein are my own and do not
reflect the opinions or policies of my employer.
===================================================
From: Lyman S. Taylor
Subject: Re: strongly-typed lisp WAS: Re: How can I obtain type errors
Date:
Message-ID: <3756BC14.500C44DB@mindspring.com>
Michael Vanier wrote:
...
>
> I find it curious that all the ML family of languages (as well as lazy
> languages like Haskell and Miranda) have abandoned the lisp syntax, despite
> the numerous advantages which have been described in a different thread. I
> can think of no good reason why this has to be the case. Any thoughts on
> this?
I don't think ML family of languages place a high priority on "programs
as data" and macros.
I believe another factor is "marketing" rather than some technical issue.
Why is it that the new high end HP calculator has an "algebric" mode and
isn't RPN only? Because some folks don't "get" RPN and don't feel the
need to master it. Fortunately, you can be in one mode or the other.
With Lisp I'm not so sure that's true.
I think you loose some the dynamic resolution.
(defun bar () ... (foo ... ) ... )
(defun foo () ... )
If I later redefine foo does bar continue to use the "old" foo? For that
matter can I even define foo after bar? Strong type checking requires
omniscient knowledge... Lisp doesn't require you to line up all your
ducks in single, "declare before use" file. [ Well macros are sometimes
an exception, but for the most part there is not much of a restriction. ]
If type checking means you need the whole program do the analysis... will
that
scale? You can check "parts" but that may or maynot leave holes in the
static analysis. Is a condom with holes useful?
As Yoda said once, "Do or not do, there is no try". I think a funny hybird
would please neither end of the spectrum. So you "loose" those folks and
are left with the folks in the middle. Are they a big enough market to
cater to? There is enough legacy inertia that retaining mostly the same
language and a retaining a large "middle" are somewhat in conflict.
Additionally, I'm not sure very many type inferencers would be happy
with hetergenuous containers. For example
'( a b "hello" #c( 0.0 -1.0) #( w o r l d ) )
This would have to a list of "anytype". Downstream from this, what can
you
infer?
With above aside... I think many of the Common Lisp implemenations could
do MUCH more with the local declarations they do get and the other scraps
of
information lying about. Machines are getting much faster and a more
exhaustive
level of checking can be done and still give responsive incremental
interaction. I like the MCL, CMUCL approach of the compiler being always
"on". The lisp compilers are usually less "lax" about stuff that are
minor
gaffs.
---
Lyman
"Lyman S. Taylor" <············@mindspring.com> writes:
> I think you loose some the dynamic resolution.
>
> If I later redefine foo does bar continue to use the "old" foo? For that
> matter can I even define foo after bar? Strong type checking requires
> omniscient knowledge...
You could disallow redefinitions that do not conform to the same signature.
> Additionally, I'm not sure very many type inferencers would be happy
> with hetergenuous containers. For example
>
> '( a b "hello" #c( 0.0 -1.0) #( w o r l d ) )
>
Type inferencers are definitely not happy about that. So most of the
languages with type inference engines have split the concept in two:
you have a homogeneous list of a given type and you have a tuple that
forms a cartesian product of a finite number of types. It's
theoretically less powerful than a heterogeneous list but in practice
it isn't much of a problem.
I'm doubtful much of this can be incorporated in Lisp without losing
many of Lisp's advantages. Those who want ML know where to find it.
--
Lieven Marchand <···@bewoner.dma.be>
If there are aliens, they play Go. -- Lasker
From: Martin Cracauer
Subject: Re: strongly-typed lisp WAS: Re: How can I obtain type errors
Date:
Message-ID: <7j8il2$7bj$1@counter.bik-gmbh.de>
Michael Vanier <·······@bbb.caltech.edu> writes:
>I find it curious that all the ML family of languages (as well as lazy
>languages like Haskell and Miranda) have abandoned the lisp syntax, despite
>the numerous advantages which have been described in a different thread. I
>can think of no good reason why this has to be the case. Any thoughts on
>this?
The prewords of some ML books tell you that they got rid of Lisp
syntax because they thought it was a major reason people didn't use
Lisp.
Also, it seems that most people who beleive in advanced type systems
with compile-time strong checking just don't like the idea of
compile-time computing (macros, codewalkers etc.) in general, for
which Lisp syntax is most useful.
What's the point in catching as many type errors (at compile-time) as
possible if you reinvent operator preference errors (which are not
even caught at runtime) in the same step, BTW?
If I look at the market today, it seems clear to me that at least the
first thing was misguided. The amount of useful Lisp code (if you
include elisp) outweights the amount of useful ML code by orders of
magnitude. One of the finest elisp packages is the C editing mode. So,
if a hardcore C programmer can master (E)Lisp to write its C editing
support, it can't be that bad.
Martin
--
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Martin Cracauer <········@bik-gmbh.de> http://www.bik-gmbh.de/~cracauer/
"Where do you want to do today?" Hard to tell running your calendar
program on a junk operating system, eh?
Michael Vanier <·······@bbb.caltech.edu> writes:
> This leads to something I've been curious about for a while: has anyone ever
> built a language using lisp parenthesized syntax but with statically-typed
> semantics similar to ML?
There's always Christopher Haynes's Infer: A Statically-typed Dialect
of Scheme.
Indiana University's Programming Languages Research page is at:
http://www.cs.indiana.edu/proglang/proglang.html
and the Infer page is at:
http://www.cs.indiana.edu/hyplan/chaynes/infer.html
Mind you, I've no idea of the current status of Infer.
--
T. Kurt Bond, ···@access.mountain.net
>>>>> "Barry" == Barry Margolin <······@bbnplanet.com> writes:
Barry> In article <···············@sevak.isi.edu>, Thomas A. Russ
Barry> <···@sevak.isi.edu> wrote:
>> You can, however, force type checking by using the the
>> CHECK-TYPE call explictly:
>>
>> (defun df* (a b) (declare (double-float a b)) (check-type a
>> double-float) (check-type b double-float) (* a b))
Barry> This is not correct. The declaration tells the compiler
Barry> that the CHECK-TYPEs are guaranteed to succeed, so it can
Barry> optimize them away! I don't have CMUCL so I can't test it,
Barry> but I suspect that its type propagation code may actually
Barry> be able to do this.
Actually, CMUCL doesn't optimize the check-type away, although it
probably has the necessary smarts to do so.
In fact, it's worse than that: CMUCL isn't able to even determine the
type of a and b anymore because check-type macroexpands into
(LOOP
(LET ((#:G1321 A))
(WHEN (TYPEP #:G1321 'DOUBLE-FLOAT) (RETURN NIL))
(SETF A (COMMON-LISP::CHECK-TYPE-ERROR 'A #:G1321 'DOUBLE-FLOAT NIL))))
and that (setf a ...) causes CMUCL to get confused on the type.
Barry> You need to put the type checks outside the scope of the
Barry> declaration. As I wrote in an earlier post, the way to
Barry> code this is:
Barry> (defun df* (a b)
Barry> (check-type a double-float) (check-type b double-float)
Barry> (locally (declare (double-float a b))
Barry> (* a b)))
This works better in CMUCL in that the declaration allows CMUCL to do
the necessary type inference.
Of course, in CMUCL, the original version with just the declaration
would have worked as desired because CMUCL would have checked the
types anyway (if safety were high enough).
Ray
In article <··············@rtp.ericsson.se>,
Raymond Toy <···@rtp.ericsson.se> wrote:
>Actually, CMUCL doesn't optimize the check-type away, although it
>probably has the necessary smarts to do so.
Hmm, the message I read in the group just before yours says exactly the
opposite. I suspect you didn't have the right optimization settings when
you performed your test.
--
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Burlington, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
>>>>> "Barry" == Barry Margolin <······@bbnplanet.com> writes:
Barry> In article <··············@rtp.ericsson.se>, Raymond Toy
Barry> <···@rtp.ericsson.se> wrote:
>> Actually, CMUCL doesn't optimize the check-type away, although
>> it probably has the necessary smarts to do so.
Barry> Hmm, the message I read in the group just before yours says
Barry> exactly the opposite. I suspect you didn't have the right
Barry> optimization settings when you performed your test.
Yes, this is true. For my test, I only set speed to 3, and the
check-type didn't go away. I very rarely set safety to 0, because,
well, it's unsafe. :-)
Ray
Raymond Toy <···@rtp.ericsson.se> writes:
> Barry> Hmm, the message I read in the group just before yours says
> Barry> exactly the opposite. I suspect you didn't have the right
> Barry> optimization settings when you performed your test.
That would probably have been my message...
> Yes, this is true. For my test, I only set speed to 3, and the
> check-type didn't go away. I very rarely set safety to 0, because,
> well, it's unsafe. :-)
Which is a very sound strategy, of course, especially since CMUCL is so
good at optimizing _and_ doing only the necessary type-checks _at the
same time_. It's because of this that I instinctively knew I had to
set safety to 0 to get any kind of obvious effect. Otherwise even if
the CHECK-TYPE forms had been optimized away, the compiler induced type
checking for the type declarations would have remained... So in effect
I had to to some pretty strong things to get CMU CL into trouble...
The most important reason I've bothered to followup is that I forgot to
put BIG BIG DISCLAIMERS into my orginal message that globally proclaiming
(optimize (speed 3) (safety 0)) is VERY VERY BAD indeed. Though this is
of course clear from the context of the thread, and all those involved in
the thread know this themselves, I'm afraid that nowadays with DejaNews
and other archives around, assuming that sufficient context is available
to all readers is probably bad practice in Usenet postings... Of course,
my long explanation now is too late as well... Ah, well, I think I'm
getting old...
Regs, Pierre.
PS:
(with-plug (:disclaimer :satisfied-user)
"For all those interested in CMU CL and especially it's strong
compiler (called Python, a name that predated the now popular
scripting language of the same name), I'd suggest reading CMU CL's
user manual, which is a very interesting read anyways, and which has
many interesting points for optimizing Lisp code in general. CMU CL
and all documentation can be obtained from http://www.cons.org/cmucl/,
which will also probably get a major (very positive) overhaul in the
near future, thanks to some very active individuals...")
--
Pierre Mai <····@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]
From: Lyman S. Taylor
Subject: Utility of incorrect values ( was Re: How can I obtain type errors)
Date:
Message-ID: <3756A9CB.D02182B8@mindspring.com>
Raymond Toy wrote:
...
> (LOOP
> (LET ((#:G1321 A))
> (WHEN (TYPEP #:G1321 'DOUBLE-FLOAT) (RETURN NIL))
> (SETF A (COMMON-LISP::CHECK-TYPE-ERROR 'A #:G1321 'DOUBLE-FLOAT NIL))))
>
> and that (setf a ...) causes CMUCL to get confused on the type.
Curious. Is the intention that the place be set to last incorrect value
in case the "cerror" is broken out of? Or this has something to do
with the nuances of the place?
The following seems a possible better approach.
(setf a (the 'double-float
(let (( #:G1321 a))
(loop
(when (typep #:G1321 'double-float) (return nil ))
(setf #:G1321 (COMMON-LISP::CHECK-TYPE-ERROR 'A #:G1321
DOUBLE-FLOAT
NIL ))))))
However, if I specify a possible new value for "a" that is non double-float
and
then abort the next time through. "A" is still set to the original
offending
value. I imagine it is a tad more complicated to specify that the setting
only
takes effect if it is "correct", but it seems more useful. IMHO "the loop"
should return a value of the correct type. That is why you are "looping".
Secondly, if that place is computationally expensive to get to, then
setting
it to an errant value seems a serious waste of time.
If the computation is aborted it seems unlikely that the intermitted
changed
value wasn't "important". It is like a "rollback".
[ The Hyper-Spec seems to indicate that you're suppose to set the place
even
to incorrect values. ]
(progn
(LOOP
....
....)))
(setf A (the 'double-float a )))
I suppose this has a downside also, besides being likely to be optimized
away. :-)
It is a macro anyway so I suppose that implementors can stick some
nonstandard,
but more specific construct in there.
(progn
(loop
... )
(despite-the-cruft-above a is 'double-float))
Which is just fodder for the type inferencer and doesn't lead to unecessary
codegen.
----
Lyman
Barry Margolin <······@bbnplanet.com> writes:
> >(defun df* (a b)
> > (declare (double-float a b))
> > (check-type a double-float)
> > (check-type b double-float)
> > (* a b))
>
> This is not correct. The declaration tells the compiler that the
> CHECK-TYPEs are guaranteed to succeed, so it can optimize them away! I
> don't have CMUCL so I can't test it, but I suspect that its type
> propagation code may actually be able to do this.
Yes, it actually is able to do this, if you proclaim (safety 0) and
(speed 3):[1]
* (proclaim '(optimize (safety 0) (speed 3)))
EXTENSIONS::%UNDEFINED%
* (compile 'df*)
Compiling LAMBDA (A B):
In: LAMBDA (A B)
#'(LAMBDA (A B)
(DECLARE (DOUBLE-FLOAT A B))
(BLOCK DF*
(CHECK-TYPE A DOUBLE-FLOAT)
(CHECK-TYPE B DOUBLE-FLOAT) ..))
Note: Doing float to pointer coercion (cost 13) to "<return value>".
Compiling Top-Level Form:
Compilation unit finished.
1 note
DF*
T
NIL
* (df* 5 6)
Error in function UNIX::SIGSEGV-HANDLER: Segmentation Violation at #x4810F3E8.
Restarts:
0: [ABORT] Return to Top-Level.
Debug (type H for help)
(UNIX::SIGSEGV-HANDLER #<unused-arg>
#<unused-arg>
#.(SYSTEM:INT-SAP #x3FFFECF8))
Source:
; File: target:code/signal.lisp
; File has been modified since compilation:
; target:code/signal.lisp
; Using form offset instead of character position.
(DEFINE-SIGNAL-HANDLER SIGSEGV-HANDLER "Segmentation Violation")
0]
Footnotes:
[1] The reason you need to proclaim safety 0 is that otherwise CMUCL
always inserts it's own type-checks on declared variable types. That
is part of CMUCL's dual use of declarations both as optimization
hints and as type assertions.
--
Pierre Mai <····@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]