Typed Lisp, A Primer

I have convinced a number of my peers to use Emacs/Spacemacs/Doom-emacs, but my efforts to get them to even consider trying Lisp have been met with staunch rejection. These peers are familiar with Haskell, and almost all know Agda, so you'd think they'd be willing to try Lisp —it's there, part of their editor— but the superficial chasm in terms of syntax and types is more than enough apparently. In this article, I aim to explore the type system of (Emacs) Lisp and occasionally make comparisons to Haskell. Perhaps in the end some of my Haskell peers would be willing to try it out.

• ↯ I almost never use Haskell for any day-to-day dealings.

  ✓ The ideas expressed by its community are why I try to keep updated on the language.

• ↯ No one around me knows anything about Lisp, but they dislike it due to the parens.

  ✓ I love it and use it for Emacs configuration and recently to prototype my PhD research.

• ⇅ I love that I can express a complicated procedure compactly in both by using zips, unzips, filters, and maps (งಠ_ಠ)ง

  • Lately, in Lisp, I'll write a nested loop (gasp!) then, for fun, try to make it a one-liner! Sometimes, I actually think the loop formulation is clearer and I leave it as a loop —Breaking news: Two Haskell readers just died.

    

• What I like and why:

  Haskell	⇒	Executable category theory; compact & eloquent
  Lisp	⇒	Extensible language; malleable, uniform, beautiful

• Documentation?

  Haskell	⇒	Hoogle; can search by type alone!
  Emacs Lisp	⇒	Self-documenting; M-x apropos

• How has using the language affected me?

  Haskell	I almost always think in-terms compoistionality, functors, & currying
  Lisp	Documentation strings, units tests, and metaprogramming are second nature

It may not be entirely accurate to say that Lisp's type system is more expressive than Haskell's as it's orthogonal in many respects; although it is closer to that of Liquid Haskell.

Types allow us to treat objects according a similar structure or interface. Unlike Haskell and other statically typed systems, in Lisp we have that types can overlap. As such, here's our working definition.

Haskellers and others may append to this definition the following, which we will not bother with: Type membership is determined by inspecting syntactic structure and so is decidable.

✓ Typing is one of the simplest forms of “assertion-comments”: Documenting a property of your code in a way that the machine can verify.

If you're gonna comment on what kind of thing you're working with, why not have the comment checked by the machine.

Let's see some examples:

;; The universal type “t”, has everything as its value.
(typep 'x 't) ;; ⇒ true
(typep 12 't) ;; ⇒ true

;; The empty type: nil
(typep 'x 'nil) ;; ⇒ false; nil has no values.

;; The type “null” contains the one value “nil”.
(typep nil 'null) ;; ⇒ true
(typep () 'null)  ;; ⇒ true

;; “(eql x)” is the singelton type consisting of only x.
(typep 3 '(eql 3)) ;; ⇒ true
(typep 4 '(eql 3)) ;; ⇒ false

;; “(member x₀ … xₙ)” denotes the enumerated type consisting of only the xᵢ.
(typep 3 '(member 3 x "c"))  ;; ⇒ true
(typep 'x '(member 3 x "c")) ;; ⇒ true
(typep 'y '(member 3 x "c")) ;; ⇒ false

;; “(satisfies p)” is the type of values that satisfy predicate p.
(typep 12 '(satisfies (lambda (x) (oddp x)))) ;; ⇒ false
(typep 12 '(satisfies evenp) )                ;; ⇒ true

;; Computation rule for comprehension types.
;; (typep x '(satisfies p)) ≈ (if (p x) t nil)

Here's a convenient one: (booleanp x) ≈ (typep x '(member t nil)).

(booleanp 2)   ;; ⇒ false
(booleanp nil) ;; ⇒ true

Strongly typed languages like Haskell allow only a number of the type formers listed above. For example, Haskell does not allow unions but instead offers so-called sum types. Moreover, unlike Haskell, Lisp is non-parametric: We may pick a branch of computation according to the type of a value. Such case analysis is available in languages such as C# —c.f., is is as or is as is. Finally, it is important to realise that cons is a monomorphic type —it just means an (arbitrary) element consisting of two parts called car and cdr— we show how to form a polymorphic product type below.

We may ask for the ‘primitive type’ of an object; which is the simplest built-in type that it belongs to, such as integer, string, cons, symbol, record, subr, and a few others. As such, Lisp objects come with an intrinsic primitive type; e.g., '(1 "2" 'three) is a list and can only be treated as a value of another type if an explicit coercion is used. In Lisp, rather than variables, it is values that are associated with a type. One may optionally declare the types of variables, like in OCaml.

Let's review some important features of type systems and how they manifest themselves in Lisp.

It is important to realise that nearly every language is typed —albeit the checking may happen at different stages— and so, as Benjamin Pierce says: Terms like “dynamically typed” are arguably misnomers and should probably be replaced by “dynamically checked,” but the usage is standard.

In particular, dynamically typed is not synonymous with untyped, though some people use it that way since nearly every language is typed —possibly with a single anonymous type.

Some people in the Haskell community, which I love, say things like “if it typechecks, ship it” which is true more often than not, but it leads some people to avoid producing unit tests. For example, the following type checks but should be unit tested.

mcbride :: [Int] -> Int
mcbride xs = if null xs then head xs else 666

Regardless, I love static type checking and static analysis in general. However, the shift to a dynamically checked setting has resulted in greater interest in unit testing. For example, Haskell's solution to effectful computation is delimited by types, as any Haskeller will proudly say (myself included); but ask how are such computations unit tested and the room is silent (myself included).

Interestingly some unit tests check the typing of inputs and output, which is a mechanical process with no unknowns and so it should be possible to produce a syntax for it using Lisp macros. This is one of the goals of this article and we'll return to it later.

Even though I like Lisp, I'm not sure why dynamic typing is the way to go —c.f. Dynamic Languages are Static Languages which mentions the unjust tyranny of unityped systems. Below are two reasons why people may dislike static types.

First: The de-facto typing rule do binary choice is usually:

     T : 𝔹     E : α     B : α -----------------------------------------------------------------------------------------
     if T then E else B : α

That means valid programs such as if True then 1 else "two" are rejected; even though the resulting type will always be an integer there is no way to know that statically —the choice needs to be rewritten, evaluated at run time.

Indeed, in Haskell, we would write if True then Left 1 else Right "two" which has type Either Int String, and to use the resulting value means we need to pattern match or use the eliminator (|||) —from Haskell's Control.Arrow.

Second: Some statically typed languages have super weak type systems and ruin the rep for everyone else. For example, C is great and we all love it of-course, but it's a shame that we can only express the polymorphic identity function \(id : ∀{α}. α → α \;=\; λ x → x\), by using the C-preprocessor —or dismiss the types by casting pointers around.

Maybe this video is helpful, maybe not: The Unreasonable Effectiveness of Dynamic Typing for Practical Programs

( For the algebraist: Dynamic typing is like working in a monoid whose composition operation is partial and may abruptly crash; whereas static typing is working in a category whose composition is proudly typed. )

Overall I haven't presented a good defence for being dynamically checked, but you should ignore my blunder and consider trying Lisp yourself to see how awesome it is.

First: Code that manipulates code is difficult to type.

Is the type of '(+ x 2) a numeric code expression? Or just an arbitrary code expression? Am I allowed to “look inside” to inspect its structure or is it a black box? What about the nature of its constituents? If I'm allowed to look at them, can I ask if they're even defined?

What if c is a code element that introduces an identifier, say it. What is type of c? What if it doesn't introduce and thus avoids accidentally capturing identifiers? Are we allowed only one form or both? Which do we select and why?

I may be completely wrong, but below I mention a bunch of papers that suggest it's kind hard to type this stuff.

Second: The type theory just wasn't in place at the time Lisp was created.

Here's a probably wrong account of how it went down.

1913ish

Bertrand Russel introduces a hierarchy of types to avoid barber trouble; e.g., Typeᵢ : Typeᵢ₊₁.

1920s

A Polish guy & British guy think that's dumb and collapse the hierarchy.

1940s

Alonzo Church says arrows are cool.

1958

With his awesome hairdo, John McCarthy gifts the world an elegant piece of art: Lisp (•̀ᴗ•́)و

• Lisp is currently the 2ⁿᵈ oldest high-level language still in use after Fortran.
• Maxwell's equations get jealous.

Lisp introduces a bunch of zany ideas to CS:

• Introduced if-then-else “McCarthy's Conditional”; 1ˢᵗ class functions & recursion
• macros ≈ compiler plugins
• symbols ≈ raw names which needn't have values
• variables ≈ pointers
• code ≈ data; statements ≈ expressions
• read, eval, load, compile, print are all functions!

1959

My man JM thinks manual memory is lame —invents garbage collection!

• Later, 2001, he writes The Robot & The Baby.

1960s

Simula says OOPs!

1970s

Smalltalk popularises the phrase “oop”. ( B has a child named C. )

1970s

Simple λ-calculus is a fashion model for sets and functions.

1970s

Milner and friends demand variables are for types too, not just terms!

1970s

Per Martin-Löf tells us it's okay to depend on one another; Π, Σ types.

1982

A Lisp ummah is formed: “Common Lisp the Language” ♥‿♥

• In order to be hip & modern, it's got class with CLOS.
• Other shenanigans: Scheme 1975, Elisp 1985, Racket 1995, Clojure 2007

1984

A script of sorcerous schemes lords lisp over mere mortals

1990s

A committee makes a sexy camel named Haskell; Professor X's school make their own camel.

• Their kids get on steroids and fight to this day; Agda ↯↯↯ Coq.

2000s

X's camel .<becomes .~(self .<aware>.)>. —the other camel [does| the same].

• In 2015, the cam ls married Lisp and Lux was born.
• In 2016, Haskell & Lisp get involved with Prolog; Shen is born.

2019: Coq is self-aware; Agda is playing catch-up.

A more informative historical account of Lisp & its universal reverence can be read at: How Lisp Became God's Own Programming Language.

Besides Common Lisp, “Typed Lisps” include an optional type system for Clojure —see also Why we're no longer using Core.typed— Typed Racket, and, more recently, Lux ≈ Haskell + ML + Lisp and Shen ≈ Haskell + Prolog + Lisp.

For example, Common Lisp admits strong static typing, in SBCL, as follows.

  ; Type declaration then definition.
  (declaim (ftype (function (fixnum)) num-id))
  (defun num-id (n) n)

  (defun string-id (s) (declare (string s)) (num-id s))
  ; in: DEFUN STRING-ID
  ;     (NUM-ID S)
  ;
  ; caught WARNING:
  ;   Derived type of S is
  ;     (VALUES STRING &OPTIONAL),
  ;   conflicting with its asserted type
  ;     FIXNUM.

Such annotations mostly serve as compiler optimisation annotations and, unfortunately, Emacs Lisp silently ignores Common Lisp declarations such as ftype —which provides function type declarations. However, Emacs Lisp does provide a method of dispatch filtered by classes rather than by simple types. Interestingly, Lisp methods are more like Haskell typeclass constituents or C# extensible methods rather than like Java object methods —in that, Lisp methods specialise on classes whereas Java's approach is classes have methods.

Here's an example.

(defmethod doit ((n integer)) "I'm an integer!")
(defmethod doit ((s string)) "I'm a string!")
(defmethod doit ((type (eql :hero)) thing) "I'm a superhero!")

(doit 2)             ;; ⇒ I'm an integer!
(doit "2")           ;; ⇒ I'm a string!
(doit 'x)            ;; ⇒ Error: No applicable method
(doit :hero 'bobert) ;; ⇒ I'm a superhero!

;; C-h o cl-defmethod ⇒ see extensible list of specialisers Elisp supports.

We can of-course make our own classes:

(defclass person  () ((name)))
(defmethod speak ((x person)) (format "My name is %s." (slot-value x 'name)))
(setq p (make-instance 'person))
(setf (slot-value p 'name) "bobert")
(speak p) ;; ⇒ My name is bobert.

;; Inherits from ‘person’ and has accessor & constructor methods for a new slot
(defclass teacher (person) ((topic :accessor teacher-topic :initarg :studying)))

(defmethod speak ((x teacher))
  (format "My name is %s,and I study %s." (slot-value x 'name) (teacher-topic x)))

(setq ins (make-instance 'teacher :studying "mathematics"))
(setf (slot-value ins 'name) "Robert")
(speak ins) ;; ⇒ My name is Robert, and I study mathematics.

Later in this article, we'll make something like the declaim above but have it be effectful at run-time. Typing as Macros!

( If you happen to be interested in looking under the hood to see what compiler generated code looks like use disassemble. For example, declare (defun go (x) (+ 1 x) 'bye) then invoke (disassemble 'go) to see something like varref x⨾ add1⨾ discard ⨾ constant bye⨾ return. )

⇨ Each primitive type has a corresponding Lisp function that checks whether an object is a member of that type. Usually, these are the type name appended with -p, for multi-word names, and p for single word names. E.g., string type has the predicate stringp.

Type Descriptor

Objects holding information about types.

This is a record; the type-of function returns the first slot of records.

This section is based GNU Emacs Lisp Reference Manual, §2.3 “Programming Types”.

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.

I have heard more than one LISP advocate state such subjective comments as, "LISP is the most powerful and elegant programming language in the world" and expect such comments to be taken as objective truth. I have never heard a Java, C++, C, Perl, or Python advocate make the same claim about their own language of choice.

---A guy on slashdot

I learned a lot of stuff, hope you did too ^_^

Neato web articles:

• What to know before debating type systems
  • Debunks a number of fallacies such as “dynamic typing provides no way to find bugs” and “static types need type declarations”.
• Dynamic Languages Strike Back
  • Everything you might wanna know about dynamically checked languages.
• The Association of Lisp Users
  • Abundant resource relating to Lisp.
• Untyped Programs Don’t Exist
  • It's not a matter of typing but of pragmatics.
• What is Gradual Typing:
  • Discusses how static and dynamic typing can be used together hamroniously.
• CLiki — The Common Lisp Wiki
  • Contains resources for learning about and using the programming language Common Lisp.
  • The humour section is delightful.
• Strong Static Type Checking for Functional Common Lisp
  • PhD thesis regarding strong static type checking in an applicative subset of CL.
• Beating the Averages
  • Paul Graham discusses “the most powerful language available” —Lisp.
  • Other articles he's written about Lisp can be found here.
• The Bipolar Lisp Programmer
  • “Lisp is, like life, what you make of it.” Lisps attract a certain kind of personality.
• A bunch of papers on polymorphic (modal) type systems for Lisp-like multi-staged languages: This is generic, this is ML + Scheme, this for compile-time typing, and this one “allows the programmer to declaratively express the types of heterogeneous sequences in a way which is natural in the Common Lisp language.”
• Type Systems as Macros

  • After defining declare-type I thought the slogan “types by macros” sounded nifty; Googling it led me to this paper where the Racket is endowed with types.

    Lisp is great lol.

• How Lisp Became God's Own Programming Language
  • History and venerance of Lisp.
• Common Lisp HyperSpec – Type Specifiers