This is the problem with this entire debate. People act like there are two sides arguing from positions of equal merit. That is not the case. One (static) is a strict superset of the other (dynamic).
>The actual function of types, on the other hand, is to prove simple propositions about a program without running it.
The value of a tag proves something about the program. You're just proving it at run-time rather than compile time.
Which is an artificial distinction anyway, since your static types theorems are being proved during the run-time of your static type checker. All theorems are proven during some run-time.
The `declare` thing is common lisp is a bit poorly understood in general:
`declare` is not a promise the compiler makes to you to only accept the declared type.
`declare` is actually a promise YOU make to the compiler to only pass the declared type as parameter. Knowing this, the compiler can activate some optimization (it's an integer? i guess i can skip type detection then).
But let's get real:
* (defun double-integer (x)
(declare (type integer x))
(* 2 x))
DOUBLE-INTEGER
* (double-integer 2)
4
* (double-integer "qualcosa")
;; error here, stack trace omitted
* (disassemble 'double-integer)
; disassembly for DOUBLE-INTEGER
; Size: 37 bytes. Origin: #x10044E4242
; 42: 498B4C2460 MOV RCX, [R12+96] ; thread.binding-stack-pointer
; no-arg-parsing entry point
; 47: 48894DF8 MOV [RBP-8], RCX
; 4B: 488BD6 MOV RDX, RSI
; 4E: BF02000000 MOV EDI, 2
; 53: 488B0576FFFFFF MOV RAX, [RIP-138] ; #<FDEFINITION for ASH>
; 5A: B904000000 MOV ECX, 4
; 5F: FF7508 PUSH QWORD PTR [RBP+8]
; 62: FF6009 JMP QWORD PTR [RAX+9]
; 65: CC10 BREAK 16 ; Invalid argument count trap
NIL
* (defun double-integer (x)
(* 2 x))
WARNING: redefining COMMON-LISP-USER::DOUBLE-INTEGER in DEFUN
DOUBLE-INTEGER
* (disassemble 'double-integer)
; disassembly for DOUBLE-INTEGER
; Size: 38 bytes. Origin: #x1004B6CBCC
; CC: 498B4C2460 MOV RCX, [R12+96] ; thread.binding-stack-pointer
; no-arg-parsing entry point
; D1: 48894DF8 MOV [RBP-8], RCX
; D5: BF04000000 MOV EDI, 4
; DA: 488BD3 MOV RDX, RBX
; DD: 41BBA0020020 MOV R11D, 536871584 ; GENERIC-*
; E3: 41FFD3 CALL R11
; E6: 488B5DF0 MOV RBX, [RBP-16]
; EA: 488BE5 MOV RSP, RBP
; ED: F8 CLC
; EE: 5D POP RBP
; EF: C3 RET
; F0: CC10 BREAK 16 ; Invalid argument count trap
NIL
* (double-integer 2)
4
* (double-integer "qualcosa")
;; error here, stack trace omitted
The various float types and fixnum (machine register width integer) would compile down to machine code multiplication instructions without function calls, if declared or inferred that the inputs (and output in the fixnum case) are of those types, and the safety option is reduced. (In SBCL)
Just because it calls itself a type error doesn't mean it is. If you don't catch the error until your function actually runs, it's a runtime error, not a type error. Type errors are all caught before the program runs, typically in a compilation step.