などのように書かれています。たとえば Bool は True と False の2つの値からなる集合だし、Intは整数の集合というように、型は値の集合というふうにみることができます。それならば型などと呼ばずに集合と呼べばいいと思いますが、「異なるものには異なる名前をつけろ」という先人の教えを信じれば、型というのは集合とは似て非なるものということになります。

型とは何か
型としての命題
論理パズルに挑戦
排中律の悪魔
採用情報

型とは何か

では型は何者なのかというと、それは個々の型理論によるので一概になんだというのは難しいものです。たとえばマーティン・レフの型理論では型はSetoidのようなものと解釈されるし、ホモトピー型理論では空間として解釈されるし、Cubical型理論では立方体集合の何かで解釈されるし、という具合で、型理論では型が単なる集合として扱われることはまずありません。

そんな深遠で小難しい型ですが、プログラミングをする上で式や値の型を考えるというは極めて自然なことでもあります。たとえばシェルスクリプトでは明示的に型を書くことはありませんが、値がただの文字列 String なのか、それとも文字列のリスト [String] なのか、プログラマーは必ず頭の中で区別しているはずです。たとえ動的型付け言語であったとしても、ここはスカラコンテキストだとか、この変数の中身は数値だとか、意識しているはずです。

ド・ブラウン(De Bruijn)は、数学において（型なし集合論であるZF公理系などと比較して）型付き集合を採用することを熱く主張していました。彼の言葉を引用すれば、

I believe that thinking in terms of types and typed sets is much more natural than appealing to untyped set theory. Here the word natural of course refers to our mathematical culture and not to the nature of things or to the nature of mathematics.
型と型付き集合の観点から考えることは、型なし集合の理論に訴えるよりもはるかに自然だと思います。ここで言う「自然な」という言葉は、もちろん私たちの数学的文化を指し、物事の性質や数学の性質を指すものではありません。（Google翻訳）
---- 『On the roles of types in mathematics』 N.G De Bruijn

拡大解釈かもしれませんが、同じことはプログラミングにも当てはまるのではないかと個人的には思っています。ド・ブラウンの熱い語りが個人的に大好きなのでもう少し引用しますが、

If we have a rational number and a set of points in the Euclidean plane, we cannot even imagine what it means to form the intersection. The idea that both might have been coded in ZF with a coding so crazy that the intersection is not empty seems to be ridiculous. (中略) Some types might be considered as subtypes of some other types, but in other cases two different types have nothing to do with each other. That does not mean that their intersection is empty, but that it would be insane to even talk about the intersection.
有理数とユークリッド平面上の点の集合があるとして、それらの交点を形成する意味をイメージすることはできません。両方をZF公理系にクレイジーに符号化すれば交点が空ではないとみなせるかもしれない、という考えはばかげています。（中略）一部の型は他の型の部分型と見なされる場合もありますが、そうでない場合は2つの異なる型は互いに関係ありません。それは交点が空であると言っているのではなく、交点について話すことさえ正気ではないということです。
---- 『On the roles of types in mathematics』 N.G De Bruijn

世の中には動的に型変換してよくわからない意味論の演算子をひたすら発明しているプログラミング言語もあるようですが、そのようなことはばかげているのであって、そのような演算子は便利でないと言っているのではなく、そのような演算子について話すことさえ正気ではない、ということです。（と私は感じました。）

型としての命題

そんな型ですが、Haskellerであれば（いやそうでなくても）ぜひ知っておきたいことがあります。それは俗に、型としての命題(Propositions as Types)と呼ばれるものです。これはカリー＝ハワード同型対応(Curry-Howard correspondence)とも呼ばれます。（このカリーとはハスケル・カリー(Haskell Brooks Curry)のことで、プログラミング言語Haskellの名前の元になった人でもあります）。

1934年、カリーはA -> Bという関数の型が「AならばB」という命題として読み替えることができるという興味深い事実を発見しました。さらにA -> B型の式（つまり関数）がこの命題の証明と対応することにも気づきました。その後の1969年、ハワードはカリーの考察をさらに推し進めて、同じ対応が自然演繹と単純型付ラムダ計算にも成り立つことをみつけ、さらにこの対応が表面上のものではなく、もっと深く対応していることを指摘しました。つまり式の評価が証明の簡約に対応していたわけです。（詳しい歴史については Propositions as Types - Philip Wadlerを参照してください。）

このPropositions as Typesという標語は、単に型が命題とみなせるというだけでなく、その型の式は命題の証明とみなせる(proofs as programs)というより深い対応があり、さらに式の評価はちゃんと証明の簡約に対応している(simplification of proofs as evaluation of programs)という、最深部まできっちりと対応しているということを言います。これは恐ろしい事実で、とても偶然一致したなどという話ではありえません。

とはいえ、こんな難しい話を聞いてもピンとこないので、実際に簡単な命題論理をHaskellで証明してみましょう。Propositions as Typesでは、命題を型であらわし、その型の関数を実装することで命題を証明する、という風に考えます。

まずは命題論理の基本的な推論規則であるモーダスポネンスを証明します。モーダスポネンスとは、「AならばB」と「A」が成り立つならば「B」も成り立つ、というものです。これをHaskellの型で表せば、

modus_ponens :: (a -> b) -> a -> b

という風になります（Haskellでは型変数は小文字なのでaやbを使いました）。これを実装するのは簡単で、

modus_ponens :: (a -> b) -> a -> b
modus_ponens f a = f a

となります。これは簡単というよりも、むしろこれ以外の実装方法でまともなものはひとつもありません。（ほかの実装がありうるか考えてみてください、実はほかの実装がいくつかありえます… しかし今はそのことを忘れておきます）。

これは注意すべき事柄で、つまりあなたはこの型(a -> b) -> a -> bをみただけで、実際の実装をみなくても、その実装がほぼ完全に分かったはずだということです。もし関数を実装することが命題を証明することならば、当然めちゃくちゃな実装が許されるはずがありません。逆にもし実装できたのであれば、あなたはHaskellによる証明のチェックを通過したのであり、その実装はほぼ間違っているはずがない、ということでもあります。もちろん、これは極端な例ではありますが。

おれは仕様書を書かない、なぜならHaskellの型が仕様書だからだ！と豪語してまわりの反感を大人買いしているHaskellerがいるかもしれませんが、彼/彼女のいうことにも真理があったわけです。

次は三段論法を証明してみましょう。三段論法とは、よく知っているとは思いますが、「AならばB」と「BならばC」が成り立つならば「AならばC」が成り立つ、というものです。これをHaskellの型で表すと、

syllogism :: (a -> b) -> (b -> c) -> (a -> c)

となります。これもまともな実装は一通りしかなく、

syllogism :: (a -> b) -> (b -> c) -> (a -> c)
syllogism f g = g . f

となります。

さて命題論理では命題の否定￢があります。これはどのように型で表せれるのでしょうか？単純には表現しづらいですが、少し見方を変えるとできます。「Aでない(￢A)」というのは、もしAが証明できてしまったら矛盾している、という風に考えることができます。では矛盾している命題、つまり証明できていはいけない命題は型で表現できるのでしょうか？

証明＝実装なので、証明できてはいけないのならば、絶対に実装できない型でなければいけません。Haskellでは空のデータ型を使うことができます。

data Bottom

この界隈では矛盾のことをよくボトム(Bottom, ⊥)と呼びます。名前はさておき、このBottom型は、普通ならあるはずのデータ型宣言の右側がありません。つまりデータコンストラクタがないため、このBottom型の値を作成することはできません。よってこれが矛盾を表す型として使えます。

そして「Aでない(￢A)」というのは、Bottomを使ってA -> Bottomという型で表すことができます。もしAの値が手に入ると、この型の関数を使ってBottomを作れてしまい矛盾します。つまりAの値は手に入らない、ということを表しています。

命題の否定が手に入ったので、さっそく対偶が成り立つか確認してみましょう。対偶とは「AならばB」ならば「￢Bならば￢A」というものでした。これをHaskellの型で書くと、

contra :: (a -> b) -> (b -> Bottom) -> (a -> Bottom)

となります。少しややこしい型になりましたが、これも以下のように実装することができます。

contra :: (a -> b) -> (b -> Bottom) -> (a -> Bottom)
contra f notb a = notb (f a)

この a -> Bottom は頻繁に使いますが、型としては少し読みづらいので型シノニムを使って別名をつけておきます。

type Not a = a -> Bottom

これを使うと先ほどのcontraの型は以下のようになります。

contra :: (a -> b) -> Not b -> Not a

論理パズルに挑戦

ここまでで大分こつが掴めてきたと思います。せっかくなのでもう少し面白いものを解いてみましょう。

『不思議の国のアリス』で有名なルイス・キャロル(Lewis Carroll)は、実際にはオックスフォード大学の数学の教授だったそうです。彼が論理とナンセンスが大好きだっただろうことは本からよくわかりますが、彼は一般人向けに論理的な思考の訓練のためのパズルを作成していたそうです。ということで、このWebサイト(3E Lewis Carroll Puzzles)からキャロルの問題をいくつか引用します。

（a）すべての赤ちゃんは非論理的です
（b）クロコダイルを手なずけられる人は嫌われません
（c）非論理的な人は嫌われています

さてこの３つ文から導けることは何でしょうか？赤ちゃんはクロコダイルを手なずけられるでしょうか？答えは、手なずけられない、です。それをHaskellで導いてみましょう。

まず文章を命題論理として扱うために、すべてを記号に置きかえます：

B : 赤ちゃんである
L : 論理的である
M : クロコダイルを手なずけられる
D : 嫌われている

このように記号を置けば、上の３つの文章は次のように言い換えることができます：

(a) B -> Not L
(b) M -> Not D
(c) Not L -> D

この３つを前提として、導きたい答えは「赤ちゃんはクロコダイルを手なずけられない B -> Not M」です。これをHaskellの型であらわすと、

puzzle :: (b -> Not l)
       -> (m -> Not d)
       -> (Not l -> d)
       -> (b -> Not m)

となります。かつてない長さの型ですね。実装は思ったよりもストレートです：

puzzle :: (b -> Not l) -> (m -> Not d) -> (Not l -> d) -> (b -> Not m)
puzzle b_notl m_notd notl_d b m = m_notd m (notl_d (b_notl b))

排中律の悪魔

命題論理では「AならばB」のような含意のほかに、「AかつB」や「AまたはB」なども記述できます。これらもHaskellの型で表現することができて、それぞれ、「AかつB(a, b)」、「AまたはBEither a b」と書けます。以上を組み合わせることで表現できる論理は直観論理(intuitionistic logic)と呼ばれます。

今まで見てきたように、直観論理における証明は、具体的な式を実際に構成してみせることで行います。この構成的な性格のため、直観論理では古典論理で成り立ついくつかの命題が成り立ちません。たとえば二重否定の除去(￢￢AならばA)や排中律（Aまたは￢A)を直観論理で証明することはできません：

-- 二重否定の除去
double_negative_elim :: Not (Not a) -> a

-- 排中律
excluded_middle :: Either a (Not a)

だとすると、直観論理はなにか不整合があるのかと思われるかもしれませんが、そういうわけではありません。直観論理においては、排中律は肯定することも否定することもできないので、独立した公理としてみなされます。つまり、もし排中律を公理として直観論理に足したとしてもなにも矛盾は起きません。そういう意味で、直観論理は古典論理よりも一般的で豊かな論理であるとみることができます。

「直観論理では排中律を肯定することも否定することもできない」と書きましたが、この証明はちょっと興味深いものなので、ここで紹介します。排中律を肯定することができないというのは、なんとなく分かりますが、否定することができないとはどういうことでしょうか？

実は直観論理では排中律の否定を否定的に証明できます。これは相当むずかしいので、論理パズルが簡単すぎた方はぜひ挑戦してみてください（証明の答えは、このずっと下に出てきます）。

lem_irrefutable :: Not (Not (Either a (Not a)))

二重否定の除去(￢￢AならばA)は直観論理にはないことに注意してください。この関数はその実装の形から、排中律の悪魔(the devil of the excluded middle)と呼ばれることもあります(Call-by-Value is Dual to Call-by-Name)。この悪魔には面白い寓話があるので、最後にそれを紹介します。

昔々、悪魔が男のもとにきて言った。

「(a) 君に10億ドルあげるか、(b) もし君が10億ドルくれたらどんな願いでも叶えてあげよう。ただし、(a)か(b)のどちらを提示するかはおれが決める」

男は用心深く、魂を明け渡す必要があるか確認した。「いいや、君がする必要があるのは申し出を受け入れることだけだ」と悪魔は答えた。

男は考えた。もし(b)を提示された場合、願いを買うことはとてもできないが、しかしこのチャンスを利用したところで何か害があるわけでもない。結局、男は「受け入れます」と答えた。「それで(a)なのか？(b)なのか？」

悪魔は少し考えて「(b)だな」と答えた。

男は失望したが、驚くことはなかった。それはそうだと思った。しかしどんな願いでも叶えられるという申し出は男を蝕んだ。それから男は何年もお金を貯め始めた。時には悪いこともした。そしてそれこそが悪魔の狙いだったんだろうとぼんやりと思った。やがて男は10億ドルを手にし、そして悪魔が再び男の前に現れた。

「ここに10億ドルある」そう言って男はお金を手渡した。「願いを叶えてくれ！」

悪魔はお金を手に取り、男に言った、「あれ、おれは前に(b)なんて言ったっけ？ごめん、(a)のつもりだったんだ。君に10億ドルあげれてとても嬉しいよ」そういって悪魔は、今受け取ったお金をそのまま男へ返した。

---- Call-by-Value is Dual to Call-by-Name, Philip Wadler

この話だけ読んでも意味不明ですが、排中律の否定の否定の実装と見比べると意味がわかります。ということで、先ほどの答えを書きますと、

lem_irrefutable :: Not (Not (Either a (Not a)))
lem_irrefutable choose = choose (Right (\money -> choose (Left money)))

となります。話に合わせて変数名をchooseとmoneyにしてみました。このchooseはいわゆる継続(continuation)になっており、悪魔はまず最初に男にRightつまり(b)を渡しておき、そのあとでもし男が10億ドルのお金を持って戻ってきたら、ただちにLeftつまり(a)に切り替えて継続を呼びなおす、というとても悪魔らしいずるいことをやります。この式を計算的に実行するとそのように解釈できる、という話でした。

いかがでしたでしょうか。少しでもHaskellと型に興味を持ってもらえたら幸いです。

採用情報

朝日ネットでは新卒採用・キャリア採用を行っております。

2019-10-21

エンジニアが育休を取ってみた　～育休取得と復帰後の生活実態～

はじめまして。朝日ネットの 223 と申します。

今回はテクニカルな話から離れてプライベートと仕事の関わりについて自分の例を紹介してみたいと思います。仕事をしながらどんな日常を過ごすのか、実態が気になる方もいると思うので参考になればと思います。

執筆者の現在の状況はこんな感じです。

これを執筆時点で入社13年、ほぼすべての期間を運用監視の部門に所属。現場の人間としては古株の部類。
妻と4歳半、3歳の子がいる。
第2子出産の際に6か月育休取得、産前に2カ月含めて復職まで8カ月程度休んでいる。

育休を取る事にする

個人的に会社と家との関わりの中で一番大きなイベントだったのですが、運用部門で過ごしていた入社9年目、ちょうど3年ほど前になるのですが、表題の通り育休を取得しました。発端は我が家で第2子の出産前トラブルで妊娠30週から出産まで妻が長期の管理入院になった事でした。その間の第1子の面倒は自分が見るという事にして、仕事はどうしようと考えた時に育休取得前提で進めようと思いつつ、一方でリモートワークも選択肢として考えていたのですが、その点を上長と総務とで話し合いをしたところ、速攻で

「リモートは無理だべ」

と返事が返ってきて育休が取得が決定しました。実際のところ、1歳半の相手をワンオペで行おうとすると何かやる事ができるのは子供が寝ている数時間が限度で、起きている時に仕事でもやろうものなら横から何されるか分かったものではないです。1歳半を甘く見てはいけません。

休みに入ってから

という事で、妻の入院開始のタイミングで仕事から外れる事になり、一旦6か月の育休を取る事としました。正確には育休は「出産した日」からしか取得できないので、その前は産休は無いので有休扱いなのですが、その期間を含めて8カ月ほど職場から離れる事になりました。第1子の時から「男はおっぱいあげる以外全部やるよね」の精神だったのでワンオペ育児でもオペレーション自体はあまり変わらなかったのですが、元々運用の仕事をしながら、子供の相手とサーバの相手って

普段と違うやばい事があると何かしらのメッセージを発する（だから普段の様子はきちんと見ておけ）
やばい兆候を見逃すor放置すると、よりやばい状態が特大ブーメランで返ってくる（だから気が付いたらすぐに対処を考えろ）
馬鹿正直に動く（なのでリソース配分は気を付けて）

というあたりで共通点があるよね、と思っていたのでやる事がガラリと変わったという感覚はありませんでした。

出産後

母子共に生還でき、育休期間が始まりましたが、妻は長期入院で体力が相当に落ちてしまい回復が思わしくなく、その後も育児は私がメインでした。

復帰までの間、会社の人間とコンタクトをとる機会が以下のような感じでありました。

部署に新規メンバーが入社したので歓迎会に来ないかというお誘い（日程が出産日の翌日でタイミング悪くてごめんなさいした）
同僚が陣中見舞いとして我が家を訪問
会社で子育て中のメンバーでのランチ会

最後のランチ会ですが、朝日ネットでは数カ月に一回程度のペースですが、育休中の社員、これから産休育休に入る社員、子育て真っ最中の社員で近況報告＋情報交換＋その後の会社の動きを共有する会を自由参加で行っています。私も育休中に2回ほど顔を出し、復帰後も声かけてもらって参加しています。育休中の社員が子連れで来ることもあり、和やかな会となっています。

復帰の時

育休5カ月が過ぎたあたりでも妻の状態がよろしくなかったため育休を伸ばすかどうか考えたのですが、長期戦になりそうでだらだら伸びそうな予感がしたため、その状況を会社に伝えた上で、保育園、一時保育、地域の子育て支援、祖父母の協力を総動員し、復帰前提の体制を整えることにしました。（総務の方は延長するものだと思っていたらしく「お前達観しすぎだろ」とツッコミを受けました）

その後

復帰後も家庭の方でトラブルは続いたのですが1年少々で何とか落ち着き、現在は平和な生活に戻る事ができています。家族みんな元気なのはよいのですが、出産トラブルの修羅場を乗り越えた母子が微妙に強くなっており、特に第2子の横になると飛んでくるヒップアタックと就寝中に飛んでくるかかと落としが最近馬鹿にならない威力になっているのが悩みどころです。

仕事的には現在は運用監視業務＋その業務改善＋教育担当的な役割を担う立ち位置についていて、育休当初よりも求められるものが多くなっています。

f:id:watanabe06:20191017120459p:plain

最後に

朝日ネットでは男性社員の育休は私が2例目で、技術系の部門では最初だったのですが、その後、技術系部門の一般社員以外にも部長と執行役員が育休取得という例が続いています。女性社員も3人目を出産後に普通に復帰している方もかなりいて「●●さん育休なんだ。いつ復帰するの？」というような空気が日常になっているように思います。家庭と仕事との両立はやりやすい会社なんじゃないかなと思います。この文章を執筆する段階で男性社員の育休は5例ほどありますが、女性社員に関しては正直数えるのが面倒なレベルで、9月に行ったランチ会には復帰後の社員、これから産休に入る社員、休職中の社員合わせて15名が参加しています。（お子様も3名ほど参加していました）

復帰後に個人的には育休中の変化には割とすぐに追いついたのですが、以前の仕事を塩漬けで覚えている必要はなく、今の状況を把握して改めて自分にインプットする方が復帰の時は大事だなと思いました。仕事を忘れるという事はそこまで恐れなくてもよいのかなと思います。

1日の例にも書きましたが、自分の時間を作ろうとしないと作れない感じの日々ですが、会社に来ると自分のペースで時間配分ができて周りと言葉でコミュニケーションがとれるのがありがたいと感じます。（自宅にいるモンスターには主導権取られっぱなし）

2019-10-15

BigQuery+Tableau でデータ分析環境を作った話

はじめに

こんにちは。朝日ネットでWebアプリケーションの開発を行っている tommy です。

昨年、BigQueryとTableauを使った、ちょっとした、社内データの分析環境を構築しました。
今回は、そのことについて書いていこうと思います。

2019-10-09

朝日ネットにおけるソフトウエア・ロードバランサーの導入（第5回）

HAProxy pfSense

朝日ネットでのインフラ設計・構築を担当しているラピー・ステファンです。前回の冗長構成・拡張可能な設計の説明に続き、今回は運用負担を軽減する便利な設定について紹介します。

第1回第2回第3回第4回

2019-09-26

SmokePingのMaster/Slaveを、もくもくと設定する

お前は誰？

はじめまして、朝日ネットのkenji-as4685と申します。
現在は、今年の4月から新設された『サービス基盤部』という部署に所属しており、主にネットワークの回線サービス(PPPoE/IPoE)のサービスレベルの定義、サービス品質の可視化を担当しております。

お前は誰？
で、なに書くの？
SmokePingってなに？
で、SmokePingでなにしたいの？
SmokePingのMaster/Slaveってなに？
Master/Slaveでつまずくポイント
- ポイント1(secretファイルのパーミッション)
- ポイント2(slaveサーバの名前解決)
- ポイント3(MasterのRRDディレクトリのパーミッション)
おわりに
採用情報

で、なに書くの？

4月の異動より、ネットワークのサービスレベルの(再)定義と、可視化を上司より言い渡されまして、でもネットワークの品質といえば、やはり『パケットロス』と『遅延』が一番わかりやすい、ということもあり、また、過去に所属した会社でSmokePingによる可視化を行っていたので、朝日ネット版SmokePing導入の話を書きたいと思います。

なお、SmokePingは現在、単純にインストールだけならyumやaptコマンドで出来ます。また、基本的な設定は、日本語で書かれている多数のブログ情報もいろいろありますが、しかしながら、特に、SmokePingの有用な機能のひとつ『Master/Slave』は、日本語の情報が少ないので、せっかくなのでこちらで紹介させていただければと考えました。

朝日ネット　技術者ブログ

朝日ネットのエンジニアによるリレーブログ。今、自分が一番気になるテーマで書きます。

Peering Asia 3.0 参加レポート

AD環境のホスト再構築でDNS解決ができなくなる

Haskellの型と直観論理

型とは何か

型としての命題

論理パズルに挑戦

排中律の悪魔

採用情報

エンジニアが育休を取ってみた　～育休取得と復帰後の生活実態～

育休を取る事にする

休みに入ってから

出産後

復帰の時

その後

最近の日常

最後に

BigQuery+Tableau でデータ分析環境を作った話

はじめに

朝日ネットにおけるソフトウエア・ロードバランサーの導入（第5回）

SmokePingのMaster/Slaveを、もくもくと設定する

お前は誰？

で、なに書くの？