読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングと計算機科学とかわいさ

Programming in Scalaを読んでいる時のメモ

Scala

Programming in Scala: A Comprehensive Step-by-Step Guide, Third Edition (English Edition)

Programming in Scala: A Comprehensive Step-by-Step Guide, Third Edition (English Edition)

を読んでいる時に気になったことをメモします.
2nd Editionなので若干内容が古いやつっぽいのと本文はかなり飛ばし読みしてるので変なことを言っているかも.

疑問が解決したらちゃんと補足していく予定.

Chapter9以前

  • 関数はブロック内の最後の値が戻り値になるっぽい. 慣れないと若干気持ち悪い.
  • (a:A, b:B) => { c:C }ラムダ式みたいなものかな? 便利だしdefとかあんまり要らなさそう.
  • objectはただの名前空間みたいなものだと思って気軽に使っていいのかな?
  • x.f(y)x f yとかけるから中置記法が使えるらしい. 面白いし変なsyntaxと間違う余地がなければかなり便利っぽい.
  • Scalaでは0引数関数と定数の区別が曖昧になっている箇所がある(defの定義のところとか). 要確認.
  • for-exprはforM関数とリスト内包表記を混ぜたみたいな感じ.

Chapter10

  • abstract classは実装もかけるのか.
  • classのパラメータ書くところにprivateとかつけられるの魔剤ンゴ!? 内部ではパラメータは全部ただのvalに置き換わってるからかなあ.
  • classのoverrideとか(おそらくメソッド名等々)の解決はコンパイル時に行われるっぽい
  • finalを付けるとそれを継承したclassやoverrideしたmethodを定義できなくなる. どこで使うのこれ?

Chapter11

  • Javaきもこわちかよらんとこ
  • nullはNull型になっていてValueTypeとはcompatibleじゃない
  • Nothingがbottom

Chapter12

  • traitはそれ自体の値も作れるし継承してクラスを作ることもできる
  • traitはパラメータをもてないのとsuperが動的に解決されるのに注意
  • classより使い勝手よさそう
  • 複数のtraitを継承してmethodが衝突した場合は最後のやつだけが有効
  • reusableならtrait それ以外はabstract classみたいな感じでいいらしい

Chapter15

  • case classというのが作れるらしい. closure conditionをコンパイラに伝えるためのものかな?
  • pattern matchingだ!これで勝つる!
  • valの中身がconstantかどうかまでmatchingの時に判定するので注意
  • _*ワイルドカード任意個の意味になる
  • Anyで受け取ったものをtypeでmatchingもできるらしい. 最高に気持ち悪い.
  • @でmatchした項全体を変数で受け取れる
  • case [pat] if [cond]でpattern guardも使える つよい
  • valの定義やfor-exprの変数定義でpatternを使った束縛もできる

Chapter16

  • List concatは:::
  • foldが/::\なのは流石にヤバくない???

Chapter19

  • subtyping特有のあれこれがあって注意が必要そう
  • S <: T ~> K[S] <: K[T]のようにsubtyping relationを保つときKはこの引数についてcovariantという. 関係が逆になるものをcontravariantという.
  • 型パラメータがcovariant/contravariantであるべきという性質を+A/-Aで要求できる.
  • T >: UでTはUのsupertype, UはTのlower boundであることを要求できる.
  • 「あるクラスを含む全てのクラス」「あるクラスに含まれる全てのクラス」に対する実装を書く(そんなことが本当にあれば)ことができるようになるんだと思う

Chapter20

  • traitの中にはtype/def/val/varをメンバーとして含めることができる
  • member_=でmemberのsetterを定義する. Agdaのmixfix operatorみたいな感じ(完全にmixfixできるの? 多分そんなことはないよね?).
  • lazyを付けると変数の初期化と生成を遅延できる

Chapter21

  • implicit危険なので気をつけよう
  • implicit coercionとimplicit parameterがある
  • <:をimplicit coercion込みで解決してくれるやつは<%とかく
  • この辺使いまくるとコンパイルに時間かかりそう

Chapter28

  • 異なる型の比較とかをうまくやろうとするとそりゃあ大変だよねって話. そもそもそういうことが起こること自体なんか変なのでは?と思うけど
  • subtypingの事情があるのは分かるけど、そんなに何でもかんでも同一視することが大事なのかはよく分からない

Chapter30

  • actor便利かよ〜〜〜
  • ここだけ別の資料なりなんなりでちゃんと勉強したほうがよさそう

λ→のtyping & unification algorithm

Haskell

λ→の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で優勝せえへん?

terminal環境

メモです.
現状イマイチなところがありありなのでどうにかしたい.

環境

以下に同じ端末環境を作りたかった.

zsh

zshを入れてデフォルトのshellをzshにする.

prezto

github.com

を入れる.
入れたら.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を再起動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をいじっても見た目変えられるっぽいし.

最終形態

f:id:myuon_myon:20160718120251p:plain

優勝?

優勝には程遠い感じ.
変えたいところ:

  • tmuxのpowerlineのテーマ
  • preztoは果たして必要なのか? (zshにpowerlineを入れておいてそれを自分で改造すればよくない?)
  • preztoやめるならzsh関係のプラグインはzplugとかで管理するか?

なんかいまいちイケてないので模索していきたい.

参考