singletonsの型レベル関数を使ってしまうと示せない性質の例

↓の話

サンプルコードはここ

サンプルコードでやろうとしていることは「リストの反転はリスト内要素の置換の一種であることを示す」というもの

まず,2つの型レベルリストが置換の関係にあることを定義する.

data Permutation :: [k] -> [k] -> Type where
  PermutationNil   :: Permutation '[] '[]
  PermutationSkip  :: Sing a -> Permutation xs ys -> Permutation (a : xs) (a : ys)
  PermutationSwap  :: Sing a -> Sing b -> Permutation (a : b : xs) (b : a : xs)
  PermutationTrans :: Permutation xs ys -> Permutation ys zs -> Permutation xs zs

少しこの定義について確認していく.実際にひとつの例について置換関係にあること確認してみる.

testPermutation :: Permutation [1,2,3,4] [2,4,3,1]
testPermutation =
  PermutationTrans (PermutationSwap s1 s2) $
  PermutationTrans (PermutationSkip s2 $ PermutationSwap s1 s3) $
  PermutationTrans (PermutationSkip s2 $ PermutationSkip s3 $ PermutationSwap s1 s4) $
  PermutationSkip s2 $ PermutationSwap s3 s4

置換は同値関係のひとつなので,反射律,

refl :: Sing xs -> Permutation xs xs
refl  SNil        = PermutationNil
refl (SCons x xs) = PermutationSkip x $ refl xs

対称律,

sym :: Permutation xs ys -> Permutation ys xs
sym  PermutationNil          = PermutationNil
sym (PermutationSkip s p)    = PermutationSkip s $ sym p
sym (PermutationSwap a b)    = PermutationSwap b a
sym (PermutationTrans p1 p2) = PermutationTrans (sym p2) (sym p1)

推移律が示せる.

trans :: Permutation xs ys -> Permutation ys zs -> Permutation xs zs
trans = PermutationTrans

先頭への要素の追加と,途中への要素の追加は,置換関係的には同じことを意味する.といった性質も示せる.

here :: Sing a -> Sing xs -> Sing ys -> Permutation (a : xs :++ ys) (xs :++ (a : ys))
here a  SNil ys        = PermutationSkip a $ refl ys
here a (SCons x xs) ys = PermutationTrans (PermutationSwap a x) (PermutationSkip x $ here a xs ys)

さて,反転が置換の一種であること reverseIsPermutation は,

reverseIsPermutation :: Sing xs -> Permutation xs (L.Reverse xs)

のような型をしている.しかし,実際にこれの実装(=証明)を与えようとすると,

reverseIsPermutation SNil = PermutationNil
reverseIsPermutation (SCons x xs) = _

までしか進められない.このtyped holeを確認すると,

[-Wtyped-holes]
    • Found hole:
        _ :: Permutation
               (n0 : n1)
               (Data.Singletons.Prelude.List.Let6989586621679793554Rev
                  (n0 : n1) n1 '[n0])

となっている.Let6989586621679793554Revって何と,singletonsライブラリのreverseの定義を確認すると,

$(singletonsOnly [d|

(snip.)

  reverse                 :: [a] -> [a]
  reverse l =  rev l []
    where
      rev :: [a] -> [a] -> [a]
      rev []     a = a
      rev (x:xs) a = rev xs (x:a)

(snip.)

|])

であり,このreverseの定義からTHで生成されるReverseはexportされているが,reverse定義中のwhere節にあるrevはexportされていないので,そこを期待した型が現れてしまうと証明が進められずに止まってしまう.

これはもうどうしようもないので,やるなら自前でreverseを定義して補助関数も参照できるようにしなければならない.

$(singletonsOnly [d|
 myReverse :: [a] -> [a]
 myReverse l = myReverseAcc l []
 myReverseAcc :: [a] -> [a] -> [a]
 myReverseAcc [] ys = ys
 myReverseAcc (x:xs) ys = myReverseAcc xs (x:ys)
                   |])

このmyReverseの定義から生成される MyReverse や MyReverseAcc により,同様に反転が置換であることを示すと

myReverseIsPermutation :: Sing xs -> Permutation xs (MyReverse xs)
myReverseIsPermutation xs' = gcastWith (nilIsRightIdentityOfAppend xs') (go xs' SNil)
  where
    go :: Sing xs -> Sing ys -> Permutation (xs :++ ys) (MyReverseAcc xs ys)
    go  SNil        ys = refl ys
    go (SCons x xs) ys = PermutationTrans (here x xs ys) (go xs (SCons x ys))

のように示すことができる.nilIsRightIdentityOfAppend は [] がリスト結合演算に対する右単位元であることを示している.

nilIsRightIdentityOfAppend :: Sing xs -> (xs :++ '[]) :~: xs
nilIsRightIdentityOfAppend  SNil        = Refl
nilIsRightIdentityOfAppend (SCons _ xs) = gcastWith (nilIsRightIdentityOfAppend xs) Refl

といったように,singletonsのSingの定義は別段問題無いが,Data.Singletons.Prelude 以下のモジュールで定義されている型レベル関数を使ったインターフェースは,それだけで証明ができなくなってしまうようなものが多数存在している.whereやletなどの補助関数により定義されているものは恐らく全滅じゃないだろうか.なので,こういったものをライブラリ外にexportする場合は,そのままsingletonsのものを使うのではなく適宜hideした上で,自分で定義した証明可能なもので代替してexportしたほうが親切じゃないかなと.

cerealのgetFloat*多用はメモリ長者にのみ許されし贅沢

約1年も書いてなかったのか.


ここ2,3年はそこそこのサイズの配列をどうこうする機会が多く,そういうとき特に何も考えなければ Data.Vector に突っ込んでおきたいキモチになる.で,実際に大きな配列をHaskellで扱うとメモリ不足でOOM Killerに殺されたりするわけだけど,そんな原因のひとつについて.

サンプルコードはココにあるのでヒマな人はどうぞ.

stack init
stack build

まずputterというexecutableがそこそこ大きな要素数を持ったFloatの配列をlittle endianで出力する.

stack exec putter

これでカレントディレクトリにoutput.dat という50MBくらいのファイルができたかと.次にnaive-getterというexecutableでoutput.datを読み出す.やっていることは,Floatの配列に戻して総和を取り,元の配列の総和と一致するかを見ているだけ.

stack exec naive-getter

naive-getterの実装でByteStringからFloatのVector変換する部分は,次の通りcerealでgetFloat32leを使った脳直実装になっている.自然

runGetLazy (V.replicateM len getFloat32le) dat

しかし,コイツが想像以上にメモリをバカ食いするので,適当にプロファイルを見てみる.

stack build --profile
stack exec -- naive-getter +RTS -hc -p -s
stack exec -- hp2ps -c naive-getter.hp
open naive-getter.ps

するとこんな感じになる.すごい.

f:id:notogawa:20180902010856p:plain

8秒ちょいまではputterが出した配列をgetterでも再度作って総和とか評価してる部分なので無視するとして,Unboxed Vectorではないことを考慮しても以降のメモリ消費は立ち上がり過ぎている.どういうことかとgetFloat32leの実装を見に行くと,次のようになっている.

-- | Read a Float in little endian IEEE-754 format
getFloat32le :: Get Float
getFloat32le = wordToFloat <$> getWord32le

(snip.)

{-# INLINE wordToFloat #-}
wordToFloat :: Word32 -> Float
wordToFloat w = unsafeDupablePerformIO $ alloca $ \(ptr :: Ptr Word32) -> do
    poke ptr w
    peek (castPtr ptr)

1要素毎にコレやるわけだが,配列のようなコレクション中の要素を一気にたくさん変換するなら雑に次のような関数でいいかなと別の手段を用意する.

getFloat32leVector :: Int -> Get (V.Vector Float)
getFloat32leVector n = do
  v <- V.replicateM n getWord32le
  return $ unsafeDupablePerformIO $ alloca $ \ptr -> do
    V.mapM (\x -> poke ptr x >> peek (castPtr ptr)) v

これでgetFloat32leを置き換えて次のように使ったrevised-getterを作り,

runGetLazy (getFloat32leVector len)

こちらでもnaive-getter同様にprofileを取る.

stack build --profile
stack exec -- revised-getter +RTS -hc -p -s
stack exec -- hp2ps -c revised-getter.hp
open revised-getter.ps

結果はだいぶ減ったことがわかる.それでもまだ大富豪様ではあるわけだが

f:id:notogawa:20180902011918p:plain

別に総和くらいだったらストリーム処理すばいいんだろうけどそれは簡単のために総和を置いてるだけで,現実的にはもっと配列全体をガチャガチャする処理が控えているためそういうわけにも.

Deep Learning Acceleration勉強会 で発表してきました

Deep Learning Acceleration勉強会 - connpass にてスライドはこちら

www.slideshare.net

普段は出ても関数型言語やら形式手法やらの勉強会とかなため,アウェー感にややソワソワしていた.なんかこの発表で低レイヤマンと思われる可能性があるけどそれでウッカリここに辿り付かれてもスイマセンこのブログの他の記事でもわかるように超高級言語使いですとしか言えない.

思った以上に様々なレイヤーに関する発表がありどこもカリカリにしようとするとガンバリだよねと.そりゃ「計算機科学の全てのレイヤーに精通」とかになっちゃうよなみたいなトコロもこうなってくるとわからんではない.界隈でよくあるやつだとFPGAについての話が無かったので次があるならFPGA勢の進捗は聞いてみたい.


個人的には秋葉さんに「あの記事の者です」と挨拶できたのでよかった.「(ひとつ前の記事)について不快にさせたようで申し訳ない,他のUnagiの方々にもよろしくおねがいします.」と.氏の発表でも自己紹介でKagglerであるというところで「手段を選ばず勝ちにいきます」と言っててここ数日の流れを踏まえてのセリフチョイスしてくれたのかなーと思って面白かった.


既にトゥギャられてるのでこちらも参考

togetter.com

ICFP Programming Contest が本当に縛っていたもの

以前,ここ数年のICFP Programming Contestについて思っていることについてのツイート(群の一部)が, Rustが最強のプログラミング言語である証明 — hayato.io で取り上げらたため, @chokudai さんに届いて反応してくれたようでうれしい.一連の氏のツイートをRTした後,思わず,

一点,ツイッターだと前後の文脈ザックリ落ちることがあるから仕方ないんだけど,正しく伝わってるのか気になったのが,「縛り」の本質について,

取り上げられたツイートの直後のこのツイートからもわかるように,同僚という固定メンバーとやることが決まってるオシゴトとは異なりチーム組みからできるコンテストでも,推し言語の差を強い制約と認識した場合「いくら強いことがわかってても宗教が違うため組めない奴が出てくる」ことこそがこのコンテストにおける重要な「縛り」であり,何も「言語を一つしか使わないこと」が「縛り」の本質ではないと思っている.

これは,このときの流れの中で @mametter さんとのやりとりでも,

とにかく強い奴で集めたから強いぜ!ということだったら本当にナンデモアリな他のコンテストだろうがそれこそオシゴト・現実世界でもみんなわかっている.

勝ちに行くのもコンテストに参加する上であたりまえのことだし,ルールが何かこの点について縛ってるわけではないのでナンデモアリなコンテストと形式は同じなんだけど,折角 ICFP Programming Contest なら「組めない奴が出てくる」という特徴を愉しめばいいんじゃないかなというのが私見.

まぁ,

という話もあるので, ICFP Programming Contest も他のコンテストと今はもう何も変わらないのかもしれない.たぶん似たようなことを感じてるのは他にも @shinh さんとかくらいなのかな.

いずれにせよおっさんばかり…なの…では?「組めない奴が出てくる」と思ってたのも思い込みだったのかもしれない.最初から ICFP Programming Contest は言語なんてどうでもよかったのかもしれない.

というわけで結論としては最終的にどうでもいい話であるという所に落ち着く.


ただ, @chokudai さんは自らもコンテスト(サイト)を運営する者として,他のコンテスト(だけじゃなく何らかのコミュニティや文化に)乗り込む場合,勝ちだけじゃなくて「それは何を目的にして開催されているのか」についてのこだわりに対し,単に強さを振り回し彼のツイートにある言葉を借りるならば「水差す」ことがないよう多少思いを巡らせて欲しいかなと思う部分もある.自分は彼のつよいぜドヤァみたいなツイートも好きだし実際それ以上につよい.単なる勝ちだけにこだわらず,そういった部分もリスペクトした上でなお勝つ力が彼には十分あると思っている.

一方,彼の場合コンテストで身を立てるのもオシゴトな部分がある.みんながプライベートとして参加するコンテストであっても彼にとっては宣伝・広報を含んだ商業的な意味をメインではないにしろ持たざるを得ないし,周囲もそう捉えると考えるのが自然だろう.彼の事業性質上は強いメンバー集めて勝ってブランディング・アピールするというのはメンバーを集める上でも効果があり正着だ.彼自身がコンテスト強くて成功するモデルケースにならなければならないのだから.だとしたら舐めプにも見えるような甘いムーブをオーディエンスに見せるわけにもいかないだろうし,ましてやそれで負けるのもマイナスではないにしろ機械損失的なものはあるかもしれない.このあたりの立場を考慮すると単にコンテストに参加するだけにしても他の参加者にはない期待を背負っているしリスクを取っている部分があり大変だろうなぁと勝手に心配している.

これからも体に気を付けてがんばって頂きたい.

TensorFlowで訓練したパラメータをChainerのモデルにrestoreする

何がどうなってか深層学習〜的なものに触れる機会が増えたので,何かそれっぽい話を

「他のフレームワークに比べてなんだか学習済み(pre-trained)モデルが公開されてないような?」

Chainerを使ってみた深層学習マンはきっとこのお気持ちになったことがあるんじゃないだろうか.ユーザ数の差だろうか?数は力だよ兄貴!Caffeのモデルファイル(.caffemodel)であれば,ものによってはchainer.links.caffe.CaffeFunctionでロードできるので一応使えはする.global pooling 等で非対応がありロードできないこともあるが,できない部分は飛ばしてロードしてスキマを自分で書いて〜とかできなくはないので,スンナリとロードはできなくともガンバリでロードはできる気がする.

一方,なんだかんだTensorFlowのpre-trainedモデルがckptファイルで公開されていることは多い.

こいつをいざChainerから利用したいとなってもあんまり記事とかが見当たらない.まぁ逆についても無いというか,そもフレームワークを越えてどうにかする話があんまりない.どうにかしたいという雰囲気や動きは散見されるけど,全体からみたらまだ二の次案件のように見える.よく訓練された深層学習マンにはこんなこと呼吸に等しいタスクだからなのか,それともあんまりこういったマネはしないからなのか,もしくは,そんなことせんでも計算資源がありあまってて新規に学習しちゃえばいいだろということなのか.

いずれにせよ,あのモデルをChainerで書いてみたちょっとちゃんと動くか試したい…けど学習済みのものは無くて〜程度のことで,最近あの東京大学でさえ節約していると噂の貴重な貴重な電力(と時間)を消費して新規に学習し始めるというのも心苦しい.Gentoo使いならおさらだ.なので,やっぱりクロスフレームワークでも再利用したいというのはあるんじゃないかなと.

というわけでckptファイル(群)のパラメータをChainerのモデルにrestoreする方法は,

  1. ckptファイル(pre-trainedなモデル)を入手
  2. そのckptファイルを学習したTensorFlowのモデルを入手
  3. TensorFlowのモデルを眺めて各パラメータに付けられた名称を調べる
  4. TensorFlowのモデルと同じモデルをChainerで書く
  5. TensorFlowのCheckpointReaderでckptファイルを開く
  6. ckptファイルから各名称のパラメータを引っ張り出す
  7. TensorFlowとChainerではweightのdimの順番が違うので必要に応じて転置
  8. chainer.Linkの対応するパラメータに代入していく

みたいな流れになる.

class CKPT:
    def __init__(self, path):
        # ckptファイルを開く
        self.ckpt = tf.train.NewCheckpointReader(path)

    # ndim見て決め打ってるけど,そのパラが何のものかはモデルからわかってるので,
    # 本当は個別にget_conv2d_weightとかget_fc_weightとかを用意したほうがいい
    def get(self, name):
        arr = self.ckpt.get_tensor(name)
        nd = np.ndim(arr)
        # 必要に応じて転置
        if nd == 4: # おそらく 2D Convolution だろうと
            return arr.transpose(3,2,0,1).copy() # TensorFlow -> Chainer
        if nd == 2: # おそらく Fully Connected だろうと
            return arr.transpose(1,0).copy()     # TensorFlow -> Chainer
        if nd == 1: # biasやBatchNormのパラメータだろうと
            return arr
        else:
            pass # unknown weight type # TODO: raise Exception

(snip.)

# Chainer版のモデル
class YourModel(chainer.Chain):
    def __init__(self):
        super(YourModel, self).__init__(
            c0 = L.Convolution2D(3   ,   16, 7, 3, 3, nobias=True),
            bn = L.BatchNormalization(16, 0.9997, 0.001)
            c1 = L.Convolution2D(None,   32, 3, 1, 1),
(snip.)
        )

    def __call__(self, x):
(snip.)

    def restore_from_ckpt(self, path):
        ckpt = CKPT(path)
        # 各名称のパラメータを引っ張り出す
        self.c0.W.data        = ckpt.get('PreTrainedModel/Conv2d_0/weights')
        self.bn.beta.data     = ckpt.get('PreTrainedModel/BatchNorm/beta')
        self.bn.gamma.data    = ckpt.get('PreTrainedModel/BatchNorm/gamma')
        self.bn.avg_mean.data = ckpt.get('PreTrainedModel/BatchNorm/moving_mean')
        self.bn.avg_var.data  = ckpt.get('PreTrainedModel/BatchNorm/moving_variance')
        self.c1.W.data        = ckpt.get('PreTrainedModel/Conv2d_1/weights')
        self.c1.b.data        = ckpt.get('PreTrainedModel/Conv2d_1/bias')
(snip.)

if __name__ == '__main__':
    model = YourModel()
    model.restore_from_ckpt('pre-trained.ckpt')
(snip.)

もちろん,これで万事うまくいくというわけではないだろうが.

名前調べるのめんどくさいなぁという場合,CheckpointReaderのget_variable_to_shape_mapでshapeと共に一覧できるので,それ見て判断とかでもできなくはないこともある.

コンテキストの順番を入れ換えると互換性が崩れることがある

(注:この記事はかなり前に書いて公開し忘れていたことに今日気付いたものです.もう当たり前になってるかもしれないけどもったいないので一応)

ghc8以降TypeApplications拡張が入ったこともあり一応の注意喚起.

たとえば,次のように関数fとgを定義する.時系列的にはfの型をgの型に変更したような想定で.

data X a b = X a b

f :: (Show a, Show b) => X a b -> String
f (X a b) = show a ++ show b

-- fと比べて型変数aとbに対するShowコンテキストを入れ換えたもの
g :: (Show b, Show a) => X a b -> String
g = f

普通に使っている分にはfからgの変更に問題無い.

x :: X Int Char
x = X 1 '0'

fx :: String
fx = f x

gx :: String
gx = g x

だけど,TypeApplications付けて使ってる箇所は型検査に失敗する.

{-# LANGUAGE TypeApplications #-}

fx :: String
fx = f @Int x

gx :: String
gx = g @Int x -- Error

といったように,コンテキストの順番変更も型の変化に相当する場合がある.また,コンテキストを減らすことができるケースであっても,それにより型変数の出現順が変わるとTypeApplicationsにより型検査に失敗するようになることがある.

互換性破壊してるのにhackageバージョニングポリシに従ったバージョン上げを行っていないライブラリをアップロードしてしまうことになるかもしれないので,ライブラリ作者はTypeApplications拡張の存在も気にして互換性の管理をするべきだと思われる.逆に,ライブラリ利用者としてはTypeApplications拡張使っているとこういう漏れてきた互換性破壊を踏んでしまうかもしれないという認識を持つべきなのかな.

問題を解決するつもりでキッチリ型を付けた先にある高い壁


過ぎたるは猶及ばざるがごとし.


最近null安全?だかの話のからみで,(静的な)型で契約云々を表現してシアワセになれるんだぜーと言うのをチラホラ見聞きする.たとえば,pythonで統計なり機械学習なりやっててnumpy弄るような人が,ndarray(多次元配列)shape(多次元配列の形)が合わずエラーで落ちたりとかそういうアレについて云々という.なるほど型があれば実行前に止めることができ,実行時,エラー*1になってファーみたいなことは避けられるだろう.

しかし,これが天国へ続く道かどうかはまた別の話.(依存)型で舗装しているのは地獄への道かもしれないのだ.冒頭ツイートの通り陰腹召してでも諫めておかねば,その希望,容易に絶望に反転し得る.

では実際に見ていこう.内容としては,numpy ndarrayとその上での操作をいくつか取り上げ,配列要素だけでなくshapeまで型レベルで扱うことで,間違えたshapeを持つ操作を禁止できるようにしてみるというもの.サンプルコードはコチラ.全体の流れとしてはndarrayを定義,reshape,dot,transposeを実装,それらを使ってtensordotを実装してみるとどうなるかをみていく.

前回の記事に続き,今回も型レベルでアレコレするのでアタマのほうはこんな感じ.singletonsも使っていく.

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}

import Data.Singletons
import Data.Singletons.Prelude.Enum
import Data.Singletons.Prelude.List
import Data.Singletons.Prelude.Num
import GHC.TypeLits

shapeと中身の型aを型レベルに持つNDArray型を定義する.今回は中身の計算には興味が無いので,shapeに関する情報だけ抱えておくことにする.

data NDArray (shape :: [Nat]) a = NDArray (Sing shape) -- 中身はshape意外省略

まずは,numpy.reshapeを実装してみる.

reshape :: Product from ~ Product to => Sing to -> NDArray from a -> NDArray to a
reshape = const . NDArray

素数が同じでshapeの違う別のndarrayに変換する操作だが,別段不可思議なところは無い.コンテキスト部分により要素数が同じという条件を付けており,以下のように確かに条件に合わない場合は型検査で失敗する.

-- reshape可
reshapeable :: NDArray '[2,3,4] a -> NDArray '[3,8] a
reshapeable = reshape sing

-- 型検査でreshape不可 (次元の積が合わない)
-- unreshapeable :: NDArray '[2,3,4] a -> NDArray '[3,3,4] a
-- unreshapeable = reshape sing -- Couldn't match type ‘24’ with ‘36’

次に,numpy.dotを実装する.

dot :: (Last xs ~ Last (Init ys), Num a) =>
       NDArray xs a -> NDArray ys a -> NDArray (Init xs :++ Init (Init ys) :++ '[Last ys]) a
NDArray xs `dot` NDArray ys = NDArray (sInit xs %:++ sInit (sInit ys) %:++ SCons (sLast ys) SNil)

dot積を取る2つのndarrayのshapeから結果のshapeが決定する.1つ目のshape最後の要素と,2つ目のshape最後から2番目の要素が同じという条件が付いている.これも,以下のように条件に合わない場合と結果の型が合わない場合は型検査で失敗する.

-- dot可
dottable :: Num a => NDArray '[2,3,4] a -> NDArray '[3,4,2] a -> NDArray '[2,3,3,2] a
dottable = dot

-- 型検査でdot不可 (結果の型が合わない)
-- undottable1 :: Num a => NDArray '[2,3,4] a -> NDArray '[3,4,4] a -> NDArray '[2,3,3,2] a
-- undottable1 = dot -- Couldn't match type ‘4’ with ‘2’

-- 型検査でdot不可 (引数の型が合わない)
-- undottable2 :: Num a => NDArray '[2,3,4] a -> NDArray '[4,3,2] a -> NDArray '[2,3,4,2] a
-- undottable2 = dot -- Couldn't match type ‘4’ with ‘3’

最後に,numpy.transposeを実装する.

transpose :: Sort axes ~ EnumFromTo 0 (Length shape - 1) =>
             Sing axes -> NDArray shape a ->
             NDArray (Map ((:!!$$) shape) axes) a
transpose axes (NDArray shape) =
  NDArray (sMap (singFun1 (toProxy shape) (shape %:!!)) axes) where
    toProxy :: Sing (shape :: [Nat]) -> Proxy (Apply (:!!$) shape)
    toProxy _ = Proxy

条件は少し複雑になり,軸(次元)の転置方法に相当するパラメータaxesが,ちゃんとshape全体のpermutationを意味するパラメータになっていなければならない.これも,次のように各理由で整合しない場合は型検査で失敗する.

transposable :: Sing '[1,0,2] -> NDArray '[2,3,4] a -> NDArray '[3,2,4] a
transposable = transpose

-- transpose不可 (axesにshapeの長さ以上のものが含まれる)
-- untransposable1 :: Sing '[1,0,3] -> NDArray '[2,3,4] a -> NDArray '[3,2,4] a
-- untransposable1 = transpose -- Couldn't match type ‘3’ with ‘2’

-- transpose不可 (axesに同じ要素が2つ以上含まれる)
-- untransposable2 :: Sing '[1,0,0] -> NDArray '[2,3,4] a -> NDArray '[3,2,2] a
-- untransposable2 = transpose -- Couldn't match type ‘1’ with ‘2’

-- transpose不可 (axesの長さとshapeの長さが一致しない)
-- untransposable3 :: Sing '[1,0] -> NDArray '[2,3,4] a -> NDArray '[3,2] a
-- untransposable3 = transpose -- Couldn't match type ‘'[]’ with ‘'[2]’

-- transpose不可 (結果の型が合わない)
-- untransposable4 :: Sing '[1,0,2] -> NDArray '[2,3,4] a -> NDArray '[3,2,5] a
-- untransposable4 = transpose -- Couldn't match type ‘4’ with ‘5’

さて,reshape,dot,transposeが定義されたので,これらを使ってnumpy.tensordotが定義できる.はずである.実際に「こうすればいいよね」という感覚に従って実装してみよう.

tensordot :: (Num a, ns ~ Nub ns, ms ~ Nub ms,
              Map ((:!!$$) xs) ns ~ Map ((:!!$$) ys) ms) =>
             NDArray xs a -> NDArray ys a -> (Sing ns, Sing ms) ->
             NDArray (Map ((:!!$$) xs) (EnumFromTo 0 (Length xs - 1) :\\ ns) :++
                      Map ((:!!$$) ys) (EnumFromTo 0 (Length ys - 1) :\\ ms)) a
tensordot x@(NDArray xs) y@(NDArray ys) (ns, ms) = result where
  range n = sEnumFromTo (sing :: Sing 0) (n %:- (sing :: Sing 1))
  notinns = range (sLength xs) %:\\ ns
  notinms = range (sLength ys) %:\\ ms
  tx = transpose (notinns %:++ ns) x
  ty = transpose (ms %:++ notinms) y
  dimsIn xs = sMap (singFun1 (toProxy xs) (xs %:!!)) where
    toProxy :: Sing (shape :: [Nat]) -> Proxy (Apply (:!!$) shape)
    toProxy _ = Proxy
  (oldxs, oldys) = (dimsIn xs notinns, dimsIn ys notinms) where
  rtx = reshape (SCons (sProduct oldxs) $ SCons (sProduct $ dimsIn xs ns) SNil) tx
  rty = reshape (SCons (sProduct $ dimsIn ys ms) $ SCons (sProduct oldys) SNil) ty
  result = reshape (oldxs %:++ oldys) (rtx `dot` rty)

とりあえずだが,コンテキストによる条件の表現としては,tensordotを取る2つのndarrayのshapeに対し,dotを取る部分の軸指定がpermutationの部分列になっており,かつ,指定された軸について同じ形をしているという条件相当を付けておいた.

このtensordotの定義は型検査に失敗し,5件くらいしか無いクセにトータル1200行くらいの長大なエラーメッセージを吐く.もちろん実装者も吐く.そして泣く.これは,ニンゲンには自明なことであっても,機械(型検査器)にはわからないことがあるためだ.それは,

  • transpose時の条件,転置方法が正しくpermutationに相当する値(型レベルの)になっているかがわからない.(130行のエラー x txとtyについて2箇所)
    • ニンゲンにとって,ある列の中からいくつかを取り出し(notinnsやnotinms),取り出した後の最初や最後にくっつけて(transposeの引数)も,順番が変わるだけで中身は一緒(=permutation)であることはわかる.
    • けど,機械(型検査器)にとっては自明ではない.
  • reshape時の条件,reshape前後の要素数が(型レベルで)同じであるかどうかがわからない.(280行のエラー x rtxとrtyについて2箇所 + 400行のエラー x resultについて1箇所)
    • ニンゲンにとって,ある正数の列を2グループに分け(xsに対するoldxsとそれ以外,ysに対するoldysとそれ以外),それぞれの積を取ったものの積は,元の列の積と同じことはわかる.
    • けど,機械(型検査器)にとっては自明ではない.

ことからきている.dotの条件についてのエラーが出ていないが,この条件についてはわかっているのかというと,それはtensordot自体の条件(Mapのやつ)から機械(型検査器)にもわかる.また,reshapableやtransposable等で使ったとき問題無かったのは,具体的な型レベルでの値(型レベル自然数リテラル)が入っているためであり,対して今回のtensordotの定義中では(型)変数のままなので,機械(型検査器)が計算を進められるかの状況が異なる.

このエラーを解決するためには,恐らく2つ方法がある.

  • 無視する.といってもエラーではどうしようもないので前回の記事と同じような方法を使い,transposeやreshapeを使ってもエラーにならないケースを作り出す.ここで無視するのは以下2点だ,
    • (ニンゲンとって自明にunreachableな)エラーケースがコード上発生すること
    • これらを使う人には条件を示すことを要請する癖に,自分が使うときは自明だからいいだろと無視するカッコ悪さ
  • 使える情報から機械(型検査器)がわかる情報にニンゲンが変換して教えてあげる.

前者について,ニンゲンにとって自明とは言うものの,複雑な条件になると本当に自明かどうかはニンゲンにもわかるか怪しいし,そもそも自明だと思ったこと自体も錯誤かもしれない.わざわざ型レベルでどうにかしようという話自体,そういったニンゲンによるミスをどうにかしようというモチベーションだった筈であり,解決の方向性としてはどうなのソレという感がある.

後者が正攻法となるが,実は,それがこの界隈で何と呼ばれているか私達は既に知っている.それは定理証明と呼ばれるヤツである.こうなるとワンチャン証明器からextractしたほうが使い易いまである.Haskellでも実際GHC.TypeLits.Natはペアノ数ではない*2ようなので,そのままではInductionが効かず証明相当のサギョウがやりにくいことこの上無かったりする.


まとめると,各種契約を型で云々~に期待されるようガチガチに型レベルで設計されたものは,言語にも使う側にも型レベルでガチな取り組みを求められることがある.型レベルへ条件を持ち上げることは「人はミスせずに作業ができるか」という問題を「人は定理証明ができるか」という問題へと変換することなのだ.となると,最近null安全?とかの話から複雑な契約も型でヤッター!と言ってる方々はたぶん皆このへんについても「覚悟完了!当方に迎撃の準備有り!」なので,定理証明についても何でも*3聞いて大丈夫ということになる.やったぜ

*1:ChainerやらTensorFlowやらで時間をかけた学習後セーブもせず喰わせるデータ(のshape)間違えたりとか

*2:そもそもなんでこうなってるんだっけ?型レベル自然数リテラルはペアノ数へのエイリアスでよかったようにも思うんだけど

*3:ん?今