sweirich / pi-forall

A demo implementation of a simple dependently-typed language

pi-forall language

This language implementation is designed to accompany four lectures at OPLSS during Summer 2023. Notes for these lectures are included in the distribution:

• oplss.pdf

(The documentation README.md includes details about how the notes are typeset.)

These lecture notes correspond to an increasingly expressive demo implementation of a dependently-typed lambda calculus. Each of the following subdirectories is a self-contained implementation and all are generated from the same source, located in the main/ directory.

• version1/: Basic language implementation
• version2/: Basic language extended with nontrivial definitional equality
• version3/: Above, extended with irrelevant arguments
• full/: Full language with datatypes

The implementation README.md includes instructions about how to compile and work with these implementations. Edits should only be for versions in the main/ directory.

History

This is a revised version of lecture notes originally presented at OPLSS during 2022, 2014, and 2013.

Videos from the 2022 and 2014 lectures are available from the OPLSS website. If you watch these videos, you should look at the corresponding branch of this repository.

An abridged version of these lectures was also given at the Compose Conference, January 2015. Notes from this version are also available.

-- Stephanie Weirich

pi-forall's Issues

Broken due to upstream Unbound changes

Several Unbound imports fail because many modules no longer exist or aren't exposed. I noticed this while trying to run ghci version1/src/Main.hs.

Why there is no content in pi-forall/version1/test/Lec1.pi?

The Lec1.pi in version1 is just the namespace, is it the same as Lec1.pi in version2?

doc: Footnote weirdness

I noticed some footnote weirdness in the rendered .pdf.

The following footnote

\footnote{Note that
  this rule makes our language inconsistent as a logic, as it can encode
  Girard's paradox.}

got cut up and rendered on two different pages:

Broken with parsec 3.1.5

Gives the error

Parser.hs:119:11:
    Could not deduce (MonadTrans (ParsecT s u))
      arising from a use of ‘lift’
    from the context (Monad (ParsecT s u FreshM))
      bound by the instance declaration at Parser.hs:118:10-35
    In the first argument of ‘(.)’, namely ‘lift’
    In the expression: lift . fresh
    In an equation for ‘fresh’: fresh = lift . fresh
Failed, modules loaded: PrettyPrint, Environment, TypeCheck, Syntax, LayoutToken, Equal.

Forcing parsec version 3.1.4 works fine.

Using GHC 7.8.2

Cannot install with Stack with LTS 6.13

$ stack install pi-forall
[...]
--  While building package pi-forall-0.1.1 using:
      /Users/chen/.stack/setup-exe-cache/x86_64-osx/setup-Simple-Cabal-1.22.5.0-ghc-7.10.3 --builddir=.stack-work/dist/x86_64-osx/Cabal-1.22.5.0 build --ghc-options " -ddump-hi -ddump-to-file"
    Process exited with code: ExitFailure 1
    Logs have been written to: /Users/chen/.stack/global-project/.stack-work/logs/pi-forall-0.1.1.log

    Configuring pi-forall-0.1.1...
    Building pi-forall-0.1.1...
    Preprocessing library pi-forall-0.1.1...

    /private/var/folders/xz/z3wrll111zn03hdhkd_pxs5w0000gp/T/stack55559/pi-forall-0.1.1/src/Main.hs:10:8:
        Could not find module ‘Modules’
        Perhaps you meant Module (needs flag -package-key ghc-7.10.3)
        Use -v to see a list of the files searched for.
[...]