Bug with cons?

[FrankBro]

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 👍

[david-christiansen]

I'm happy you like the book!

Sometimes, Pie needs some help with determining the type of an expression. You can provide this help with the, which is described in the Recess beginning on page 62.

Here's an example:

#lang pie

(claim +
  (-> Nat Nat
    Nat))
(define +
  (lambda (j k)
    (iter-Nat j k (lambda (x) (add1 x)))))

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

We didn't include all the the-hints in the text because it would cause the code to grow too large.

Your second issue, where Pie says "U is a type, but it does not have a type.", is because U is not described by U. Your function my-cons expects something of type U in its first two arguments, but U doesn't have any type at all.

[FrankBro]

I see. Using the indeed fixes all of my problems. Thanks for the quick response.