Haskell定理証明士がEmptyCase拡張によって受ける恩恵と効能

EmptyCaseが入ってきた．absurd pattern matchingがHaskellで使えるのでHaskell証明士には朗報だ．

具体的にEmptyCaseの有無で世界がどう変わるかを把握してる範囲で書く．

まず，矛盾(bottom)の扱いについて．矛盾は「値を構成できない型」になればよいので，通常次のいずれかになる．

data Bottom

data Bottom = Bottom Bottom

直観主義における「矛盾からは何でも導ける(bottom elimination)」は，型としては，

bottomElimination :: Bottom -> whatever

となるが，今まではこれの実装は，

bottomElimination bot = bottomElimination bot

bottomElimination (Bottom bot) = bottomElimination bot

などにせざるをえなかった．結局のところ値を構成できない型であることを上手く使えておらず，無限ループのbottomに入り込むことによって任意の命題を引き出していたが，これがみんなの健康によくないのは明らかである．CoqやAgdaなどの定理証明系では停止性チェッカがあるため，このような実装は通常与えられない．

そして，これは「Bottomに限らず何からでもよいから何でも引き出せる」という命題を作ってよいのかという話でもある，たとえば，

getWhatYouWantFrom :: a -> whatever
getWhatYouWantFrom anything = getWhatYouWantFrom anything

のように，同様にして任意の命題から任意の命題を引き出せてしまう，そのため，型を証明に使うことを重視するのであればどうみてもunsafeな実装(証明)方法になっている．

計算機においてbottomは「値を持ち得ないもの」や「計算が停止しないもの」に相当するが，証明において後者は本当に秘密道具たっぷりつまった四次元ポケット的ジョーカーなので，定理証明系は停止しない計算が慎重に排除された系として設計されている．

EmptyCaseが入ると，最早このようなunsafeな実装を使う必要は無い(といっても，Haskellである以上書けてはしまうところは変わるわけでもないのだが)

{-# LANGUAGE EmptyCase #-}
data Bottom

bottomElimination :: Bottom -> whatever
bottomElimination bot = case bot of {}


次に，bottomを使う証明オブジェクトの作成，たとえばシンプルなところで命題の否定について．命題の否定Notは次のようになる．

type Not prop = prop -> Bottom

簡単に言うなら「propならば矛盾する」ので「propではない」である．

具体的な話として，TrueとFalseが等しくないという命題は正しいので証明が与えられるはずだ．

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
data Bottom

type Not prop = prop -> Bottom

data a :==: b where -- propositional equality のようなもの
    Refl :: a :==: a

type a :/=: b = Not (a :==: b)

trueNotEqualFalse :: True :/=: False
trueNotEqualFalse = 証明？

しかし，この証明(実装)を上手く与える方法は実はそんなに無い．EmptyCaseのドキュメントではerror関数を与えていたが，これが型の上で証明に用いるに相応しいものでないことは明らかだし，そのように書かれてもいる．

やるとすれば次のようにTypeFamiliesを使う方法があった．

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
data Bottom

type Not prop = prop -> Bottom

data PropEq a b where -- (:==:) をメインに使っていきたいので別に定義
    Refl :: PropEq a a

type family (a :: k) :==: (b :: k)
type instance True  :==: True  = PropEq True True
type instance True  :==: False = Bottom
type instance False :==: True  = Bottom
type instance False :==: False = PropEq False False

type a :/=: b = Not (a :==: b)

trueNotEqualFalse :: True :/=: False
trueNotEqualFalse = id

この方法では，PropEq True FalseがBottomと同じく値を持たないことが(Haskellにも)わかり，Not (PropEq True False)についてもその実体はBottom -> Bottomという型になるため，TrueとFalseが等しくないことをid関数で証明できる．のだが，執拗にtype instanceを作り込んでダメなケースが矛盾なんだよとHaskellに教えてあげなければならない．しかも，この(:==:)は他のものにも使えるはずだが，それらについてもイチイチ何が矛盾かと教えていたらキリが無い．

正直，他に良い方法があるならとても興味があるので教えて頂きたい．

これが，EmptyCase後では単に次のようにすればよい．

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyCase #-}
data Bottom

type Not prop = prop -> Bottom

data a :==: b where
    Refl :: a :==: a

type a :/=: b = Not (a :==: b)

trueNotEqualFalse :: True :/=: False
trueNotEqualFalse eq = case eq of {}

これまでは，その型には値が無いことはわかっても，それがBottomと同じ型になっているという事実を上手く使えなかったのだが，EmptyCaseによりそれを適切な形で利用できるようになっていることがわかる．

copatterns概要

ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつつ読むと，なにやらこんなカンジのようだ．

タプルをレコードで定義すると，次のようになる．

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

タプルのフィールドとしては1番目の要素であるfstと2番目の要素であるsndを持っていて，recordをopenすればこれらは普通に関数として使える．

通常，タプルを与えるような関数は最終的にタプルをコンストラクトすることになる．

pair : {A B : Set} → A -> B -> A × B
pair a b = a , b

swap : {A B : Set} → A × B -> B × A
swap p = snd p , fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
swap3 t = snd (snd t) , (fst (snd t) , fst t)

で，リリースノートによると，copatternsによってこれらが以下のように書けるようになるのだという．ふぁー

pair : {A B : Set} → A → B → A × B
fst (pair a b) = a
snd (pair a b) = b

swap : {A B : Set} → A × B → B × A
fst (swap p) = snd p
snd (swap p) = fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t)       = snd (snd t)
fst (snd (swap3 t)) = fst (snd t)
snd (snd (swap3 t)) = fst t

つまり，タプルというデータをコンストラクトするのではなく，タプルを作る関数に対して，fstとsndを適用したときの外延的な性質だけで定義しようという試みのようだ．実際にpairやswapやswap3が「タプルの構造を作る」かはわからないけど，fstとsndに対してタプルと同じ挙動をする何かになるので「型としてはタプル」でいいのだ．と，ここまでをウカツに圏論に触れてしまった人が見ると「圏論的な定義だ！カッコイイ！」とか言うんだけど，わたしはあまりよくしらないのでホウホウおもしろいとだけ思っておく．

タプルみたいに簡単なやつならともかくとして，たとえば群とか環とかモナドとかイロイロな代数構造もみんなレコードになっているので，「何かがその代数構造を持つ」ことを示すときに，結合則はこうでー交換則はこうでーみたいな証明の書きかたが少々キレイにカッコイイ感じにはなるかもしれない．

が，これがだから何なんだというか普通にcopatternsを使わずに定義するのと見た目以外の一体どこに差があるんだという話なんだけど，そもそもcopatternsは余帰納的データ型を上手く扱うために導入されたものらしい．

通常，Agdaで余帰納的データ型を作ると，たとえばストリームでは次のように余帰納になる部分の型を∞でラップした型を持つコンストラクタを作る．この部分はブラックボックスになっており，♯で閉じたり♭で空けたりしながら扱うことになる．♯は「空けないとわからない状態の値」を作るためのもので，♭は「空けたときに実際入っていた値」を取り出すものだ．

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

しかし，この表現では次のような一見自明に見える命題が証明できない．

repeat : ∀ {A} → A → Stream A
repeat x = x ∷ ♯ repeat x

lem : repeat 0 ≡ 0 ∷ ♯ repeat 0

「任意のストリームsに対し，ある値eとストリームs'が存在し，ストリームs = 先頭がeで残りがs'のストリーム 」であるにもかかわらず，この種の命題はヒトの直観と異なりどれも証明できない状態になっている．

これは，データはコンストラクトしなければ(使命感)ということを前提とした場合，等価性の証明もコンストラクトベースになることに起因する．いつか必ず末尾のある帰納的データ型に対してはそれで帰納法(再帰関数)を書いて証明すれば(再帰が停止することがわかるので)全く問題無い．しかし，終わりが無いかもしれない余帰納的データ型に対しては，字面上自明に等価な場合を除き，無限に等価性を追い続ける必要が出てきて決定不能になってしまう．

一方，copatternsを使ったストリームの定義では，同様の命題が，

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream

repeat : {A : Set} (a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

lem : repeat 0 ≡ record { head = 0, tail = repeat 0 }

のようになり，ストリームのレコードが持つフィールドheadとtailに関して，観測結果がどちらも同じ式になるため，これらは共に自明にreflにすることができ，期待通りの証明を与えることができる．らしい(まだリリースされてないので試してもいない)

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をしたの私だ