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 拡張を用いて、以下のような定義ができるでしょう1。
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
を使って 「> そもそも型ではなく値に ... 持つほうが素直」の方針で 実装して下さいました。動的な扱いについても解説付き。勉強になります。
-
このエントリをポストした時点では、シンタックスハイライトが対応してなくて表示が崩れてますが、ご愛嬌ということで。 ↩