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

Haskell

↓の話

サンプルコードはここ

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

まず，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したほうが親切じゃないかなと．