λ→のtyping & unification algorithm
この記事のunification algorithmは間違っているので
λμのTypeCheckerの実装 - Just $ A sandboxを参考にしてください
λ→のtypingアルゴリズム.
variableとabstractionは型が一意に決まるので, 問題はapplication.
MN:aからM:?x -> aの?xをどうやって決定するかという問題になる.
holeの導入
型変数とは別に, hole(goal)を導入する.
holeは確定していない型で, どんな型も入ることができる. さらにtypingが下から上に, 左から右に進む関係上, typingが進むにつれて段々確定していく.
例:
|- λf. λx. f x : ??
-> f:?0, x:?1 |- f x : ?? <-- abstractionした
-> f:?0, x:?1 |- f:?0 f:?0, x:?1 |- x:?1 <-- application
-> f:?1 -> ?2, x:?1 |- f x :?2 <-- fは関数型なので{?0 = ?1 -> ?2}を代入した
-> |- λ(f: ?1 -> ?2). λ(x: ?1). f x : (?1 -> ?2) -> ?1 -> ?2 <-- abstractionした
applicationの時にholeの代入が必要になる.
この時, holeの等式を代入するという操作をするが, これはbase(|-の左側)と現在確定している型の中身にも代入する必要がある.
このように, 等式が与えられるとそれらに含まれるような最大の型を取ってくるという操作が必要になり, これをunificationという.
unificationは失敗することもある.
x:?0 |- x x : ??
-> x:?0 |- x:?0 x:?0 |- x:?0 <-- {?0 = ?0 -> ?1}はunification不可能
typing algorithm
実際のtyping algorithmは次のような感じになるはず.
-- var G |- x : ?? -> G |- x : G(x) -- abs G |- λx. e : ?? -> G, x:?n |- e : Type(e) -> G |- λx. e : ?n -> Type(e) -- app G |- M N : ?? -> G |- M : Type(M) G |- N : Type(N) -> unify {Type(M) = Type(N) -> ?n} -> G |- M N : ?n
unification algorithmは必要な部分で左辺を右辺に置き換える処理を書くだけのはず.
data Typ = TVar String | TArr Typ Typ | Hole Int data Untyped = Var String | App Untyped Untyped | Abs String Untyped type Base = [(String, Typ)] data Checking = Checking { _base :: Base, _freshHole :: Int, _holes :: [(Int, Typ)] } makeLenses ''Checking fresh :: (Monad m) => StateT Checking m Int fresh = do n <- use freshHole freshHole += 1 return n typing :: Untyped -> Either String Typ typing t = flip evalStateT (Checking [] 0 []) $ go t where go :: Untyped -> StateT Checking (Either String) Typ go (Var v) = do gs <- use base case lookup v gs of Just t -> return t Nothing -> lift $ Left $ "Not in scope: " ++ v ++ " in " ++ show gs go (Abs x e) = do n <- fresh base <>= [(x, Hole n)] t <- go e hs <- use holes return $ apply hs $ TArr (Hole n) t go (App e1 e2) = do t1 <- go e1 t2 <- go e2 n <- fresh unify t1 (TArr t2 (Hole n)) hs <- use holes return $ apply hs (Hole n) apply :: [(Int, Typ)] -> Typ -> Typ apply bs (Hole n) = case lookup n bs of Just t -> apply bs t Nothing -> Hole n apply bs (TVar a) = TVar a apply bs (TArr t1 t2) = TArr (apply bs t1) (apply bs t2) replace :: Int -> Typ -> Base -> Base replace n typ = fmap (second go) where go :: Typ -> Typ go (TVar a) = TVar a go (Hole m) | m == n = typ | otherwise = Hole m go (TArr t1 t2) = TArr (go t1) (go t2) allHoles :: Typ -> [Int] allHoles (Hole n) = [n] allHoles (TArr x y) = allHoles x ++ allHoles y allHoles _ = [] unify :: Typ -> Typ -> StateT Checking (Either String) () unify (Hole n1) t = if n1 `elem` allHoles t then lift $ Left $ "Unification failed: " ++ show (Hole n1) ++ " in " ++ show t else base %= replace n1 t >> holes <>= [(n1,t)] unify t1 (Hole n) = unify (Hole n) t1 unify (TVar a) (TVar b) | a == b = return () | otherwise = lift $ Left $ "Type mismatch: " ++ a ++ " /= " ++ b unify (TArr t1 t1') (TArr t2 t2') = unify t1 t2 >> unify t1' t2' unify (x@(TArr _ _)) y = lift $ Left $ "Unification failed: " ++ show x ++ " and " ++ show y
動かす
なんかこんな感じになる.
λx. x : Right ?0 -> ?0 λx. λy. y x : Right ?0 -> (?0 -> ?2) -> ?2 λf. λg. λx. f (g x) x : Right (?3 -> ?2 -> ?5) -> (?2 -> ?3) -> ?2 -> ?5 λx. x x : Left "Unification failed: ?0 in ?0 -> ?1" λx. x y : Left "Not in scope: y in [(\"x\",?0)]" λf. λx. f (x x) : Left "Unification failed: ?1 in ?1 -> ?2"
はたして
で上のアルゴリズムで本当に合っているのかはよく分からない.
TaPLにこのアルゴリズムについての説明があるらしいので気になる人はどうぞ.
tmuxからのpowerlineで優勝せえへん？
メモです.
現状イマイチなところがありありなのでどうにかしたい.
環境
以下に同じ端末環境を作りたかった.
zsh
prezto
を入れる.
入れたら.preztorcのcompletionとかその他のあれこれをオンにする.
promptでテーマを変えられる.
自分は今はsorinにしてる. 色のついた矢印がかわいい.
tmux
.tmux.confを作って色々書く.
自分はprefixをC-zにして, さらにemacsっぽいキーバインドを設定したりした.
powerline
tmuxとかzshとかvimとかのpowerlineは全てpowerlineという名前で1つに統合されたらしい.
しかしまだ古い情報(tmux-powerlineとか)が結構ヒットするので注意.
$ pip3 install --user powerline-status
で入れる.
pipをMacの場合はbrewで入れることになると思うけど, その場合は--userはつけてはいけないって誰かが言ってた気がするけど普通に入ったので多分問題ない.
tmux(とzsh)にpowerlineの設定をする.
- tmux: Other plugins — Powerline beta documentation
- zsh: Shell prompts — Powerline beta documentation
これでtmuxを再起動orリロードすれば反映されているはず.
されてなければ
$ powerline-deamon -r
とかするといけるかもしれない.
テーマを変えたりする場合はconfig_filesをコピーして~/.config以下の方を触るようにする.
しかし, 新しいsegmentを追加(電池残量とか)しようとするとcolorschemeに定義がないと言って怒られたりするし, colorschemeについての説明も公式ドキュメントに全然ないのでよくわからない.
# Linux $ cp -r ~/.local/lib/python3.5/site-packages/powerline/config_files/ ~/.config/powerline/ # Mac $ cp -r /Library/Frameworks/Python.framework/Versions/3.5/lib/python3.5/site-packages/powerline/config_files/ ~/.config/powerline
まぁ, powerlineはデフォルトでもそれなりに使えるので良いと思う.
.tmux.confをいじっても見た目変えられるっぽいし.
最終形態
優勝？
優勝には程遠い感じ.
変えたいところ:
- tmuxのpowerlineのテーマ
- preztoは果たして必要なのか？ (zshにpowerlineを入れておいてそれを自分で改造すればよくない？)
- preztoやめるならzsh関係のプラグインはzplugとかで管理するか？
なんかいまいちイケてないので模索していきたい.
参考
React ComponentにImmutable.jsは(多分)だめ
ここにもはっきり書いてあるように,
Note that state must be a plain JS object, and not an Immutable collection, because React's setState API expects an object literal and will merge it (Object.assign) with the previous state.
React ComponentのstateをImmutableデータ構造にするのは良くない.
これをするとsetStateで渡ってくるものが(型情報的には確かにImmutable.Listでも)JSArrayになってたりする.
ググったら以下の2つの方法をとっている人が多かった.
- setState内では全ての
state.piyoをImmutable.DataType(state.piyo)みたいにラップする
これは一見うまく行くように見えて, たまたまラップすることを忘れたりするとImmutable.List.unshiftじゃなくてArray.unshiftが発動したりして死ぬ可能性がある.
- state一つ一つをImmutableにするんじゃなくてstateをまるごとImmutable.Mapにする
これはデータの取り出しがImmutable.Map.get("nyan")みたいになるので(型をつけている場合は)型情報が消滅するので自明にダメ.
なお一瞬だけMapのKeyにString Literal Typeを渡すみたいなのも考えたけど, 与えられたデータ構造からString Literal Typeをメタ生成するとかできるんだろうか. できてもやりたくはないけど.
他にいい方法があるなら知りたい.
(やはりTypescriptでも型レベルMapを作るしかない)
(ていうかこんな分かりやすいトラップがあるのにImmutable.jsはReactと相性がいいって言ったやつ誰だよ)
(interfaceの貧弱っぷりを見るにつけてもTypescriptはまだまだ改良の余地ｱﾘｱﾘな感じがする)
