singletonsの型レベル関数を使ってしまうと示せない性質の例
↓の話
実際singletonsが乱舞するんだけど,singletonsから提供されてる型レベル関数の中には使うと「それ以上証明が進まなくなる」やつが結構な割合で含まれてて,面白味のあるない以前に怒りが先行してしまう.あれは型レベル計算のためのライブラリでしかなくて証明のためのライブラリにはなれてない. https://t.co/ckCcUpWQLK
— Noriyuki OHKAWA (@notogawa) January 3, 2019
サンプルコードはここ
サンプルコードでやろうとしていることは「リストの反転はリスト内要素の置換の一種であることを示す」というもの
まず,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したほうが親切じゃないかなと.