Reading

動機 這已經雪藏很久了，久在github page還沒用到之前就在我的google docs中 整理一下貼出來 ...

動機 不記實際上怎麼跑與跑了什麼，只記設計與方便未來查詢的部分 畢竟這是基於linux2.6的 ...

動機 偶然找到Green Threads Explained很讚，做點筆記 ...

動機 都買了就讀一下 ...

動機 翻翻The Pragmatic Programmer 20週年紀念版的一些紀錄我感覺很重要的部分 ...

ch0: 執行環境 想用wsl來跑sml的話，poly/ml是不錯的選項 ch1: 定義type datatype num = ZERO | ONE_MORE of num datatype ‘a Slist = NIL of ‘a | SCONS of ‘a Slist ch2: 寫function datatype Abc = A | B of Abc | C of Abc fun only_B(A) = true | only_B(B(x)) = only_B(x) | only_B(C(x)) = false (only_B : Abc -> bool) datatype ‘a Xyz = X of ‘a | Y of ‘a Xyz | Z of ‘a Xyz fun is_xy(X(x)) = true | is_xy(Y(x)) = is_xy(x) | is_xy(Z(x)) = false (is_xy : ‘a Xyz -> bool) ch3: 在list上遞迴 fun rem_B(A) = A | rem_B(B(x)) = rem_B(x) | rem_B(C(x)) = C(rem_B(x)) fun C_in_fron_of_B(A) = A | C_in_fron_of_B(B(x)) = C(B(C_in_fron_of_B(x))) | C_in_fron_of_B(C(x)) = C(C_in_fron_of_B(x)) fun subst_B_C(x) = rem_B(C_in_fron_of_B(x)) (* OR *) fun subst_B_C(A) = A | subst_B_C(B(x)) = C(subst_B_C(x)) | subst_B_C(C(x)) = C(subst_B_C(x)) (* 都是走訪同一list故可以用同一種走訪，把兩個式子結合起來(map fusion) *) ch4: tuple & 多參數function (A,X,A) :: (Abc * Xyz * Abc) datatype Abc = A | B | C fun add_a(A) = (A,A) | add_a(B) = (B,A) | add_a = (C,A) (add_a : Abc -> (Abc * Abc)) 可以利用type variable來打少一點字...

來證明啦 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...

Ch1 Zero to “It Works!” Gem的檔案結構 $ bundle gem rulers create rulers/Gemfile create rulers/Rakefile create rulers/LICENSE.txt create rulers/README.md create rulers/.gitignore create rulers/rulers.gemspec # !! create rulers/lib/rulers.rb # !! create rulers/lib/rulers/version.rb Initializating git repo in src/rulers rulers/rulers.gemspec放的是gem的資訊與dependency rulers/lib/rulers.rb就是主程式 dependency分成development與runtime # rulers.gemspec gem.add_development_dependency "rspec" gem.add_runtime_dependency "rest-client" rack進入點 與 rack app回傳值的資料結構 # best_quotes/config.ru run proc { [200, {'Content-Type' => 'text/html'}, ["Hello, world!"]] } 狀態值,header,資料 rack app 的 interface # rulers/lib/rulers.rb require "rulers/version" module Rulers class Application def call(env) [200, {'Content-Type' => 'text/html'}, ["Hello from Ruby on Rulers!...

前言 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可以記下目前看過的東西的特性來改寫呢?...