Nathan Baum <···········@btinternet.com> writes:
>> For example, if you have a tree of nodes with a label and a variable
>> number of children, you should use: LEAFP, MAKE-NODE, NODE-LABEL and
>> NODE-CHILDREN. You can still implement your nodes with lists:
>>
>> (defun LEAFP (object) (not (consp object)))
>> (defun MAKE-NODE (label &rest children) (cons label children))
>> (defun NODE-LABEL (node) (first node))
>> (defun NODE-CHILDREN (node) (rest node))
>> [...]
> This doesn't completely solve the problem. There's no standard way to
> process a form/file checking for type errors, which is really the
> point. I can still type
>
> > (defun bad ()
> (node-label 12))
>
> which is Obviously Wrong.
How so? I've not specified anything about the type of the labels.
(The type of children is infered from &rest children : it's LIST.)
> It would be useful to do
> > (typecheck bad)
> *** argument to NODE-LABEL is FIXNUM, expecting NODE.
Well, perhaps you're expecing SYMBOL. Just say so:
(defun MAKE-NODE (label &rest children)
(declare (type symbol label))
(cons label children))
>> As for type inference, what more do you want than:
>>
>> * (defun k (x) (car (+ 1 x)))
>> ; in: LAMBDA NIL
>> ; (CAR (+ 1 X))
>> ;
>> ; caught WARNING:
>> ; Asserted type LIST conflicts with derived type (VALUES NUMBER &OPTIONAL).
>> ; See also:
>> ; The SBCL Manual, Node "Handling of Types"
>> ;
>> ; compilation unit finished
>> ; caught 1 WARNING condition
>
> Sure, but that isn't a requirement of the standard.
So what? It's not a standard requirement either! If you have this
requirement, choose an implementation that does it, like SBCL.
> Way back when I
> tested Corman and LispWorks, and I didn't notice them doing any type
> inference.
Nonetheless, all the implementations I know do type checking (at
run-time at least) unless you compiled with (declaim (optimize (speed
3) (safety 0))).
> Of course, the hypothetical linting library could perform this kind of
> type checking, and attach explicit type annotations. This kind of
> functionality doesn't actually need to be 'in the language', but it
> would be useful functionality to have access to, I think.
You may want to try ACL2. http://www.cs.utexas.edu/users/moore/acl2/
--
__Pascal Bourguignon__ http://www.informatimago.com/
READ THIS BEFORE OPENING PACKAGE: According to certain suggested
versions of the Grand Unified Theory, the primary particles
constituting this product may decay to nothingness within the next
four hundred million years.
On Mon, 7 Aug 2006, Pascal Bourguignon wrote:
> Nathan Baum <···········@btinternet.com> writes:
>>> For example, if you have a tree of nodes with a label and a variable
>>> number of children, you should use: LEAFP, MAKE-NODE, NODE-LABEL and
>>> NODE-CHILDREN. You can still implement your nodes with lists:
>>>
>>> (defun LEAFP (object) (not (consp object)))
>>> (defun MAKE-NODE (label &rest children) (cons label children))
>>> (defun NODE-LABEL (node) (first node))
>>> (defun NODE-CHILDREN (node) (rest node))
>>> [...]
>> This doesn't completely solve the problem. There's no standard way to
>> process a form/file checking for type errors, which is really the
>> point. I can still type
>>
>> > (defun bad ()
>> (node-label 12))
>>
>> which is Obviously Wrong.
>
> How so? I've not specified anything about the type of the labels.
> (The type of children is infered from &rest children : it's LIST.)
Except that clearly isn't what node-label does. The way you've quoted it,
node-label attempts to find the FIRST of 12, which clearly has no FIRST.
>> It would be useful to do
>> > (typecheck bad)
>> *** argument to NODE-LABEL is FIXNUM, expecting NODE.
>
> Well, perhaps you're expecing SYMBOL. Just say so:
>
> (defun MAKE-NODE (label &rest children)
> (declare (type symbol label))
> (cons label children))
No, I'm expecting NODE. I think that's pretty clear from the
expected error message.
Even assuming we correct your misunderstanding of what NODE-LABEL does, a
TYPE declaration isn't the answer. The OP laments the lack of 'static'
type checking. TYPE declarations might not be checked statically; they
might not be checked at all.
>>> As for type inference, what more do you want than:
>>>
>>> * (defun k (x) (car (+ 1 x)))
>>> ; in: LAMBDA NIL
>>> ; (CAR (+ 1 X))
>>> ;
>>> ; caught WARNING:
>>> ; Asserted type LIST conflicts with derived type (VALUES NUMBER &OPTIONAL).
>>> ; See also:
>>> ; The SBCL Manual, Node "Handling of Types"
>>> ;
>>> ; compilation unit finished
>>> ; caught 1 WARNING condition
>>
>> Sure, but that isn't a requirement of the standard.
>
> So what? It's not a standard requirement either! If you have this
> requirement, choose an implementation that does it, like SBCL.
>
>> Way back when I tested Corman and LispWorks, and I didn't notice them
>> doing any type inference.
>
> Nonetheless, all the implementations I know do type checking (at
> run-time at least) unless you compiled with (declaim (optimize (speed 3)
> (safety 0))).
Which is:
1. Irrelevant, because that isn't type inference.
2. Inaccurate, because (in my experience) neither Corman nor LispWorks are
diligent about enforcing TYPE declarations: they only enforce types
when calling system functions which require arguments of a certain
type. This is permitted by the standard, because "the consequences are
unspecified" if a TYPE declaration is ever violated.
>> Of course, the hypothetical linting library could perform this kind of
>> type checking, and attach explicit type annotations. This kind of
>> functionality doesn't actually need to be 'in the language', but it
>> would be useful functionality to have access to, I think.
>
> You may want to try ACL2. http://www.cs.utexas.edu/users/moore/acl2/
Except that ACL2 is neither a Common Lisp linting library nor an
implementation of Common Lisp which includes one.
> --
> __Pascal Bourguignon__ http://www.informatimago.com/
>
> READ THIS BEFORE OPENING PACKAGE: According to certain suggested
> versions of the Grand Unified Theory, the primary particles
> constituting this product may decay to nothingness within the next
> four hundred million years.
>
Nathan Baum <···········@btinternet.com> writes:
> On Mon, 7 Aug 2006, Pascal Bourguignon wrote:
>> Nathan Baum <···········@btinternet.com> writes:
>>>> For example, if you have a tree of nodes with a label and a variable
>>>> number of children, you should use: LEAFP, MAKE-NODE, NODE-LABEL and
>>>> NODE-CHILDREN. You can still implement your nodes with lists:
>>>>
>>>> (defun LEAFP (object) (not (consp object)))
>>>> (defun MAKE-NODE (label &rest children) (cons label children))
>>>> (defun NODE-LABEL (node) (first node))
>>>> (defun NODE-CHILDREN (node) (rest node))
>>>> [...]
>>> This doesn't completely solve the problem. There's no standard way to
>>> process a form/file checking for type errors, which is really the
>>> point. I can still type
>>>
>>> > (defun bad ()
>>> (node-label 12))
>>>
>>> which is Obviously Wrong.
>>
>> How so? I've not specified anything about the type of the labels.
>> (The type of children is infered from &rest children : it's LIST.)
>
> Except that clearly isn't what node-label does. The way you've quoted
> it, node-label attempts to find the FIRST of 12, which clearly has no
> FIRST.
Yes, right. I wasn't awake. Sorry.
The point is that lisp is a dynamic language.
It would be silly to signal an error when you enter:
(defun bad () (node-label 12))
because you might enter:
(defgeneric node-label (object)
(:method ((self cons)) (first self))
(:method ((self t)) self))
just after, and then:
(bad)
would be perfectly good.
>> [...]
>> Nonetheless, all the implementations I know do type checking (at
>> run-time at least) unless you compiled with (declaim (optimize
>> (speed 3) (safety 0))).
>
> Which is:
>
> 1. Irrelevant, because that isn't type inference.
>
> 2. Inaccurate, because (in my experience) neither Corman nor LispWorks are
> diligent about enforcing TYPE declarations: they only enforce types
> when calling system functions which require arguments of a certain
> type. This is permitted by the standard, because "the consequences are
> unspecified" if a TYPE declaration is ever violated.
If you want Haskell, how would a language diametrically opposed help?
(Well, I understand that a Haskell with sexp syntax could be
useful. At least, more readable than normal Haskell syntax... But
sexpifying a programming language doesn't make it lisp.)
--
__Pascal Bourguignon__ http://www.informatimago.com/
"You cannot really appreciate Dilbert unless you read it in the
original Klingon"
On Mon, 7 Aug 2006, Pascal Bourguignon wrote:
> Nathan Baum <···········@btinternet.com> writes:
>
>> On Mon, 7 Aug 2006, Pascal Bourguignon wrote:
>>> Nathan Baum <···········@btinternet.com> writes:
>>>>> For example, if you have a tree of nodes with a label and a variable
>>>>> number of children, you should use: LEAFP, MAKE-NODE, NODE-LABEL and
>>>>> NODE-CHILDREN. You can still implement your nodes with lists:
>>>>>
>>>>> (defun LEAFP (object) (not (consp object)))
>>>>> (defun MAKE-NODE (label &rest children) (cons label children))
>>>>> (defun NODE-LABEL (node) (first node))
>>>>> (defun NODE-CHILDREN (node) (rest node))
>>>>> [...]
>>>> This doesn't completely solve the problem. There's no standard way to
>>>> process a form/file checking for type errors, which is really the
>>>> point. I can still type
>>>>
>>>> > (defun bad ()
>>>> (node-label 12))
>>>>
>>>> which is Obviously Wrong.
>>>
>>> How so? I've not specified anything about the type of the labels.
>>> (The type of children is infered from &rest children : it's LIST.)
>>
>> Except that clearly isn't what node-label does. The way you've quoted
>> it, node-label attempts to find the FIRST of 12, which clearly has no
>> FIRST.
>
> Yes, right. I wasn't awake. Sorry.
>
>
> The point is that lisp is a dynamic language.
> It would be silly to signal an error when you enter:
>
> (defun bad () (node-label 12))
>
> because you might enter:
>
> (defgeneric node-label (object)
> (:method ((self cons)) (first self))
> (:method ((self t)) self))
>
> just after, and then:
>
> (bad)
>
> would be perfectly good.
Ah, but this depends upon *when* you signal the error. It would indeed be
silly for 'the compiler' to signal an error at 'compile time'. (Unless
NODE-LABEL was inline, or there was some non-standard declaration in force
which meant that NODE-LABEL would never be redefined.)
On the other hand, to be able to type (typecheck 'bad) at the REPL and get
messages about type conflicts *as they are at that time* would (IMO) be
useful. SBCL does as much whenever you define a function,
> (defun bad () (car 12))
...
; caught WARNING:
; Asserted type LIST conflicts with derived type
; (VALUES (INTEGER 12 12) &OPTIONAL).
...
which seems to be a net win.
It's my experience that static type checking is a powerful, albiet not
universal, tool for detecting certain classes of error in a program.
You correctly identify that following common-sense coding standards like
using abstract data types can make it easier to remember what types go
where -- I imagine it's easier to remember that (NODE-LABEL node) is
(should be) a SYMBOL than (CAR node). I have no argument with that.
One can (and IMO should) also use unit tests to detect errors, including
type errors.
But one should not, I think, dismiss static type checking simply because
there are other alternatives available. I like to follow the engineering
practice of having "multiple independent failsafes".
Although static type checking can't detect all errors, it can detect some.
And although all the errors it can detect are avoidable by following
coding standards and detectable by running unit tests, that's no guarantee
that they actually will be avoided or detected by standards or tests.
>>> [...]
>>> Nonetheless, all the implementations I know do type checking (at
>>> run-time at least) unless you compiled with (declaim (optimize
>>> (speed 3) (safety 0))).
>>
>> Which is:
>>
>> 1. Irrelevant, because that isn't type inference.
>>
>> 2. Inaccurate, because (in my experience) neither Corman nor LispWorks are
>> diligent about enforcing TYPE declarations: they only enforce types
>> when calling system functions which require arguments of a certain
>> type. This is permitted by the standard, because "the consequences are
>> unspecified" if a TYPE declaration is ever violated.
>
> If you want Haskell, how would a language diametrically opposed help?
>
> (Well, I understand that a Haskell with sexp syntax could be
> useful. At least, more readable than normal Haskell syntax... But
> sexpifying a programming language doesn't make it lisp.)
At the same time, adding type inference to a language doesn't make it
*not* Lisp (as SBCL proves).
Additionally, I've never advocated changes to 'the language'. The basic
point of my post was that (1) type inference and static type checking can
be a win and (2) in Lisp they can implemented as a library.
> --
> __Pascal Bourguignon__ http://www.informatimago.com/
>
> "You cannot really appreciate Dilbert unless you read it in the
> original Klingon"
Nathan Baum <···········@btinternet.com> writes:
> On the other hand, to be able to type (typecheck 'bad) at the REPL and
> get messages about type conflicts *as they are at that time* would
> (IMO) be useful.
* (defun typecheck (fun) (funcall fun))
TYPECHECK
* (defun bad () (node-label 12))
BAD
* (typecheck 'bad)
debugger invoked on a TYPE-ERROR: The value 12 is not of type LIST.
;-)
> But one should not, I think, dismiss static type checking simply
> because there are other alternatives available. I like to follow the
> engineering practice of having "multiple independent failsafes".
This is a subject over discussed from dynamically typed languages news
groups to statically typed language news groups. There's no interest in it.
If you want static typing, use Haskell. If you want dynamic typing,
use Lisp.
You can (try to) develop tools to automatically prove any program
property you want, and I don't say I wouldn't use them with lisp if
they were available, but they're not needed.
IMO, for the kind of software I write (and what 99% of the programmers
write I'd say), static typing impacts less than 1% of the success of
the project.
> [...]
> At the same time, adding type inference to a language doesn't make it
> *not* Lisp (as SBCL proves).
>
> Additionally, I've never advocated changes to 'the language'. The
> basic point of my post was that (1) type inference and static type
> checking can be a win and (2) in Lisp they can implemented as a
> library.
--
__Pascal Bourguignon__ http://www.informatimago.com/
The mighty hunter
Returns with gifts of plump birds,
Your foot just squashed one.