The Little Typer: Exercises for Chapters 4 and 5

list-elimination.rkt

#lang pie

;; Exercises on Pi types and using the List elimiator from Chapters 4 and 5
;; of The Little Typer
;;
;; Some exercises are adapted from assignments at Indiana University

(claim elim-Pair
  (Π ((A U)
      (D U)
      (X U))
     (-> (Pair A D) (→ A D X) X)))
(define elim-Pair
  (lambda (A D X)
    (lambda (p f)
      (f (car p) (cdr p)))))

;; Exercise 4.1
;;
;; Extend the definitions of kar and kdr (frame 4.42) so they work with arbirary
;; Pairs (instead of just for Pair Nat Nat).
(claim kar
  (Π ((A U)
      (D U))
     (→ (Pair A D)
        A)))
(define kar
  (lambda (A D)
    (lambda (p)
      (elim-Pair
       A D
       A
       p
       (lambda (a d)
         a)))))
(check-same Nat
  (kar Nat Nat (cons 1 2))
  1)
(check-same Nat
  (kar Nat Nat (cons 2 1))
  2)

;; Exercise 4.2
;;
;; Define a function called compose that takes (in addition to the type
;; arguments A, B, C) an argument of type (-> A B) and an argument of
;; type (-> B C) that and evaluates to a value of type (-> A C), the function
;; composition of the arguments.

;; compose :: (b -> c) -> (a -> b) -> (a -> c)
(claim compose
  (Π ((A U) (B U) (C U))
     (→ (→ B C) (→ A B) (→ A C))))
(define compose
  (lambda (A B C)
    (lambda (f g)
      (lambda (p)
        (f (g p))))))

(check-same (-> (Pair (Pair Atom Nat) Nat) Atom)
  (lambda (p) (car (car p)))
  (compose (Pair (Pair Atom Nat) Nat)
           (Pair Atom Nat)
           Atom
           (lambda (p) (car p))
           (lambda (p) (car p))))


;; Exercise 5.1
;;
;; Define a function called sum-List that takes one List Nat argument and
;; evaluates to a Nat, the sum of the Nats in the list.

;;; import +
(claim + (-> Nat Nat Nat)) (define + (lambda (n m) (rec-Nat n m (lambda (n-1 h) (add1 h)))))

;; (rec-List target
;;  base
;;  step)

(claim sum-List
  (-> (List Nat) Nat))

(define sum-List
  (lambda (lon)
    (rec-List lon
      0
      (lambda (e es h)
        (+ e h)))))

(check-same Nat
  (sum-List (:: 3 (:: 2 (:: 1 nil))))
  6)

;; Exercise 5.2
;;
;; Define a function called maybe-last which takes (in addition to the type
;; argument for the list element) one (List E) argument and one E argument and
;; evaluates to an E with value of either the last element in the list, or the
;; value of the second argument if the list is empty.

(claim maybe-last
  (Π ((E U))
     (-> (List E) E E)))
(define maybe-last
  (lambda (E)
    (lambda (es)
      (rec-List es
        (the (-> E E) (lambda (default) default))
        (lambda (e _ maybe-last/default)
          (lambda (_) (maybe-last/default e)))))))

(check-same Atom
  (maybe-last Atom nil 'default)
  'default)
(check-same Atom
  (maybe-last Atom (:: 'hello (:: 'world nil)) 'default)
  'world)
(check-same Nat
  (maybe-last Nat (:: 1 (:: 2 nil)) 42)
  2)


;; Exercise 5.3
;;
;; Define a function called filter-list which takes (in addition to the type
;; argument for the list element) one (-> E Nat) argument representing a
;; predicate and one (List E) argument.
;;
;; The function evaluates to a (List E) consisting of elements from the list
;; argument where the predicate is true.
;;
;; Consider the predicate to be false for an element if it evaluates to zero,
;; and true otherwise.

(claim if0
  (Pi ((X U))
      (-> Nat X X X)))
(define if0
  (lambda (X)
    (lambda (test then else)
      (which-Nat test
                 else
                 (lambda (_) then)))))

(claim filter-List
  (Pi ((E U))
      (-> (-> E Nat) (List E) (List E))))
;; use. (filter-List >2 (list 2 3 1 5)) => (list 3 5)
(define filter-List
  (lambda (E)
    (lambda (pred es)
      (rec-List es
        (the (List E) nil)
        (lambda (e _ h)
          (if0 (List E) (pred e)
            (:: e h)
            h))))))


;; import >
(claim > (-> Nat (-> Nat Nat)))
(define > (lambda (n) (rec-Nat n (the (-> Nat Nat) (lambda (m) 0)) (lambda (n-1 n-1>) (lambda (m) (rec-Nat m 1 (lambda (m-1 _) (n-1> m-1))))))))

(check-same (List Nat)
  (filter-List Nat (lambda (n) (> n 2))
               (:: 2 (:: 3 (:: 1 (:: 5 nil)))))
  (:: 3 (:: 5 nil)))

;; Exercise 5.4
;;
;; Define a function called sort-List-Nat which takes one (List Nat) argument
;; and evaluates to a (List Nat) consisting of the elements from the list
;; argument sorted in ascending order.

;; insert :: a -> [a] -> [a]
;; insert [] = \x -> [x]
;; insert (y:xs) = \x -> | x > y     = y : insert xs x
;;                       | otherwise = x : y : xs

(claim insert-Nat (-> (List Nat) Nat (List Nat)))
(define insert-Nat
  (lambda (es)
    (rec-List es
      (the (-> Nat (List Nat)) (lambda (e) (:: e nil)))
      (lambda (e es ins/h)
        (lambda (e0)
          (if0 (List Nat) (> e0 e)
            (:: e (ins/h e0))
            (:: e0 (:: e es))))))))

(claim sort-List-Nat
  (-> (List Nat) (List Nat)))
(define sort-List-Nat
  (lambda (es)
    (rec-List es
      (the (List Nat) nil)
      (lambda (e _ h)
        (insert-Nat h e)))))

(check-same (List Nat)
  (sort-List-Nat (:: 2 (:: 3 (:: 1 nil))))
  (:: 1 (:: 2 (:: 3 nil))))
(check-same (List Nat)
  (sort-List-Nat (:: 1 (:: 2 (:: 3 nil))))
  (:: 1 (:: 2 (:: 3 nil))))
(check-same (List Nat)
  (sort-List-Nat (:: 3 (:: 2 (:: 1 nil))))
  (:: 1 (:: 2 (:: 3 nil))))