#+Title: Typed Lisp, A Primer
#+Description: Exploring Lisp's fine-grained type hierarchy.
#+DATE: <2019-08-21 19:29>
#+AUTHOR: Musa Al-hassy
#+EMAIL: alhassy@gmail.com
#+fileimage: emacs-birthday-present.png
#+IMAGEHEIGHT: 350
#+IMAGEWIDTH: 350
#+filetags: types lisp program-proving emacs
* Abstract :ignore:
:PROPERTIES:...
#+TOC: headlines 2
Let's explore Lisp's fine-grained type hierarchy!
We begin with a shallow comparison to Haskell, a rapid tour of type theory,
try in vain to defend dynamic approaches, give a somewhat humorous account of history,
note that you've been bamboozled ---type's have always been there---,
then go into technical details of some Lisp types, and finally conclude by showing
how macros permit typing.
Goals for this article:
1. Multiple examples of type constructions in Lisp.
2. Comparing Lisp type systems with modern languages, such as Haskell.
3. Show how algebraic polymorphic types like Pair and Maybe can be defined in Lisp.
Including heterogeneously typed lists!
4. Convey a passion for an elegant language.
5. Augment Lisp with functional Haskell-like type declarations ;-)
Unless suggested otherwise, the phrase “Lisp” refers to
Common Lisp as supported by Emacs Lisp. As such, the resulting discussion
is applicable to a number of Lisp dialects
---I'm ignoring editing types such as buffers and keymaps, for now.
* LaTeX stuffs :ignore:
:PROPERTIES:...
#+LATEX_HEADER: \usepackage{multicol,xparse,newunicodechar}
#+LATEX_HEADER: \newunicodechar{↯}{ !! }
#+LATEX_HEADER: \newunicodechar{✓}{ !! }
#+LATEX_HEADER: \newunicodechar{⇅}{ !! }
#+LATEX_HEADER: \newunicodechar{…}{ \ensuremath{\ldots} }
#+LATEX_HEADER: \newunicodechar{⋯}{ \ensuremath{\cdots} }
#+LATEX_HEADER: \newunicodechar{′}{ \ensuremath{'} }
#+LATEX_HEADER: \newunicodechar{≈}{ \ensuremath{\approx} }
#+LATEX_HEADER: \newunicodechar{₀}{ \ensuremath{_0} }
#+LATEX_HEADER: \newunicodechar{₁}{ \ensuremath{_1} }
#+LATEX_HEADER: \newunicodechar{ₙ}{ \ensuremath{_n} }
#+LATEX_HEADER: \newunicodechar{ᵢ}{ \ensuremath{_i} }
#+LATEX_HEADER: \newunicodechar{∧}{ \ensuremath{\land} }
#+LATEX_HEADER: \newunicodechar{⇒}{ \ensuremath{\Rightarrow} }
#+LATEX_HEADER: \newunicodechar{τ}{ \ensuremath{\tau} }
#+LATEX_HEADER: \newunicodechar{σ}{ \ensuremath{\sigma} }
#+LATEX_HEADER: \newunicodechar{α}{ \ensuremath{\alpha} }
#+LATEX_HEADER: \newunicodechar{β}{ \ensuremath{\beta} }
#+LATEX_HEADER: \newunicodechar{ಠ}{ }
#+LATEX_HEADER: \newunicodechar{ง}{ }
#+LATEX_HEADER: \newunicodechar{♥}{ }
#+LATEX_HEADER: \newunicodechar{‿}{ }
* Photograph Credit :ignore:
:PROPERTIES:...
#+LaTeX: \iffalse
#+HTML: <small> <center>
( Original print by Baneen Al-hassy as a birthday present to me. )
#+HTML: </center> </small>
#+LaTeX: \fi
* HTML stuffs :ignore:
:PROPERTIES:...
#+BEGIN_export html
<style>
.figure-number {
display: none;
}
.table-number {
display: none;
}
/* Using source blocks “math” as aliaas for haskell */
pre.src-math:before { content: 'Mathematical! Algebraic! Axiomatic!'; }
/* Execute this for alias: (add-to-list 'org-src-lang-modes '("math" . haskell)) */
</style>
#+END_export
#
# This essentially lets us make an alias for the minted backend.
* “Loving Haskell & Lisp is Inconsistent”
:PROPERTIES:...
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.
#+CAPTION: xkcd - Lisp is a language of timeless elegance
https://imgs.xkcd.com/comics/lisp_cycles.png
+ ↯ 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.
#+caption: From the awesome “Land of Lisp” book
https://i.stack.imgur.com/jvSOG.png
:Unrelated:...
+ 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.
* Why Bother with Types? A Terse Tutorial on Type Systems
:PROPERTIES:...
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.
#+begin_center org
A type is a collection of possible objects.
To say “$e$ has type $τ$” one writes $e : τ$, or in Lisp: (typep e 'τ).
#+end_center
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.
#+begin_quote org
✓ 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.
#+end_quote
#+caption: Lisp's type hierarchy is a “complemented lattice” ♥‿♥
| Common types | integer, number, string, keyword, array, cons, list, vector, macro, function, atom |
| Top | t has everything as an element |
| Unit | null has one element named nil |
| Bottom | nil has no elements at all |
| Union | (or τ₀ τ₁ … τₙ) has elements any element in any type τᵢ |
| Intersection | (and τ₀ τ₁ … τₙ) has elements that are in all the types τᵢ |
| Complement | (not τ) has elements that are not of type τ |
| Enumeration | (member x₀ … xₙ) is the type consisting of only the elements xᵢ |
| Singleton | (eql x) is the type with only the element x |
| Comprehension | (satisfies p) is the type of values that satisfy predicate p |
Let's see some examples:
#+BEGIN_SRC emacs-lisp
(typep 'x 't) (typep 12 't)
(typep 'x 'nil)
(typep nil 'null) (typep () 'null)
(typep 3 '(eql 3)) (typep 4 '(eql 3))
(typep 3 '(member 3 x "c")) (typep 'x '(member 3 x "c")) (typep 'y '(member 3 x "c"))
(typep 12 '(satisfies (lambda (x) (oddp x)))) (typep 12 '(satisfies evenp) )
#+END_SRC
Here's a convenient one: (booleanp x) ≈ (typep x '(member t nil)).
#+BEGIN_SRC emacs-lisp
(booleanp 2) (booleanp nil) #+END_SRC
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.
#+begin_center org
Lisp (primitive) types are inferred!
“Values have types, not variables.” ---Paul Graham, ANSI Common Lisp
#+end_center
Let's review some important features of type systems and how they manifest themselves
in Lisp.
** Obtaining & Checking Types
:PROPERTIES:...
The typing relationship “:” is usually deterministic in its second argument for
static languages: e : τ ∧ e : τ′ ⇒ τ ≈ τ′. However this is not the case with
Lisp's typep.
#+caption: Where are the types & /when/ are they checked?
| Style | Definition | Examples |
|---------+-------------------------------------------+------------------|
| Static | Variables have a fixed type; compile time | Haskell & C# |
| Dynamic | Values have a fixed type; runtime | Lisp & Smalltalk |
In some sense, dynamic languages make it easy to produce polymorphic functions.
Ironically, the previous sentences is only meaningful if you acknowledge the importance
of types and type variables.
In Lisp, types are inferred and needn't be declared.
However, the declaration serves as a nice documentation to further readers ;-)
#+BEGIN_SRC emacs-lisp
(setq ellew 314)
(type-of ellew)
(setq ellew "oh my")
(type-of ellew) #+END_SRC
+ The type-of function returns the type of a given object.
+ Re variables: Static ⇒ only values can change; dynamic ⇒ both values and types change.
We may check the type of an item using typep, whose second argument
is a “type specifiers”
---an expressions whose value denotes a type; e.g., the or expression below
forms a ‘union type’.
There's also check-type: It's like typep but instead of yielding true or
false, it stays quiet in the former and signals a type error in the latter.
#+BEGIN_SRC emacs-lisp
(check-type 12 integer) (check-type 12 (or symbol integer)) (check-type "12" (or symbol integer)) #+END_SRC
In summary:
| (equal τ (type-of e)) | ≈ | (typep e τ) |
| (check-type e τ) | ≈ | (unless (typep e 'τ) (error "⋯")) |
( Note: (unless x y) ≈ (when (not x) y) .)
** Statics & Dynamics of Lisp
:PROPERTIES:...
#+BEGIN_quote
Types are the central organising principle of the theory of programming languages.
Language features are manifestations of type structure.
The syntax of a language is governed by the constructs that define its types, and
its semantics is determined by the interactions among those constructs.
--- Robert Harper, Practical Foundations for Programming Languages
#+END_quote
Besides atoms like numbers and strings,
the only way to form new terms in Lisp is using “modus ponens”,
or “function application”. Here's a first approximation:
#+BEGIN_SRC math
f : τ₁ → ⋯ → τₙ → τ e₁ : τ₁ … eₙ : τₙ
-----------------------------------------------------------------------------------------
(f e₁ … eₙ) : τ
#+END_SRC
One reads such a fraction as follows: If each part of the numerator ---the ‘hypothesises’--- is true, then so is the denominator ---the ‘conclusion’.
An abstract syntax tree, or ‘AST’, is a tree with operators for branches
and arguments for children. A tree is of kind τ if the topmost branching operator has τ as its resulting type. Here's an improved rule:
#+BEGIN_SRC math
f : τ₁ → ⋯ → τₙ → τ e₁ : AST τ₁ … eₙ : AST τₙ
-----------------------------------------------------------------------------------------
(f e₁ … eₙ) : AST τ
#+END_SRC
A Lisp top-level then may execute or interpret such a form to obtain a value:
When we write e at a top-level, it is essentially (eval e) that is invoked.
#+BEGIN_SRC math
e : AST τ
-----------------------------------------------------------------------------------------
(eval e) : τ
#+END_SRC
However, we may also protect against evaluation.
#+BEGIN_SRC math
e : AST τ
-----------------------------------------------------------------------------------------
(quote e) : AST τ
#+END_SRC
We have the following execution rules, where ‘⟿’ denotes “reduces to”.
#+BEGIN_SRC math
(eval a) ⟿ a ;; for atom ‘a’
(eval (quote e)) ⟿ e
(eval (f e₁ … eₙ)) ⟿ (f (eval e₁) ⋯ (eval eₙ)) ;; Actually invoke ‘f’
#+END_SRC
#+begin_center
A conceptual model of Lisp is eval.
#+end_center
** Variable Scope
:PROPERTIES:...
There's also the matter of “scope”, or ‘life time’, of a variable.
#+caption: Local variables temporarily mask global names …
| Style | Definition | Examples |
|---------+--------------------------+----------------------------------------|
| Lexical | … only in visible code | Nearly every language! |
| Dynamic | … every place imaginable | Bash, Perl, & allowable in some Lisps |
That is, dynamic scope means a local variable not only acts as a global variable
for the rest of the scope but it does so even in the definitions of pre-defined methods
being invoked in the scope.
#+BEGIN_SRC elisp
(setq it "bye")
(defun go () it)
(let ((it 3)) (go))
(setq lexical-binding t)
(let ((it 3)) (go)) #+END_SRC
#+begin_center org
Dynamic scope lets bindings leak down into all constituents in its wake.
#+end_center
That is fantastic when we want to do unit tests involving utilities with side-effects:
We simply locally re-define the side-effect component to, say, do nothing. (─‿‿─)
** Casts & Coercions
:PROPERTIES:...
#+caption: The frequency of implicit type coercions
| Style | Definition | Examples |
|--------+-------------------------+----------------|
| Strong | Almost never | Lisp & Haskell |
| Weak | Try as best as possible | JavaScript & C |
Strong systems will not accidentally coerce terms.
Lisp has a coerce form; but coercion semantics is generally unsound
in any language and so should be used with tremendous caution.
( Though Haskell has some sensible coercions as well as unsafe one. )
#+BEGIN_SRC math
e : α
----------------------------------------------------------------------------------------
(coerce e β) : β
#+END_SRC
We have a magical way to turn elements of type α to elements of type β.
Some languages call this type casting.
Here's a cute example.
#+BEGIN_SRC emacs-lisp
(coerce '(76 105 115 112) 'string) #+END_SRC
** Type Annotations
:PROPERTIES:...
We may perform type annotations using the form the; e.g.,
the Haskell expression (1 :: Int) + 2 checks the type annotation,
and, if it passes, yields the value and the expression is computed.
Likewise, (the type name) yields name provided it has type type.
#+BEGIN_SRC emacs-lisp
(+ (the integer 1)
(the integer 2))
(+ (the integer 1)
(the integer "2")) #+END_SRC
Computationally, using or as a control structure for lazy sequencing with left-unit nil:
| (the τ e) ≈ (or (check-type e τ) e) |
** Type-directed Computations
:PROPERTIES:...
Sometimes a value can be one of several types.
This is specified using union types; nested unions are essentially flattened
---which is a property of ‘or’, as we shall come to see.
#+BEGIN_SRC emacs-lisp
(typep 12 'integer) (typep 'a 'symbol)
(setq woah 12)
(typep woah '(or integer symbol))
(setq woah 'nice)
(typep woah '(or integer symbol)) #+END_SRC
When given a union type, we may want to compute according to the type of a value.
+ Case along the possible types using typecase.
+ This returns a nil when no case fits; use etypecase to have an error instead of nil.
#+BEGIN_SRC emacs-lisp
(typecase woah
(integer (+1 woah))
(symbol 'cool)
(t "yikes"))
#+END_SRC
** Type Specifiers: On the nature of types in Lisp
:PROPERTIES:...
#+begin_quote
Types are not objects in Common Lisp. There is no object that corresponds to the type
integer, for example. What we get from a function like type-of, and give as an argument
to a function like typep, is not a type, but a type specifier.
A type specifier is the name of a type. ---Paul Graham, ANSI Common Lisp
#+end_quote
Type specifiers are essentially transformed into predicates as follows.
#+BEGIN_SRC emacs-lisp
(typep x 'τ) ≈ (τp x) (typep x '(and τ₁ … τₙ)) ≈ (and (typep x τ₁) … (typep x τₙ))
(typep x '(or τ₁ … τₙ)) ≈ (or (typep x τ₁) … (typep x τₙ))
(typep x '(not τ)) ≈ (not (typep x τ))
(typep x '(member e₁ … eₙ)) ≈ (or (eql x e₁) … (eql x eₙ))
(typep x '(satisfies p)) ≈ (p x)
#+END_SRC
Type specifiers are thus essentially ‘characteristic functions’ from mathematics.
** Making New Types with deftype
:PROPERTIES:...
If we use a type specifier often, we may wish to abbreviate it using
the deftype macro ---it is like defmacro but expands into a type specifier
instead of an expression.
We can define new types that will then work with typecase and friends
as follows:
1. Define a predicate my-type-p.
2. Test it out to ensure only the elements you want satisfy it.
3. Register it using deftype.
You could just do number 3 directly, but it's useful to have the
predicate form of a type descriptor.
For example, here's the three steps for a type of lists of numbers drawn from (-∞..9].
#+BEGIN_SRC emacs-lisp
(defun small-number-seq-p (thing)
(and (sequencep thing)
(every #'numberp thing)
(every (lambda (x) (< x 10)) thing)))
(setq yes '(1 2 4))
(setq no '(1 20 4))
(small-number-seq-p yes)
(deftype small-number-seq ()
'(satisfies small-number-seq-p))
(typep yes 'small-number-seq) (typep no 'small-number-seq) #+END_SRC
Arguments are processed the same as for defmacro except that optional
arguments without explicit defaults use * instead of nil as the default value.
From the deftype docs, here are some examples:
#+BEGIN_SRC emacs-lisp
(cl-deftype null () '(satisfies null)) (cl-deftype list () '(or null cons))
(cl-deftype unsigned-byte (&optional bits)
(list 'integer 0 (if (eq bits '*) bits (1- (lsh 1 bits)))))
(unsigned-byte 8) ≡ (integer 0 255)
(unsigned-byte) ≡ (integer 0 *)
unsigned-byte ≡ (integer 0 *)
#+END_SRC
+ Notice that type specifiers essentially live in their own namespace; e.g., null is the
predicate that checks if a list is empty yet null is the type specifying such lists.
Let's form a type of pairs directly ---which is not ideal!
This is a <<<polymorphic>>> datatype: It takes two type arguments, called a and b below.
#+BEGIN_SRC emacs-lisp
(deftype pair (a b &optional type)
`(satisfies (lambda (x) (and
(consp x)
(typep (car x) (quote ,a))
(typep (cdr x) (quote ,b))))))
(typep '("x" . 2) '(pair string integer)) (typep '("x" . 2) '(pair symbol integer)) (typep nil '(pair integer integer)) (typep 23 '(pair integer integer))
(setq ss "nice" nn 114)
(typep `(,ss . ,nn) '(pair string integer)) (typep (cons ss nn) '(pair string integer))
(typep '(ss . nn) '(pair string integer)) (typep `(cons ss nn) '(pair string integer)) #+END_SRC
Exercise: Define the polymorphic maybe type
such that (maybe τ) has elements being either nil or a value of τ.
:Hide:...
#
# Recursive types are types whose definitions refer to themselves.
#
Let's define type ~list-of~ such that ~(list-of τ)~ is the type of lists
whose elements are all values of type τ.
#+BEGIN_SRC emacs-lisp
(defun list-of-p (τ thing)
(and (listp thing) (every (lambda (x) (typep x τ)) thing)))
(list-of-p 'integer '(1 2 3)) (list-of-p 'integer '(1 two 3)) (list-of-p 'string '()) (list-of-p 'string '(no))
(deftype list-of (τ)
`(satisfies (lambda (thing) (list-of-p (quote ,τ) thing))))
(typep '(1 2 ) 'list) (typep '(1 two) 'list)
(typep '(1 2) '(list-of integer)) (typep '(1 "2") '(list-of string)) (typep '(1 "2") '(list-of (or integer string))) #+END_SRC
Notice that by the last example we can control the degree of heterogeneity in our lists!
So cool!
Here's some more exercises. The first should be nearly trivial, the second a bit more
work, and the last two have made me #sad.
1. Define a type (rose τ) whose elements are either τ values or rose trees of type τ.
2. Define a type record so that (record τ₁ … τₙ) denotes a record type whose iᵗʰ
component has type τᵢ.
3. Define a type constructor ∃ such that, for example, (∃ τ (pair integer τ)
denotes the type of pairs where the first components are integers and the second
components all have the same type τ, but we do not know which one.
My idea was to let τ denote the type of the first occurrence of a value
at that location, then all subsequent checks now refer to this value of τ.
Sadly, I could not define this type :'(
Upon further reading, this may be doable using a variable watcher.
4. Produce a record for monoids and keep-track of the monoid instances produced.
Define a the predicate (monoid τ) to check if any of the monoid instances
has τ as its carrier type. In this way we could simulate Haskell typeclasses.
:getting_started:...
Let me know if you do cool things!
** Algebraic Data Types a la Haskell
:PROPERTIES:...
Consider the Haskell expression type, example, and integer evaluator.
#+BEGIN_SRC haskell :tangle expr.hs
data Expr a = Var a | Expr a :+: Expr a | Neg (Expr a) deriving Show
ex :: Expr Int
ex = Var 5 :+: (Var 6 :+: Neg (Var 7))
int :: Expr Int -> Int
int (Var n) = n
int (l :+: r) = int l + int r
int (Neg e) = - (int e)
#+END_SRC
If we view a constructor declaration C a₁ … aₙ with superfluous parenthesis
as (C a₁ … aₙ), then a translation to Lisp immediately suggests itself:
#+begin_center
Haskell constructors ≅ Lisp lists whose car are constructor names
#+end_center
A nearly direct translation follows.
#+BEGIN_SRC lisp
(defun exprp (τ thing)
(pcase thing
(`(var ,n) (typep n τ))
(`(add ,l ,r) (and (exprp τ l) (exprp τ r)))
(`(neg ,e) (exprp τ e))))
(setq ex '(add (var 5) (add (var 6) (neg (var 7)))))
(exprp 'integer ex)
(declare-type int : (expr-of integer) integer)
(defun int (thing)
(pcase thing
(`(var ,n) n)
(`(add ,l ,r) (+ (int l) (int r)))
(`(neg ,e) (- (int e)))))
(int ex) #+END_SRC
There are of-course much better ways to do this in Lisp; e.g.,
use identity, +, - in-place of the var, add, neg tags
to produce “syntax that carries its semantics”
or express the interpreter int as a one liner
by replacing the formal tags with their interpretations then
invoking Lisps eval. I doubt either of these are new ideas,
but the merit of the former seems neat ---at a first glance, at least.
Support for ADTs in Common Lisp along with seemingly less clunky pattern matching
can be found here ---which I have only briefly looked at.
The Haskell presentation has type-checking baked into it, yet our
Lisp interpreter int does not! This seems terribly worrying, but
that declare-type declaration actually handles type checking for us!
#+BEGIN_SRC lisp
(deftype expr-of (τ)
`(satisfies (lambda (thing) (exprp (quote ,τ) thing))))
(typep '(1 2) '(expr-of integer)) (typep ex '(expr-of integer))
(int '(var 6 4))
#+END_SRC
Notice that invalid cases yield a helpful (run-time) error message!
* In Defence of Being Dynamically Checked
:PROPERTIES:...
#+begin_center org
Lisp gets a bad rap for being untyped; let's clarify this issue further!
#+end_center
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.
#
# I dont feel this anymore.
#
# Examples of languages that don't carry dynamic type tags and so may be considered
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.
#+BEGIN_SRC haskell
mcbride :: [Int] -> Int
mcbride xs = if null xs then head xs else 666
#+END_SRC
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:
#+BEGIN_SRC math
T : 𝔹 E : α B : α -----------------------------------------------------------------------------------------
if T then E else B : α
#+END_SRC
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
#+begin_quote org
( 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. )
#+end_quote
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.
* With its hierarchy of types, why isn't Lisp statically typed?
:PROPERTIES:...
#+begin_center org
I haven't a clue. Here are two conjectures.
#+end_center
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.
#+caption: xkcd
https://imgs.xkcd.com/comics/lisp.jpg
* Lisp Actually Admits Static Typing!
:PROPERTIES:...
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.
#+BEGIN_SRC common-lisp
(declaim (ftype (function (fixnum)) num-id))
(defun num-id (n) n)
(defun string-id (s) (declare (string s)) (num-id s))
#+END_SRC
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.
#+BEGIN_SRC emacs-lisp
(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) (doit "2") (doit 'x) (doit :hero 'bobert)
#+END_SRC
We can of-course make our own classes:
#+BEGIN_SRC emacs-lisp
(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)
(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) #+END_SRC
Later in this article, we'll make something like the declaim above
but have it be effectful at run-time. Typing as Macros!
#+begin_quote org
(
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.
)
#+end_quote
* ELisp's Type Hierarchy
:PROPERTIES:...
⇨ 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”.
** Number
:PROPERTIES:...
Numbers, including fractional and non-fractional types.
| integer | float | number | natnum | zero | plus | minus | odd | even |
The relationships between these types are as follows:
| (numberp x) ≈ (or (integerp x) (floatp x)) |
| (natnump x) ≈ (and (integerp x) (≤ 0 x)) |
| (zerop x) ≈ (equal 0 x) |
| (plusp x) ≈ (< 0 x) |
| (minusp x) ≈ (> 0 x) |
| (evenp x) ≈ (zerop (mod x 2)) |
| (oddp x) ≈ (not (oddp x)) |
+ Integer: Numbers without fractional parts.
There is no overflow checking.
#+BEGIN_SRC emacs-lisp
(expt 2 60) (expt 2 61) (expt 2 62) #+END_SRC
Numbers are written with an optional sign ‘+’ or ‘-’ at the beginning and
an optional period at the end.
| -1 ≈ -1. | 1 ≈ +1 ≈ 1. |
They may also take inclusive (and exclusive) ranges:
The type list (integer LOW HIGH) represents all integers between
LOW and HIGH, inclusive. Either bound may be a list of a single
integer to specify an exclusive limit, or a * to specify no
limit. The type (integer * *) is thus equivalent to integer.
Likewise, lists beginning with float, real, or number
represent numbers of that type falling in a particular range.
( The Emacs Common Lisp Documentation )
#+BEGIN_SRC emacs-lisp
(typep 4 '(integer 1 5)) (typep 4 '(integer 1 3))
(typep 12 'integer) (typep 12 'number)
(typep 23 'odd)
(typep 12 '(integer * 14)) (typep 12 '(integer 0 *))
(typep -1 '(not (integer 0 *))) (typep 1 '(not (integer 0 *)))
(typep 1 '(integer 1 2)) (typep 1 '(integer (1) 2))
(typep 1.23 '(float 1.20 1.24))
(typep 1.23 'number) (typep 123 'number) (typep 1.23 'real) (typep 123 'real)
(typep 1.23 'integer) (typep 123 'integer) (typep 1.23 'fixnum) (typep 123 'fixnum)
(typep 1.23 'float) (typep 123 'float) (typep 123.0 'float) #+END_SRC
+ Floating-Point: Numbers with fractional parts; expressible using scientific notation.
For example, 15.0e+2 ≈ 1500.0 and -1.0e+INF for negative infinity.
+ Aliases:
The type symbol real is a synonym for number, fixnum is a
synonym for integer, and wholenum is a synonym for natnum.
+ The smallest and largest values representable in a Lisp integer are in the
constants most-negative-fixnum and most-postive-fixnum
#+BEGIN_SRC emacs-lisp
(< -1e+INF most-negative-fixnum most-positive-fixnum 1e+INF) #+END_SRC
** Character
:PROPERTIES:...
Representation of letters, numbers, and control characters.
A character is just a small integers, up to 22 bits;
e.g., character A is represented as the integer 65.
One writes the character ‘A’ as ?A, which is identical to 65.
Punctuations ()[]\;"|'`# must be \-escaped; e.g.,
| ?\( ≈ 40 | ?\\ ≈ 92 |
Whereas ?. ≈ 46.
#+BEGIN_SRC emacs-lisp
(characterp ?f) (characterp t) #+END_SRC
Emacs specfic characters control-g C-g, backspace C-h, tab C-i, newline C-j, space,
return, del, and escape are expressed by ?\a, ?\b, ?\t, ?\n, ?\s, ?\r, ?\d, ?\e.
Generally, control characters can be expressed as ?\^𝓍 ≈ ?\C-𝓍,
and meta characters by ?\M-𝓍; e.g., C-M-b is expressed
?\M-\C-b ≈ ?\C-\M-b.
Finally, ?\S-𝓍 denotes shifted-𝓍 characters.
There are also ?\H-𝓍, ?\A-𝓍, ?\s-𝓍 to denote Hyper- Alt- or Super-modified keys;
note that lower case ‘s’ is for super whereas capital is for shift,
and lower case with no dash is a space character.
** Symbol
:PROPERTIES:...
A multi-use object that refers to functions and variables, and more.
A symbol is an object with a name; different objects have different names.
#+BEGIN_SRC emacs-lisp
(typep 'yes 'symbol) (symbolp 'yes)
(typep 12 'symbol) (symbolp 12) #+END_SRC
| symbol ≈ Is it a symbol? |
| bound ≈ Does it refer to anything? |
#+BEGIN_SRC emacs-lisp
(typep 'xyz 'bound)
(setq xyz 123)
(typep 'xyz 'bound) #+END_SRC
See this short docs page for more info on when a variable is void.
Names have a tremendously flexible syntax.
#+BEGIN_SRC emacs-lisp
(setq +*/-_~!@$%^&:<>{}? 23)
(setq \+1 23) (setq \12 23)
(setq this\ is\ woah 23) (+ this\ is\ woah 1) #+END_SRC
If the symbbol name starts with a colon ‘:’, it's called a keyword symbol
and automatically acts as a constant.
#+BEGIN_SRC emacs-lisp
(typep :hello 'keyword) #+END_SRC
Symbols generally act as names for variables and functions, however there are
some names that have fixed values and any attempt to reset their values signals an error.
Most notably, these include t for true or the top-most type,
nil for false or the bottom-most type, and keywords.
These three evaluate to themselves.
#+BEGIN_SRC emacs-lisp
t nil :hello
(setq t 12) (setq nil 12) (setq :x 12)
(set 'x 12) x
(equal t 't) (equal nil 'nil) (equal :x ':x)
(equal :x 'x) #+END_SRC
In particular, :x ≠ 'x!
** Sequence
:PROPERTIES:...
The interface for ordered collections; e.g.,
the (elt sequence index) function can be applied to any sequence
to extract an element at the given index.
#+begin_center org
| sequence | seq |
#+end_center
The latter is an extensible variant of the former
---for when we declare our own sequential data types.
#+BEGIN_SRC emacs-lisp
(typep '(1 2 3) 'sequence) #+END_SRC
There are two immediate subtypes: array and cons, the latter has list
as a subtype.
#+BEGIN_SRC emacs-lisp
(typep [1 2 3] 'array) (typep '(1 2 3) 'cons) (typep '(1 "2" 'three) 'list) #+END_SRC
- Array :: Arrays include strings and vectors.
* Vector :: One-dimensional arrays.
* Char-Table :: One-dimensional sparse arrays indexed by characters.
* Bool-Vector :: One-dimensional arrays of t or nil.
* Hash Table :: Super-fast lookup tables.
#+BEGIN_SRC emacs-lisp
(typep "hi" 'string) (typep 'hi 'string) #+END_SRC
- Cons cell type :: Cons cells and lists, which are chains of cons cells.
These are objects consisting of two Lisp objects, called car and cdr.
That is they are pairs of Lisp objects.
#+BEGIN_SRC math
'(x₀ x₁ x₂)
≈ '(x₀ . (x₁ . (x₂ . nil)))
≠ '(x₀ x₁ . x₂)
≈ '(x₀ . (x₁ . x₂))
#+END_SRC
Notice that when there is no ‘.’, then a list
is just a nested cons chain ending in ‘nil’.
Note that '(x₀ . x₁ . x₂) is meaningless.
Cons cells are central to Lisp and so objects which are not a cons
cell are called atoms.
#+BEGIN_SRC emacs-lisp
(typep 123 'atom) (typep 'ni 'atom) #+END_SRC
Computationally:
| | (atom x) |
| ≈ | (typep x 'atom) |
| ≈ | (not (consp x)) |
| ≈ | (not (typep x 'cons)) |
| ≈ | (typep x '(not cons)) |
Interestingly, one writes atom, not atomp.
** Function
:PROPERTIES:...
Piece of executable code.
A non-compiled function in Lisp is a lambda expression: A list whose
first element is the symbol lambda.
#+BEGIN_SRC emacs-lisp
(consp (lambda (x) x)) (functionp (lambda (x) x))
(functionp (lambda is the first)) (typep (lambda stuff) 'function) #+END_SRC
It may help to know that a defun just produces an alias for a function:
#+BEGIN_SRC emacs-lisp
(defun name (args) "docs" body)
≈ (defalias (quote name) (function (lambda (args) docs body)))
#+END_SRC
Here's some more examples.
#+BEGIN_SRC emacs-lisp
(typep #'+ 'function) (typep 'nice 'function)
(defun it (x) (format "%s" (+1 x)))
(typep #'it 'function) (functionp #'it) #+END_SRC
** Macro
:PROPERTIES:...
A method of expanding an expression into another expression.
Like functions, any list that begins with macro, and whose cdr
is a function, is considered a macro as long as Emacs Lisp is concerned.
#+BEGIN_SRC emacs-lisp
(macrop '(macro (lambda (x) x))) #+END_SRC
Since defmacro produces an alias, as follows,
#+BEGIN_SRC emacs-lisp
(defmacro name (args) "docs" body)
≈ (defalias (quote name) (cons (quote macro) (function (lambda (args) docs body))))
#+END_SRC
You may be concerned that (macrop x) ≟ (equal 'macro (car x)), and so if a user
gives you a macro you might think its a cons cell of data.
Fortunately this is not the case:
#+BEGIN_SRC emacs-lisp
(defmacro no-op () )
(macrop #'no-op) (consp #'no-op) (functionp #'no-op)
(typep #'no-op '
(satisfies (lambda (x) (and (listp x) (equal 'macro (car x)))))) #+END_SRC
Why not? Well, you could think of a macro as a ‘record’ whose label is macro and
its only element is the associated function.
** Record
:PROPERTIES:...
Compound objects with programmer-defined types.
They are the underlying representation of defstruct and defclass instances.
For example:
#+BEGIN_SRC emacs-lisp
(defstruct person
name age)
#+END_SRC
The type-of operator yields the car of instances of such declartions.
| (record τ e₀ … eₙ) ≈ #s(τ e₀ … eₙ) |
#+BEGIN_SRC emacs-lisp
(setq bobert (make-person :name "bobby" :age 'too-much))
(type-of bobert) #+END_SRC
Componenets may be indexed with aref.
#+BEGIN_SRC emacs-lisp
(aref bobert 1) (person-name bobert) #+END_SRC
A record is considered a constant for evaulation: Evaluating it yields itself.
#+BEGIN_SRC emacs-lisp
(type-of #s(person "mark" twelve)) (recordp #s(nice)) #+END_SRC
* Typing via Macros & Advice
:PROPERTIES:...
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.
#+BEGIN_SRC emacs-lisp
(declare-type 'f ((:x₁ σ₁) … (:xₘ σₘ)) (τ₁ … τₙ τ))
#+END_SRC
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.
#+BEGIN_SRC emacs-lisp :tangle yes
(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)
"
(should (and (listp types) (or (listp key-types) (symbolp key-types))))
(letf* ((pairify (lambda (xs) (loop for i in xs by #'cddr for j in (cdr xs) by #'cddr collect (cons i j)))) MA (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)
(letf* ((all-args
(-split-at
(or (--find-index (not (s-blank? (s-shared-start ":" (format "%s" it)))) args) ,num-of-types)
args)) (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))))))
(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))
(loop for (k . v) in key-args
do (shucks (cdr (assoc k (quote ,key-types))) k v))
(setq fun-result (apply orig-fun args))
(shucks (quote ,result-type) "for the result type (!)" fun-result)
fun-result))
(advice-add (function ,f) :around (function ,advice-name))
,notify-user )))
#+END_SRC
#+RESULTS:
: 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. )
:Hide:...
We accidentally forgot to consider an argument.
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₁ (:z string :w list) integer symbol string)
(cl-defun f₁ (x y &key z w) (format "%s" x))
(f₁ 'x) #+END_SRC
The type declaration said we needed 3 arguments, but we did not consider one of them.
We accidentally returned the wrong value.
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₂ (:z string :w list) integer symbol string)
(cl-defun f₂ (x y &key z w) x)
(f₂ 144 'two)
#+END_SRC
We accidentally forgot to supply an argument.
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₃ (:z string :w list) integer symbol string)
(cl-defun f₃ (x y &key z w) (format "%s" x))
(f₃ 144)
#+END_SRC
A positional argument is supplied of the wrong type.
#+BEGIN_SRC emacs-lisp :tangle yes
(f₃ 'one "two")
(f₃ 144 "two")
#+END_SRC
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.
#+BEGIN_SRC emacs-lisp :tangle yes
(f₃ 1 'two :z 'no₀ :w 'no₁)
(f₃ 1 'two :z "ok" :w 'no₁)
(f₃ 1 'two :z "ok" :w 23)
(f₃ 1 'two :z "ok" :w '(a b 1 2)) #+END_SRC
We have no optional arguments.
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₄ : integer symbol string)
(cl-defun f₄ (x y &key z w) (format "%s" x))
(f₄ 144 'two :z "bye")
(f₄ 144 'two) #+END_SRC
We can incorporate type specfiers such as unions!
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₅ : (or integer string) string)
(cl-defun f₅ (x) (format "%s" x))
(f₅ 144) (f₅ "neato")
(f₅ 'shaka-when-the-walls-fell)
#+END_SRC
No positional arguments but a complex optional argument!
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₆ (:z (satisfies (lambda (it) (and (integerp it) (= 0 (mod it 5))))))
character)
(cl-defun f₆ (&key z) ?A)
(f₆ 'hi) (f₆) (f₆ :z 6)
(f₆ :z 10) #+END_SRC
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.
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₇ : (satisfies (lambda (it) (= it 5)))
integer)
(cl-defun f₇ (n) n)
(f₇ 4)
(f₇ 5) #+END_SRC
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$.
#+BEGIN_SRC emacs-lisp :tangle yes
(declare-type f₈ : (satisfies (lambda (in) (> in 5)))
(satisfies (lambda (out) (> out 2))))
(cl-defun f₈ (n) n)
(f₈ 4)
(f₈ 72) #+END_SRC
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.
:HideMe:...
* Closing
:PROPERTIES:...
#+begin_quote org
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
#+end_quote
I learned a lot of stuff, hope you did too ^_^
* References
:PROPERTIES:...
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
* COMMENT How using compile can increase speed :experiment:
:PROPERTIES:...
#+BEGIN_SRC emacs-lisp
(defmacro measure-time (&rest body)
"Measure the time it takes to evaluate BODY."
`(let ((time (current-time)))
,@body
(message "%.06f seconds" (float-time (time-since time)))))
(setf a (make-vector 1000000 1.0))
(defun sum-elts (a)
(let ((sum 0.0))
(dotimes (r 1000000)
(incf sum (aref a r)))
sum))
(measure-time (sum-elts a))
(byte-compile 'sum-elts)
(measure-time (sum-elts a)) #+END_SRC
#+RESULTS:
: 0.000002
So there is no way to "compile the same definition again."
https://ftp.gnu.org/old-gnu/Manuals/elisp-manual-20-2.5/html_node/elisp_197.html