Skip to content

Latest commit

 

History

History
180 lines (120 loc) · 6.14 KB

2017.09.21.md

File metadata and controls

180 lines (120 loc) · 6.14 KB

未命名的讀書會 #0

這是 cschat.taichung 第 0 次聚會！

由於活動的性質與主題都還沒有確定下來，不對活動主題設限。

  • 19:30-20:00 點餐、集合
  • 20:00-20:30 導讀 Philip Wadler 的 Comprehending Monads
  • 20:30-22:00 自由分享

Comprehending Monads 全文可以在 https://ncatlab.org/nlab/files/WadlerMonads.pdf 找到。

目前挑選的場地沒有投影機，請大家擠在一起盯著同一台電腦吧。

待辦事項：

  • 決定下次聚會時間、地點
  • 決定一個 logo

Comprehending Monads 導讀

Phlip Wadler 在此文中從 list comprehension 開始，講解它和 monad 的關係，並且以同樣的語法，構造出 identity, strictness, state transformer, state reader, parser, IO 與 continuation monads 。並解釋怎麼將這樣的結構與 call-by-value, call-by-name 的 impure language 連結起來。

Introduction

介紹了在 pure language 中模擬 impure language 的好用功能（例如改變變數的值）所帶來的麻煩與過往的解決方案，再帶出怎麼靠 monad comprehensions 解決這問題。要注意的是，那時還沒有 do notation 跟 type classes ，很多寫法今天看來很彆扭。

Comprehensions and monads

首先介紹 map 的性質，接著將 list comprehension 和 unit, map, join 三個 function 對應起來：

-- [t | Λ] = unit t
unit :: a -> m a
-- [t | x <- u] = map (\x -> t) u
map :: (a -> b) -> m a -> m b
-- [t | p, q] = join [[t | q] | p]
join :: m (m a) -> m a

於是：

[(x, y) | x <- [1, 2], y <- [3, 4]]

可以寫成：

[(x, y) | x <- [1, 2], y <- [3, 4]]
join [[(x, y) | y <- [3, 4]] | x <- [1, 2]]
join (map (\x -> [(x, y) | y <- [3, 4]]) [1, 2])
join (map (\x -> (map (\y -> (x, y)) [3, 4])) [1, 2])

Two trivial monads

這章介紹 identity monad 和 strictness monad ，前者什麼也不做，可以看成 let ，後者控制哪時要 evaluate 成 WHNF(Weak Head Normal Form) 。

identity monad 的 unit, map, join 長這樣：

data Id a = a
unitId x = x
mapId f x = f x
joinId x = x

於是：

[(x, y) | x <- 3, y <- 4]
joinId [[(x, y) | y <- 4] | x <- 3]
joinId (mapId (\x -> [(x, y) | y <- 4]) 3)
joinId (mapId (\x -> (mapId (\y -> (x, y)) 4)) 3)
joinId (mapId (\x -> (\y -> (x, y) 4)) 3)
joinId ((\x -> (\y -> (x, y)) 4) 3)
(\x -> (\y -> (x, y)) 4) 3
(3, 4)

strictness 除了 f x 時會把 x 做到 WHNF 外，和 identity 一樣。另外也提到 strictness 會讓 map 的一些性質消失。

Manipulating state

介紹了怎麼讓 monad comprehension 幫你把 state 傳下去，而不用每個 function 都手動傳。

data State a = s -> (a, s)
unitState x = \s -> (x, s)
mapState f st = \s -> let (x, s') = st s in (f x, s')
joinState sst = \s -> let (st, s') = sst s; (x, s'') = st s' in (x, s'')

並加上 fetch :: State s 用來讀出現在的 state ， assign :: s -> State () 用來寫入 state ， init :: s -> State x -> x 用來提供初始 state 。

fetch :: State s
fetch = \s -> (s, s)

assign :: s -> State ()
assign x = \s -> ((), x)

init :: s -> State x -> x
init s st = let (x, s`) = st s in x

若 state 一開始為 0 ，想加上 1 後存回去，可以這樣做：

init 0 [y | x <- fetch, _ <- assign (x + 1), y <- fetch]

Alex 表示可以看成：

let
  s = 0
  (x, s') = fetch s
  (_, s'') = (assign (x + 1)) s'
  (y, s''') = fetch s''
in
  y

文中繼續以 lambda calculus 中的名稱替換（alpha equvalence）、更新 array 、 interpreter 為例子。並以 interpreter 告訴我們，有時候要讀複數個值，但是並沒有改變 state ，光靠 state transformer monad 無法描述這件事，引出 state reader monad ，並在兩者間轉換。

Filter

介紹如果想在 monad comprehension 中用到 filter ，得多加一個產生空的 monad 的 function zero :: a -> m b

Monad morphisms

介紹怎麼寫出 monad 間的轉換，並以此證明用 state transformer monad 做的 interpreter 和 加入 state reader monad 的 interpreter 是相等的。

More monads

  • 介紹怎麼做一個用來處理 lambda calculus 的 parser monad
  • 介紹怎麼用 monad 描述 exception ，也就是 maybe monad
  • 介紹怎麼樣組織 type ，可以用 monad 描述 IO
  • 介紹怎麼用 monad 描述 continuation ，並做出 call/cc

這邊 IO 裡放的是 String ，我猜和當時 IO 仍需要由一個 impure 程式把 String 餵給 pure 程式有關。還不明白後來怎麼演變成描述外在世界變化的 RealWorld 的。

Translation

介紹怎樣把 call-by-value, call-by-name language 用 monad comprehension 轉換成 pure lambda calculus ，還強調雖然 call-by-name 在用到時才 evaluate ，但和 call-by-need(lazy) 不同，會有副作用。

然後以 non-deterministic language 採用 call-by-value 與 call-by-name 策略時的不同結果當做例子。

例如 [\a -> a + a | 1 ``choice`` 2] 在 call-by-value 時，結果為 {2, 4} ，在 call-by-name 時，結果為 {2, 3, 4} 。

b4283 認為前者可以理解成 (1 + 1) ``choice`` (2 + 2) ，後者是 (1 ``choice`` 2) + (1 ``choice`` 2) 。

又介紹 call-by-value 如何以 continuation-passing style 來描述作結。

雜談

  • 原來 Alex 是看到 Meetup 的推薦才來的 XD
  • b4283 a.k.a. 德瑞克
  • 手寫的 non-deterministic choice operator 被嫌畫得不夠方 XDDD

下次聚會的方向

雖然沒能決定下次聚會主題，但大致決定了方向：

  • SKI combinator calculus (b4283)
  • 繼續讀 SPJ 的 STG 論文 (caasi)
  • SML (b4283)

caasi 希望可以挑 10~15 分鐘可以介紹完的題目，這樣大家都能分享自己想看的主題，也不會給人太大的壓力。

下次聚會時間地點

b4283 得開車從中清交流道下來，應該選靠近中清路的場地。