the-little-typer/pie

The Pie language, which accompanies The Little Typer by Friedman and Christiansen

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 available on the Racket package server. If you don't plan to make your own changes to Pie, then it is easiest to install it from there.

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.

pie's Issues

Is it possible to create an alias for a higher kind type?

Thanks for The Little Typer and this interesting language!
I want to write something about Leibniz Equality in Pie, so I define it as this:

(claim L-≡ (Π ((A U)) (→ A A U)))
(define L-≡
  (λ (A x y)
    (Π ((P (→ A U))) (Pair (→ (P x) (P y)) (→ (P y) (P x))))))

But it causes an error: "U is a type, but it does not have a type.".
After thinking, I found that it is because (Π ((P (→ A U))) (Pair (→ (P x) (P y)) (→ (P y) (P x)))))) is not a U, for (→ A U) is not a U.
Although the above can't be compiled, the Leibniz Equality could be expressed in Pie. We need a "partial definition":

(claim L-≡p (Π ((A U)) (→ A A (→ A U) U)))
(define L-≡p
  (λ (A x y P)
    (Pair (→ (P x) (P y)) (→ (P y) (P x)))))

Then we have to write (Π ((P (→ A U))) (L-≡p A x y P)) wherever we want to express the "real" (L-≡ A x y).
Is there a way to define L-≡ directly, or is it possible to add some macro syntax in Pie?

better error msg for duplicate definitions

This program

#lang pie

(claim foo Atom)
(define foo 'f)

(define foo TODO)

Currently errors with the error message "No claim: foo ". It seems like it would be much more intuitive to say something like "foo is already defined" or similar.

I'm happy to look into this but don't want to context switch at the moment -- pushing it onto the proverbial stack ;-)

confusing error message on (4)

When I run this program (or many other syntactically invalid programs):

#lang pie

(4)

... I get the error message

?: expected more terms starting with rand
  parsing context: 
   while parsing application in: (4)

I don't understand what 'rand' has to do with this situation. Could this error message be improved?

Thanks!

Useful techniques for sharing the ideas about type system implementation.

Recently reading the book "Design Patterns" by Erich Gamma, Richard Helm, Ralph Johnson and John Vlissides.
And thinking about your teaching of NbE in davidchristiansen.dk/tutorials/nbe.
I found that in their terms, the following ideas about type system implementation,
can be called "application specific design pattern" (where our "specific application domain" is type system):

• Closure (for lexical scope)
• Bidirectional type checking (reading inference rule as type checking algorithm)
• Normalization by evaluation
• Elaboration during type checking (clear separation of roles)
• And many others...

And beside this mere "calling", their also provide a very systemic way for sharing these ideas
(which is better acquired by reading the book).

Maybe we can borrow some of their techniques to sharing those very very valuable ideas about type system implementation.

bug when duplicate arg names present

This definition of pair is accepted when it should error (i.e. in terms of the Π's identifiers, we are supposed to provide a function which returns a (Pair A D), we instead return a (Pair D D) and pie doesn't complain):

#lang pie
(claim pair (Π ([A U]
                [D U])
              (-> A D (Pair A D))))
(define pair
  (λ (_ _ a d)
    (cons d d)))

This seems to be an incorrect handling of shadowing while type checking a λ. Here is a equivalent definition of pair that may help illustrate:

(define pair (λ (X)
               (λ (X)
                 (λ (a)
                   (λ (d)
                     (cons d d))))))

With this definition accepted, usages of pair lead to internal errors, e.g.:

(pair Nat Atom 42 'batman)

produces the error:

...pkgs/pie/normalize.rkt:458:2: match*: no matching clause for (list 'NAT (QUOTE 'batman))

But perhaps this latter error is just an artifact of things already being cattywampus and it isn't a "separate issue".

Let construct

It'd be really, really nice to have access to let and let-values.

neutral inductive form printing incorrect

pie/pretty.rkt

Line 154 in 28fe6d4

(vsep print-pie targets)))]

Targets of induction are printed at the tail end of the s-expression instead of at the head.

I played around with a potential fix but it seemed like there might be some creative decision making that @david-christiansen would be better suited to address (i.e. if there are two targets, are they printed on the same line as the induction form? If so... what if they span multiple lines (i.e. because they are large neutral terms as well)... etc)

Error messages should not mention Sigma and Pi

Trying to take the car of a Nat or trying to apply an Atom as a function leads to error messages that readers of the book may not understand before they've gotten a few chapters in. It would be better if it said "not a pair type:" and "not a function type: ".

doc entry for cong has a typo

(= X (fun from) (fun to)) should read (= Y (fun from) (fun to)) in the docs for cong.

Package "pie" has invalid version

I just migrated from 8.7 to 8.10, and when running raco setup, noticed the following:

raco setup: --- checking package dependencies ---                  [13:18:06]
raco setup: invalid package version declaration:
raco setup:   package: "pie"
raco setup:   declared version: "0.01"
raco setup: --- summary of package problems ---                    [13:18:29]
raco setup: package has invalid version:
raco setup:   package: "pie"
raco setup:   version: "0.01"

Add "Recursion is not an option." in error message, when recursive definition is detected.

It would be so fun.

An unbounded variable is not reported

I want to simulate the Sigma type by hand:

#lang pie

(claim my-cons (Π ((A U)
                   (B (→ A U))
                   (x A)(y (B x))
                   (E U)
                   (f (Π ((x A)) (→ (B x) E))))
                 E))
(define my-cons (λ (A B x y) (λ (E f) (f x y))))

(claim my-car (Π ((A U)
                  (B (→ A U))
                  (p (Π ((E U)(f (→ A (B x) E))) E)))
                A))
(define my-car (λ (A B p) (p A (λ (a b) a))))

(claim my-car1 (Π ((A U)
                   (B (→ A U))
                   (p (Π ((E U)(f (Π ((x A)) (→ (B x) E)))) E)))
                 A))
(define my-car1 (λ (A B p) (p A (λ (a b) a))))

On line 13 in the definition of my-car the variable x is unbounded, but the pie type checker did not report anything.

the right definition should be my-car1.

Binding arrows for Absurd don't work

Every other keyword shows the #lang as the binding site, but Absurd does not.

No evaluator for [Absurd]

#lang pie

(claim Fin
  (-> Nat U))
(define Fin
  (λ (n)
    (rec-Nat n
      Absurd
      (λ (k Fin-k)
        (Either Trivial Fin-k)))))


(claim really-only-2-values
  (Π ([x (Fin 2)])
    (Either (= (Fin 2) x (left sole))
            (= (Fin 2) x (right (left sole))))))
(define really-only-2-values
  (λ (x)
    (ind-Either x
      (λ (?) (Either
               (= (Fin 2) ? (left sole))
               (= (Fin 2) ? (right (left sole)))))
      (λ (l-val)
        (left (same (left l-val))))
      (λ (r-val)
        (right
          (ind-Either r-val
            (λ (?) (= (Fin 2)
                     (right ?)
                     (right (left sole))))
            TODO
            TODO))))))

Produces the following error: .../6.12/pkgs/pie/normalize.rkt:22:0: No evaluator for (the Absurd x₁)

After completing the proof (i.e. filling in the TODOs with programs that type check) the error goes away, so it's probably a bug specific to partially complete proofs.

Can look into it more later --- posting for now before I forget =)

Start the GUI?

Is the GUI you've used in your different presentations available somewhere? I see that there is a gui folder in this repo but I can't seem to start it. Fairly new to racket.

Interestingly, I did raco pkg install pie and I do see some dependencies named containing the word gui but can't seem to start it.

Thank you.

Output from TODO should be updated to match the book exactly

Right now, Pie produces a listing for the TODO form that does not match the book character-for-character, even though the information is the same. This should be updated.

Super-simple doc typo (#10 redux)

Looks like #10 addressed the type given in the header, but not the type listed in the explanation.

Specifically:

The cong documentation states that cong returns a

(= Y (fun from) (fun to))

I believe this is correct. The last line of the explanation, though, says

"then (cong target fun) is an
(= X (fun from) (fun to))”

I believe this should instead read

"then (cong target fun) is an
(= Y (fun from) (fun to))”

(note the replacement of X with Y).

Thanks!

John

ind-= typo

There's a little typo in the ind-= helper function for val-of:

When the target isn't a neutral term, the base is given to do-ap, instead of the motive.

The following change should fix it:

(: do-ind-= (->  Value Value Value Value))
(define (do-ind-= tgt-v motive-v base-v)
  (match tgt-v
    #;[(SAME v) (do-ap (do-ap base-v v) (SAME v))]
    [(SAME v) base-v]
    [(NEU (EQUAL A from to) ne)
     (NEU (do-ap (do-ap motive-v to) tgt-v)
          (N-ind-= ne
                   (THE (Π-type ((to A)
                                 (p (EQUAL A from to)))
                                'UNIVERSE)
                        motive-v)
                   (THE (do-ap (do-ap motive-v from)
                               (SAME from))
                        base-v)))]))

error defining vs directly using a Pi type

I understand that Pie has a trivial universe heirarchy... but I was surprised that simply whether or not I used a variable vs the expression that variable was defined to be affected whether or not Pie accepted the program.

i.e. in the code at the bottom of this issue, this snippet works without issue:

(claim dblneg->pem-works
  (-> (Π ([P U])
        (-> (Not (Not P)) P))
    (Π ([P U])
      (Either P (Not P)))))

but this snippet does not:

(claim dblneg->pem-works
  (-> (Π ([P U])
        (-> (Not (Not P)) P))
    (Π ([P U])
      (Either P (Not P)))))

even though the two are the same (modulo defines/names).

Here's the full example:

#lang pie

(claim Not (-> U U))
(define Not
  (λ (P) (-> P Absurd)))

(claim dblneg
  (Π ([P U])
    (-> (Not (Not P)) P)))
(define dblneg TODO)

(claim pem
  (Π ([P U])
    (Either P (Not P))))
(define pem TODO)

; this should work, right?
(claim dblneg->pem-broken
  (-> dblneg pem))
; currently it just errors with the following message:
; Expected U but given
;   (Π ((P U))
;    (→ (→ (→ P
;              Absurd)
;          Absurd)
;      P))

(claim dblneg->pem-works
  (-> (Π ([P U])
        (-> (Not (Not P)) P))
    (Π ([P U])
      (Either P (Not P)))))

Will it be better to elaborate `rec-List` to `ind-List`?

By doing so, we can check that some application of rec-List is equal to some application of ind-List.

(And similar is true for rec-Nat and ind-Nat, and friends...)

A proposal for correcting the incorrect `concat`

We know that:

at page 124, In frame 61, the definition of concat is incorrect. It reverses its second argument.

If there will be a second edition.
I suggest the following proposal for correcting the incorrect concat:

• define snoc -- reuse step-append
• define reverses
• define concat -- use reverses and reuse step-reverses

This also teaches something about reusing step-functions in recursive combinators.

;; reusing `step-append`
(claim snoc
  (Pi ([E U])
    (-> (List E) E
      (List E))))
(define snoc
  (lambda (E es e)
    (rec-List es
      (:: e nil)
      (step-append E))))

;; test `snoc`
(check-same (List Nat)
  (snoc Nat (:: 1 (:: 2 nil)) 3)
  (:: 1 (:: 2 (:: 3 nil))))

(claim step-reverse
  (Pi ([E U])
    (-> E (List E) (List E) 
      (List E))))
(define step-reverse 
  (lambda (E e es almost)
    (snoc E almost e)))

(claim reverse 
  (Pi ([E U])
    (-> (List E)
      (List E))))
(define reverse
  (lambda (E x)
    (rec-List x
      (the (List E) nil)
      (step-reverse E))))

;; test `reverse`
(check-same (List Nat)
  (reverse Nat (:: 1 (:: 2 (:: 3 (:: 4 nil)))))
  (:: 4 (:: 3 (:: 2 (:: 1 nil)))))

;; reusing `step-reverse`
(claim concat 
  (Pi ([E U])
    (-> (List E) (List E)
      (List E))))
(define concat
  (lambda (E x y)
    (rec-List (reverse E y)
      x (step-reverse E))))

;; test `concat`
(check-same (List Nat)
  (concat Nat (:: 1 (:: 2 nil)) (:: 3 (:: 4 nil)))
  (:: 1 (:: 2 (:: 3 (:: 4 nil)))))

trans/vector/read-back bug

An internal match error is produced by the pie program at the bottom of this message. It produces the following error message:

.../pie/normalize.rkt:458:2: match*: no matching clause for (list (VEC (NEU 'UNIVERSE (N-var 'Y)) (NEU 'NAT (N-iter-Nat (N-var 'n) (THE 'NAT (NEU 'NAT (N-var 'k))) (THE (PI 'n 'NAT (HO-CLOS #<procedure:...ie/normalize.rkt:18:29>)) (LAM 'x (FO-CLOS '() 'x '(add1 x))))))) (VEC:: (NEU (NEU 'UNIVERSE (N-var 'Y...

i.e. it looks like it is trying to read-back a vec:: whose type is (Vec Y blah) where blah is a neutral Nat.

The error is caused by the trans clause in the body of the inductive case in foo.

The error message goes away if trans is not used (i.e. just use the cong since the first equality in the trans is a same), or if the annotation on the first argument to trans is omitted (but I tested separately and the annotation itself seems fine/valid -- so it appears to be is some combination of the two from what I've observed).

Sorry the example isn't smaller. I tried a few but failed to recreate the error and decided to at least post a summary and what I had so far.

#lang pie

(claim succ (-> Nat Nat))
(define succ (λ (x) (add1 x)))

(claim + (-> Nat Nat Nat))
(define + (λ (x y) (iter-Nat x y succ)))

(claim * (-> Nat Nat Nat))
(define * (λ (x y) (iter-Nat x 0 (+ y))))


(claim bar
  (Π ([E U]
      [n Nat]
      [m Nat])
    (-> (Vec E n) (Vec E m)
      (Vec E (+ n m)))))
(define bar
  (λ (E n m xs ys)
    (ind-Vec n xs
      (λ (z v) (Vec E (+ z m)))
      ys
      (λ (k h t q)
        (vec:: h q)))))


(claim baz
  (Π ((A U)
      (B U)
      [n Nat])
    (-> (-> A B)
        (Vec A n)
      (Vec B n))))
(define baz
  (λ (A B n f v)
    (ind-Vec n v
      (λ (n v) (Vec B n))
      vecnil
      (λ (? x _ qwerty)
        (vec:: (f x) qwerty)))))



(claim foo
  (Π ((X U)
      (Y U)
      (f (-> X Y))
      (j Nat)
      (k Nat)
      (fred (Vec X j))
      (wilma (Vec X k)))
    (= (Vec Y (+ j k))
       (bar Y j k (baz X Y j f fred) (baz X Y k f wilma))
       (baz X Y (+ j k) f (bar X j k fred wilma)))))
(define foo
  (λ (X Y f j k fred wilma)
    (ind-Vec j fred
      (λ (j fred) (= (Vec Y (+ j k))
                     (bar Y j k (baz X Y j f fred) (baz X Y k f wilma))
                     (baz X Y (+ j k) f (bar X j k fred wilma))))
      (same (baz X Y k f wilma))
      (λ (n x xs IH)
        (trans (the (= (Vec Y (add1 (+ n k)))
                      (bar Y (add1 n) k (baz X Y (add1 n) f (vec:: x xs)) (baz X Y k f wilma))
                      (vec:: (f x) (bar Y n k (baz X Y n f xs) (baz X Y k f wilma))))
                 (same (vec:: (f x) (bar Y n k (baz X Y n f xs) (baz X Y k f wilma)))))
          (cong IH (the (-> (Vec Y (+ n k))
                          (Vec Y (add1 (+ n k))))
                     (λ (?) (vec:: (f x) ?)))))))))

do-ap error in normalize.rkt

The following program in DrRacket v6.11

#lang pie

(claim inc (-> Nat Nat))
(define inc (λ (n) (add1 n)))
(claim plus (-> Nat Nat Nat))
(define plus (λ (n j) (iter-Nat n j inc)))

(check-same Nat (plus zero zero) zero)
(check-same Nat (plus 1 2) 3)
(check-same Nat (plus 40 2) 42)

(claim mult (-> Nat (-> Nat Nat)))
(define mult (λ (n) (iter-Nat n
                      (the (-> Nat Nat) (λ (m) zero))
                      (λ (times-n-1)
                        (λ (m) (plus m (times-n-1 m)))))))

(check-same Nat (mult zero zero) zero)
(check-same Nat (mult 1 0) 0)
(check-same Nat (mult 40 2) 80)

produces the error:

Repos/plt/6.11/add-on/6.11/pkgs/pie/normalize.rkt:23:2: match: no matching clause for (NEU 'NAT (N-var 'times-n-1))

which points here.

Don't have time to look into it today -- tomorrow I'll give it a look if no one has tackled it yet.

ind-Nat not strictly more powerful than iter-Nat?

While re-implementing Pie I avoided unnecessary eliminators and added them as Pie definitions instead. Because of that I tried to implement Fin using ind-Nat, but failed, because "U is a type, but it does not have a type."

(claim Maybe (-> U U))
(define Maybe (lambda (X) (Either X Trivial)))

(claim Fin (-> Nat U))
;(define Fin (lambda (n) (iter-Nat n Absurd Maybe)))
(define Fin (lambda (n) (ind-Nat
                          n
                          (lambda (k) U)
                          Absurd
                          (lambda (smaller acc) (Maybe acc)))))

As far as I understand, Fin cannot be implemented with ind-Nat because of this. Is this intentional? Am I missing something?

PS:
Of course I couldn't implement it with my version of iter-Nat either, because I had to provide a type again:

(claim iter-Nat2 (Pi ((X U)) (-> Nat X (-> X X) X)))
(define iter-Nat2 (lambda (X target base step)
                    (ind-Nat
                      target
                      (lambda (n) X)
                      base
                      (lambda (smaller acc) (step acc)))))
(define Fin (lambda (n) (iter-Nat2 U n Absurd Maybe)))

Reader is too liberal

Our re-use of the Racket reader leads to this implementation accepting programs that the book implies should be rejected. Here are examples from an email that I received:

1. Pipe-Delimited Atoms

In the textbook, an Atom is supposedly an apostrophe followed by one or more letters or hyphens. However, in the current version of Pie you can also use pipes.
Example code:

(check-same Atom '|sam| 'sam)
(check-same Atom '|s||a||m| 'sam)
(check-same Atom '|||s|am 'sam)
(check-same Atom '|| '||||||)

2. Spaces in Atoms

I don't think this matters as much, but a space is not a letter or hyphen, so I might as well mention it. Also, this messes with the syntax highlighting.
Example code:

(check-same Atom '    abc 'abc)
(check-same Atom '      abc '  abc)

3. Number Oddities

I doubt anyone would ever stumble upon this unless they've already programmed in Racket. Also, I don't think any of these even need changing. Anyway, here's the example code:

(check-same Nat -0 0)
(check-same Nat 0/3 0)
(check-same Nat -0/3 0)
(check-same Nat 12/4 3)
(check-same Nat #e5 5)
(check-same Nat 2+0i 2)
(check-same Nat #x10 16)

+, which nat etc not available?

I'm trying to work through the little typer, but for some reason +, which nat etc are not defined when I do racket -I pie. Is this intentional? Thank you.

Is it safe to let `synth` return `Value` (for type) and `Core` (for exp) instead of `Core` and `Core`?

By doing so, we can avoid some repeated readback and evaluate in synth.

Bug with cons?

I see a lot of examples using cons, car and cdr. One example is in chapter 6:

(Vec
  (cdr
    (cons 'pie
      (List (cdr (cons Atom Nat)))))
  (+ 2 1))

According to frame 9 of chapter 6, this should result in

(Vec (List Nat) 3)

However, when I try it, I get:

Can't determine a type

Is this normal? Every use of these functions yield the same result. In a previous chapter, I had to define

(claim cons-atom
  (-> Atom Atom
    (Pair Atom Atom)))
(define cons-atom
  (lambda (a d)
    (cons a d)))

To be able to cons Atoms together. I tried to define:

(claim my-cons
  (Pi ((A U)
       (D U))
    (-> A D
        (Pair A D))))
(define my-cons
  (lambda (A D)
    (lambda (a d)
      (cons a d))))

And while this works for some cases:

> (my-cons Nat Atom 3 'atom)
(the (Pair Nat Atom)
  (cons 3 'atom))

It fails for some cases, which might be explainable because I don't fully master everything from the book yet.

> (my-cons U U Atom Nat)
. . interactions from an unsaved editor:21:11:  U is a type, but it does not have a type.

What is happening here? Why so many uses of these functions in examples if I seem unable to use them?

By the way, great book 👍

Is this book going to have a free online version?

Syntax highlighting for vim

Its very rough and quickly whopped together, but this vim plugin makes it nice to work with pie.
I'd be happy to hand this over to the-little-typer if you want to take it further than I can.

https://github.com/felipesere/pie-highlight.vim

Here is a screenshot with my vim them:

documenting check/synth of forms

In a previous discussion with @david-christiansen and @dfried00 there was a desire to have the documentation indicate which positions are visited in check-mode and which are visited in synthesis-mode by the type checker.

Would superscript "c" (for check) and "s" (for synthesis) on identifier names (with a comment at the top of the docs indicating their meaning) be a reasonable solution? e.g.: