Just $ A sandbox

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

鬱モード全開だったときに

今から大体3年くらい前の、大学学部2回生の頃に唐突に精神が死んだことがあった。

という話をするけど、この先読んでも特にオチはありません。
ただの身の上話なので。

非常に運がよかったため自分は3回生の進路振り分け的なものに必要な単位を前期で全て揃えていたので これによる留年及び進路が狭められるといった良くない結果が将来にもたらされることは一切なかった。
これがもう2-3ヶ月早く発症していたら、専門も2回目の語学も落として無事留年が確定していたので運がよいというレベルではなかった。

で、精神が死んでいた頃、毎日大学にも行かず、家でずっとつらいつらいと思いながら日々を過ごしていた。
具体的に言うと次のような一日を過ごしていた。

  • 朝11時前後に起床する。今日も2限に寝坊したという絶望感と、そのくせに全く疲れが取れておらず、眠いし体中のだるさに悲しくなる。
  • ﾂｲｯﾀｰ等を眺めるが眠いしどうでもいいツイートが並んでいてつまらない。けれど何もやる気が起きないので30分くらい見てる。
  • 起きるのが遅いので昼ごはんも遅くなる。12時半くらいにご飯を食べながら、いやいやもう3限目今更行ってもしょうがなくないか…という気持ちになる*1。
  • 13時を過ぎてやはり3限目に行かなかったことにじわじわ罪悪感を覚え始める。
  • 暇すぎて趣味(絵/プログラミング/ゲーム/勉強etc)をするが眠いし全く脳が働かず、集中できず10分も持たない。どうでも良いことをネットで調べたりぼーっと動画を見たりして時間を潰す。
  • 気がつくと4限・5限もぶっちしている
  • 19時を回り「今日も何もしなかった…」と思う。
  • 22時を回り段々目が冴えてくるが「今じゃないんだよ」という気持ちになる
  • 2時ごろになって「そろそろ寝ようかな」と思う
  • 布団に入るが全く眠れない。布団の中で「明日もまたこの無意味な一日を繰り返すのか」と思って悲しくなる。
  • 実際に眠るのは布団に入って2-3時間後

自分は趣味が多いほうだと思っていたのだけれど、どれも全く楽しめず、集中力も持たないのですぐやめていた。
結局自分から何も考えなくても時間が潰れる動画サイト等に行き着くのだけれど「自分は何でこんな無駄なことをしているのだろう」という気持ちがあるのでそちらでもあまり楽しむことはできなかった。

そもそも睡眠の質が低すぎて日中ずっと眠いというのが一番キツかったけれど、ずっと引きこもっているので体力が有り余った状態で布団に入っても眠れないのでどんどん睡眠のリズムが崩れるというのを繰り返していた気がする。
可能なら外に出れる状態のうちに毎日少しでも外に出るというのをやってみるといいと思う。あるいは太陽の光を直接浴びるとか。これをやるかどうかはかなり重要だと思うので今は割とそうしてる。

一応他の人につらいという愚痴をこぼしてみたりもしたことがあるが、あんまり解決はしなかったのと自分のゴミっぷりを再確認することで余計つらい気持ちになれたのであまりおすすめはしない。

で、結局どうやって解決したかというと多分外に出れたのがきっかけだったように思う。

そもそもこの生活を始めてしばらくしてから、外に出るのも怖く、大学はおろか近所のコンビニに行くために玄関に立つだけで何か恐ろしくなって行くのをやめるという感じで、一切家の外に出ることができなかった。

しかし流石にこのままではまずいと思い、大学のカウンセリングセンター的なところを訪れようと決意したのだった。
当然、カウンセリングセンターに行くには大学に行かねばならず、これは自分にとって非常に高いハードルだったので、カウンセリングを受けることを決心するのにn日、カウンセリングセンターの場所を調べることを決意するのにn日、センターの人に伝えるべき自分の今の状況を頭の中でまとめるのにまたn日というすごい時間をかけていた気がする。

まぁとにかくカウンセリングを受ける決意は固まり、しかしいきなり大学に行ってカウンセリングを受けるのは難しそうだったので、
「まずは大学に行ってセンターの前を通過し、そして改めて後日訪れよう」という感じの決意を固めて家を出たのだった。

結論から言うとこの「今日は建物の前を通過するだけで中には入らないぞ」という決意は自分の心を非常に軽くしてくれるとても良い決意だったみたいで、
結局その日は大学に行くのだけれど、大学に着いてから「あれ、でも大学来れたなら授業出ればいいじゃん」となって、その翌日から普通に授業に出始めたのであっさりと治ってしまうのだった。

まぁとにかく、この「まずは前を通過するぞ」というつらい行動を2ステップに分けるタイプの決意は非常に有効なので、
困っている人はよければ参考にしてください。

ちなみにコレ以降、ひきこもりから抜けれなくなって精神がやられるタイプの精神的なつらみはほぼなくなるのだった。
今では規則正しい睡眠リズムと毎日外に出るのは重要だなと思ってる。

おわり

*1:補足しておくとその頃とっていた授業は2限目に講義、3限目に演習というタイプのやつが多かった

Theorem Prover Haskellの紹介

Haskell 定理証明

この記事はTheorem Prover Advent Calendar 2016の1日目の記事です。

今年も残り1ヶ月になったことを信じたくないと思いつつ、
まあ学生的には4月始まりだから大丈夫と自分に言い聞かせてます。

今回のアドベントカレンダーのネタを必死に1週間くらい前から頑張って探した結果
何も見つからなかったのでHaskellで証明を書きます。

みなさんHaskellで証明を書くのはつらいと思うかもしれませんが
実はEquational Reasoningも使えるし
最近バージョンが上がって少し賢くなったコンパイラの強力なサポートも受けられるので
意外とマシです。(当社比)

さてHaskellで証明をすることについてですが、
ここでは定理証明界のFizzBuzzとも名高い*1、リストのreverse関数が2回やると元に戻ることを示します。

Leanで書いた同じ証明も置いとくので、ぜひ見比べてみてください↓
Leanバージョン

ポイントをいくつか解説します。

cong :: a == b -> f a == f b
cong Refl = Refl

-- fを具体化
congAppend :: Sing x -> a == b -> a ++ Cons x Nil == b ++ Cons x Nil
congAppend _ Refl = Refl

congは上で定義していますが、証明中ではほとんど使っていません。
どうもcongはこの形だとfの曖昧性が残るのでいちいちfを具体的にした命題を置いて使います。

これは、TypeFamiliesで定義した(Reverseとか)type functionはGHC的にはk -> kカインドの関数とは違う(type functionに対しては部分適用を認めない)ようで、fにTypeApplications拡張で直接代入しようとしても引数の数が足りないというエラーになるためです。
ここは型コンストラクタへの部分適用ができるようになればTypeApplicationsでなんとかなるはずです。

--

data instance Sing (typ :: List a) where
  SNil :: Sing Nil
  SCons :: Sing x -> Sing xs -> Sing (Cons x xs)

singleton typeです。

Listカインドの型を保持したままListの項と同型な構造を持つデータを定義します。
これは帰納法を回すときに"xsの内部の項"を引数でとるために使っています。

Haskell依存型プログラミングでは頻出のテクニックであり、
この辺はsingeltonsパッケージあたりを使うとちょっと楽になれます多分。

--

(===) :: Sing a -> Sing b -> Sing (Mk2 a b)
(===) a b = STuple a b

infixl 3 `by`
by :: Sing (Mk2 a b) -> a == b -> b == c -> a == c
by _ = trans

qed :: forall a. a == a
qed = refl

ex :: Sing a -> Sing b -> Sing c -> Sing d -> a == b -> b == c -> c == d -> a == d
ex a b c d ab bc cd =
  a === b `by`ab $
  b === c `by` bc $
  c === d `by` cd $ qed

Equational Reasoningです。
大体Agdaのと同じようなノリで定義しました。

個人的には左辺が右辺と等しい時にそれを省略できる記法を考えたかったですが
めんどくさいので実装が楽なtransをそのまま持ってくる方法を採用しました。
でも証明は同じことをなんども書くので超面倒になります。

あとは証明を読んでもらえばわかると思います。
というわけでHaskellでも比較的楽に証明が書けるよっていうアレでした。

(いや本当は全然楽ではない)
(めっちゃつらかった)
(つらいと思った人はすぐにIdrisかAgdaに助けを求めましょう)

--

*1:今考えた

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便利かよ〜〜〜
  • ここだけ別の資料なりなんなりでちゃんと勉強したほうがよさそう