「依存関係のある値のうちの一部をrewriteしようとしたときの問題」をAgdaで書くとどうなるか

依存関係のある値のうちの一部をrewriteしようとしたときの問題 - にわとり小屋でのプログラミング ブログ をAgdaで書くとどうなるか．

こういうことだろうか？

module AC-2013-5 where

open import Data.Nat
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)

postulate
  f : ∀ n → n > 0 → ℕ
  h : (n : ℕ) → (H : 2 * n > 0) → f (2 * n) H ≡ n

n≡m→m>0→n>0 : ∀ {n} {m} → n ≡ m → m > 0 → n > 0
n≡m→m>0→n>0 n≡m m>0 rewrite n≡m = m>0

2*1>0 : 2 * 1 > 0
2*1>0 = s≤s z≤n

lemma : ∀ x
      → (eq : x ≡ 2 * 1)
      → let x>0 = n≡m→m>0→n>0 eq 2*1>0 in f x x>0 ≡ 1
lemma x eq rewrite eq = h 1 2*1>0

-- もしくはこっち？
lemma' : ∀ x → (H : x > 0) → (eq : x ≡ 2 * 1) → f x H ≡ 1
lemma' x H eq rewrite eq = h 1 H

だよね？

まぁ，元記事のHについても普通に証明書いて突っ込むので他の証明と特に変わりは無いかなと

後者だった場合，特に問題なくhにH突っ込んで終わり

kikさんによるとどうもxとHもpostulateではないかという話なので，その場合も

module AC-2013-5 where

open import Data.Nat
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)

postulate
  f : ∀ n → n > 0 → ℕ
  h : (n : ℕ) → (H : 2 * n > 0) → f (2 * n) H ≡ n
  x : ℕ
  H : x > 0

lemma'' : (eq : x ≡ 2 * 1) → f x H ≡ 1
lemma'' = lemma' x H
  where
    lemma' : ∀ x → (H : x > 0) → (eq : x ≡ 2 * 1) → f x H ≡ 1
    lemma' x H eq rewrite eq = h 1 H

かな．

前のほうでも使ったlemma'はgeneralizeした定義での証明なので，それを使う．つまり元記事でのCoqの証明と同じことをしてるかな．

(追記)chiguriさんが先にやってた．俺がスロゥリィ

パッケージを跨いだ再exportの危険性

この記事は Haskell Advent Calendar 2013 1日目後半の記事です．前半の記事もよろしく．

「ある露出モジュールAで隠蔽モジュールA.Xをimportし，AでA.Xのシンボルを選択的に(あるいはモジュールごと全部のシンボルを)露出させることで，AとA.Xを含むパッケージAから提供するインターフェースをコントロールする」ことができる再exportは，パッケージ内部でのモジュール構成をパッケージ外への公開状態とは切り離すことのできる，とても便利ですばらしい機能だ．

module A ( foo, bar, baz, module A.Y ) where

import A.X ( baz )
import A.Y

foo = ...
bar = ...

ただし，これがパッケージを跨いで行われる場合，その事情は相当異なってきて，結論から言うならば害悪だと思っている．

あるパッケージBがパッケージAのモジュールをimportし，再exportしていたとする．(実際このようなexportは多くのパッケージで見られる)

module B ( foo ) where

import A ( foo )

パッケージBの依存関係には当然パッケージAが入ってくるだろう．そしてパッケージBを使う何かプログラムCを作ったとき，パッケージBがキチンと設計されていれば，CはパッケージBに直接依存する関係は持つが，パッケージAへの依存関係は陽に持たずに済むようになっているはずだ．でなければ，このようなexportを行う意味が無い．

一方，このモジュールBで再度exportされたシンボルは，パッケージAのものであると同時にパッケージBのものでもあるという状態になる．となると，B-1.0とA-1.0の組でビルドしたときと，B-1.0とA-1.1の組でビルドしたときでは，パッケージBから露出しているパッケージAのシンボルの質が異なっているかもしれない．つまり，

• パッケージBのバージョンは変わっていないのにBから提供されているシンボルの型が変わっているかもしれない
• パッケージBのバージョンは変わっていないのにBから提供されている型のコンストラクタが増減しているかもしれない
• パッケージBのバージョンは変わっていないのにBから提供されているクラスのインターフェースが増減しているかもしれない

などなど，という事態が普通にあり得る．通常，パッケージ自身で提供しているシンボルに関し上記のような変更があるのなら，hackageのバージョニングルールに従いバージョン番号の2番目以上を上げなければならないようなケースに該当するだろう．にもかかわらず，そのことが検知されない．「パッケージ提供者がインターフェースの硬さについて保証し，変える場合はパッケージのバージョンを上げる」というバージョニングの基本に対する抜け穴になってしまう．バージョンが上がらないままいろいろ変わってしまう．

型の変更やインターフェースの減少が警戒されるのはバージョニングルール上明らかだが，前述した中で増加まで問題にしている点はすぐにはピンとこないかもしれない．たとえば，開発時に，ある環境でプログラムCをB-1.0に陽に依存させた上で，Bの依存関係的にA-1.1が入ってきた状態で作っているかもしれない．この環境からプログラムCを別の環境，A-1.0があらかじめ入っているような環境に持って行ってビルドすると，Bに対する依存関係は間違っていないにも関わらず，インターフェースが減少したのと同様の状況になり，ビルドできないことがある．そのためA-1.0/1.1の間で単に増加するだけであっても依存関係的にはマズいのだ．

このようなパッケージAとパッケージBの関係は随所に見られるが，近々に遭遇したケースを挙げると，wai-extraとwai-logger-0.3.1/0.3.2のペアがある．wai-loggerのNetwork.Wai.Logger.Format.IPAddrSourceをwai-extraはNetwork.Wai.Middleware.RequestLogger.IPAddrSourceとして再exportしている．そして，wai-loggerが0.3.1から0.3.2になったときに，IPAddrSource型のコンストラクタにFromFallbackが追加された*1．その結果wai-extraのバージョンが上がっていないにも関わらず，wai-extraのNetwork.Wai.Middleware.RequestLoggerをimportしておけば，追加したFromFallbackもまた使えるようになってしまった．つまり，FromFallbackをwai-extraにのみ陽に依存させプログラム中で意気込んで使うと，陽に依存していないはずのwai-loggerがまだ0.3.1の環境でビルドできなくなってしまう．たとえwai-extraのバージョンが同じであってもだ．

パッケージBのみに陽に依存させていればよいプログラムCから見たら，パッケージBのバージョンが上がっていないにも関わらず，何故か陽に依存していないパッケージAのバージョンアップを食らってビルドできなくなるという事態に陥る．こうなると泣く泣くプログラムCもパッケージAに依存させねばならず，ならなんのためにわざわざパッケージBがパッケージAのシンボルを再exportしてるのかというトコロに立ち戻ってしまう．

正直，こういったパッケージ跨ぎでの再exportは一切やめて欲しい．もしかすると私が気付いてない有用性があるのかもしれないが，それが一体何であっても前述したデメリットが大き過ぎて余程大きなメリットがあったとしても許容できそうにない．

*1:というかこれ追加するpull reqをしたの私だ

砂場遊びは地獄のかほり

この記事は Haskell Advent Calendar 2013 1日目前半の記事です．後半の記事もよろしく．

cabal sandboxは便利だけどdep hellが無くなったわけではない．ほとんどにわかに見えなくなっただけだ．むしろsandboxに甘えて針穴通すようなbuild-dependsを書いてしまうようでは，すぐにまた地獄は-よりおぞましくなって-我々の前にその姿を現すだろう．しかも，そうなったときは最早避けようもない．みんなgems/bundlerやらcpan/cpanmやら先達のアレコレ見てきてイロイロと「こうなってるとマズい」という反省も貯まっているんじゃないのかねぇ？

特に，Debianなど全体で一貫した依存関係を目指し，かなりの気合いを入れてhackageも取り込んでメンテナンスしてくれてるディストリビューションにおいて

• dep hellに引き摺り込むようなhackageが忌避されパッケージングされない/外される
• dep hellを避けるために妙に古いバージョンのものが使われ，更新できない

といった事態を発生させるかもしれない．これは大きなマイナスだ．そんなことになるようだと，いくらHaskell良い言語でみんな使えばと勧めたところで使う気が起きなくもなるだろう．いくら「成功を回避してきた」とか言っても限度はあるだろうし，関数はコンポーザビリティが高いんだよーとか言い放ちつつライブラリ同士はdep hellのせいでコンポーザビリティが無くなってしまったんだなどとなったらジョークにしても全然笑えない．

現実的には特にWeb系のパッケージは更新やインターフェースの変更やたら多くて頻繁だし*1，難しい面もあるにはある．が，地獄のような未来を回避し，あかるくケンゼンなHaskell界隈を守るために，何かLibraryだのExecutableだのを公開する際には，当然だけど，

• できるだけdependencyをスリムにし，いたずらに多くのhackageに依存させない
• できるだけdependencyを広いバージョンに対応させ，いたずらに狭いバージョンのみに依存させない
• 実際に広いバージョンやいろいろな環境でテストしておく

といったことに気を配る必要がある．今回は，そのための小技をいくつか記しておきたい．

Since *.*.*.*

これは，言語の機能でもcabalの機能でもなんでもないが，使っているライブラリのどのバージョンに対応しているかをcabalファイルに記述する際に「メッチャたすかるわー」と思うhaddock記述における慣習で，主にConduit系というか，まぁMichael Snoyman系？のhackageでよくやってるなーという印象．こういうやつだ．つまり，そのインターフェースはそのライブラリのどのバージョンから存在しているかをSinceなんちゃらという形でドキュメントに残すされるようにしてある．もし同じ名前でもインターフェース(型)が変われば，Sinceは更新される．

こうなってくれてると，自分がcabalファイルでbuild-dependsに依存バージョンのレンジを記述する際に，対応している下限がどれになるのがとても調べ易い．最新のhaddockだけ見ればいいからだ．そのライブラリの古いバージョンのhaddockをバイナリサーチで虱潰しに探す作業をしなくていいのである．とりあえずみんなこれやるべき．

本当は，パッケージ合わせるのも型でなんとかなればいいと思うし，なんかそういうことしようとしてる/してたみたいな話も聞くには聞くので，そういう未来も良いかもしれない．どうみても私はよい子全一なのでサンタさんにおねがいしておいた．

asTypeOfで助えるdependencyがあるかもしれない

Aに依存したBを使うとき，Bのインターフェースを使うためにAもbuild-dependsに入れなきゃいけない事態って割とある．特にAの関数としては何も使わないのに，Bの関数を使うときにAに定義された型を明示しなきゃならないとかそういうケースだ．そんなとき，自分が作ってるものをCとすると，既にA <- Bという依存があってAが入ってるのは確定なのに，必要としているB <- Cの他にA <- Cとという依存も明示的に付けなきゃならなくなって，Aの動向も追わなきゃならなくなる．これはどうにも無駄ではないか．

そんなとき，場合によっては，普段あまり使われることが無いPreludeの関数第一位に燦然と輝くかもしれないasTypeOfによって，型が推論され得る値さえあれば，型は同じハズだけど推論が効いてない全然別の値に対し，型情報だけ伝搬させられるケースがある．上手くいけば，内々に型情報を伝搬できる設計にできて，明示的にAに依存させる必要がなくなるかもしれない．あくまでもかもしれない．

Travis CIのhaskell用モードを使わない

Travis CIでテストを流している場合，.travis.ymlに"language: haskell"を使うと，Haskellプロジェクトを簡単に扱える設定になる．参考はこことここ．しかし，後者のページにある通り，

Haskell workers on travis-ci.org use Haskell Platform 2012.2.0.0 and GHC 7.4.1.

と，微妙に古いHaskell PlatformとGHCひとつだけでしか動作確認されずもったいない．どうせなんだし，いろんなバージョンのHaskell PlatformやGHCを同時に確認しておきたい．

ではどうするかというと，世の中には親切な人が親切をおすそわけしてくれている．スバラシイ．このmulti-ghc-travisを使うと複数バージョンのGHCやらHaskell Platformの設定で，Travis CIでテストをマトリクス実行することができ，古い環境に対する対応状況などを崩さないように，あるいは崩れたらそのことがわかるように開発を行うことができる．

もちろん，古い環境にどれだけ，そして，いつまで対応させるのかはライブラリ作者の判断次第だし，あまりにも古い環境に対して対応が切れたとしても何も言えはしないだろう．ただ，このようにTravis CIでいちどきに複数バージョンの動作確認が取れるのであれば，「テスト環境が用意できない」から考慮から外すという後ろ向きな対応を取る必要は薄くなってきてる気がする．

個人的な目安としては「現行Debian stableの古さ」まで可能ならばサポートし，それより古いのは切るくらいだと良心も痛まないかなと思っている．別にdebian使いではないが．

適切にラップしてバージョン間ギャップを吸収する

こんなのHaskellじゃなくたってあたりまえの話なんだけど，一応，基本的と思われる方法を書いておく．と言いつつGHC拡張になっちゃうんだけど仕方ないしまあいいよね．

GHCのCプリプロセッサ拡張を利用し，MIN_VERSION_*マクロなどを使う．たとえば，Network.Socket.sCloseなどは，network >=2.4ではdeprecatedになっており，かわりにNetwork.Socket.closeを使うようにとなっている．このギャップを吸収するNetwork.Socket.Wrapperモジュールを書くとなると次のようになる．gracefulパッケージより抜粋．

{-# LANGUAGE CPP #-}
module Network.Socket.Wrapper
    ( close
    , module Network.Socket
    ) where

import qualified Network.Socket as NS
#if MIN_VERSION_network(2,4,0)
import Network.Socket hiding ( close )
#else
import Network.Socket hiding ( sClose )
#endif

-- | wrap close/sClose
close :: Socket -> IO ()
#if MIN_VERSION_network(2,4,0)
close = NS.close
#else
close = NS.sClose
#endif

ビルド環境のnetworkのバージョンを見て，マクロが適切なものを残してくれるようにラップしている．他のモジュールでNetwork.Socketが必要な箇所では，変わりにNetwork.Socket.Wrapperをimportし，networkのバージョンが古い環境であってもラップされたcloseを使えばよい．

他にも，たとえばbytestringで0.10から入ってきたfromStrict/toStrictなんかを使ってる程度であれば，bytestring-0.9以前でも同様にラップしてあげた上でfromStrict/toStrictはカンタンなので自前で提供してあげれば，bytestring >= 0.10に制約する必要は特に無くもっと広く依存バージョンを取れる．こういうの結構あったりする．

まとめ

とにかくみんなもっとパッケージングには気を遣おう．いくら言語が型で守られていると言っても，エコシステムまで型が守ってくれているわけではないので，エコシステムを守るのはいまのところ個々人の良識+知識に依存している．コーディング時に型によって浮いた分の労力を，わずかでも上手いパッケージングに割いていただきたい．

*1:だから基本気にくわないのだが，Web自体がコギタナくてキレイに抽象化できてないため仕方無い部分もある

CoqのtacticやコマンドとAgda上操作の対応

この記事は Theorem Prover Advent Calendar 2013 1日目の記事です．
注意事項がひとつあります．本記事にはAgdaコードを含めようとしていますが，記事内でちゃんと書けてない文字があるかもしれません．だが私は悪くねぇ！

　　 　 　 ﾊヽ／::::ヽ.ヘ===ｧ
　　 　 　 {::{/≧=＝=≦V:/
　　 　 　 >:´:::::::::::::::::::::::::｀ヽ、
　　　 γ:::::::::::::::::::::::::::::::::::::::::ヽ
　 _／/::::::::::::::::::::::::::::::::::::::::::::::ﾊ　　　　　　私知ってるよ
.　| ll ! :::::::l::::::/|ハ::::::::∧::::i :::::::i　　　　　 みんなCoqの記事ばっか書くってこと
　 ､ヾ|:::::::::|:::/｀ト-:::::/ _,X:j:::/:::l
　　 ヾ:::::::::|≧ｚ　!Ｖ　ｚ≦　/::::/
　　　 ∧::::ト “　 　 　 　 “ ﾉ:::/!
　 　 /::::（＼　　 ー'　 　/￣）　 |
　　　 　 |　｀`ー――‐''|　　ヽ、.|
　　　　　 ゝ　ノ　　　　 ヽ　 ノ　|
￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣ 　　　　　　　

なので，出バナでCoq-erをAgdaに誘導(特にAgda Challengeに誘導)する記事出そうという方針で1日目を取る．あとネタ被りされると私のような定理証明弱者はネタが無くて死ぬのでそれを避ける意味でも．

レガシーCoqの基本的なtacticとかコマンドなどアレコレを，Software Foundationsに出てくる順とかに見ていってAgdaにマッピングするとだいたいのところagda-modeのどんな操作とかどんなコードに対応するかという話をしよう．ちなAgda標準ライブラリ有りでザックリと．

match ... with ... end.

いきなりtacticじゃないけどまあよく使うのでパターンマッチあたりから．

とりあえずHaskellとかと同じ．

even : ℕ → Bool
even 0 = true
even 1 = false
even (suc (suc n)) = even n

もしくは，Function.case_of_などを使って．

even' : ℕ → Bool
even' n = case n of λ
  { 0 → true
  ; 1 → false
  ; (suc (suc n)) → even' n
  }

まぁコレもパターンマッチ付きのラムダ使ってるから最初のとあまり変わり無いと言えば無いんだけど，停止性がわかんなくなることがあるらしいのでちょい注意．

reflexivity tactic

Relation.Binary.PropositionalEquality.reflとか等価性が定められるものには大体reflがあるからそれ使えばいい．

A≡A : ∀ {a} {A : Set a} → A ≡ A
A≡A = refl

simpl tactic

特に何かあるわけではなく適宜実行されてる？みたい．

0+0≡0 : 0 + 0 ≡ 0
0+0≡0 = refl

Inductive Data Type

これもtacticじゃないけどInductiveは普通の(=#や♭を使わない)データ定義．

data nat : Set where
  zero : nat
  suc : nat → nat

Haskellと同じカンジだけど，こっちは依存型バリバリだから常にGADTとかそのへんがONになってる状態と思ってもらえば．

Eval simpl in ~

Eval simpl in ~ は agda-mode の c-c c-n に対応している．
c-c c-n すると "Expression: [∏]"と式の入力を促され，式を入力してEnterで式の評価結果が表示される．
また，ゴール内で式を書いて c-c c-n すると，そのゴール内に書いた式がそのゴールの環境において評価されて表示される．

Admitted

Admittedはpostulateに対応．

たとえば，直観主義では証明できないPeirce's lawを定義しておくには以下のようになる．

postulate
  peirce : (P Q : Set) → ((P → Q) → P) → P

Check

Check は agda-mode の c-c c-d に対応している
c-c c-d すると "Expression: [∏]"と式の入力を促され，入力してEnterで式の型が表示される
また，ゴール内で式を書いて c-c c-d すると，そのゴール内に書いた式の型そのゴールの環境において評価されて表示される．

Notation

Notationに相当する機能は無い．というかprefix/suffix/mixfix operatorとそれらの結合優先度が使えるから必要性がほぼ無い．

intro/intros tactic

intro/introsはゴールのλ抽象を1から数段外して仮定に加えるということをするだけ．

0+n≡n : ∀ n → 0 + n ≡ n
0+n≡n = ?

に対して，ゴール?の型は(n : ℕ) → 0 + n ≡ nなので，そのまま証明した証明オブジェクトは

0+n≡n = λ n → refl

だが，intro/intros相当の書き換え(=λ抽象を1から数段外し)をすると

0+n≡n n = ?

を証明することになり，ゴール?の型が0 + n ≡ nになるので，証明オブジェクトは

0+n≡n n = refl

ということになる．

rewrite tactic

rewrite tactic は rewrite pattern もしくは Relation.Binary.PropositionalEquality.Core.subst が対応する．

n≡m→n+n≡m+m : ∀ n m → n ≡ m → n + n ≡ m + m
n≡m→n+n≡m+m n m n≡m
  rewrite n≡m
        = refl -- このときゴールの型は m + m ≡ m + m

rewrite H はこれでいいが，逆方向の書き換え rewrite ← H については，Relation.Binary.PropositionalEquality.Core.sym を使う．

n≡m→n+n≡m+m : ∀ n m → n ≡ m → n + n ≡ m + m
n≡m→n+n≡m+m n m n≡m
  rewrite sym n≡m
        = refl -- このときゴールの型は n + n ≡ n + n

destruct tactic

agda-mode の c-c c-c に対応しており，これは対象の変数に対し，その変数部分の網羅的なパターンマッチに展開する．

b∧c≡t→b≡t : ∀ b c → b ∧ c ≡ true → b ≡ true
-- b∧c≡t→b≡t b c b∧c≡t = ? まで書いて c-c c-l
-- b∧c≡t→b≡t b c b∧c≡t = { }0 となるので，このゴールの中で c-c c-c
-- すると "pattern variables to case:   [∏]"となるので対象の変数bを入れEnter
-- b∧c≡t→b≡t true c b∧c≡t = { }0
-- b∧c≡t→b≡t false c b∧c≡t = { }1
-- のようにbについて場合分けされる．
-- b∧c≡t→b≡t true c b∧c≡t = { }0 のほうのゴールはtrue ≡ true なので refl
b∧c≡t→b≡t true c b∧c≡t = refl
-- b∧c≡t→b≡t false c b∧c≡t = { }1 のほうのゴールはfalse ≡ true なので ⊥ になるはず，
-- このとき仮定b∧c≡tがもう成立していないハズなので．さらに c-c c-c で b∧c≡t すると．
b∧c≡t→b≡t false c ()
-- と仮定が空(⊥)にマッチして証明完了．

ゴールに対象の変数を書いてから c-c c-c でもよい．また，複数の変数を同時に展開することもできる．

b∧c≡t→b≡t' : ∀ b c → b ∧ c ≡ true → b ≡ true
-- b∧c≡t→b≡t' b c b∧c≡t = ? まで書いて c-c c-l
-- b∧c≡t→b≡t' b c b∧c≡t = { }0 となるので，このゴールの中に次のように書き，
-- b∧c≡t→b≡t' b c b∧c≡t = {b b∧c≡t }0 そして c-c c-lすると，
-- b∧c≡t→b≡t' true .true refl = { }
-- b∧c≡t→b≡t' false c ()
-- と場合分けされ後者のケースは即終わる．前者はrefl入れて終わり．
b∧c≡t→b≡t' true .true refl = refl
b∧c≡t→b≡t' false c ()

イントロパターンに相当するものは無いのでAgdaが適当に変数名を補完する．気に入らなければ展開後に直せばいい．先にやるか後でやるかの違い程度．

induction tactic

induction は destruct と同じくc-c c-c で展開し，その変数が再帰的なデータ型であれば， 証明オブジェクトが構造再帰関数となるだけ．

n+0≡n : ∀ n → n + 0 ≡ n
-- c-c c-c で n について場合分け
-- これが base case
n+0≡n zero = refl
-- こっちが step case
n+0≡n (suc n)
  rewrite n+0≡n n -- nについて再帰したものは使ってOK(=使っても停止することはわかっている)
        = refl

assert tactic

assertは着目したい部分だけwhere節などで取り出したりするだけ．
やはりイントロパターンに相当するものは無いが，どのみち適当に名付けないと本筋で使えないのでどうでもいい．

replace tactic

replace t with u は rewrite (仮定等から t ≡ u を作る式) に対応．

remember tactic

Relation.Binary.PropositionalEquality.inspect による．

eqℕ : ℕ → ℕ → Bool
eqℕ zero zero = true
eqℕ zero (suc b) = false
eqℕ (suc a) zero = false
eqℕ (suc a) (suc b) = eqℕ a b

3or5 : ℕ → Bool
3or5 n with eqℕ n 3
3or5 n | true = true
3or5 n | false = eqℕ n 5

odd : ℕ → Bool
odd zero = false
odd (suc n) = not (odd n)

eqℕ-a-b→odd-a≡odd-b : ∀ a b → eqℕ a b ≡ true → odd a ≡ odd b
eqℕ-a-b→odd-a≡odd-b zero zero p = refl
eqℕ-a-b→odd-a≡odd-b zero (suc b) ()
eqℕ-a-b→odd-a≡odd-b (suc a) zero ()
eqℕ-a-b→odd-a≡odd-b (suc a) (suc b) p = cong not (eqℕ-a-b→odd-a≡odd-b a b p)

3or5-odd : ∀ n → 3or5 n ≡ true → odd n ≡ true
-- eqℕの定義に従い，まずはeqℕ n 3の結果で場合分けするが，
-- eqℕ n 3をどちらに評価したかも使うのでinspectで覚えさせる
3or5-odd n p with eqℕ n 3 | inspect (eqℕ n) 3
3or5-odd n p | true | [ eq ] = eqℕ-a-b→odd-a≡odd-b n 3 eq
-- eqℕの定義に従い，次にeqℕ n 5の結果で場合分けするが，
-- eqℕ n 5をどちらに評価したかも使うのでinspectで覚えさせる
3or5-odd n p | false | [ eq ] with eqℕ n 5 | inspect (eqℕ n) 5
3or5-odd n p | false | [ eq₁ ] | true | [ eq ] = eqℕ-a-b→odd-a≡odd-b n 5 eq
3or5-odd n () | false | [ eq₁ ] | false | [ eq ]

inversion tactic

absurd pattern matching で矛盾引き出して終わり．

ring tactic

Data.Nat.PropertiesのRingSolverによる．

環上の多項式のequalityを示すには

f : ∀ x a b → x * x + (a + b) * x + a * b ≡ (x + a) * (x + b)
-- 式をRingSolver用の構造(_:*_;  _:+_; _:+_)で書き直す
f = solve 3 (λ x a b → x :* x :+ (a :+ b) :* x :+ a :* b := (x :+ a) :* (x :+ b)) refl
-- 3は式内の変数のarity，reflはまぁ，おやくそく的に

リフレクションを使えば構造を自分で書き直している部分を自動化したものを定義することもできる．

まぁ，他にもいろいろあるだろうけどとりあえずこのくらいで．

cabal sandbox環境のpackage DBを参照する(改)

前回の記事は調査不十分だった．

まず，sandbox環境では，

cabal install --only-dependencies --enable-tests
cabal configure --enable-tests
cabal build
cabal test

を実行したときと，

cabal install --enable-tests

を実行したときで，config dist prefixが異なる．前者では，これまで同様にdistで，後者ではdist/dist-sandbox-HASHとなる．HASHの決まり方は前回の記事参照．

このHASH付きのprefixが使われるのはちゃんとした理由がある．cabal sandboxにはadd-sourceというローカルパッケージディレクトリに依存させる機能がある．どういうことかというとパッケージBがパッケージAに依存していて共にローカルにソースツリーがある場合．

cd /path/to/B
cabal sandbox init
cabal sandbox add-source /path/to/A
cabal install --only-dependencies

とすることで，ローカルに置いてあるパッケージAを依存パッケージとして使うことができるというものだ．このとき，BのためにビルドされるAは．/path/to/A/dist/dist-sandbox-[Bの.cabal-sandboxのフルパスを基準にしたHASH]以下で作業される．もし，パッケージAをパッケージBとパッケージCからそれぞれcabal sandbox add-sourceするような場合に，Bからcabal installする場合のAの依存関係はBの依存関係に引きずられ，Cからcabal installする場合のAの依存関係はCの依存関係に引きずられるため，それぞれ違うパッケージバージョンセットに依存してビルドされたAが必要になっているかもしれない．同じdistディレクトリを使っていたままでは，BとCを並列にビルドするようなときに衝突してしまうため，Bを基準に決まるHASH，Cを基準に決まるHASHの付いたディレクトリにそれぞれ分けられてA以下でビルドされる．

このことがテストなどビルドが必要な操作に影響するのは前回書いた通りであるが，前回はcabal install --enable-testsのときの話しかしておらず，sandboxかどうかだけで分ければいいと思っていた．明らかに間違いである．正しい認識では「sandbox環境ではどのcabal subcommandからテストが実行されるかによってconfig dist prefixを変えなければならない」ということになる．sandboxかどうかだけでは判断できない．

これに影響を受けるもので最も身近なのは恐らくdoctestだと思う．CPP拡張やPath_*.hsを使っているモジュールに対してdoctestを実行するような場合などは必ずautogen以下を使う必要がある．たとえば，test-suite doctestsのコードは，

-- doctests.hs
import Test.DocTest

main :: IO ()
main = doctest [ "-isrc"
               , "-idist/build/autogen/"
               , "-optP-include"
               , "-optPdist/build/autogen/cabal_macros.h"
               , "Test.Target.Module"
               ]

といった具合になるわけだが，このままではこの記事の冒頭に示した2通りのテスト実行コマンド列をカバーできておらず，実際cabal install --enable-testsのほうであたりまえのようにコケる．cabal_macros.hがみつからないか，みつかったとしても期待してるのと別のファイルを見てるハズだ．なので，2通りのどちらで実行されたかを知らねばならないのだが，残念なことにあまり良い方法が無い．Setup.hsに手を入れて上手いこと判断できるような気はするのだが，Setup.hsを弄るのは面倒が増えるし地獄っぽいのであまりやりたくない．というかCabalパッケージをあまり見たくない．目がー！ってなる

結局，テスト実行バイナリが自身のファイルの位置を基準にする方法がリーズナブルではないだろうか．バイナリファイルの位置は，前者のケースではdist/build/doctests/doctests，後者のケースではdist/dist-sandbox-HASH/doctests/doctestsになる．たとえば，linux環境下では/proc/self/exeがプロセス自身のファイルへのシンボリックリンクになるので，test-suite doctestとしては，

-- doctests.hs
import Test.DocTest

import System.FilePath
import System.Posix.Files

getConfDistDir :: IO FilePath
getConfDistDir = fmap (dirname . dirname . dirname) getModuleFile where
    dirname = takeDirectory
    getModuleFile = readSymbolicLink "/proc/self/exe" -- ghc 7.6.1 以降なら getExecutablePath

main :: IO ()
main = do
  confDistDir <- getConfDistDir
  doctest [ "-isrc"
          , "-i" ++ confDistDir ++ "/build/autogen/"
          , "-optP-include"
          , "-optP" ++ confDistDir ++ "/build/autogen/cabal_macros.h"
          , "Test.Target.Module"
          ]

のようになる．これなら冒頭に示したどちらのケースで実行されても期待する通りにテストが走る．Windowsは知らないけどたぶん似たようなことできるだろう．ghc 7.6.1 以降なら getExecutablePath でよさげ．でも，現在のdebian wheezyはghc 7.4.1なので，そこへんまでカバーさせたいライブラリでテストも対応させたいなら別の方法で．

cabal sandbox環境のpackage DBを参照する

cabal-install-1.18 がきた．全国のHaskeller待望のcabal sandboxが使える．cabal-devさん今までありがとう．さようなら．

この記事は余計なことをしている可能性があります！

さて，テスト時にプログラムをビルドする必要があるとする．これは*.cabalファイルに設定したtest-suiteのプログラムのことではなく，test-suiteのプログラム内からさらにghcを呼び出してビルドするようなケースだ．たとえば，gracefulパッケージなどは「特定のsignalを受けて何かするプロセス」を作るためのパッケージなので，テストの中でそのプロセスをビルドして立ち上げている．他にもTemplateHaskell系のパッケージだとビルドそのものができるかというテスト書く必要とかもあるのでは？

この際，package DB(以前はpackage conf)が指定されていなければ，*.cabalに設定されたbuild-dependsが取れないので，通常は-package-db(もしくは-package-conf)オプションに"dist/package.conf.inplace"を渡す必要がある．

$ ghc --make Foo.hs -package-db "dist/package.conf.inplace"

しかし，cabal/cabal-devまでの世界であればconfig dist prefixは大体"dist"固定で考えていればよかった(debを作ろうとすると"dist-ghc"とか違う名前を設定したりするみたいだけど)が，cabal sandboxではそうもいかなくなった．sandbox環境ではconfig dist prefixが"dist/dist-sandbox-[HEX8桁]"という名前になる．このHEX8桁部分はどの設定ファイルにも吐き出されてないみたいなので，sandbox環境でも同様にテストを流すためには自分で構成してあげなければならない．

で，どうやらこのHEX8桁部分はJenkins hash functionで".cabal-sandbox"ディレクトリのフルパスをハッシュしたものらしい．たとえば，*.cabalファイルの置かれているディレクトリが"/home/notogawa/work/somepackage"で，この環境をsandbox化すると"/home/notogawa/work/somepackage/.cabal-sandbox"ができ，この環境では"/home/notogawa/work/somepackage/dist/dist-sandbox-975dcfa2"がconfig dist prefixになる．

結局，sandbox環境でもそうでなくとも適切にpackage DBを設定して*.cabalのbuild-dependsを反映させてビルドするためのコードはたとえば次のようになる．

packageOption :: String
#if __GLASGOW_HASKELL__ < 706
packageOption = "-package-conf"
#else
packageOption = "-package-db"
#endif

build :: FilePath -> IO ()
build file = do
  conf <- packageConf
  (code, _out, _err) <- readProcessWithExitCode "ghc"
                        [ "--make", file
                        , packageOption, conf
                        ] ""
  code `shouldBe` ExitSuccess

packageConf :: IO FilePath
packageConf = maybe "dist/package.conf.inplace" id `fmap`
              sandboxPackageConf

sandboxPackageConf :: IO (Maybe FilePath)
sandboxPackageConf = do
  cd <- getCurrentDirectory
  let prefix = cd ++ "/.cabal-sandbox"
  let confDistDir = "dist/dist-sandbox-" ++ showHex (jenkins prefix) ""
  let conf = confDistDir ++ "/package.conf.inplace"
  putStrLn conf
  exist <- doesFileExist conf
  return $ if exist then Just conf else Nothing

jenkins :: String -> Word32
jenkins str = loop_finish $ foldl' loop 0 str
  where
    loop :: Word32 -> Char -> Word32
    loop hash key_i' = hash'''
      where
        key_i   = toEnum . ord $ key_i'
        hash'   = hash + key_i
        hash''  = hash' + shiftL hash' 10
        hash''' = hash'' `xor` shiftR hash'' 6
    loop_finish :: Word32 -> Word32
    loop_finish hash = hash'''
      where
        hash'   = hash + shiftL hash 3
        hash''  = hash' `xor` shiftR hash' 11
        hash''' = hash'' + shiftL hash'' 15

ICFP Programming Contest 2013

今年ものとがわさんパンピーやった(1年ぶりn度目)

問題はここ．64bit非負整数に対する限られた関数と単純なlambda式からなるプログラムがコンテストサーバ側にいっぱいあってIDが付いている．サーバ側にある各プログラムの具体的な形はわからない．プログラムは全て 64bit非負整数->64bit非負整数 の型を持つ．サーバ側には

• myprograms: プログラムのサイズや含まれてる関数などの一覧を取得するAPI
• eval: あるIDのプログラムに，指定した入力を適用したときにの出力を一度に最大で256組取得するAPI
• guess: あるIDのプログラムはコレじゃないの？と回答するAPI

などが用意されており，解きたい問題をmyprogramsから選んでevalでブラックボックスに入出力ペアを取得し，プログラムを推定して最初のevalから5分以内にguessする．正しければ1点ゲット．

• train: 練習用のプログラムが得られるAPI

もあり，一応テストできるが，trainも含めAPIには1チームあたり20秒あたり5回までというアクセス回数制限がかかっている．

割と誰でも手をつけやすい敷居の低さで，しかも難しいものは難しく，それに対処したときの効果もわかりやすい．大きな難易度幅を持ち，参加者の思考を促すようなとても良い出題だったと思う．APIのアクセス回数制限によって，時間を消費させつつもできるだけ早くアイデアを形にしなければならないという煽りも秀逸．ただ多くの参加者が思うようにleaderboardが無い理由だけはよくわからなかった．

言語はHaskell

結果はこんな感じ．

リポジトリはここで，コンテスト中に書いた分はだいたい以下の通り．

   53   235  2038 ./BV-proxy/main.hs
   49   286  1668 ./language-BV/Language/BV/Eval.hs
  155   967  5760 ./language-BV/Language/BV/Syntax.hs
  627  3510 26420 ./BV-infer/main.hs
  884  4998 35886 合計

1日目

問題を読んで，うーんこの．と思いながらとりあえずASTと評価器を作る．Haskell．特に問題無し．プログラムにはfoldがいっこしかないとかなので，"foldを含むかどうか"，と"fold内にある式なのかfoldの外にある式(もしくはfold)なのか"をGADTsでタグ付けしたりTypeFamiliesとか使ってたりして型で区別しておく．これでプログラムにfoldを2つ埋めてしまうとかイロイロとミスできなくしておく．Eqとか後述のArbitraryのインスタンスにするとかが困る感じになったがまぁそのへんは雑に．

次に肝心のプログラム推定器だが，じゃあまず「運ゲー状況作るか！」といきなり思考停止．画面見ない勢の本領発揮．

おもむろにASTをTest.QuickCheck.Arbitraryクラスのインスタンスにして同じくTest.QuickCheck.sample'でランダムサンプリングしたプログラムがたまたまevalの結果と正しいかどうかをチェックしてguessするようなものを書いた．あるサイズ以下のプログラムをランダムに生成させたかったのだが，Arbitraryは型からしか情報が取れないので，手っ取り早くunsafePerformIOでIORefに「今解いてる問題の情報」を持ってしまうことにした．どうせアクセス回数制限と5分時間制限のせいで，複数の問題を同時に処理するつもりは無くなってたため，このunsafeはまぁそんなにunsafeじゃないだろうと．これで小さいプログラムに対しては大体解けるってくらいの運ゲー感．2日目3日目でコイツが大きなサイズをたまたま解いてる！？のを見るとかなり得した気分になる程度．

全体としてはシンプルでソルバを起動すると，

1. myproblemsで問題を全部取得
2. 解けそうなやつを選ぶ
3. evalで人口的に適度にビット立てた256入力に対してサンプリング
   • ビット演算が主だったのでビットの位置関係に配慮した
4. この256サンプルを満たすものを求める
5. guess

で最後までこれはほぼ変わらない．毎回myproblemsするのも効率悪いけどマシン複数台使ったりとかそんなリソース無いし，これでもザックリ1時間で最速300問処理れるからまぁいいかなと．ゆっくりしていってね！

とりあえずコレをmyprogramsの小さい問題やtfoldの問題を選んで回してlightning用とする．まだこの時点でアクセス制限対策は無く，1問トライしたら20秒待つという雑な仕事して夜は寝る．ただ変に回っちゃって易い問題を失敗で消費してしまうのも怖いので何かエラー想定外状況時はそこで見切りを付けて終わり．案の定起きたらmissmatchで止まってた．

2日目

さすがにちょっと運ゲーだけだとダメだよなーと少し真面目になる．反省

guessの結果がmissmatchだったらその反例も加えて再度ブン回す処理を追加．

あるサイズのプログラムを全列挙し初める．ただし探索するときは問題に与えられたサイズ以下のプログラムを小さいほうから探索する．1日目に運ゲーでtrainやmyproblemsを解いてるとき，

• 問題のプログラムには無駄な演算が入っていることが多々ある
  • サイズや演算が必要最小限よりも大きく多くなっていることが多々ある
  • 2日目終わって寝てる間にヒントとして公式にアナウンスされた
• 別にサイズや演算が同じでなくても同じ結果を与えればスコアになる

ことは気付いていたので，小さいプログラムで済むならそれが速い．演算の性質も鑑みて適宜枝刈りも入れていった．結局この全探索と運ゲーに加え，5分のタイムアウトをControl.Concurrent.Asuncで並列化．

パワーが足りなくなってきたのでVMへのリソース割り当てを増やす．メモリ8GB，8コアからメモリ32GB，12コアへ

また，20秒待つとか雑なコントロールを廃止し，アクセス制限対策のコントローラを書いて推定器とコンテストサーバの間に入れた，と言っても普通のサーバに20秒(安全のため+数秒してるが)で復活するリソースを5個持たせ，それがひとつ取得できるまでは接続されても何もせず待ち，取得できたらプログラム推定器からの通信をコンテストサーバに横流しし，コンテストサーバからの通信内容を推定器に横流しするだけ．STMモナド無い言語でこういうの書く気もうまるで起きないのですが皆様いかがお過ごしでしょうか？

おもむろにこのエントリを書きはじめる．

イロイロ微調整したりしてると夜になったので走らせて寝る．起きたらサーバから "Unable to decide equality" 出てきて止まってた．なんだこれ．

3日目

3日目開始あたりで11位から50位がスコアレンジ300-550にいるとのアナウンスが．あれ？案外点数低そう？上はもう1000余裕みたいな感じじゃないの？とか思ってた．

bonusとかいうのが出てていかにも重そうだったのでひとまず無視するコードを追加．

最終日だし翌日昼間の仕事もあるので休暇をとらねばと，何かエラー出ても無視するようにしてひたすらブン回しておき，自分はニコ動を見たり暑い中蛍光灯を買いに出たりといった功夫を積んで過ごす．マスターオブライフ

そろそろbonus以外の問題ひととおりトライし切るかなと思ったあたりでbonusについて考え初める．bonusの特徴は(lambda (x) (if0 P T F))に決まってるっぽかったので，まずは1問に対するevalの回数を増やし，決め打ちの256+ランダム256*3の1024サンプル取得するようにした．まずはT(もしくはF)の候補Eをサイズ1から生成していって(lambda (x) E)でサンプルを処理してみる．先頭がif0ということは，あるプログラム(lambda (x) E)が1024サンプルの半分以上をパスするのであれば，このEはT(もしくはF)の候補に価すると判断する．今度はパスしなかったサンプルだけかき集めて，これらを全て通すようなF(もしくはT)候補を求める，あとは(if0 E T F)か(if0 E F T)となるようなEがあればこのEをPとみてguessを投げた．これは30未満のbonusをサクサク解いていってくれた．さすがに31以上はキツいのかタイムアウト多い．

夜になったのでこれをブン回して寝る．朝起きて出社前にプログラム止めて最終スコア確認．bonusはbonusだけあってそれなりにおいしかったようだ．

やったことメモ

• foldの含有，fold内外をGADTで型制約
  • ArbitraryとGADTスゲー相性悪い感があるけど自分だけですかね？
  • あとEqにも困った
  • 上手く使えてない感，反省
• アクセス数制御対策のproxy
  • 作成中のサーバ用ライブラリがあったので，50行くらいで
• プログラム中の変数はx,y,zだけ
  • fold が無い場合，式中の自由変数は高々1個(x)
    • プログラム先頭のlambdaが束縛する分
  • fold が有る場合，fold外の自由変数は高々1個(x)
    • プログラム先頭のlambdaが束縛する分
  • fold が有る場合，fold内のlambda内の自由変数は高々2個(y,z)？
    • プログラム先頭のlambdaが束縛する分(x)は入ってこない？
    • この制約は記述がたぶん無かったがtrainをいくら引いてきてもそうだったので決め打ち
  • tfold には shadowing があるので2個(x,y)
• プログラム生成順序
  • 解こうとしてる問題サイズより小さいものから生成
  • fold > if0 > op2 > op1 の順に先頭への出現優先度 (気分)
  • 二項演算と単項演算については，できるだけ適用先でなく演算のほうが入れ変わるように (気分)
• プログラム生成時の枝刈り
  • not . not
  • (and/or/xor) E E
  • (not以外のop1) 0
  • op2 0
  • if0 (0/1) T F
  • if0 P E E
  • shr*が適用され続けるときはshr1→shr4→shr16の適用順に正規化

やれてなかったことメモ

• プログラム生成時の枝刈り
  • op2 a b と op2 b a を同一視する
    • なぜやってないことに気付いていなかったのか…
  • size nのプログラムを作るときにsize 1のもの(0/1/x/y/z)を含んでいた…
    • bonusやってるときに気付いて刈った
    • bonus以外は刈ってないものでやってしまった
    • どういうことなの？これものすごい計算無駄にしたのでは…

やらなかったアイデアとか

• サイズ大きいプログラムは予めデータベース化しておく
  • 以下の情報を持たせてクエリできるようにしておく
    • サイズ
    • 含まれる演算
    • 決まった定数個のサンプルに何を返すか
  • 枝刈りwith全生成の質にもっと早く納得できればやってみたかも
• モンテカルロ木探索的な生成
  • "有力な枝"を決める基準であまりよいものができなさそうだと感じた
• GAやSA
  • "良いやつを少し変更したものも同じくらい良い"ような気があまりしなかった
  • 5分で辿り付けるかが疑問だった