しりとりの圏の実装(未完) #Haskell

haskell入門の著者の一人、hirataraです。といっても、このエントリは書籍とはまったく関連のないお遊びです

ということで、今回は10年ほど前のエントリであるしりとりの圏を、Haskellで実装しようと試みましたので、その過程をだらだらと書いていきます。

前置き

しりとりの圏とは以下のようなものです。

対象(Object)は文字 'あ' 'い' 'う' ・・・
射(Morphism)は文字列 "はすける" :: 'は' -> 'る'
恒等射(Identity)は一文字 "あ" : 'あ' -> 'あ'
合成は文字列の結合 "るびー" . "はすける" == "はすけるびー"

この圏は直感的にわかりやすい圏で、圏論の初学者が集合圏以外の圏に触れるきっかけとしてはちょうどよい題材と言えます。

しかし、「圏論と言えばHaskellだろう」と安易に考えてこの圏をHaskellのプログラムで表現しようとすると、すぐに暗礁へ乗り上げてしまいます。というのも、Haskellで用意されている圏を表す型クラス Category の対象は型だからです。しりとりの圏の対象は、値である 'あ' や 'い' などの文字ですので、ここに大きなギャップがあります。標準規格のHaskellではしりとりの圏をそのまま Category 型クラスのインスタンスにすることはできません。

しかし、GHCには Datatype promotion という拡張が用意されています。この拡張は、値を昇進させて型として使うことができるようにするというものです。まさに今回の目的にぴったりですね！この拡張を使えば、しりとりの圏を Category 型クラスのインスタンスをにできるかもしれないという希望が出てきました。

単語を型にエンコードする

DataKinds 拡張はデータコンストラクタを型コンストラクタとしても使えるようにしてくれるものですが、それ以上でもそれ以下でもありません。例えば、 型レベルに昇進した値 (型、です) から、その値を取り出して式の中で使うといったことをしたければ、別のパッケージ(例えば singletons )が必要となります。

そこで今回は、GHCに用意されている Nat カインドに属する型レベル自然数を使うことにします。文字のUnicodeポイントを Nat カインドを持つ型レベル自然数として表現するわけです。

また、それにあわせて文字列は単語を文字列の値として持つのではなく、型レベルリストを使って [Nat] カインドを持つ型にエンコードします。そうすると、 GADTs 拡張を用いて、以下のような定義ができるでしょう¹。

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

xs :: [Nat] が単語、 a :: Nat が始まりの文字、 b :: Nat が終わりの文字を表す型です。例えば、 Siri '[12427, 12403, 12540] 12427 12540 という型は「るびー」という単語を表します。しりとりの圏で言うと、 12427 型から 12540 型への射と言えますね。

また、射の合成は singletons ライブラリから型レベルリストの合成である (:++) を借りてくれば、簡単に定義することができます。型レベルでだけ合成が行われて、値は単一の値 proxy を形式的に引き回しているだけになってます。言い換えると、コンパイル時にのみ意味のある計算が行われるということですね。

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')

Category型クラスのインスタンスとする

さて、このまま Siri xs 型コンストラクタを Category 型クラスのインスタンスとしたいところですが、単語を型にエンコードした部分 xs :: [Nat] が可変となっています。しりとりの圏の文脈で言うと、1つの Siri xs 型コンストラクタからは、1つの単語しか生成できないということです。きちんと全ての単語が表現できるような型コンストラクタを用意しないと圏とは言えません。

そこで存在型 ExistentialQuantification によって Siri をラップします。

data AllSiri a b = forall xs. AllSiri (Siri xs a b)

これで xs はどんな単語でも良いことになりました。幸運なことに、 AllSiri 型の合成は siriConcat を用いて次のように書けます。

allSiriConcat :: AllSiri a b -> AllSiri b c -> AllSiri a c
allSiriConcat (AllSiri k1) (AllSiri k2) = AllSiri (siriConcat k1 k2)

これでめでたく AllSiri 型コンストラクタは Category クラスのインスタンスとなります。 AllSiri のカインドは Nat -> Nat -> * であり、先頭の文字を表す Nat カインドを持つ第一引数の型から、最後の文字を表す Nat カインドを持つ第二引数の型への射である、単語を表現する型です。カインド * である型から型への射ではなく、カインド Nat を持つ型レベル自然数から型レベル自然数への射を持つインスタンスをきちんと定義できました。

instance Category AllSiri where
  id = AllSiri (SiriUnit Proxy)
  f . g = g `allSiriConcat` f

これを使ったコードは次のようなものになります。型チェックにより、しりとりの関係にないような単語同士を連結しようとするとコンパイルできません。 . の定義は、後ろの引数を前の引数と連結している、ということに気をつけましょう。

main :: IO ()
main = do
  let はすけるびー = るびー . はすける
      -- これはだめ = はすける . るびー
  return ()

はすける = AllSiri はすける'
はすける' = SiriCons (Proxy @12399)
         $ SiriCons (Proxy @12377)
         $ SiriCons (Proxy @12369)
         $ SiriUnit (Proxy @12427)

るびー = AllSiri るびー'
るびー' = SiriCons (Proxy @12427)
       $ SiriCons (Proxy @12403)
       $ SiriUnit (Proxy @12540)

なお、ここまでのコードを動かすための import 文は以下のようになります。 DataKinds 以外にも様々な拡張が必要になりますね。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.TypeLits (Nat)
import GHC.TypeLits.List (KnownNats, natsVal)
import Data.Proxy (Proxy(..))
import Control.Category (Category(..))
import Data.Singletons.Prelude.List ((:++))
import Prelude hiding ((.))

また、 singletons と typelits-witnesses パッケージを使うので、 stack を使っている方は予め stack build singletons stack build typelits-witnesses としておくといいでしょう。

(未完)型から単語を取り出す

と、残念ながらうまくできたのはここまでです。次に、しりとりに使った単語を表示することを考えます。 Siri 型にエンコードされている単語を取り出すには、 GHC.TypeLits.List の natsVal を使えるでしょう。

showSiri :: KnownNats xs => Siri xs a b -> String
showSiri (_ :: Siri xs a b) = map (toEnum . fromEnum) $ natsVal (Proxy @xs)

この定義を使うと、以下のように はすける' を表示させることができます。

main = do
  putStrLn $ showSiri はすける'

しかし、存在型でラップした AllSiri はこの方法では単語を取り出すことはできません。 KnownNats 型制約が必要となるからです。この型制約は型レベルの値がコンパイル時に決まっていること、つまりリテラルに由来していることを追跡するための型制約ですが、 AllSiri 内の forall. xs にはそのような制約はありません。

では AllSiri 側に KnownNats 制約を与えるとどうかというと、この場合 Category の型変数 a :: Nat や b :: Nat が KnownNat とは限らないため、恒等射 id を定義するときに a :: Nat を AllSiri 内にエンコードすることができなくなります。

そもそも型ではなく値に String 型の文字列として単語を持つほうが素直だし表示のときに何も考えなくてはいいのではとも思いましたが、この場合も id を定義するときに型 a :: Nat を値に変換する必要があるので、結局 KnownNat 型制約が必要になってきます。

ということで、私はここで頑張ることを辞めてしまったので、 showSiriAll を正しく実装することは読者へのクリスマスプレゼントとしようと思います。うまく実装できた方は、教えてください( Haskell (その3) Advent Calendar 2017 がまだ空いてますので、そちらでどうぞ )。

それではみなさん、よいクリスマスを！

【12/7 追記】 @notogawa さんが singleton を使って ~~「> そもそも型ではなく値に ... 持つほうが素直」の方針で~~ 実装して下さいました。動的な扱いについても解説付き。勉強になります。

このエントリをポストした時点では、シンタックスハイライトが対応してなくて表示が崩れてますが、ご愛嬌ということで。 ↩