Idrisと1年半まったり戯れた軌跡

このエントリはただの集団 Advent Calendar 2018 の4日目です。昨日は ishiki-hironori さんの linear-gradientを使ったいつもと違う実装例でした。

かれこれ1年半ほど社内で毎週続けていたIdrisランチ勉強会がそろそろ（あと2回ほどで）終わりそうということもあり、せっかくなのでこのエントリで振り返りたいと思います。

そもそもIdrisとは

依存型という「値に依存する型」を扱うことができるプログラミング言語です。それによって、例えば行列の掛け算をする関数だと「a × b の行列と b × c の行列を受け取って、a × c の行列を返す」ということをシグネチャに書くことができます。このような強い型によってより型安全なプログラミングができたり、証明ができたりします。ちなみに文法はHaskellとほぼ同じです。

きっかけ

書こうと思ったらtakezoeさんが書いてくれてたのでパス。

takezoe.hatenablog.com

2017年4月から11月

便利とかいうレベルを超越したショートカットに感動
ショートカットについてtakezoeさんが書いたブログがちょっと話題になる
キャストが理解できない
Scalaが太刀打ちできないレベルのコンパイルの遅さにビビる
再帰的な構造を持つデータ型が衝撃的に遅い
行列の基本演算を実装したいがとにかくコンパイルが通らない
Manningの半額キャンペーンを定期的にSlackにお知らせしていたら勉強会参加者が全員Idris本持ちになる
データストアを作る演習あたりでメンバーの心が折れ始める
演習をガッツリやらずサクサク進める方向にシフトしはじめる

社外向け勉強会

社外向けの勉強会でIdrisを扱ってみることを決める
誰も来なかったらどうしようと不安になるも、定員18人で参加者16名とかなり参加率の高いイベントになる
Haskell書ける方？と聞いてみたら8割ぐらい手が挙がる
Coqわかる方がいらっしゃったので、自分も色々教えていただく
終わったあと参加者の方に楽しかったです！と言っていただける

2017年12月から2018年3月

欅坂46にドハマリしたため食事時間にファン活動の進捗報告をし始める
このへんから証明が書けないとコンパイルができなくなってくる
「型が定義されている」と「その型の値が存在する」(type is inhabited) は違うことなのだと気づく
Refl は神
俺たちはVoidのことを何も知らなかった
Vectから値を消すだけの関数を自力で書ける気がしない
Viewを使ってデータを任意の形でデコンストラクトしてパターンマッチするテクニック登場

ScalaMatsuri

どこか狭いところでひっそりやろうと軽い気持ちでアンカンのふせんに書いてみたところ、採用→一番広いホールでのセッション、という急展開が発生
通訳さんと打ち合わせしたりした
資料は前の勉強会でやったものをベースにしたが、特に練習してなかったのでしんどかった
話し終わったあと何人か質問に来ていただけたのがありがたかったです

2018年4月〜

オフィスの配置換えにより参加者のフロアが離れ、滅亡の危機
無限が登場。totalityやらとの絡みでややこしくなる。
アクションとrun関数の分離やFuelなど、後々おなじみになる概念登場
ここでようやくミュータブルなステートを扱うことができるようになり、スタックへのプッシュ/ポップなど、めちゃくちゃ普通のプログラムを型安全に書き始める
分岐する型が登場
ステートマシンを型安全に書く。一連の手順を型にすることで決まった手順を必ず踏むことを保証させるパターンが頻出
一周回ってIdrisがシンプルに見えてくる（錯覚）
会社の書棚にType Driven Development With Idrisが入荷する。誰だ買ったの。

所感

ブルーオーシャン

Idrisは一部界隈を除いてはそもそも知っている人がほとんどおらず、難しいことやひねったネタを頑張って考えなくても人前で発表することができます。発表をやってみたいけどネタを持っていない、というような人はこういう誰も知らないようなところを狙っていくのも一つの戦略かなと思います。

わからないことをやる

定期的にわからないことに向き合って自分の頭の悪さに絶望することは必要なんじゃないかと思っています。それは変に自意識を肥大化させないためでもありますし、新しいものに対して楽観的になるためでもあります。Idris はプロダクションで使われているほとんどのプログラミング言語より圧倒的にしんどい言語なので、奴と比べれば大抵のプログラミング言語にはビビる必要はありません。

発表する

社内＆社外の人に話すために本を読み込んだり資料を作ったりした際にものすごく学習が促進されるのを実感しました。いろんなところで言われていますがやはりアウトプット大事。しかも自分の理解できるかできないかギリギリのラインをアウトプットするとめちゃくちゃ効果高そうです。

理論への関心

普段実用的なプログラミングばかりしているとどうしても理論よりプラクティカルなところに目が行きがちなのですが、こういう理論的なところをそのまま持ってきたような技術を勉強するとちょっとイメージが具体的になるのでその裏にある理論にも興味が湧いてきます。というかこれをやらずに依存型の説明をされてもまるでわかる気がしません…。

演習のやり方は悩みどころ

本の演習問題はやりたいのですが、やるといかんせん進みが遅くなるんですよね…。特にIdrisのように絶望的に慣れていない言語だと1ページに数時間かかっちゃったりします。あまりに進まないとゴールまでモチベーションが保たないと判断して後半では演習問題をすっ飛ばしましたが、やはりしっかりコードを書いたときに比べると理解度がかなり落ちちゃうので難しいところです。

次なにやるかな…