PLT 板


LINE

看板 PLT  RSS
因為有人提到,所以複習了一下.. 1. Y combinator in Haskell Y combinator 在 untyped lambda calculus 中是 \f -> (\x -> f (x x)) (\x -> f (x x)) 試著寫成 Haskell: y :: (a -> a) -> a y f = (\x -> f (x x)) (\x -> f (x x)) f 的型別是 a -> a, 而 y 取 f 的 fixed-point, 所以 y 的型別是 (a -> a) -> a. 但是這個型別一看就有問題:把 type 看成邏輯的話, 這個 type 若有證明就會有 inconsistency. 果然, Haskell 不讓這個程式 typecheck: Occurs check: cannot construct the infinite type: t = t -> a Probable cause: `x' is applied to too many arguments In the first argument of `f', namely `(x x)' In the expression: f (x x) 操作上的理由是:在 (x x) 之中,x 的型別又是 t -> a, 又是 t, 而 t = t -> a 遞迴定義。 解決方法也很簡單,就頭痛醫頭腳痛醫腳,做一個 t 與 t -> a 同構的遞迴型別囉。 data Fix a = Rec (Fix a -> a) -- Fix a 和 Fix a -> a 同構 有了 Fix 就可以寫 Y combinator 了。 y :: (a -> a) -> a y f = (\(Rec x) -> f (x (Rec x))) (Rec (\(Rec x) -> f (x (Rec x)))) 和前一個版本比較,這裡多了很多 Rec,其實是在告訴 typechecker 何時要把 Fix 展開。 2. 用 Y 定義遞迴函數 假設 Haskell 不允許遞迴定義(正確地說,允許遞迴資料型別,但 不允許遞迴的 term),那要怎麼寫遞迴函數呢? 遞迴版本的階層是這麼寫的: fact :: Int -> Int fact 0 = 1 fact (n+1) = (n+1) * fact n 沒有遞迴的話,就用 Y 取 fixed-point 囉。首先定義這個 factF: factF :: (Int -> Int) -> (Int -> Int) factF g 0 = 1 factF g (n+1) = (n+1) * g n 和 fact 的差別是 factF 只做 fact 的第一層。注意 factF 的型別。 然後 fact 就是 factF 的 fixed-point: fact :: Int -> Int fact = y factF 由此可知一個語言如果有提供 closure, 就可以不用把遞迴當作 primitive. 3. Mutual Recursion Mutual recursion 其實也是一樣的,只是同時定義一組東西。 比如說一般 even 和 odd 可以這樣定: even, odd :: Int -> Bool even 0 = True even (n+1) = odd n odd 0 = False odd (n+1) = even n 如果沒有遞迴,就定義一個從「一對」函數到一對函數的函數: evenOddF :: (Int -> Bool, Int -> Bool) -> (Int -> Bool, Int -> Bool) evenOddF (ev, od) = (\n -> if n == 0 then True else od (n-1), \n -> if n == 0 then False else ev (n-1)) evenOddF 拿一對函數 (ev,od),產生一對函數,各自只做 even 和 odd 的第一層。本來該是遞迴的地方分別呼叫 od 和 ev. (如果該語言沒有 pair, 就用 lambda 來模擬。) 然後我們也用 Y 取 evenOddF 的 fixed-point: evenOdd :: (Int -> Bool, Int -> Bool) evenOdd = y evenOddF even 就是第一個,odd 就是第二個: even = fst evenOdd odd = snd evenOdd 只是還有一點小問題:在 Haskell 中 y evenOddF 不會終止。 簡單的解決方法是把 evenOddF (ev, od) = ... od .. ev ... 改成 evenOddF evod = ... snd evod ... fst evod ... 看起來比較漂亮,其實一樣的方法是用 lazy pattern: evenOddF ~(ev, od) = ... od .. ev ... 這樣就可以囉! *Main> even 10 True *Main> odd 10 False --



※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 123.192.160.134
1F:推 SansWord:Cool! Thanks! 06/04 00:58







like.gif 您可能會有興趣的文章
icon.png[問題/行為] 貓晚上進房間會不會有憋尿問題
icon.pngRe: [閒聊] 選了錯誤的女孩成為魔法少女 XDDDDDDDDDD
icon.png[正妹] 瑞典 一張
icon.png[心得] EMS高領長版毛衣.墨小樓MC1002
icon.png[分享] 丹龍隔熱紙GE55+33+22
icon.png[問題] 清洗洗衣機
icon.png[尋物] 窗台下的空間
icon.png[閒聊] 双極の女神1 木魔爵
icon.png[售車] 新竹 1997 march 1297cc 白色 四門
icon.png[討論] 能從照片感受到攝影者心情嗎
icon.png[狂賀] 賀賀賀賀 賀!島村卯月!總選舉NO.1
icon.png[難過] 羨慕白皮膚的女生
icon.png閱讀文章
icon.png[黑特]
icon.png[問題] SBK S1安裝於安全帽位置
icon.png[分享] 舊woo100絕版開箱!!
icon.pngRe: [無言] 關於小包衛生紙
icon.png[開箱] E5-2683V3 RX480Strix 快睿C1 簡單測試
icon.png[心得] 蒼の海賊龍 地獄 執行者16PT
icon.png[售車] 1999年Virage iO 1.8EXi
icon.png[心得] 挑戰33 LV10 獅子座pt solo
icon.png[閒聊] 手把手教你不被桶之新手主購教學
icon.png[分享] Civic Type R 量產版官方照無預警流出
icon.png[售車] Golf 4 2.0 銀色 自排
icon.png[出售] Graco提籃汽座(有底座)2000元誠可議
icon.png[問題] 請問補牙材質掉了還能再補嗎?(台中半年內
icon.png[問題] 44th 單曲 生寫竟然都給重複的啊啊!
icon.png[心得] 華南紅卡/icash 核卡
icon.png[問題] 拔牙矯正這樣正常嗎
icon.png[贈送] 老莫高業 初業 102年版
icon.png[情報] 三大行動支付 本季掀戰火
icon.png[寶寶] 博客來Amos水蠟筆5/1特價五折
icon.pngRe: [心得] 新鮮人一些面試分享
icon.png[心得] 蒼の海賊龍 地獄 麒麟25PT
icon.pngRe: [閒聊] (君の名は。雷慎入) 君名二創漫畫翻譯
icon.pngRe: [閒聊] OGN中場影片:失蹤人口局 (英文字幕)
icon.png[問題] 台灣大哥大4G訊號差
icon.png[出售] [全國]全新千尋侘草LED燈, 水草

請輸入看板名稱,例如:Soft_Job站內搜尋

TOP