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-last 1 types))) (types (-drop-last 1 types)) (num-of-types (length types)) (key-types-og (unless (symbolp key-types) key-types)) (key-types (funcall pairify key-types-og)) (advice-name (intern (format "%s-typing-advice" f))) (notify-user (format "%s now typed %s → %s → %s." `,f key-types-og types result-type))) `(progn (defun ,advice-name (orig-fun &rest args) ;; Split into positional and key args; optionals not yet considered. (letf* ((all-args (-split-at (or (--find-index (not (s-blank? (s-shared-start ":" (format "%s" it)))) args) ,num-of-types) args)) ;; The “or” is for when there are no keywords provided. (pos-args (car all-args)) (key-args (funcall ,pairify (cadr all-args))) (fun-result nil) ((symbol-function 'shucks) (lambda (eτ e g) (unless (typep g eτ) (error "%s: Type mismatch! Expected %s %s ≠ Given %s %s." (function ,f) eτ e (type-of g) (prin1-to-string g)))))) ;; Check the types of positional arguments. (unless (equal ,num-of-types (length pos-args)) (error "%s: Insufficient number of arguments; given %s, %s, but %s are needed." (function ,f) (length pos-args) pos-args ,num-of-types)) (loop for (ar ty pos) in (-zip pos-args (quote ,types) (number-sequence 0 ,num-of-types)) do (shucks ty (format "for argument %s" pos) ar)) ;; Check the types of *present* keys. (loop for (k . v) in key-args do (shucks (cdr (assoc k (quote ,key-types))) k v)) ;; Actually execute the orginal function on the provided arguments. (setq fun-result (apply orig-fun args)) (shucks (quote ,result-type) "for the result type (!)" fun-result) ;; Return-value should be given to caller. fun-result)) ;; Register the typing advice and notify user of what was added. (advice-add (function ,f) :around (function ,advice-name)) ,notify-user )))
declare-type
There are some notable shortcomings: Lack of support for type variables and, for now, no support for optional arguments. Nonetheless, I like it —of course. ( Using variable watchers we could likely add support for type variables as well as function-types. )
We accidentally forgot to consider an argument.
(declare-type f₁ (:z string :w list) integer symbol string) ;; ⇒ f₁ now typed (:z string :w integer) → (integer symbol) → string. (cl-defun f₁ (x y &key z w) (format "%s" x)) ;; ⇒ f₁ now defined (f₁ 'x) ;; ⇒ f₁: Insufficient number of arguments; given 2, (x), but 3 are needed.
The type declaration said we needed 3 arguments, but we did not consider one of them.
We accidentally returned the wrong value.
(declare-type f₂ (:z string :w list) integer symbol string) (cl-defun f₂ (x y &key z w) x) (f₂ 144 'two) ;; ⇒ f₂: Type mismatch! Expected string for the result type (!) ≠ Given integer 144.
We accidentally forgot to supply an argument.
(declare-type f₃ (:z string :w list) integer symbol string) (cl-defun f₃ (x y &key z w) (format "%s" x)) (f₃ 144) ;; ⇒ f₃: Insufficient number of arguments; given 1, (144), but 2 are needed.
A positional argument is supplied of the wrong type.
(f₃ 'one "two") ;; ⇒ f₃: Type mismatch! Expected integer for argument 0 ≠ Given symbol one. (f₃ 144 "two") ;; ⇒ f₃: Type mismatch! Expected symbol for argument 1 ≠ Given string "two".
Notice: When multiple positional arguments have type-errors, the errors are reported one at a time.
A keyword argument is supplied of the wrong type.
(f₃ 1 'two :z 'no₀ :w 'no₁) ;; ⇒ f₃: Type mismatch! Expected string :z ≠ Given symbol no₀. (f₃ 1 'two :z "ok" :w 'no₁) ;; ⇒ f₃: Type mismatch! Expected string :w ≠ Given symbol no₁. (f₃ 1 'two :z "ok" :w 23) ;; ⇒ f₃: Type mismatch! Expected string :w ≠ Given integer 23. (f₃ 1 'two :z "ok" :w '(a b 1 2)) ;; ⇒ okay; no type-error.
We have no optional arguments.
(declare-type f₄ : integer symbol string) (cl-defun f₄ (x y &key z w) (format "%s" x)) (f₄ 144 'two :z "bye") ;; ⇒ f₄: Type mismatch! Expected nil :z ≠ Given string "bye". ;; ( We shouldn't have any keyword :z according to the type declaration! ) (f₄ 144 'two) ;; ⇒ "144"
We can incorporate type specfiers such as unions!
(declare-type f₅ : (or integer string) string) (cl-defun f₅ (x) (format "%s" x)) (f₅ 144) ;; ⇒ "144" (f₅ "neato") ;; ⇒ "neato" (f₅ 'shaka-when-the-walls-fell) ;; ⇒ f₅: Type mismatch! Expected (or integer string) for argument 0 ;; ≠ Given symbol shaka-when-the-walls-fell.
No positional arguments but a complex optional argument!
(declare-type f₆ (:z (satisfies (lambda (it) (and (integerp it) (= 0 (mod it 5)))))) character) (cl-defun f₆ (&key z) ?A) (f₆ 'hi) ;; ⇒ Keyword argument 144 not one of (:z) (f₆) ;; ⇒ 65; i.e., the character ‘A’ (f₆ :z 6) ;; ⇒ f₆: Type mismatch! ;; Expected (satisfies (lambda (it) (and (integerp it) (= 0 (mod it 5))))) :z ;; ≠ Given integer 6. (f₆ :z 10) ;; ⇒ 65; i.e., the expected output since 10 mod 5 ≈ 0 & so 10 is valid input.
Preconditions! The previous example had a complex type on a keyword, but that was essentially a pre-condition; we can do the same on positional arguments.
(declare-type f₇ : (satisfies (lambda (it) (= it 5))) integer) (cl-defun f₇ (n) n) ;; The identity on 5 function; and undefined otherwise. (f₇ 4) ;; ⇒ f₇: Type mismatch! Expected (satisfies (lambda (it) (= it 5))) for argument 0 ;; ≠ Given integer 4. (f₇ 5) ;; ⇒ 5
Postconditions! Given an integer greater than 5, we present an integer greater than 2; i.e., this is a constructive proof that \(∀ n • n > 5 ⇒ n > 2\).
(declare-type f₈ : (satisfies (lambda (in) (> in 5))) (satisfies (lambda (out) (> out 2)))) (cl-defun f₈ (n) n) ;; The identity on 5 function; and undefined otherwise. (f₈ 4) ;; ⇒ f₈: Type mismatch! Expected (satisfies (lambda (in) (> in 5))) for argument 0 ;; ≠ Given integer 4. (f₈ 72) ;; ⇒ 72; since indeed 72 > 5 for the input, and clearly 72 > 2 for the output.
As it currently stands we cannot make any explicit references between the inputs
and the output, but that's an easy fix: Simply add a local function old to the
declare-type macro which is intentionally exposed so that it can be used in the
type declarations to refer to the ‘old’, or initial, values provided to the function.
Additionally, one could also add keyword arguments :requires and :ensures
for a more sophisticated pre- and post-condition framework.
Something along these lines is implemented for Common Lisp.
Here's a fun exercise: Recast the Liquid Haskell examples in Lisp using this
declare-type form.