The Pie language, which accompanies The Little Typer by Friedman and Christiansen
Switch branches/tags
Nothing to show
Clone or download
Latest commit e3579c2 Nov 19, 2018
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
gui Track renamings for freshness during elaboration Jan 24, 2018
.gitignore Initial export from book Jan 5, 2018
.travis.yml Add Racket 6.12 to CI Mar 19, 2018
COPYING Add AGPL license Jan 5, 2018
README.md Fix link Jan 10, 2018
alpha.rkt Initial export from book Jan 5, 2018
basics.rkt Improve in-source documentation for laziness and other features Sep 7, 2018
fresh.rkt Initial export from book Jan 5, 2018
info.rkt add rackunit-lib to deps Oct 9, 2018
interactive-editing.rkt Initial export from book Jan 5, 2018
locations.rkt Initial export from book Jan 5, 2018
main.rkt Make output from TODO match the book precisely May 4, 2018
normalize.rkt Improve in-source documentation for laziness and other features Sep 7, 2018
parser.rkt Make descriptions of syntax match the book text better Nov 19, 2018
pie-err.rkt better pie error highlighting in DrRacket Jan 31, 2018
pie-info.rkt Initial export from book Jan 5, 2018
pie.scrbl Fix mistake in Pie reference Nov 19, 2018
pretty.rkt Fix pretty-printing of neutral induction forms Mar 8, 2018
rep.rkt Improve in-source documentation for laziness and other features Sep 7, 2018
resugar.rkt Fix desugaring of core cong Mar 8, 2018
serialization.rkt Initial export from book Jan 5, 2018
show-goal.rkt Improve in-source documentation for laziness and other features Sep 7, 2018
slideshow.rkt Initial export from book Jan 5, 2018
test-todo-output.rkt Test the TODO output May 4, 2018
tests.rkt Slightly more thorough testing of call-by-need Sep 7, 2018
todo-test.pie Test the TODO output May 4, 2018
tooltip.rkt Initial export from book Jan 5, 2018
typechecker.rkt Improve in-source documentation for laziness and other features Sep 7, 2018

README.md

Pie: A Little Language with Dependent Types

This is Pie, the companion language for The Little Typer by Daniel P. Friedman and David Thrane Christiansen.

How to Use Pie

Pie is a Racket language, requiring Racket version 6.5 or newer. After installation, Racket will interpret any file beginning with #lang pie as a Pie program.

TODO items

If you can't figure out what to write at some point in a Pie program, it's OK to leave behind a space to be filled out later. This corresponds to the empty boxes in The Little Typer. These TODOs are written TODO in Pie.

DrRacket Integration

Pie provides additional information to DrRacket, including tooltips and other metadata. Point the mouse at a pair of parentheses, a name, or a Pie constructor or type constructor to see information about the expression.

Additionally, Pie supports the DrRacket TODO list for incomplete programs.

Command-Line REPL

If you prefer an editor other than DrRacket, it may be convenient to start a Pie REPL on a command line. To do so, use the command racket -l pie -i to start Racket with the pie language in interactive mode.

Installation Instructions

Pie is not yet officially released. However, it is on the Racket package server.

From DrRacket

Click the "File" menu, and then select "Install Package...". Type pie in the box, and click the "Install" button.

From a Command Line

Run the following command: raco pkg install pie

Updates

Because it exists to support a book, the Pie language is finished and will not change. However, this implementation of Pie might someday acquire additional features, or it might require updates to keep up with new computers. In that case, update it as you would any Racket package.

Updating in DrRacket

Click the "File" menu, and then select "Install Package...". Type pie in the box, and click the "Update" button.

Updating from a Command Line

The command raco pkg update pie updates Pie.