ロジックパズルの解説

この記事は Haskell Advent Calendar 2014 6日目の記事です．

関数プログラミング実践入門 第6章 最終節にあるロジックパズルは，一体なにをどうやるとこのインターフェース設計になるのかという話．元々内容的に入門っぽくならないものないんだけど，特徴的なサンプルでもあったし詳解せずに「こういうこともできないようにすることができるよ」と紹介するに留めといた部分になる．

Bottom

まずはBottom型

data Bottom

通常data定義にはコンストラクタとかが伴う．たとえば，

data Bool = False | True

このBool型なら，FalseとTrueとによって真値と偽値相当の値を持つ．Bool型になる値は2つだ．

しかし，Bottom型には何もない．つまり，Bottom型は「ひとつも値を持たない型」だ．Bottom型を持つ値は「存在しない」．

もっと具体的にどういうことかというと，

boolValue :: Bool
boolValue = ?

の?にはBool値になる式を実装すれば型が合う．FalseやTrueでも実装したことになる．同様に，

bottomValue :: Bottom
bottomValue = ?

の?にはBottom値を記述すれば型が合う．しかし，Bottom値は「存在しない」ので，?に型の合う意味ある式を実装することはできない．

ここで「意味ある」式とわざわざ修飾したのは，実装してもあまり嬉しくないものなら実装できるものがあるからだ．

たとえば，止まらない再帰だったり

bottomValue :: Bottom
bottomValue = let loop = loop in loop

エラーだったり

bottomValue :: Bottom
bottomValue = error "dummy"

未定義だったり

bottomValue :: Bottom
bottomValue = undefined

これらは「任意の型になれる」ので，実装して型も合うが別に嬉しくもなんともない．なんだかよくわからないbottomValueはともかくとして，boolValueとしてこれらが実装されてて嬉しいかどうかイメージしてもらえばいい．

要点は，値を持たない型を持つ式はマトモには実装できないということだ．

(:==:)

次は(:==:)について，

data (:==:) :: k -> k -> * where
   Refl :: a :==: a

(:==:)は型の上での演算子であり，GHC拡張TypeOperatorsが必要になる．

また，この(:==:)のdata定義の仕方もまたHaskell標準のdata定義ではなく，GADT(Generalised Algebraic DataType)というGHCの拡張を使ったdata定義になっている．

GADTを使うと

data List a = Nil | Cons a (List a)

のようなリストの定義は，

data List a where
   Nil  :: List a
   Cons :: a -> List a -> List a

という定義になる．

このNilやConsは最終的にList a型の値を作っているが，GADTは，全てのコンストラクタが必ずしも同じ型の値を作らなくてもよい．次のようにコンストラクタによって型変数部分を選ばせることができる．

data Value a where
   IntValue  :: Int  -> Value Int
   BoolValue :: Bool -> Value Bool

この定義では，IntValueによってValue Int型の値を，BoolValueによってValue Bool型の値を，それぞれ作ることができる．逆に言うならば，Value Char型を作る方法は与えられていないので，Value Char型の値は「存在しない」．

話を(:==:)に戻す．

data (:==:) :: k -> k -> * where
   Refl :: a :==: a

(:==:)もGADTによって定義されている．コンストラクタReflがひとつだけ存在しており，(a :==: a)型つまり，(:==:)の左右の型が同じ場合の値になっている．逆に言うならば，(:==:)の左右の型が違う場合，その値は「存在しない」．つまり，(Int :==: Double)型や(Int :==: Int)型という型自体は作れる．しかし，値Reflを持つのは後者のみとなる．

ここで，kや*は種(kind)と呼ばれる「型の型」である．IntやDoubleといった通常の値を持つ型はみんな種*の型だ．kは種変数である．つまり，(:==:)は，両辺に同一の種変数kで表される種を持つ型をそれぞれ取り，種*の型になる．

Not

ある型pからBottom型への関数の型がNot pだと読める．

type Not p = p -> Bottom

しかし，先程Bottom型の値は「存在しない」という話をしたばかりなので，このような関数は定義できそうにない(=Not p型の値も存在しない？)ように思われる．が，実はひとつだけ定義できる条件が存在する，それはp型の値も同様に「存在しない」ときだ．

次のような関数notFuncを考えてみよう．

notFunc :: Not Bottom -- Bottom -> Bottom
notFunc bottomParam = ?

このときbottomParamはBottom型の値なので，引数になっているもののこの引数として入ってくる値は「存在しない」．では，実際には「存在しない」値に対してパターンマッチを行うと実際どうなるだろう．

パターンマッチとは「場合分け」だった．ある場合(=値があるコンストラクタで作られている状況)についてはこれこれこういう定義を与える，また別の場合(=値が別のコンストラクタで作られている状況)についてはこれこれこういう定義を与える．といったように関数を定義する．

「存在しない」値に対してパターンマッチするということは，「これこれこういう定義を与える」べき場合がそもそも「存在しない」ということだ．つまり，それ以上の定義を行わなくて良い．

GHC拡張EmptyCaseを使うと，値が「存在しない」型を認識し，次のようにパターンマッチを行うことができる．

notFunc :: Bottom -> Bottom
notFunc bottomParam = case bottomParam of {}

bottomParamをパターンマッチし「これこれこういう定義を与える」べき必要が無い状況であることを理解してくれる．

実は，「これこれこういう定義を与える」べき必要が無いので，引数に値の「存在しない」型の値があるのであれば，結果の型は何でもいい．

whatever :: Bottom -> a
whatever bottomParam = case bottomParam of {}

なので，Bottomでもいいのだ．

(:/=:)

(:/=:)はNotによって作られる．

type a :/=: b = Not (a :==: b)

aとbの型が異なるとき，(a :==: b)型はBottom型同様に値が「存在しない」ものだった．つまり，aとbの型が異なるとき，(a :==: b)型とは逆にNot (a :/=: b)型の値は存在し，aとbの型が同じとき，(a :==: b)型とは逆にNot (a :/=: b)型の値は存在しない．

PeopleとFood

Peopleは登場人物3人を，Foodはメニュー3品を定義している．どちらも同様なのでPeopleだけピックアップする．

data People = Tonkichi | Chinpei | Kanta

class IsPeople (people :: People)
instance IsPeople Tonkichi
instance IsPeople Chinpei
instance IsPeople Kanta

People型はTonkichi,Chinpei,Kantaを値に持つ型である．しかし，次のIsPeopleクラス定義を見るとTonkichi,Chinpei,Kantaは値ではなくまるで型のように扱われている．これはいったいどうしたことだろう．

実はGHC拡張DataKindsにより，実際にTonkichi,Chinpei,Kantaという型も定義されている．

DataKinds拡張を使うと，data定義時に同名のkindもまた定義したことになる．つまり，今回は，{Tonkichi,Chinpei,Kanta}という値を持つ型Peopleと，{Tonkichi,Chinpei,Kanta}という型を持つ種Peopleを同時に定義している．

TonkichiやChinpeiやKantaはその名前からは値かもしれないし型かもしれない．明示的に値のほうのTonkichiではなく型のほうのTonkichiを示す場合，'Tonkichiと頭に'を付ける．

ちなみに，Tonkichi型やChinpei型，Kanta型を持つ値は無い．値を持つ型は種*を持つ型のみだ．

まとめると，GHC拡張DataKindsによりPeopleのデータ定義から以下のようなものが定義される．

値	型	種
Tonkichi,Chinpei,Kanta	People	*
	Tonkichi	People
	Chinpei	People
	Kanta	People

IsPeople/IsFood

イロイロ推敲してたときの名残リで実際不要．まぁ，あっても何の効果も無い状態なので間違いというわけでもないのだが．

Neq

Neqは(a :/=: b)型の値neqを持つクラスだ．

class (a :: k) `Neq` (b :: k) where
    neq :: a :/=: b
    neq x = case x of {}

a,bは型でkは種．neqにはデフォルト定義がある．Neqは型変数を2つ持つクラスだが，Haskell標準ではこれは許されておらず，GHC拡張MultiParamTypeClassesが必要になる．

たとえば，(Tonkichi `Neq` Tonkichi)はこのクラスのインスタンスにすることはできない．

neq :: Tonkichi :/=: Tonkichi
neq = ?

が実装できないためだ．

各PeopleとFoodについて，以下のように作れるものはNeqのインスタンスにしているが，

instance Tonkichi `Neq` Chinpei
instance Tonkichi `Neq` Kanta
instance Chinpei `Neq` Kanta
instance Chinpei `Neq` Tonkichi
instance Kanta `Neq` Tonkichi
instance Kanta `Neq` Chinpei

インターフェースを簡略化するために定義しているだけで，本当はNeq共々不要とすることもできる．理由は後述．

Eat/NotEat

data Eat :: People -> Food -> * where
    EatRemainFood   :: ( f1 `Neq` f2
                       , f2 `Neq` f3
                       , f3 `Neq` f1
                       ) =>
                       p `NotEat` f1
                    -> p `NotEat` f2
                    -> p `Eat` f3
(snip.)

Eatは「誰かが何かを食べた」ことを意味するdata定義で，これもGADTを使っている．各コンストラクタが，人間がこのパズルを解く際の推論規則に対応する．

EatRemainFoodの型クラス制約では，「f1/f2/f3が全て違う食べものであること」を要請している，そのため同じだったら型が合わない．

実際には型クラス制約を使わず，以下のような形を取ってもいい．

data Eat :: People -> Food -> * where
    EatRemainFood   :: f1 :/=: f2
                    -> f2 :/=: f3
                    -> f3 :/=: f1
                    -> p `NotEat` f1
                    -> p `NotEat` f2
                    -> p `Eat` f3

この場合，Neq型クラスは不要になるが，実際にこのインターフェースを使う箇所で，

-- kantaEatRamen = EatRemainFood kantaHateCurry kantaHateSoba
kantaEatRamen = EatRemainFood (\x -> case x of {}) (\x -> case x of {}) (\x -> case x of {}) kantaHateCurry kantaHateSoba

と，自明なEmptyCaseを書き並べる必要が生じる．

型クラス制約は，型情報と定義されている型クラスのインスタンスから，適切な処理(型情報から自明な何か)を選んでくれる．型クラスを利用したインターフェースにしたほうがよいか，あるいはそのままにしたほうがよいかは実際は状況次第となる．

今回のケースではinstance定義時に組み合わせ爆発が起こる．3人で3種類の食べものだったので，組み合わせは3!=6通りずつだったが，もっと増えるとinstance定義の数がひどいことになる．なので，型クラスにしないのが普通だと思うが，自明なEmptyCase実装を並べなきゃならないのがサンプルコード的に見栄えがよろしくないのではと判断し，あえて型クラスNeqを用意した．

correctAnswer/wrongAnswer

correctAnswerの型を持つ関数は定義できる．wrongAnswerの型を持つ関数は，どこかで型が合わず型検査でエラーになる．もしくは，これまで説明したような値が「存在しない」部分が出てきてしまい，実装できなくなる．

まとめ

このネタ自体は明らかに定理証明寄りのネタなので，マトモに説明するともっとムキムキになってしまう．今回はできるだけそっちっぽさを出さずに説明してみた．なので，こういうのもっと詳しくやりたい人は定理証明やるのがいいんじゃないかな．Try Agda もヨロシク．