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

[haskell入門](https://www.amazon.co.jp/dp/4774192376) の著者の一人、hirataraです。といっても、このエントリは書籍とはまったく関連のないお遊びです :smirk: 

ということで、今回は10年ほど前のエントリである [しりとりの圏](http://d.hatena.ne.jp/m-hiyama/20060821/1156120185) を、Haskellで実装しようと試みましたので、その過程をだらだらと書いていきます。

## 前置き

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

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

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

しかし、「圏論と言えばHaskellだろう」と安易に考えてこの圏をHaskellのプログラムで表現しようとすると、すぐに暗礁へ乗り上げてしまいます。というのも、Haskellで用意されている圏を表す型クラス [Category](https://www.stackage.org/haddock/lts-9.12/base-4.9.1.0/Control-Category.html#t:Category) の **対象** は **型** だからです。しりとりの圏の **対象** は、 **値** である `'あ'` や `'い'` などの文字ですので、ここに大きなギャップがあります。[標準規格](https://www.haskell.org/onlinereport/haskell2010/) のHaskellではしりとりの圏をそのまま `Category` 型クラスのインスタンスにすることはできません。

しかし、GHCには [Datatype promotion](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#datatype-promotion) という拡張が用意されています。この拡張は、 **値** を昇進させて **型** として使うことができるようにするというものです。まさに今回の目的にぴったりですね！ この拡張を使えば、しりとりの圏を `Category` 型クラスのインスタンスをにできるかもしれないという希望が出てきました。

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

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

そこで今回は、GHCに用意されている [Nat](https://hackage.haskell.org/package/base-4.10.0.0/docs/GHC-TypeLits.html#t:Nat) カインドに属する [型レベル自然数](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#type-level-literals) を使うことにします。文字のUnicodeポイントを `Nat` カインドを持つ型レベル自然数として表現するわけです。

また、それにあわせて文字列は単語を文字列の値として持つのではなく、型レベルリストを使って `[Nat]` カインドを持つ型にエンコードします。そうすると、 [GADTs](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#generalised-algebraic-data-types-gadts) 拡張を用いて、以下のような定義ができるでしょう[^highlight]。

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

```haskell
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` を形式的に引き回しているだけになってます。言い換えると、コンパイル時にのみ意味のある計算が行われるということですね。

```haskell
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` をラップします。

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

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

```haskell
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` を持つ型レベル自然数から型レベル自然数への射を持つインスタンスをきちんと定義できました。

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

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

```haskell
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` 以外にも様々な拡張が必要になりますね。

```haskell
{-# 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](https://hackage.haskell.org/package/singletons) と [typelits-witnesses](https://hackage.haskell.org/package/typelits-witnesses) パッケージを使うので、 `stack` を使っている方は予め `stack build singletons` `stack build typelits-witnesses` としておくといいでしょう。

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

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

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

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

```haskell
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](https://qiita.com/advent-calendar/2017/haskell3) がまだ空いてますので、そちらでどうぞ :santa:  )。

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

----

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

https://gist.github.com/notogawa/a7d14ee02ca80a5729fdcb9b6788fb0c