2016-07-18

tmuxからのpowerlineで優勝せえへん？

terminal環境

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

環境

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

Ubuntu 16.04
Mac OS X El Capitan
Debian jessie (Mac上のVM環境)

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とかで管理するか？

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

参考

2016-07-03

React ComponentにImmutable.jsは(多分)だめ

Typescript

github.com

ここにもはっきり書いてあるように,

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はまだまだ改良の余地ｱﾘｱﾘな感じがする)

2016-05-15

variable-free type theoryの圏論的な解釈について

myuon-myon.hatenablog.com

の続き. いくつか疑問が解消されたのでそれについて.

var-free type theoryについて

syntaxはcontext, type, term, substからなる.
contextはtypeの有限列(通常はvariableとそのtypeの組の列だが, 今回はvariable-freeなのでtypeだけの列になる).
typeはground typeと関数型A → Bとsubstが代入された型(σ[s]の形をしているもの)のいずれか.
termは1と代入された項M[s]のいずれか.
substはidと合成f . gとshift↑とextension<f:subst, M:term>のいずれか.

termは型付けをde Bruijn indexで考える.
term1はcontextの直近のtypeに対応する項とみなす. 例えば, Γ,σ ⊢ 1:σなどである.

substはcontextの間の変換とみなす.
例えばΓ ⊢ id:Γはid(Γ)=Γを表す. また, 合成は通常と逆向きに書くらしい(多分見やすさの都合).
shift↑はindexをすべて1つ加算するような変換とみなす. 例えばΓ,σ ⊢ ↑:Γはindexが上に1つずれるので一番新しいtypeσを忘れるものとみなす.

extensionのtyping ruleは次のようなものである:
Γ ⊢ f:Γ', Γ' ⊢ σ, Γ ⊢ M:σ[f] ⇒ Γ ⊢ <f,M>:Γ',σ

これは, Mによってcontextに新しいtypeを付け加える操作と考えることができる.
あるいは, 変換fをMによって拡張したものとみなしてもよい.

locally cartesian closed categoryでの解釈

ML theoryはLCCCとイイカンジに対応する.
ここではcategory with attributesを使った解釈を使うことにする.

すると上で導入したsyntaxはLCCC(cwa)でいい感じに解釈できる.

contextはobject, contextΓのtypeはΓ-cod morphismとみなす.
type Aをもつtermは, Aに対応するmorphism(shift)のsection.
substはmorphismとみなす.

以上の対応で, 上のsyntaxはcwaの構造で超いい感じになる.

function type→はPi-typeを使って定義するので一旦忘れる. (論文にあるようなcwaを構成するとdependent product/sum, extensional identity typeを持つ)
substidはidentity, 合成はcompositionになる.
shift↑はcwaのcanonical projection operatorになる.
代入された項M[s](M:Γ → Γ,A, s:Γ'→Γ)はpullbackΓ'×Γ,A[s]overΓのUMPから誘導されるmorphism
extension<f,M>はpullbackの対角線にあたるmorphism(Mとfのliftを合成する).
1=<id,id>はpullbackのUMPからつくる.

Set model

上のだけだとよく分からないのでSetで解釈する.

shiftはshift写像<gi,a:A> ~> <gi>
termはこのsectionなので, A型の値の追加, <gi> ~> <gi,a:A>になる. これはa:Aと同一視できる.
代入項に登場するpullbackはΓ'×Γ,A[s] = {(gi', gi, a) | s(gi')=gi, a=M} = {(gi',M)}と同一視できる.
よってM[s]は<gi'> ~> (<gi'>,M)とみなせる.
extensionは<f,t:A> = ↑*f . t ; <gi'> ~> <gi',t> ~> <f(gi'),t>になる.