しりとりの圏の回答、または定理証明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の定理証明ではよくあることです。 (12/9追記) これはHaskellだからとかは関係なくて、必要な証明をサボっているだけです。ちゃんとやったバージョンは こちら になりますが、さすがに複雑なので次節で紹介する方法を使うのがベターだと思います。

出来上がったコードを改めて見てみると、何を証明したのかが今一つ分かりづらいですが、AllSiri a b 型の値を作れた事をもって、 KnownNats (xs :++ xs1) が示せたのだとお考え下さい。

という訳で、以下のように合成結果を文字列として出力することに成功しました。

main :: IO ()
main = do
  let はすけるびー = るびー . はすける
  putStrLn $ showAllSiri はすけるびー
  return ()

はすける = (略)
るびー = (略)

(12/9追記) constraintsを使った方法

コメント欄にてnotogawa様より、もっとちゃんとした方法を教えて頂きました。
https://gist.github.com/notogawa/105ad2762faf344c820156465080367f

constraintsパッケージは ConstraintKinds GHC拡張によって、制約を直接的に扱う事を可能にしています。これによって「KnownNats xs かつ KnownNats xs1 のとき KnownNats (xs :++ xs1)」という命題を直接証明してやれば、最初はエラーになった AllSiriContent (siriConcat x y) を通す事ができます。
すごい！

なお

Haskellの依存型については、さらにアドバンスドな事が計画されているそうです。

この二つの変更だけでHaskellが完全な依存型言語になるというのが面白い。さらに、従来から当然視されていた特徴はなるべく壊さないようになっていて、例えば実行時に渡ってくる値とコンパイル時に消去される型は厳格に(構文レベルで)区別されるし、型推論はちゃんと動くし、止まらない関数も書ける

— mkotha (@mkotha) 2017年11月8日

今回は型レベルのリストを扱うためにGHC.TypeLits.Listのユーティリティを多用したり、型から値を作るためにProxy型を使用したり(今回活躍したNatListは、実質的にはProxyの配列です)といった独特の点が多くありましたが、これがもう少し自然に書けるようになるのかな、と勝手に期待しています。

それから、本来この枠で書こうと思っていたpipesの記事については、Haskell (その3) Advent Calendar 2017 の12/20に回そうと思います。よろしくお願いします。