Typed Lisp, a Primer

Summary

Checking the type of inputs is tedious and so I guessed it could be done using macros and advice. Looking at Typed Racket for inspiration, the following fictitious syntax would add advice to f that checks the optional arguments xᵢ have type σᵢ and the mandatory positional arguments have type τᵢ according to position, and the result of the computation is of type τ. To the best of my knowledge, no one had done this for Emacs Lisp —I don't know why. (declare-type 'f ((:x₁ σ₁) … (:xₘ σₘ)) (τ₁ … τₙ τ)) To modify a variable, or function, we may simply redefine it; but a much more elegant and powerful approach is to “advise” the current entity with some new behaviour. In our case of interest, we will advise functions to check their arguments before executing their bodies. Below is my attempt: declare-type. Before you get scared or think it's horrendous, be charitable and note that about a third of the following is documentation and a third is local declarations. (cl-defmacro declare-type (f key-types &rest types) "Attach the given list of types to the function ‘f’ by advising the function to check its arguments’ types are equal to the list of given types. We name the advice ‘⟪f⟫-typing-advice’ so that further invocations to this macro overwrite the same advice function rather than introducing additional, unintended, constraints. Using type specifiers we accommodate for unions of types and subtypes, etc ♥‿♥. ‘key-types’ should be of the shape (:x₀ t₀ ⋯ :xₙ tₙ); when there are no optional types, use symbol “:”. E.g., (declare-type my-func (:z string :w integer) integer symbol string) " ;; Basic coherency checks. When there aren't optional types, key-types is the “:” symbol. (should (and (listp types) (or (listp key-types) (symbolp key-types)))) (letf* ((pairify (lambda (xs) (loop for i in xs by #'cddr ;; Turn a list of flattenned pairs for j in (cdr xs) by #'cddr ;; into a list of explicit pairs. collect (cons i j)))) ;; MA: No Lisp method for this!? (result-type (car (-take...