介紹Pie怎麼用

ch1 & ch2 & ch3

  • 所有東西都是expression
    • 有人斷言expression有某種屬性或與其他expression有共通的特質是judgment
      • Sentences get their meaning from those who understand them.
      • The sentences capture thoughts that we have, and thoughts are more important than the words we use to express them.
    • 描述某一群expression的expression是Type
      • 當type constructor在頂部就是type (Pair Nat Nat)
    • constructor在頂部就是Value
      • constructor會產生某個type的實體(像add1會產生Nat的實體，8也是Nat的實體)
      • eliminator會分解value取出構成value的資訊
    • 當某一expression無法再被改寫時叫normal form
      • 改寫expression叫evaluation
    • expression因為有變數而無法繼續改寫叫neutral
  • 只要長的一樣就是same (不是等於，之後會用same去證等於)
  • total function對任何一個值都能產生對應的值
  • 沒有遞迴
    • 因為每個expression都一定要收斂
    • 所以有其他東西來做類似的效果

evaluation & value

在dependent type中，evaluation得到的是expression 在一般PL(像lisp)中，evaluation得到的是value 在一般PL中，expression與value是不同類別的東西

ch4 & ch5

claim & define

在pie中要產生一個變數要先claim再define

(claim one
    Nat)
(define one
    (add1 0))

函數的部分用(-> arg1 arg2 ... ret)宣告 函數或是需要type作為參數用(Pi ((arg1 type1) (arg2 type2) ...)) ...)宣告

len

;; 原本
(define (len l)
  (if (null? l)
      0
      (add1 (len (cdr l)))))

;; now
(claim len
  (Pi ((T U)) ;; U是Universe，意指所有的type(但不包含自己)
    (-> (List T) Nat)))
(define len
  (λ (T l) ;; Pie的lambda會自己curry
    (rec-List l
      0
      (λ (car_L cdr_L ret) ;; rec-{type}會把做遞迴的參數分解，以及把ret塞回來，可以想成backtrace的部分
        (add1 ret)))))

還有其他老朋友，但就先跳過

ch6 & ch7

vector與list很像，但有長度在type中

first

(claim first
  (Pi ((T U)
       (n Nat))
    (-> (Vec T n) T)))

(define first
  (λ (T n v)
    (head v)))

這個傳空的就會出事

可以改宣告，限制只吃只少有一個的vec

(claim first
  (Pi ((T U)
       (n Nat))
    (-> (Vec T (add1 n)) T)))
  
(define first
  (λ (T n v)
    (head v)))

last

原本rec-List或rec-Nat都是回傳type不變的值，但現在vec有長度，所以會變!!

對此我們要ind-Nat，意思是對整數做歸納法 ind-Nat多了一個東西是motive，函數，會吃一個正在做歸納法的值，回傳應該有的type

而motive也於ind-Nat其他部位有關係

(claim last
  (Pi ((T U)
       (n Nat))
    (-> (Vec T (add1 n)) T)))
  
(define last
  (λ (T n v)
    (ind-Nat n
      (λ (x) (-> (Vec T (add1 x)) T))
      (λ (v1) (head v1))
      (λ (n-1 ret) ;; 有沒有覺得與rec-Nat有點像
        (λ (v)
          (ret (tail v)))))))

(claim last-motive
  (-> U Nat U))
(define last-motive
  (λ (T)
    (λ (n)
      (-> (Vec T (add1 x)) T)))) ;; 把last的Pi的參數拿掉剩下就是我們要的

(claim last-base
  (Pi ((T U))
    (last-motive T 1))) ;; 原本應該是0，但已經限制要大於1
(claim last-step
  (Pi ((T U)
       (n Nat))
    (-> (last-motive T n) ;; 吃舊的值(n-1,或是叫他回傳值)
        (last-motive T (add1 n))))) ;; 丟新的值

(define last-base
  (λ (T v)
    (head v)))

(define last-step
  (λ (T)
    (λ (n-1 ret)
      (λ (v)
        (ret (tail v))))))

(define last
  (λ (T v)
    (ind-Nat v
      (last-motive T)
      (last-base T)
      (last-step T))))

到這裡基本的Pie已經說完了，剛剛last有寫兩個版本，重要的是理解ind-Nat的motive與motive是怎麼與其他ind-Nat的部位有關係的