A proposal for correcting the incorrect `concat`

[xieyuheng]

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)))))

[david-christiansen]

Thanks for the proposal!

We have already sent in a fixed version, so it should be corrected in the latest reprinting, though I haven't gotten it in my hands to see yet.

I'd like to keep this repository about this implementation of the Pie language, rather than about the book generally, and I'd like to keep this bug database about bugs in this implementation of Pie rather than discussions of the book, so I'm closing this issue.

Thanks again for the careful reading.