Lisp

動機 state monad是left 2 right，對應到iteration (左遞迴) reverse state monad是right 2 left，對應到recursion (右遞迴) ...

動機 興趣 ...

動機 整理continuation與CPS轉換 ...

動機 久遠筆記搬到github這裡，不過也是改寫超多東西的 ...

來證明啦 ch8 & ch9 & ch10 & ch11 現在說用type證明，但實際上怎麼做? 在claim寫下想證的東西，在define證出來 incr & + (claim incr (-> Nat Nat)) (define incr (λ (n) (iter-Nat n 1 (+ 1)))) (claim + (-> Nat Nat Nat)) (define + (λ (a b) (iter-Nat a b (λ (ret) (add1 ret))))) +1=add1 證對於任何整數，add1等於+1 (claim +1=add1 (Pi ((n Nat)) (= Nat (+ 1 n) (add1 n)))) 所以我們需要一個value的type是(= Nat (+ 1 n) (add1 n))) 先把1帶入+中，會發現根本就是(add1 n) 也就是兩邊都一樣，same!! (define +1=add1 (λ (n) (same (+ 1 n)))) incr=add1 同樣的來試試incr=add1...

介紹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...

前言 The Seasoned Schemer(TSS)的目的是補完TLS中沒有提及的狀態。 這篇筆記同樣不依照章節順序，用主題式的方式，把我心中的這本書呈現出來。 行前須知 知道什麼是? Scheme 遞迴 accumulator parameter reverse 如果要反轉list，在有append情況下可以寫成 (define (rev l) (if (null? l) '() (append (rev (cdr l)) (cons (car l) '())))) 但我們需要一直append嗎? 如果我們可以從第一個開始就先cons出來的東西，不就是我們要的。 (define (rev l acc) (if (null? l) acc (rev (cdr l) (cons (car l) acc)))) 引入acc可以記下我們從頭到目前看過的東西。 flatten 同樣在要攤平list時，如果有append可寫成 (define (atom? x) (and (not (pair? x)) (not (null? x)))) (define (fl lol) (cond [(null? lol) '()] [(atom? (car lol)) (cons (car lol) (fl (cdr lol)))] [else (append (fl (car lol)) (fl (cdr lol)))])) 這裡是不是可以利用剛剛acc可以記下目前看過的東西的特性來改寫呢?...

前言 The Little Schemer(TLS)的目的是教讀者寫遞迴。 這篇筆記不依照章節順序，用主題式的方式，把我心中的這本書呈現出來。 行前須知 知道什麼是? base 與 inductive case 在歸納法中大概的意思 快速Scheme Tutorial 調用: (<function-or-operator) <args...>) 宣告變數: (define <var-name> <value>) 條件式: (if <predicate> <when-true> <when-false>) (cond [<predicate> <do-somthing>] ... [else <do-somthing>]) 函數: (define <func-name> (lambda (<args...>) <do-somthing>)) ;; OR (define (<func-name> (<args...>)) <do-somthing>) 匿名函數: (lambda (<args...>) <do-somthing>) 本書用到的資料結構介紹 Atom <line-of-characters>還有數字 List of OO 有哪些可能性(case) base case: 空 inductive case: 有東西 建構 空 的case : ‘() 有東西 的case : cons 分解 有東西 的case : car 與 cdr 對應到cons有兩個參數，所以會有兩個解構子。 區分case 空 的case : null?...