Write Yourself a Scheme in Agda

This is very much a work in progress. I'm trying to learn Agda, and it seems that there aren't enough longer tutorials.

Table of Contents

• Write Yourself a Scheme in Agda
  • Progress
  • Installation
    • Nix
    • Building

Progress

The following lists the parts of "Write Yourself A Scheme" and whether or not they're implemented:

• First Steps: Compiling and running
• Parsing
• Evaluation, Part 1
• Error Checking and Exceptions
• Evaluation, Part 2
• Building a REPL: Basic I/O
• Adding Variables and Assignment: Mutable State in Haskell
• Defining Scheme Functions: Closures and Environments
• Creating IO Primitives: File I/O
• Towards a Standard Library: Fold and Unfold
• Conclusion & Further Resources

(Non)-features

This Scheme doesn't come nearly as close to the one in that Wikibook to being R5RS-compliant. In particular, it is missing:

• Dotted lists
• Multiple kinds of equality

The focus is on practical programming with Agda, not on getting everything right or creating a "true" Scheme.

Installation

Nix

If you use the Nix package manager, you can use nix-shell to jump into a shell with

• Agda
• GHC + two packages required for compiling Agda to binary

Building with nix-build doesn't currently work.

Building

Do this:

for project in "agda/agda-stdlib" "gallais/agdARGS" "gallais/agdarsec"; do
  git clone "https://github.com/$project" || true
done

agda --library-file=./libraries \
      --library=standard-library \
      --library=agdarsec \
      --library=agdARGS \
      --compile-dir=build \
      -i "$PWD" \
      -c Main.agda

This clones the following three libraries:

• https://github.com/agda/agda-stdlib
• https://github.com/gallais/agdARGS
• https://github.com/gallais/agdarsec

and then compiles the main file.