# Posts tagged "types":

## Typed Lisp, A Primer

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:

- Multiple examples of type constructions in Lisp.
- Comparing Lisp type systems with modern languages, such as Haskell.
- Show how algebraic polymorphic types like
`Pair`

and`Maybe`

can be defined in Lisp. Including heterogeneously typed lists! - Convey a passion for an elegant language.
- 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.

## Graphs are to categories as lists are to monoids

Numbers are the lengths of lists which are the flattenings of trees which are
the spannings of graphs.
Unlike the first three, graphs have *two* underlying types of interest
–the vertices and the edges– and it is getting to grips with this complexity
that we attempt to tackle by considering their ‘algebraic’ counterpart: Categories.

In our exploration of what graphs could possibly be and their relationships to lists are,
we shall *mechanise,* or *implement,* our claims since there will be many details and it is easy
to make mistakes –moreover as a self-learning project, I'd feel more confident to make
**bold** claims when I have a proof assistant checking my work ;-)

Assuming slight familiarity with the Agda programming language, we motivate the need for
basic concepts of category theory with the aim of discussing adjunctions with
a running example of a detailed construction and proof of a free functor.
Moreover, the article contains a host of `exercises`

whose solutions can be found in the
literate source file. Raw Agda code can be found here.

Since the read time for this article is more than two hours, excluding the interspersed exercises, it may help to occasionally consult a some reference sheets:

Coming from a background in order theory, I love Galois Connections and so
our categorical hammer will not be terminal objects nor limits, but rather adjunctions.
As such, *everything is an adjunction* is an apt slogan for us :-)

-- This file has been extracted from https://alhassy.github.io/PathCat/ -- Type checks with Agda version 2.6.0.