ghc-mod-4 でfaceを反映させる

ghc-mod-4以降ではghc-modiを使うためにflymakeへの依存を切っており，flymake的な挙動は自前で実現している．

そのため，今まで反映されていたflymake用のface設定が反映されなくなるので，バージョンアップ後急にさびしい絵面になったりする．

もし，

(set-face-background 'flymake-errline "red4")
(set-face-foreground 'flymake-errline "black")
(set-face-background 'flymake-warnline "yellow")
(set-face-foreground 'flymake-warnline "black")

のようにflymakeのfaceを設定していたのなら，これを反映させるには，ghc-modが独自に持っているfaceに対しても同様に設定しなければならない．

;; ghc-mod
(autoload 'ghc-init "ghc" nil t)
(add-hook
 'haskell-mode-hook
 (lambda ()
   (ghc-init)
   (set-face-background 'ghc-face-error "red4")
   (set-face-foreground 'ghc-face-error "black")
   (set-face-background 'ghc-face-warn "yellow")
   (set-face-foreground 'ghc-face-warn "black")))

みんなきおつけろ！

IOアクションひとつひとつを利用許諾し・テスト可能にする

IOのテストってたいへんだ．これをどうにかするために，先人たちは色々考え，

  • 利用対象の特定IOアクションを慎重に取捨選択し，MonadHogeIOのような型クラスによりインターフェースを与えてからそのインターフェース上のアクションとして実装する．実行時は目的のインスタンスの上で走らせるし，テスト時はMock用インスタンスの上で走らせる
  • 同様に特定IOアクションを慎重に取捨選択し，FreeモナドやOperationalモナドによりインターフェースを与えて以下略．目的のランナーで走らせたり，テスト用のランナーで走らせたりする

といった手段を取る．

で，普通テスト用のものはピュアになるように実装し，テストしやすくする．具体的には，型クラスとモナドと Free モナド - あどけない話や，Freeモナドを超えた！？operationalモナドを使ってみよう - モナドとわたしとコモナドがわかりやすいかな．

でも，どちらの方法を取るにせよ，IOアクションが適切に取捨選択された状態になければならない．IOアクションaとIOアクションbだけ使うIOアクションx (x = a >> b)と，IOアクションbとIOアクションcだけ使うIOアクションy (y = b >> c)があるとき，a,b,cそれぞれに相当するインターフェースを持った型クラスやらデータ型のコンストラクタやらを用意することになる．もくは，aとbだけ，bとcだけにそれぞれ相当するやつだけ持ったものを用意するだろうか？いずれにせよ，特定のものに限定した環境を作ってその上で戦うことになる．というのがこのあたりの話

で，この記事の本題．上のツイートで「制限されてなければ（義務感）」みたいに自分でも言っておいて，果たして今でも本当にそんな状態なのかとちょろっと考えてみた結果を簡単にライブラリ(まだhackageに上げてない)にしてみた．

notogawa/genjitsu · GitHub

このライブラリは，ザックリ言うとIOアクションの利用制限及びモック差し替えを自由に行うための，インターフェース・型クラス制約生成系及び，それを利用した例としてのPreludeの置き換えモジュールとなっている．

TemplateHaskellにより任意のIOアクションからextensible-effectsのEffアクションを生成し，あるIOアクションに対応して生成された特定の型クラス制約がコンテキストに無い場所ではそのIOアクションを元に生成されたEffアクションは使えないという制約を付けることができる．加えて，Effアクションがコンテキストに持つ型クラス制約に対するインターフェースだけをモック実装すればそのEffアクションはテスト可能になる．というものだ．

自分で上手く言えてないのわかってるのでたぶん何言ってるかわからないと思う．さっさとサンプル示そう．

まず，IOアクションからEffアクションを生成するTemplateHaskellについてだが，たとえば，Control.Genjitsu.THのgenjitsuを使い，

import qualified Prelude as P
$(genjitsu 'P.putStrLn)

のようにすると，これにより次のようなコードが生成される．

class AllowPutStrLn m where
    allowPutStrLn :: String -> m a

instance AllowPutStrLn IO where
    allowPutStrLn = putStrLn

putStrLn :: ( Typeable1 m
            , AllowPutStrLn m
            , Member (Lift m) r
            , SetMember Lift (Lift m) r) =>
            String
         -> Eff r ()
putStrLn x = lift (allowPutStrLn x)

Prelude.Genjitsuモジュールは，これをPreludeのIOアクション全てに行い，元の名前の関数を新たに生成された同じ名前の関数で置き換えているだけだ．

実際にPrelude.Genjitsuを使うと次のようなコードになる．

sample1 :: ( Typeable1 m
           , AllowReadLn m    -- readLnが使える
           , AllowPutStrLn m  -- putStrLnが使える
           , Member (Lift m) r
           , SetMember Lift (Lift m) r
           ) =>
           Eff r ()
sample1 = do
  n <- readLn
  let s = n + 1 :: Int
  -- putStr "is denied"
  putStrLn (show s)

sample1は型の部分に目を潰ると，中身はただのIOモナドのように見える．ただし，このsample1のコンテキストでは，readLnとputStrLnしか許されていない．そのため，readLnとputStrLnは使えるが，putStrを使おうとするとコンパイルエラーになる．

また，別のケースも見てみよう．

sample2 :: ( Typeable1 m
           , AllowPutStr m    -- putStrが使える
           , AllowPutStrLn m  -- putStrLnが使える
           , Member (Lift m) r
           , SetMember Lift (Lift m) r
           ) =>
           Eff r ()
sample2 = do
  putStr "Start..."
  putStrLn "Done"

こちらのsample2では，putStrが使えるようにコンテキスト指定されているのでputStrが使える．

さて，これらを実際にIOアクションに還元してあげるのは簡単だ．extensible-effectsのLiftを使っているのでrunLiftしてあげればいい．

sample1IO :: IO ()
sample1IO = runLift sample1

sample2IO :: IO ()
sample2IO = runLift sample2

また，sample1/sample2に対してテストを書く場合，これらの各コンテキストにある型クラス制約で許可されたものだけインスタンス実装すればいい．たとえば，sample1をテストするのにStateモナドを使ってみると，

-- 各自適切なGHC拡張は補完してネ
newtype Mock1 a = Mock1 { runMock1 :: State String a } 
    deriving ( Functor, Applicative
             , Monad, MonadState String, Typeable)

-- sample1はAllowReadLnをコンテキストに持つのでMock実装が要求されている
instance AllowReadLn   Mock1 where
    allowReadLn   = fmap read get

-- sample1はAllowPutStrLnをコンテキストに持つのでMock実装する
instance AllowPutStrLn Mock1 where
    allowPutStrLn = put

test1 = ((),"3") == runState (runMock1 $ runLift sample1) "2"

sample2のほうも同様にしてpureなテストを書くことができる．sample2についてはsample1と異なりテスト対象として入力のアクションを含まないのでWriterモナドでモック実装してあげれば十分だろう．ここまでのサンプルコード

genjitsuがMonadHogeIOインターフェースやFree/Operationalモナド方式に対して持つ利点は，

  • 必要なクラスやらの生成がTemplateHaskellでだいぶラク
    • runLiftでIOアクションに戻したものを再度genjitsuしておくようなことも簡単
  • あらかじめ利用したいアクションを取捨選択して制限しておく必要が無い
    • その場その場で本当に必要ならコンテキストとして与えればよい
  • アクション単位の利用許可を型で表すことができる
    • ウカツにいろんな種類のIOアクションを使ってしまうようなことを防げる
  • 何を実装すれば走らせることができるかが型レベルで明確になる
    • 許可されているものに対してのみ実装を与えれば走る
    • モック書いたりするときに着目しているテスト対象に対して余計なインターフェースを気にしなくてよい

とか．そのへん．

感覚的にだいぶ楽だと思うんだけどどうだろうか？正直なところ言うとコンセプトにイマイチ自信が無いのでhackageには上げてない．

CPS変換もいいけど融合変換もね

継続渡しなHaskellライフ - モナドとわたしとコモナド の流れで．

要約すると，元々

fb :: Int -> Either Int String
fb n = case n `gcd` 15 of
         15 -> Right "FizzBuzz"
         5  -> Right "Buzz"
         3  -> Right "Fizz"
         _  -> Left n

fizzbuzz1 :: Int -> String
fizzbuzz1 n = either show id (fb n)

みたいなコードだったのを，

fbCPS :: (Int -> t) -> (String -> t) -> Int -> t
fbCPS left right n = case n `gcd` 15 of
                       15 -> right "FizzBuzz"
                       5  -> right "Buzz"
                       3  -> right "Fizz"
                       _  -> left n

fizzbuzz2 :: Int -> String
fizzbuzz2 n = fbCPS show id n

みたいにCPS変換しておいて使えば，

条件分岐の結果を一旦代数的データに押し込み、それに対してさらに条件分岐を行おうとしているのだ……

と問題視していたデータの構成及びパターンマッチが

計算の結果を代数的データ型を介さずに受け渡しできる

ことになって無くなってくれるのでイイねぇという話．

たしかに高速化にCPS変換が効果的なのは正しい．けど，fizzbuzz1とfizzbuzz2を見比べたときにちょっとアレ？って思うところ無いだろうか．というのは，CPS変換前ではfbという部品を作りeitherという別の部品と組み合わせて全体の処理fizzbuzz1を構成していたのが，CPS変換後のものを使ったfizzbuzz2では妙に強く結合してしまったナァという印象を受ける．まぁ，元のfbと同じものはfbCPS Left Rightだからそれでいいっちゃいい．でも，Haskellは関数適用と型システムによる強くて硬いcomposabilityに裏打ちされたmodularityがウリのひとつではなかったか．それともイザ速いプログラムを書くにあたっては仕方のないことなのだろうか？

いや我々にごはんを食べさせてくれているHaskellさんはさすがにそんなことはないはずなのだ．要は代数的データ型に対し，それを消費するeitherやfoldrみたいなものと，代数的データ型の生成が自動的に打ち消されてくれればいい．ぱよえーん

たとえば次のような関数buildEを考えよう．要RankNTypes

buildE :: (forall x . (a -> x) -> (b -> x) -> x) -> Either a b
buildE g = g Left Right

buildEは，Leftに対応する変換であるa to xの関数と，Rightに対応する変換であるb to xの関数を受けてxになる関数gを受け，Either a bとなる関数である．まぁ，型をそのまま読むとそう書いてある．このbuildEを使うと，とりあえず適切なgさえ与えてあげれば，fbのような関数はなんとなく書けそうな気分になる．

さて，Either a bを生成するこの関数buildEと，Either a bを消費する関数eitherを組み合わせると，

either l r (buildE g) = g l r

という等価な式がなりたってeitherとbuildEが消える．という最適化ができる．この等式の右辺を構成する要素g,l,rの型にはEither a bは一切出現しないので右辺の処理ではEither a bの値は作られない．この最適化規則はghcではRULESプラグマとして次のようにコンパイラに教えてあげることができる．

{-# RULES "either/buildE" forall l r (g :: forall x . (a -> x) -> (b -> x) -> x) . either l r (buildE g) = g l r #-}

こうしておくと，buildEで書かれたEither a bを生じる関数は，eitherされると最適化によりEither a bの生成・パターンマッチなどが勝手に消えたコードになってくれるはずだ．

あとは実際にbuildEでfbを書き直す．

fbBuildE :: Int -> Either Int String
fbBuildE n = buildE g where
    g l r = case n `gcd` 15 of
              15 -> r "FizzBuzz"
              5  -> r "Buzz"
              3  -> r "Fizz"
              _  -> l n

この関数fbBuildEはfbと同じ型と同じ結果を持ち，CPS変換済みのコードをbuildEを介して内部に隠し持ったような形になっている．これをfizzbuzz1と同様にeitherと組み合わせ，

fizzbuzz3 :: Int -> String
fizzbuzz3 n = either show id (fbBuildE n)

とすると，fizzbuzz1と部品化の度合いは同じままで済んでおりコードの見た目は変わらない．それでいて，先程の変換規則に合致するので中間的なEither Int Stringは作らないよう最適化される．

Eitherみたいに構造が小さい代数的データ型に対してはあまり強い効果は持たないが，リストのように再帰的に大きくなる代数的データ型に対してはとても強い効果を発揮する．実際，同じようなことをするリスト用の変換規則"fold/build"などはGHC.Baseに入っている．

と，ここまで書いたけど，実際にはこれで完全に最適化がキモチよく決まるかというとghcの他の最適化機構やらイロイロなアレやコレやによって，案外そういうわけでもなかったりすることもある．加えて，正しさがよくわかってない規則であるならRULESプラグマをウカツに書くのはとてもよろしくない結果をもたらす．本当に間違った規則を書くこともできるし，変換が停止しない規則を書くこともできる．変換に関わる関数の正格性などによって正しい/正しくないが変わってしまうということもある．いまのところ，確実に何かしたい場合はCPS変換を手で書くのもアリなのだろう．CPS変換する目的自体もいろいろあるだろうし．

ただ，果たして本当にCPS変換はニンゲンがやるようなサギョウなのかというのはコードいっぱい書く前に一考する必要がある．効率化全般に言えることだけど全体からみて本当にソレがボトルネックなのかとかは最初は案外わかんない．CPS変換も人手で正しく変換してあげる必要はあるわけだし，CPS変換によって本当に変換前と意味が変わってないかはそんなにスンナリとわからないんじゃないかな．

折角Haskell使ってるんだからコンパイラとか頭いい研究者達に任せられる分はガンガン任せて，私としてはあんまり難しいこと考えずに楽したい．というかメンドクサイのであんまりやりたくない．

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

Agda Coq

依存関係のある値のうちの一部を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

この記事は 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

この記事は 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上操作の対応

Agda Coq

この記事は 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:   [&#8719;]"となるので対象の変数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&#8321; ] | true | [ eq ] = eqℕ-a-b→odd-a≡odd-b n 5 eq
3or5-odd n () | false | [ eq&#8321; ] | 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はまぁ，おやくそく的に

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


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