ふたたび移転、統合

しばらく休んでましたが、実は水面下ではてなダイアリーからはてなブログに移転実験をしていました。このたび実験が終わって本移行したので、お知らせします。
http://blog.kino3.jp/
結局、事務所やら研究所やら分離していくと、新しいのができるたびにXX所になってめんどい、という根本的な問題を解決できず、どんなネタでも同じところでやる、ということに落ち着きました。そのほうがアクセス数伸びないと思いますが、それが現実でしょう。だから、Agdaの話も日常話も同じところでやります。どちらも日常です。

Agda2.5.1のWindowsへのインストール/バージョンアップ

このたびAgdaを最新の2.5.1にバージョンアップしたので、手順を記録しておく。
特に、新しくなったライブラリ管理の設定方法がややこしかった。手順は主に以下に従った。
http://hackage.haskell.org/package/Agda-2.5.1/changelog
何にせよ、ようやくまともにインストールできるようになって嬉しい！

Agdaのインストール

1. 古いHaskell Platformをアンインストール(バージョンアップの人は)
2. 新しいHaskell Platformをインストール
3. cabal update*1
4. cabal install -f -cpphs
   • 相変わらず日本語環境だと-f -cpphsが必要な模様。

Emacsの設定

1. 以下の2行を.emacsに追加する*2。

   (load-file (let ((coding-system-for-read 'utf-8))
                   (shell-command-to-string "agda-mode locate")))
   



2. emacsを起動して以下のhoge.agdaを作成する。

   module hoge where
   



3. Ctrl-c Ctrl-lで型検査ができればインストールOK。

標準ライブラリのインストールと設定

1. The Agda Wiki - Standard Libraryからダウンロードするか、Githubからとってくる。適当な場所に展開する。
2. これからlibrariesという名前のテキストファイルを作る。まず、その置き場を以下のようにして探す。

   C:\Users\Shuji>agda -l hoho piyo.agda
   Library 'hoho' not found.
   Add the path to its .agda-lib file to
     'C:\Users\Shuji\AppData\Roaming\agda\libraries'
   to install.
   

   この場合C:\Users\Shuji\AppData\Roaming\agda\の下にlibrariesという名前のファイルを置く。agdaというフォルダがない場合は自分で作る。



3. librariesには、さきほど展開した標準ライブラリの中にある、standard-library.agda-libというファイルのフルパスを書く。つまり、こんな感じ。

   C:\Users\Shuji\Documents\agda-stdlib\standard-library.agda-lib



4. defaultsという名前のファイルを作成し、同じ場所に置く。中身は以下の1行。

   standard-library

このやり方はchangelogに書いてある3通りの方法のうち、3番目に該当する。何か作るのに標準ライブラリしか使わない人は、これでよいと思う。

あと、最初はgnupackのemacsにインストールしようと試みたのだが、どうもシェルの扱いかディレクトリ構成の扱いかが特殊のようで、よくわからず断念したことをメモしておく。

*1:このときwhere cabalなど入力して、新しいHPのcabalを叩いていることを確認したほうがよい。新しくインストールしたcabalが実行されるようになっていなければ、環境変数PATHの優先順位を見直す

*2:emacsを使っていない人には、NTEmacs / Emacs for Windowsの「24.5簡易IME対応版」をおすすめしておく。また、環境変数HOMEは適当な場所に設定されているものと仮定する。HOMEの下に.emacsができる

Agda2.4.2.4へのバージョンアップ

以前、2.4.2.2のインストールでだいぶ手こずった話を書いて、Agdaをやってみようという方の気をそいだ感があるのだが、このたびリリースされた2.4.2.4へは素直にバージョンアップできた。cabalを叩くだけで。

ちなみに、次のリリースは2.4.4で、ライブラリの管理方法とかいろいろ変化があるらしい。変化することもうれしい人にはうれしいのだが、もうちょっと万人が使えるようなstableなリリースを出したほうがいい、という面もあるように思っている。そのためにはAgdaからforkせざるを得ないのか、なんとか追従しながらやっていけるのか、などなどを研究のかたわらに妄想している。

関数型言語とまちづくり

関数型のプログラミング言語と、まちづくりには大きな関係があると思っている。大きな関係がある、というのはちょっと曖昧だが、ぱっと思いつくところでは

1. 地方創生あるいは過疎、人口減少という中で、徳島のサテライトオフィスのように、関数型プログラミング言語でのソフトウェア開発拠点となりますよ！という市町村があってもよいし、あると面白いと思っている*1
2. 行政で利用される業務アプリケーションは、航空や原発のようなミッションクリティカルな部分の制御系システムとは別の意味で、高信頼性が必要とされている。そういう意味でも、関数型言語での開発は向く

という点がある。どちらも、「じゃあ事例を見せろ」と言われそうで、その事例をつくるのがぼくの今後10年ぐらいのテーマだと思っているのだが、とにかく、思いついたうちに言うのが花だと思うので、言いっぱなしておく。

*1:自治体の方で興味があればご連絡ください

すっかり忘れてたけど、Agdaという名前の由来

去年のProofsummitのときに、Agdaという言語はなぜそういう名前なのかという話を飲み会でしたら結構好評だったので、あらためて調べたことも含めて。

Agdaとは何かというと、これのことみたい。

実際、Agda the henでググってみると
http://bit.ly/1aBKbbH
という本が出てきて、明確に

The name Agda comes from a Swedish song about Agda the Hen, a pun on the Coq rooster.

と書いてある。(le )Coqはフランス語で雄鶏。で、Agdaはフランス語じゃないけど、スウェーデンの歌に出てくる雌鶏の名前ですよと。

で、さらによくできている話が、Coqを作った人のひとりThierry Coquand*1の奥さんCatarina Coquand（この人ですね）がAgda1の開発メンバのひとり、ということだそうで。このあたりの歴史は

• http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.History
• http://ocvs.cfv.jp/Agda/index.html

にあります。

*1:Calculus of Constructionの人という意味でそう書いてますが詳細は知りません。。。

3度目の圏論

神奈川大学圏論勉強会
https://gist.github.com/kino3/37ee4c6e2d57e490bed6

というのを作って、圏論の勉強をはじめた。JCLoveという怪しい感じのネーミングにしてみた。NAISTの修士時代、去年5月ぐらいからNAIST時代の先輩とリモートで勉強会をやろうとしたとき、いずれも挫折したり多忙で消滅したりしたので3回目になる。3度目の正直に期待したい。

しかし、ただ期待するだけではなく、今回はいけそうな感触もある。なんだかよくわからないのだが、継続した勉強の成果か、最近いろんなこと（特に数学的な概念）が「わかる」という実感がある。最初はさっぱりだったモナドも最近はしっくりくるようになったし、Agdaのいろんなことも、最近は人に説明できるようになった。一度わかった側に行く、向こう岸に行ってしまうと、わからなかったときの気持ち、がわからなくなってしまうのだが、そのあたりをうまくモナディックに保存しつつ生きていきたいと思う。

で、圏論だが、久々にAwodeyやMacLaneの本をパラパラ見ていたら、いままではしっくりこなかったこと（例えばモノイドの圏はオブジェクトがひとつ、とか）が、「そりゃそうやよね」と思えるようになっていた。ただ時間だけが解決することもあるのだなあと思いつつ、葉桜を見上げて、遠くの富士山を眺めつつ、朝のキャンパスを散歩する。

Agdaで画面づくり、は結構いけると思う話

http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/
でポスター発表してきました。ポスター（実態はスライド）も
http://www.slideshare.net/ShujiKinoshita/ppl2015-uivalidationfull
に置いてますが、それだけだと何のことかわからない部分も多いので補足しときます。
主に、PPLにいたけど同じ時間にポスター発表していて、聞いてない人向けです。

• 問題
• その問題は解決するに値すると思う理由
• その問題の解決方法
• 解決できそうだと予想する根拠

に分けて話します。

【問題】

• 残念なぐらい使いにくいソフトウェアとかサービスがたくさんある

【その問題は解決するに値すると思う理由】

• ソフトウェアやシステム、サービス、というのはほとんどの人間が日常的に触れるもの。
• 業務でパソコン等々の電子機器を使うなら、画面とにらめっこする人は多い
• クリティカルなシステム（例えば原発内で稼働するソフトウェアとか）ではオペミスが致命的なことになる。オペレーションがうまくいく、人間はストレスを感じず操作できる（つまり、画面は妥当である）、ということも何らかの形で保証したい。
• クリティカルでないシステムでも、日常的に触れるシステムが使いにくい、というのは問題。そのストレス指数みたいなものが明確に数値化されていないから、問題ではないと思っているだけで、実はものすごく問題。ユーザのイライラの総和は侮るべからず。

【その問題の解決方法】

• ソフトウェアの画面記述言語としてAgdaを使う。要するに、Agdaコードから画面用コードを自動生成するジェネレータというかコンパイラをつくる。
• Agdaの「プログラムとその性質の証明をあわせて書ける」という性質を利用して、画面定義と、その妥当性の確認を一緒に書く

【解決できそうだと予想する根拠】

• ソフトウェア一般の妥当性確認は難しいが、画面の妥当性に限れば、既存研究がたくさんある。主にユーザ中心設計（UCD）やUI/UXデザインの諸分野。ただし、形式化するという話はあまりないので、それをやる、ということ
• 形式化はできそう。やり方はいろいろ考えられるが、とにかくドキュメントの成果物を（あまり構造を考えずに）Agda上にのせるだけでも、「画面が変更になったらドキュメントも変更しないとダメ」という程度の簡単な型検査には落とせると思われる
• あるいは、「主な業務は3クリック以内で終わる」だとか、「主な業務は10秒以内に終わる」というようなことはAgdaで記述、証明できそう。
• システムの妥当性確認の分野でよく使われる、アシュランスケースをAgda上で形式的に記述できることは知られている
• Agdaで書いたアシュランスケースからXMLを出力して、それをEclipse GMFでグラフィカルに表現するツールは既にある。つまり、Agda to HTMLは技術的には（Agdaの実装をいじれば）そんなに難しくはない。
  • あわせて、Agdaとグラフィカルな表現が1対1対応できれば、グラフィカルなモックアップからのAgdaコード生成なんかもできるし、モックアップのコードをそのまま本番でも使う、というような流用も容易。

といった感じですが、もう少し面白いと思ってもらうには動くデモがないとダメだなあと痛感しました。動くデモができたら、またどこかで喋りますのでよろしくお願いします。全国1000万もとい1000人ぐらいのAgdaユーザの皆様よろしくお願いします。