しりとりの圏の回答、または定理証明Haskellを少しだけ
この記事は、Haskell (その2) Advent Calendar 2017 の4日目の記事です。
同アドベントカレンダーの5日目の記事、しりとりの圏の実装(未完) の問題を解いてみたのと、その際に定理証明Haskellのちょうどいい例題が出て来たので、解説してみます。
なお4日目の記事が5日目の記事のアンサーになるのは時空間の歪みによるもので正常な動作です。日付順に読まれている方については、申し訳ございませんが5日目の記事に飛んでいただけるようお願い致します。
idを定義するために
さしあたって、しりとりの圏を構成するSiriの定義を、親記事より拝借します。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main where
import GHC.TypeLits (Nat, KnownNat)
import GHC.TypeLits.List (KnownNats, natsVal, elimNatList, NatList(..), natsList)
import Data.Proxy (Proxy(..))
import Control.Category (Category(..))
import Data.Singletons.Prelude.List ((:++))
import Prelude hiding ((.))
-- しりとりの圏(単相)
data Siri (xs :: [Nat]) (a :: Nat) (b :: Nat) where
SiriUnit :: Proxy a -> Siri '[a] a a
SiriCons :: Proxy a -> (Siri ys b c) -> Siri (a ': ys) a c
-- 射の合成
siriConcat :: Siri xs a b -> Siri xs' b c -> Siri (xs :++ xs') a c
siriConcat (SiriUnit proxy) ks = SiriCons proxy ks
siriConcat (SiriCons proxy ks) ks' = SiriCons proxy (ks `siriConcat` ks')
-- 射を文字列に
showSiri :: KnownNats xs => Siri xs a b -> String
showSiri (_ :: Siri xs a b) = map (toEnum . fromEnum) $ natsVal (Proxy @xs)
Siri型はしりとりの圏の射を1つ表現する事ができるデータ型です。これを総称化した data AllSiri a b = forall xs. AllSiri (Siri xs a b) を圏にする、すなわち Category のインスタンスにして、更に文字列化する関数 showAllSiri を定義するのが、解くべき問題になります。
しかし、そのためにはxsにKnownNatsの制約を掛ける必要があり、それをどうするかが問題でした。
この記事では、親記事のこちらのアプローチを深堀りしてみます。
では AllSiri 側に KnownNats 制約を与えるとどうかというと、この場合 Category の型変数 a :: Nat や b :: Nat が KnownNat とは限らないため、恒等射 id を定義するときに a :: Nat を AllSiri 内にエンコードすることができなくなります。
この記事で行う試みは以下のように、AllSiriに恒等射のためのコンストラクタを追加してやることです。
data AllSiri a b where
AllSiriId :: AllSiri a a
AllSiriContent :: KnownNats xs => Siri xs a b -> AllSiri a b
こうすると、とりあえず id と showAllSiri が実装できます。
showAllSiri :: KnownNat a => AllSiri a b -> String
showAllSiri (AllSiriId :: AllSiri a b) = showSiri (SiriUnit (Proxy @a))
showAllSiri (AllSiriContent k) = showSiri k
instance Category AllSiri where
id = AllSiriId
f . g = g `allSiriConcat` f
concatの証明
が、次に問題になるのは allSiriConcat の定義です。
allSiriConcat :: AllSiri a b -> AllSiri b c -> AllSiri a c
allSiriConcat AllSiriId k = k
allSiriConcat k AllSiriId = k
allSiriConcat (AllSiriContent x) (AllSiriContent y) =
AllSiriContent (siriConcat x y) -- エラー！
エラーの内容は以下の通り。
• Could not deduce (KnownNats (xs :++ xs1))
arising from a use of ‘AllSiriContent’
from the context: KnownNats xs
bound by a pattern with constructor:
AllSiriContent :: forall (a :: Nat) (b :: Nat) (xs :: [Nat]).
KnownNats xs =>
Siri xs a b -> AllSiri a b,
in an equation for ‘allSiriConcat’
なるほど、xsとxs1が KnownNats だったからといって、xs :++ xs1 を勝手に KnownNats にしてくれる訳ではないようです。ここは依存型らしく「証明」の作業が必要になります。
リストにまつわる証明には、帰納を使うのが定石です。急に証明の用語が出てきて気後れしそうですが、リストの帰納というのは「再帰的にパターンマッチする」程度の意味です。詳しくは構造的帰納法で調べてみて下さい。
リストの帰納を綺麗に行う事ができる elimNatList という関数もGHC.TypeLits.Listで定義されていますが、今回は型が合わないので自力で再帰してみます。
allSiriConcat :: AllSiri a b -> AllSiri b c -> AllSiri a c
allSiriConcat AllSiriId k = k
allSiriConcat (AllSiriContent c) k = prependToAllSiri natsList c k
prependToAllSiri :: KnownNats xs => NatList xs -> Siri xs a c -> AllSiri c b -> AllSiri a b
prependToAllSiri _ (SiriUnit _) k = k
prependToAllSiri _ x AllSiriId = AllSiriContent x
prependToAllSiri (pr' :<# ns) y@(SiriCons _ x :: Siri xs a c) k =
case prependToAllSiri ns x k of
AllSiriId -> undefined -- prependToAllSiri ns x k == id のときk==idだが、分岐よりk/=id
AllSiriContent k' -> AllSiriContent (SiriCons pr' k')
NatList という余分な引数を導入してやるのがポイントです。NatList はGHC.TypeLits.Listで、こんな感じで定義されています。
data NatList :: [Nat] -> * where
ØNL :: NatList '[]
(:<#) :: (KnownNat n, KnownNats ns)
=> !(Proxy n) -> !(NatList ns) -> NatList (n ': ns)
上の例では :<# コンストラクタでGADTパターンマッチしてやる事で、 KnownNats ns の制約を導出でき、これにより AllSiriContent コンストラクタを被せるための条件を満たせます。前述の elimNatList がこの操作を内部で行っていたので、真似してやってみたら上手く行きました。あと undefined が残っているのはご容赦下さい。Haskellの定理証明ではよくあることです。
出来上がったコードを改めて見てみると、何を証明したのかが今一つ分かりづらいですが、AllSiri a b 型の値を作れた事をもって、 KnownNats (xs :++ xs1) が示せたのだとお考え下さい。
という訳で、以下のように合成結果を文字列として出力することに成功しました。
main :: IO ()
main = do
let はすけるびー = るびー . はすける
putStrLn $ showAllSiri はすけるびー
return ()
はすける = (略)
るびー = (略)
なお
Haskellの依存型については、さらにアドバンスドな事が計画されているそうです。
今回は型レベルのリストを扱うためにGHC.TypeLits.Listのユーティリティを多用したり、型から値を作るためにProxy型を使用したり(今回活躍したNatListは、実質的にはProxyの配列です)といった独特の点が多くありましたが、これがもう少し自然に書けるようになるのかな、と勝手に期待しています。
それから、本来この枠で書こうと思っていたpipesの記事については、Haskell (その3) Advent Calendar 2017 の12/20に回そうと思います。よろしくお願いします。
全くそんなことはないと思います．今回の
allSiriConcatに対してであれば，たとえばconstraintsパッケージを使って次のように与えてあげればよいのではないでしょうか．
https://gist.github.com/notogawa/105ad2762faf344c820156465080367f
undefinedが残るという状況は，証明できるはずだけど単に証明ぢからが不足しているか，
もしくはどうあがいても証明できないおかしな命題を与えてしまっているかの
どちらかの状況にあると疑ったほうがひとまずは妥当です．
ありがとうございます
デフォルトの
Category型クラスの定義では構成できないものと思ってたので、ビビりました（笑。allSiriConcat AllSiriId k = kの通り、恒等射は合成時に捨てられるのでKnownNats制約が要らないわけですね。納得です。