# Emacs Lisp Introduction

Richard Stallman is an american programmer and software freedom activist. He graduated from Harvard magna cum laude in Physics and started his PhD in Physics at MIT, but after about one year, he decided to focus on programming at the MIT AI Laboratory. There, he developed several softwares, including Emacs, which we’ll talk about in this post.

Emacs is named after Editor MACroS, since it was originally a macro editor for another editor, called TECO.

I’ve been using emacs since 2005, but never took the time to learn about elisp, which is the emacs dialect of Lisp and which emacs uses to implement a lot of its functions and the way it allows users to extend it.

In this post we’ll cover the basics of the elisp language. Most of if was based in the “Introduction to Programming in Emacs Lisp” by Robert Chassell and the Emacs Lisp Manual.

### Setting up the environment

In the following sessions we’ll have a lot of examples, so let’s setup an environment to run them.

Interpreter. For an interactive way to test the code snippets, we can use the elisp interpreter, integrated with emacs, called ielm. To open it, just run M-x ielm.

Running from a text file. An alternative to using the interpreter is by evaluating the code in a given region. To do that, select a region and run eval-last-sexp (C-x C-e).

Now, let’s cover some of the basic aspects of emacs lisp.

### Basics

List Centered. Lisp stands for list processing and as this suggests, it is highly centered on lists. Usually we use lists to perform the evaluation of some expression (which is also referred to form). One common expression is a function call. In this case, the first element of the list is the function and the other elements are parameters to the function. For example, we can call the function max:

(max 3 4) ;; returns 4


Similarly, for operators, we first provide the operator and then the parameters, so the For example, to add two numbers:

(+ 2 3)


We can see then that for arithmetic expressions we use the prefix (polish) notation, instead of the infix notation as in languages such as C++, Python and Haskell.

To use a elisp list to represent an actual list, we use the single quote.

'(1 2 3)


Printing. For simple cases, printing can be handy. On elisp we can use the function message. Run the following in the interpreter or run eval-last-sexp with that text selected:

(message "hello world")


This will print out the hello world string in the messages buffer, which can be viewed by running switch-to-buffer command (M-x b) and going to the *Messages* buffer.

Comments. In elisp, comments are inline and start after a semi-colon (unless it’s part of a string): ;.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; This is a way to emphasize a comment
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(message "hello; world")  ; simple inline comment
; will print hello; world


### Variables

As in other languages, elisp has variables. But in elisp, variable names can contain symbols that wouldn’t be allowed as in some more common languages like +,-,*.

That is possible because in elisp we don’t have in-fix notation, so a variable named a+b is not ambiguously mistaken by a plus b, which has to be defined as (+ a b)

To set a variable you can use the set function:

(set 'x '(1 2))


We quote both elements because we want their literal and not to evaluate them. In most of the cases, we want the left hand side of the assignment to be a literal (representing the variable), so we use the shortcut setq:

(setq x '(1 2)) ;; Equivalent to (set 'x '(1 2))


Another option is to use defvar. The difference between defvar and setq is that defvar won’t set the variable again if it was already defined.

(setq x '(1 2))
(defvar x '(3 4)) ;; x still holds (1 2)


When we use set/setq/defvar, we create a variable in the global scope. To restrict variables to a local scope, we can use the let.

(let (a (b 5))
(setq a 3)
(+ a b)
) ;; returns 8


For this function, the first argument is a list of the variables which will be in the local scope. You can initialize a variable with a value by providing a pair (variable value) like we did with b above.

To indicate that a variable should not be changed, we can use the defconst macro. Note that it doesn’t actually prevent from overriding with setq though.

Another form of setting variable is using the special form defcustom. The first three parameters are the same of defvar. In addition, we can provide a documentation string as the fourth parameter and following are any number of arguments in the form

<keyword>:<value>

Common examples of keywords are type, option and group.

The type can have a different set of values such as string, integer, function, etc.

A custom group represents a series of custom variables and or other custom groups. Thus, one can organize groups in a tree hierarchy. When specifying the group keyword, we can provide an existing group such as applications, or define our own.

Let’s define our custom group for learning purposes:

(defgroup my-custom-group nil
"This is my first custom group"
:group 'applications
)


In the definition above, we’re creating a group called my-custom-group. The second argument is the list of custom variables in the group, which in our case is empty. The third argument is a description of the group and then there’s a list of key-value pairs, as in defcustom. In the example above, we’re making our new group a subgroup of the existing applications group.

Now, let’s create a custom variable in that group:

(defcustom my-custom-var nil
"This is my first custom variable."
:type 'string
:group 'applications)


Let’s add these definitions to our init file (e.g. .emacs or .emacs.d/init.el) and re-open emacs.

We can browse the custom variables by typing M-x customize to go the *Customize Apropos* buffer. In this buffer, there’s the option to search for variable names or groups. Let’s search for my-custom-variable in the search box:

Figure 1: Searching for my-custom-var (click to enlarge)

We can edit its value by changing from nil in the yellow box above. Let’s put an arbitrary string, such as "some-value" and then hit the [Save for future sessions] button.

This should change the init file with something like:

(custom-set-variables
'(my-custom-variable "some-value")
)


### List Manipulation: cons, car and cdr

One distinct trait of Lisp and Emacs is their alternative naming conventions. For example, what most people refer to copy and paste, emacs uses kill and yank.

Lisp, on its merit, has two important list functions curiously named car and cdr. The function car stands for Contents of the Address part of the Register and cdr for Contents of the Decrement part of the Register.

The car function will retrieve the first element of the list and cdr will get the remaining part of it.

(car '(1 2 3)) ;; 1
(cdr '(1 2 3)) ;; (1 2 3)


Another important function with a more intuitive meaning is cons, a short for constructor. It takes an element and a list, and preprends the element to the list and returns a new list:

(cons 1 (2 3)) ;; (1 2 3)


For those familiar with Haskell, cons is like the (:) operator, car is head and cdr is tail.

### Conditionals

In elisp we can use the if special form, which can take 2 or 3 arguments.

(if <condition> <then clause> <optional else clause>

The first argument is a predicate. A predicate is anything that after evaluated returns true or false. In elisp, both nil and the empty list are considered false. Anything else is true.

If the condition evaluates to true, the second argument is evaluated and returned. If it’s false and the third argument is provided, it will evaluate it and return. If it’s false and the third argument is not provided, it will just return false (nil).

Let’s do a dummy example. Suppose we have an existing variable x and we want to print a message depending on whether it’s negative:

(if (> x 0)
(message "x is positive")
(message "x is negative")
)


Block of code. If besides printing a message we want to do some calculations, we would need to evaluate multiple statements, but the second argument of if takes a single one. To solve this, we can use the progn function, which will combine a list of statements into a single one.

In our example above, if besides printing a message in case the number is negative, we wanted to set x to positive, we could do something like:

(if (> x 0)
(message "x is positive")
(progn
(message "x is negative")
(setq x (* -1 x))
)
)


### Loops

We can use a loop with the while function. It takes a predicate as the first argument and one ore more arguments which will be executed while the predicate evaluates to true. Another simple example:

;; Print numbers from 0 to 9
(let ((x 0))
(while (< x 10)
(message (number-to-string x))
(setq x (+ x 1))
)
)


For the example above, we can alternatively use the dotimes function, which executes a series of statements an specified number of times, much like a for in other languages.

(dotimes (x 10 nil)
(message (number-to-string x))
)


It takes two or more parameters. The first is a list of three elements, the first element will represent the counter (which starts at 0), the second is the number of repetitions and the third is executed after the loop is over. The other parameters are evaluated in the loop.

Another handy function is the dolist, which will iterate through a list for us. For example:

(dotimes (elem '("a" "b" "c") nil)
(message elem)
)


It takes two or more parameters, the first is a list of three elements: a variable which will contain the an element at each iteration; the list to be iterated on; an expression to be evaluated when finishing the loop. The other parameters are the body of the loop.

### Functions

To define a function, we can use the special defun form.

(defun add (a b)
"This simple function adds to numbers"
(+ a b)
)


It takes several arguments. The first one is the name of the function, the second is a list representing the parameters of that function, the third, optional, is a string describing what the function does. The remaining arguments are executed and we evaluate a function and the last evaluated argument is returned.

Anonymous functions. W can also create an anonymous (lambda). The example above would be done as:

(setq add (lambda (a b)
(+ a b)
))


But this time we need to call this function through funcall. This is because at runtime, add can potentially have any type (not necessarily a function), so we might not know it can be invoked as a function.

(funcall add 3 4)


Recursion. We can also define a function in terms of itself to implement recursion. The classical factorial example can be done as:

(defun factorial (n)
"Computes the factorial of n"
(if (<= n 1)
1
(* n (factorial (- n 1)))
)
)


Commands. Within emacs, it’s handy to ask for the input parameters from the user. For that we can use the interactive option. Using the example above, we can ask the input for the factorial function:

(defun printFactorial (n)
(interactive "n")
(message (number-to-string (factorial n)))
)


To run this, first execute execute-extended-command and then execute printFactorial. After hitting enter, you’ll be prompted to input a number, which will feed the function printFactorial.

### Conclusion

In this post, we’ve learned a bit about elisp. In future posts, we’ll cover some of the API emacs provides for extending it.

Robert Chassell mentions that “Introduction to Programming in Emacs Lisp” is a book for non-programmers, but he digs into functions definitions and implementation details that would be uninviting for people learning how to program.

### References

[1] An Introduction to Programming in Emacs Lisp
[2] Emacs Lisp Reference Manual (v 24.3)
[3] Customization Types

# An Introduction to Agda

Per Martin-Löf is a Swedish logician, philosopher and mathematician statistician. Since 1970 he has been mainly publishing on logic.

Martin-Löf has been active in developing intuitionistic type theory as a constructive foundation of mathematics and his work on type theory has influenced computer science.

He completed his PhD program under supervision of Andrei Kolgomorov and is currently Professor at Stockholm University, being a member of the Royal Swedish Academy of Sciences.

In this post we’ll talk about assisted theorem proving, more specifically using a tool named Agda, which has it’s syntax based on Haskell and the engine is based on the Per Martin-Löf’s intuitionistic type theory.

We’ll first talk about the basic concepts such as assisted theorem proving and dependent type theory and then present a very brief introduction to Agda based on a tutorial from Ulf Norell and James Chapman [3].

### Assisted Theorem Proving

We can classify theorem proving in the following categories:

1) Manual
2) Manual with machine support
3) Interactive
4) Automated

(1) is the oldest, most known and widely used method by mathematicians. (2) Since the introduction of computers, we now can have machines to verify syntax and make manual proofs less error prone. (3) We can also write proofs in a way the machine understands so that it can perform some logical deductions steps for us. (4) In the last extreme case, we can let the machine do all the job and find proofs by itself.

### Dependent Types

Basically speaking, dependent type is a type that depends on a value. In typed programming languages we can have a type like vector T, representing a vector containing elements of type T, but in a dependent type language we could also have vector T n, representing vectors with elements of type T and length n. We’ll see an example for this type in the next section using Agda.

### Agda

Agda is a dependent type language based on intuitionistic type theory, introduced by Martin-Löf. It was first implemented by Catarina Coquand (who is married to Thierry Coquand, which inspired the Coq tool, another famous assisted proof tool). Later it was rewritten as Agda 2 by Ulf Norell, one of the authors of the tutorial we’re going to follow.

#### Installing

The first thing we want to do before starting is to get Agda running. This can be done using the cabal package manager from Haskell:

> cabal install Agda


On Mac, this will install some binaries to ~/Library/Haskell. We want to use some of those binaries, so let’s include in our bin path:

export PATH="$HOME/Library/Haskell/bin:$PATH"


Agda has a very good integration with Emacs. On Mac we can make use of that integration in Aquamacs. To set up the right configuration into the .emacs file, we can now run:

> agda-mode setup


#### Main Concepts

Latex and Unicode. Agda uses makes use of unicode characters to make the code more readable and accepts LaTeX syntax to define them. For example, we can input \rightarrow which will be transformed into the → character. Also there are shortcuts to avoid typing a lot (for example \r is expanded to \rightarrow)

Delimiters. Agda is very flexible in naming, by only considering very few characters as delimiter (including space, parenthesis and curly brackets). This means we can have names like :<a*, but then we have to be careful in adding space whenever we need to separate two variables.

Modules and name convention. Agda files have the extension .agda. For our tutorial, let’s create one called basic.agda. The first thing we want to do is to define the module, which is used to manage namespaces. By convention, the module name has to match the file name, so we write:

module basic where


Data Types. Our basic working blocks will be types and we can define them by data types, which have syntax similar to data types in Haskell. For example, we can model the boolean type, which we call Bool. In the following code we have the type named Bool which is a subset of Set (pre-defined) and we provide two constructors, both being of the type Bool.

data Bool : Set where
true : Bool
false : Bool


In the same manner we can define the set of natural numbers. Since it’s impossible to explicitly define all value like we did for booleans, we do so by defining a function suc recursively, which takes a Nat and returns its successor, like in the following example:

-- Natural numbers
data Nat : Set where
zero : Nat
suc  : Nat -> Nat


Note that we are saying the constructor suc represents a function that receives a Nat and return a Nat, but we are not providing the implementation for it.

So let’s write some functions to work with the Nat type. More specifically, addition and multiplication.

Functions. In Agda, when we write a function surrounded by underscores, like _+_, we’re defining a function that takes two arguments using infix notation. Let’s define the addition operation:

-- Addition
_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)


Note how we define everything in terms of the basic elements from Nat, that is, zero and suc, we have no notion of values. This is important because if we want to encode proofs as programs, we have to be generic and ‘value agnostic’. In this function we pattern match on different values of the first argument: If it’s zero, we are in the base case. Otherwise, the first argument must be a successor of some another value n, so we do recursion on n until it hit the base case.

Multiplication is analogous, but here we use the _+_ operator to define the second matched pattern:

-- Multiplication
_*_ : Nat -> Nat -> Nat
zero  * m = zero
suc n * m = m + n * m


The code above will cause an error because Agda requires strictly different priorities for different operators.

We can attribute some random values to these operators using infixl, which takes a priority value and a function. The higher the value, the higher the priority. Since we want multiplication to have higher priority than addition we can assign a higher number for it, for example:

-- Defining priority
infixl 6 _*_
infixl 4 _+_


Parametrized types. We can define a type that depends on other types, like parametrized types in Haskell or templates in C++. In this tutorial, we’ll create a list of elements of a given type A, as in the following data type:

-- Definition of a list with parametrized type
data List (A : Set) : Set where
-- empty operator
[] : List A
-- append operator
_::_ : A -> List A -> List A


Let’s write the map function over List. Differently from Haskell, Agda doesn’t perform type inference by default, so we need to explicitly provide the types when defining/calling a function that depends on other types. In the following example, the types A and B must be provided as parameters:

map1 : (A : Set) -> (B : Set) -> (A -> B) -> List A -> List B
map1 A B f [] = []
map1 A B f (x :: xs) = f x :: map1 A B f xs


We have the following syntax sugar to combine two or more types that are subset of the same type:

(A : Set) -> (B : Set) is equivalent to (A B : Set)

Implicit Types. We have the option to make types implicit and let Agda figure out the right one. The syntax is to use curly brackets instead of parenthesis:

map2 : {A B : Set} -> (A -> B) -> List A -> List B
map2 f [] = []
map2 f (x :: xs) = f x :: map2 f xs


Dependent Types. So far the types and operations we discussed so far don’t seem to show the real power of dependent types. So let’s define a new version of List, enhanced with the length of the list, which we’ll then call Vector:

data Vec (A : Set) : Nat -> Set where
[]   : Vec A zero
-- Make the length type implicit
_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)


Here we have two parameters when defining the data type, Nat -> Set. Notice also how when defining the list recursively we update the value n properly.

One nice thing about this is that in defining a head function, we don’t need to handle the empty case as long as we restrict the type of non-empty lists:

-- Doesn't need to check for empty lists. Restriction is encoded in
-- the function type!
head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
head (x :: xs) = x


Proofs as types. We are now going to write an example on how to use dependent types to encode proofs ( as types.

Let’s start by defining data types to represent the two possible values of a boolean. Note that we don’t specify constructors here.

data False : Set where
data True  : Set where


Now we define a function to convert a boolean values into these types:

isTrue : Bool -> Set
isTrue true = True
isTrue false = False


Let’s, for instance, define a function to be use as predicate, in this case, the < operator:

-- Definition of the < operator
_<_ : Nat -> Nat -> Bool
_ < zero = false
zero  < suc n = true
suc m < suc n = m < n


We will need the following function, that returns the length of a list, in our final example:

-- Definition of the length function
length : {A : Set} -> List A -> Nat
length [] = zero
length (x :: xs) = suc (length xs)


Finally, we can now write a sample function that encodes a predicate as a type. In the following example, the function lookup accepts one member of the family of predicates in which n less than the size of the list is a true statement.

-- Function that looks up the i-th element in a list
-- param 1: list
-- param 2: look up index
-- param 3: proof
lookup : {A : Set}(xs : List A)(n : Nat) -> isTrue (n < length xs) -> A
lookup [] n ()
lookup (x :: xs) zero p = x
lookup (x :: xs) (suc n) p = lookup xs n p


This concludes our brief introduction to Agda syntax and dependent types. In following posts we’ll learn more about writing proofs and have Agda to perform logical derivations for us.

### Conclusion

I have close to zero knowledge in formal systems. I’ve been exposed briefly to it by reading parts of Gödel, Escher and Bach and the subject sounds very interesting. I based most of the content of this post in a few introductory tutorials [3-6], but I still didn’t get a good grasp of the power of systems like Agda.

I was initially interested in learn Coq but due to some problems in setting it up, I ended up looking for alternatives and found Agda. It seems that Coq is based on Ocaml and Agda is based on Haskell and since I’ve been focused in learning Haskell, it was a pleasant surprise. Agda has also has a good integration with Emacs, which is my favorite editor, so this was a plus.

### References

[1] Per Martin-Löf – Wikipedia
[2] Proof Assistant – Comparison of Systems – Wikipedia
[3] Dependently Typed Programming in Agda – Ulf Norell and James Chapman
[4] Interactive Theorem Proving, Lecture Notes 0 – Anton Setzer
[5] Interactive Theorem Proving, Lecture Notes 1 – Anton Setzer
[6] Interactive Theorem Proving, Lecture Notes 2 – Anton Setzer