TaPL読書録 #2

hkdnet.hatenablog.com

引き続きTaPL読書録です。今回は3.4.まで。

この項の構文は succ trueif 0 then 0 else 0 のような怪しげな項の形成を許すことに注意されたい(p.18)

怪しげw
「型なし算術式」なのでこの手のものを許可せざるを得ない。
評価のところまですすめたとき、評価の左辺(辺か?)にマッチせず捨て置かれることがわかる。

... この定義は複合的な部分式に付ける括弧の使用について何もいっていない(p.19)

else のない if などが導入された場合に曖昧性が出始める、とのこと。

定義3.2.3.

演習3.2.5. より、 lim のような記法が定義されていれば i -> ∞ における S_i が S と一致するはずだがそのような記法が導入されていないので和集合をとる記法になっているのかな?という話が出た。

補題3.3.3. 証明 tの深さに関する帰納法を用いる。

深さなのだろうか? size に関する演算が多く、サイズに関する帰納法なのでは?という指摘があったが、おそらくこれは深さに関する帰納法で正しい。 「t = succ t1 を満たす t, t1 において depth(t) > depth(t1) が常に成立する」 ということを暗黙的に用いて帰納法を用いている、と解釈した。

定理3.3.4. 証明(演習)

しれっと演習がまじっていて気づいていない人もいた。
基本的には補題3.3.3.の証明と同じ形式で進めればよい。のだが、基底部のケースがちょっと不明瞭……

https://github.com/hkdnet/tapl-exercise/blob/master/Ex3.3.4.md#s-%E3%81%8C%E5%AE%9A%E6%95%B0%E3%81%AE%E5%A0%B4%E5%90%88

例えば述語 Piszero とおくと iszero 0true であるが、iszero trueiszero false は評価できないので成り立たない1
しかし、s = true, false, 0 のとき depth(r) < depth(s) なる r は存在しないため、仮定法で用いる命題は成立するので、なにかおかしい気がする……。
定数群に対して必ず成り立つ述語でないといけないのかな?

この定理がどう役に立つのか?全てに成り立つ性質が示せて嬉しいか?という疑問も出た。おそらく、今後拡張が進むなかで定数部にxを含まないときにはこの性質が示せるがxを含むときには示せない、みたいな使われ方をするのでは?という話になった。

...書き出された証明を確認するより 簡単 である(p.23)

原文でも easier と書かれていることを確認した。

表示的意味論にとっての鬼門は... (p.24 †3)

鬼門は原文では "bête noire"だそうで。 https://ejje.weblio.jp/content/b%C3%AAte+noire

if true then (if false then false else false) else true) はif true then false else true` には評価されない(p.26)

if true then t1 else t2 でt1, t2から評価する規則はなく、E-IFTRUE のみしか使えないということを言っている。

次回は4章の終わりまで。


  1. true に評価されないならば成り立たない、でいいよね?

入社していくらか経ったので自分がどんな価値を出してたのか確認したよ

はいどうも。入社してから7ヶ月くらい経ってるんですが、俺って何したんだっけ?どういう価値を提供したんだっけ?というのをふと確認したくなったので確認しました。今回はそれを外に出せる部分だけ出しておこうと思います。

業務中にメインで使っているレポジトリは1つなので1ざっとPRのタイトルを抜き出して分類してまとめました。
定期的に振り返るとか苦手でまとめてざっと傾向見るくらいがちょうどいいのかもという試みです。

ざっと集計したところ404PR作っていたそうです。うちマージされなかったのが23個。マージされてないのは、POC的に「こんなんどう?」って出したあとで閉じたり、CI落ちてる原因を確かめるために試行錯誤してたり、書いてみたけどやっぱ微妙で大幅な方針転換が必要だったりという感じです。

f:id:hkdnet:20180211215917p:plain

Release っていうのはリリースするのに必要なものであったり、masterの変更をマイルストーンにマージしたりみたいなそういうやつなので実質あんまりなんもしてないやつです。2

Wording は文言変更とか、なんかちょろいの全般。Fix がバグ修正で Feature が機能追加っぽいやつです。動作が変わらない系は、Refactoring はリファクタですが、テスト追加のみだとSpecっていう分類にしてます。Disposedは上述の捨てられたやつ3。Others は、gem update とかそういう分類しにくいやつです。

Feature は8-11月くらいにやってたんですが、25%あっておもったよりも多いですね。最近バグ修正とかが多めだったから実際より少なめに見積もってたのかも。このへんを深くみるために月次で分けました。

f:id:hkdnet:20180211220517p:plain

日付はマージされた日で見ています。9999/12はDisposedです4

10月は新機能開発の追い込みで頑張ってた感じが見て取れますね。1月とかはRelease系が多いですね。
Fix系が増えてくるとだいたい調査とかであーうーとか唸っている時間が多くなるので、機能追加の終盤である(= 考えることが少なめである)10月の機能開発よりPR数が減るんでしょうか。確かに最近は調査で頭を抱えてる時間が長かったような気もします。

これ以外に、(公開はできませんが)この機能追加した、こういうの直したみたいなリストも作っています。給与とかが決まるような1 on 1のときとかに使えるとアピールするのに便利かなーという気持ちで継続的に整備していこうかなと。


話は変わって集計方法について。

今回は適当にgolangで抜いてきたのをプレーンテキストにして google spreadsheets でタグ付けしてました。でもこういうのって時々やりたくなるんでなんかフレームワーク化というか、汎用的にできたらなーと思ってぺちぺち改良をしようとしています。

上のを抜いてきたときのバージョンではないですが一番それっぽかったときの gist を貼っておきます。

main.go · GitHub

interfaceとかを定義していろいろ可変にしたそうな雰囲気が感じられますね。またこのプロジェクトに進展があったらブログで紹介しようと思います。


  1. 他レポジトリも読んだりはするけどPRはたぶん片手(10進法)で数えられる程度しか送ってない

  2. デリバリーをなんもしてないというとアレなんだけど、まあ難しくないし、僕がやらなくても誰かやるし……。面倒事を率先してやっているとは言えるかもしれない(55PR)

  3. あまり正しい英語ではない気がしている

  4. マージされずに閉じられているのだけど空欄にするとソートがアレだったので

オフラインリアルタイムどう書くE21 に参加して負けてきました

yhpg.doorkeeper.jp

負けました。敗因はなんだろ……。方針が定まりきらなかったのが敗因なのかなー。

プレイヤーベースで考えると打ったときに、そのタイミングでアタリを引いたのか、次のターンでアタリを引いたのかの場合分けがめんどくさそうだなーと思いつつ、じゃあどうするんだろー、という感じ。
今回は平行世界をたくさん用意して、リボルバーのタマの詰め方を全通り作って、アタリを引いた人と一致するパターンが正解ということにしています。
無限ループに入ってるかどうかは雑に何周したかをカウントして、まわりすぎだったら終わるって感じでやってます。

引っかかったのは、playerのidxとidで番号が1つズレているのでそれの管理ミスと、残弾数がズレてるケースを削るのを忘れてるとかそのへん。

コミットしてなかったので当時の状態がわからないけど最終形はこんな感じでした。

misc/solver.rb at master · hkdnet/misc · GitHub

勝てなさそうな印象の割にがんばれたけど負けてて悔しいですね。しょんぼり

gitコミットしぐさ

はいどうも。最近気をつけているコミットのやり方について備忘録的に書きます。1

前提として、現在はある程度成熟しているアプリケーションについての話です。新アプリの新画面ばーんってつくっていくぞみたいなときはもっと雑にコミットしてもいいんじゃないでしょうか。不具合修正であったりちょこちょこした機能追加だったりがメインな文脈です。

commit を verbose にする

いいコミットの第一歩はたぶんこれです。git CLI使っている人は git config --global commit.verbose true でOKです。あるいは git commit -v って打つか。2 これはどういうオプションかというと、コミットメッセージを書くときに下にdiffが出ます。

-v, --verbose
    Show unified diff between the HEAD commit and what would be committed at the bottom of the commit message template to help the user describe the
    commit by reminding what changes the commit has. Note that this diff output doesn't have its lines prefixed with #. This diff will not be a part
    of the commit message. See the commit.verbose configuration variable in git-config(1).

    If specified twice, show in addition the unified diff between what would be committed and the worktree files, i.e. the unstaged changes to tracked
    files.

説明にあるように、なんの変更をコミットするのかを見せてもらえるのですごくいいです。ざっと眺めることで「これってどういうタイトルつけよう?」とか「あれ、これ入れたくなかったんだけど」みたいなことが起きます。おすすめ。

リファクタリングと変更を分ける

たとえば以下のようなものを考えましょう。

SELECT  * from users WHERE foo = 1 LIMIT 100;

「普通の select 文ですね。でも order by がないですね。あと from は予約語なのに小文字ですね。直しちゃいましょう。」

$ git diff
diff --git a/tekitou.sql b/tekitou.sql
index a9a1810..f852f3c 100644
--- a/tekitou.sql
+++ b/tekitou.sql
@@ -1 +1 @@
-SELECT  * from users WHERE foo = 1 LIMIT 100;
+SELECT  * FROM users WHERE foo = 1 LIMIT 100 ORDER BY id;

はいアウトー3 from -> FROM は動作を変更しませんが、 ORDER BY の追加は動作を変更するので分けたほうがいいと思います。

まあこの例はさすがに極端なのですが、例えば以下のような変更をするときも2コミットに分けます。

class Foo
  def foo
    obj.some_method(another_obj.some_method)
  end
end

ここで another_obj.some_method を更に加工する必要が出てきたとき

まずは「リファクタリング: ローカル変数にとるようにする」のようなコミットを積んでから変更を積みます。

$ git show
commit 786849cff921477a463fe7fcd59000d3ce84c0a3 (HEAD -> master)
Author: hkdnet <xxx>
Date:   Sun Jan 28 14:12:18 2018 +0900

    リファクタリング: ローカル変数にとるようにする

diff --git a/tekitou.rb b/tekitou.rb
index c910df5..faa7b7b 100644
--- a/tekitou.rb
+++ b/tekitou.rb
@@ -1,5 +1,6 @@
 class Foo
   def foo
-    obj.some_method(another_obj.some_method)
+    tmp = another_obj.some_method
+    obj.some_method(tmp)
   end
 end

これの何がいいかっていうと、レビュアーが楽なんですよね。GitHubのPRにはコミットを順番に見る機能があるので4リファクタリングって書いてあるコミットは軽く見れます。機能が変わったコミットに集中できます。

コマンドを打ったときにコミットしておく(例外あり)

たとえばこんな感じ

$ npm install foo
$ git add .
$ git commit -m '$ npm install foo'

npm installpackage.jsonpackage-lock.json が更新されるのでそれだけでコミットします。

Gemfile の更新は、Gemfile.lock の更新を伴うのでだいたい一緒にしてます(例外)

$ vim Gemfile
# ここではコミットしない
$ bundle install
$ git add .
$ git commit -m 'Install awesome_gem'

Rails で generate したときもそれだけでコミットしてます。db:migrate とかも。

$ bin/rails g model User name:string
$ git add .
$ git commit -m '$ bin/rails g model User name:string'
$ bin/rails db:migrate
$ git add .
$ git commit -m '$ bin/rails db:migrate'

モデルとかマイグレいじるときもコミット後に積んだほうが無難かなー。

コミットメッセージにいろいろ書く

書いておくとGitHubのPRを作るときにもコピペできて便利です。

最近だと国内向けのハイフン区切り電話番号の検証をやったのですが、こんな感じのコミットメッセージになりました。

意識してるのは、正しい仕様の根拠を示すこと。なにか機能を落としてるなら明記すること。5

$ git show
commit 9a2b1b3c57308adbb2c08daaaff1459d60c2ea55 (HEAD -> master)
Author: hkdnet <xxx>
Date:   Sun Jan 28 15:02:04 2018 +0900

    xx画面での電話番号のjs検証を追加

    ref: http://www.soumu.go.jp/main_sosiki/joho_tsusin/top/tel_number/q_and_a.html#q2

    電話番号は以下の仕様となる。
      国内プレフィックス: 1桁(0固定)
      市外局番          : 1〜4桁
      市内局番          : 1〜4桁
      加入者番号        : 4桁
        ただし市外局番と市内局番は合計で5桁となる
    ハイフンは市外局番と市内局番の間、市内局番と加入者番号の間にいれる。
    そのため (2-5)-(1-4)-(4) が正しいフォーマットであるといえる。

    「ハイフン区切りの第1項と第2項の桁数の和が必ず6桁である」
    という検証は今回は行わない
...

ハイフン区切りの第1項と第2項の桁数の和が必ず6桁である

やらなかったことが明記されてるとあとで助かります。

コミットは rebase で整形しとく

PR出す前に Fix a typo とかは rebase で何事もなかったかのように消し去ってます。

$ git commit -m 'fix a typo on xxxx'
$ git rebase -i origin/master
# さっきのコミットを xxxx のコミットの下の行にもってきて fixup しとく

これは好みだから別にどっちでも。僕が間違えたことやメソッドの使い方を勘違いしていたことも1つの情報だから、コミットとして残っててもいいのかもなーと思いつつ、blameで遡っていくときの邪魔になるので消しちゃうほうが最近の好みです。


  1. 1年前だと、「まあ適当で。GitHubのPRに書いてあればなんとかなるし」派だったことを思い出すと、こういう dump が重要な気がした

  2. GUIは知らない

  3. 「あと」とか思った時点でだいたいアウト

  4. 余談だが該当画面で n を押すと次のコミットにいく、というのを結構知らない人がいたので書いておく

  5. 今回のコミットメッセージを書く上で、あとで総務省のページがリンク切れになってたらどうしよう……という不安はある

TaPL読書録 #1

2018年はmediumで記事を投稿しようと思っていたのですが、はてなブログのほうがなんだかんだ流入がいい気がしたので戻ってくることにしました。乗り換えのきっかけは、ブログのエディタの使い勝手があまりよくないことによっていたのですが、 kibela で書いてからコピペで貼ればいいや、という気持ちになって出戻りです。

mediumでは以下の3記事を書いていました。

『ふつうのLinuxプログラミング』 読了 – hkdnet – Medium

『白と黒のとびら』『精霊の箱』『自動人形の城』読了 – hkdnet – Medium

ある日 Entity Attribute Value に出会った – hkdnet – Medium

さて、今回の記事はTaPL読書録です。おそらくシリーズものになります。

型システム入門 −プログラミング言語と型の理論−

型システム入門 −プログラミング言語と型の理論−

  • 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
  • 出版社/メーカー: オーム社
  • 発売日: 2013/03/26
  • メディア: 単行本(ソフトカバー)
  • クリック: 68回
  • この商品を含むブログ (11件) を見る

PFDS勉強会から派生してTaPL勉強会ができたのでそこでの疑問や得られた知識、派生して調べたことなどをまとめる予定です。1なお、記載内容に誤りがあった場合、原因の多くは私の理解不足であろうことを先に いいわけ 謝罪しておきます。 第1回は1, 2章が対象でした。ざっくりまとめると、型にまつわる概略とプログラミング言語とのかかわりが1章、集合などの数学的な基礎知識が2章でした。

ラッセルのパラドックスは、事前学習をしたのですが、wikipediaを見てもよくわからない状態でした。 R = { x | x ∉ x } という集合の定義をみたときに、 x は要素でありながら( x ∉ x の右辺)、集合である( x ∉ x )ということを考えると、 x が要素であるような集合の要素の集合の要素の集合の……と無限ループになってしまってとらえどころがなくて……。
という話をしたところ、右辺の x と左辺の x の「型」が違うはずなのに区別しないから矛盾が導けるよね、というのがラッセルのパラドックスであると教えてもらいました。

定義2.1.8
あまりにも関数に馴染みがありすぎること、関係というと関数が思い浮かびやすいことから案外つまづきました。部分関数の定義を読んでも、これは何であって何でないのか、というのがイメージしにくかったです。いまの私の理解では、「常に t1 = t2 である」が満たされないのは参照透明でない関係のことを指しているのだと思っています(例えばランダム性のあるものなど)。

定義2.2.1
s R t かつ t R s ならば s = t であるとき、Rは反対称的である というのは少しわかりにくいなーと思います。仮定部分の仮定では「s R t かつ t R s」で非常に対称的に見えるので。しかしその場合は「s = t である」という強い制約が導かれるので、ああたしかに反対称的と言われればそうなのかもな、という感じ。

定義2.2.3
上限と下限(結びと交わり)については「S = { 1, 2, 3 }, s = 1, t = 2のとき 結び j = 2」など具体例を挙げて確認しました。どうにも「結び」「交わり」という単語に苦手意識があるのですが、英語では "join" と "meet" らしいですね。そっちのがまだニュアンスがわかるような気がする。

演習2.2.6
反射的閉包の定義をみると「R を含む最小の反射的関係 R' のことである」とあります。 関係 R' を R' = R U { (s, s) | s ∈ S } とした場合に、R' が R を含むことは明らか。 U の右オペランドが反射的閉包の必要条件であることも明らか。 R の左右のオペランドである集合はそれぞれ何かの要素を抜いた瞬間に R' が R の反射的閉包であるための必要条件が満たされなくなるので、それらの和集合は最小であるといえます。

最初、反射的閉包のイメージが掴めなかったのですがイメージが掴めると、これ同じことしかいってねーなという感じ。

f:id:hkdnet:20180118014834j:plain

画像では R = { R1, R2 }, R' = {R1, R2, R3, R4, R5}です。関係とは図中の矢印の集合であるというのがわかればまあなんとかなるかと。

演習2.2.7
R0, R1, ... というのは下図のようなイメージ。点線をひいてあるところがその関係で追加されるところです。
f:id:hkdnet:20180118014806j:plain

演習2.2.8
推移的に追っていけばなんとかなるでしょ、という感じ

2章まではこんな感じでした。次回から本編に入るので楽しみです。


  1. と大風呂敷を広げましたがめんどくさくなったら派生して調べたことがなくなり疑問のまま放置されるでしょう。

2017年を振り返って

定量的な振り返りとしてGitHubの草を置いてみる。

f:id:hkdnet:20171231224923p:plain

3331 contributions
仕事とプライベート両方見えてるので結構すくなめかも。
一応草活は続いてる。

言語別のコーディング時間

f:id:hkdnet:20171231230323p:plain

定性的な振り返りとして隔月のことを思い出して適当に書く。

……予定だったんだけど1-6月のことを思い出すのがめちゃくちゃ難しいのでやめた。

今年一番のニュースは、うーん、やっぱり転職ですかねえ。
転職したことでいろんな人に会って、いろんなことを教えてもらって、世界が広がったなーと思いました。
具体的には Ruby コミッタの人と話すようになって、crubyのソースを普通に読むようになったことですね。
「やればできる」の幅が広がったのが嬉しいし、C言語とかを普通に読み書きできるようになりつつあります。
言語とかOSとかのレイヤまでちゃんと降りていって話ができるようになるよいきっかけだったと思います。

他には、いろんな知り合いが増えたのですが、新しい人と会うとなんとなく多面的になる気がしますね。
「ある人との関係性における自分」というのが人ごとにできるのでその分だけ。
そういう意味でしがないラジオ関連、特にずっきーさんとの交流ができたのは大きい気がしました。

昨年の振り返りを見てみるとこんな感じ。

  • ブログもっとかくぞ
    • ✗: 42記事 → 37記事
  • 定量的にはかれるようにするぞ
    • △: 作ったけどそんな使ってない

やはり大晦日に入れた気合はアテにならない……。

chrome拡張 OneTab が便利

Firefox 57が出た後、しばらく浮気をしていたもののなんだかんだあって結局 Google Chrome に戻ってきました。

思えば IE で育ったあとに unDonut を使い始め数年、10年くらい前にchromeの存在を知ったあとはずっと使い続けてきた一番のお気に入りソフトであるわけです。しかし、その長きに渡るインターネット生活を一変させる chrome 拡張に最近出会いました。

それが OneTab です。

chrome.google.com

使い方はかんたんで、いれたあとは「タブ多くなってきたなー」というときに押すだけ。
開いているタブ(のうちピン留めされていないもの)をすべてリスト化して1ページにまとめてくれます。
すげー単純なんですがこれが割りと便利です。

タブの整理をするときって、すでに狭くなってる中で要不要の判定をしていたので、それがわかりやすいタイトルで並ぶだけでも結構価値があります。
さくっと試せるのでいれてみてはいかがでしょうか。