Theorem Prover Haskellの紹介

この記事はTheorem Prover Advent Calendar 2016の1日目の記事です。

今年も残り1ヶ月になったことを信じたくないと思いつつ、
まあ学生的には4月始まりだから大丈夫と自分に言い聞かせてます。

今回のアドベントカレンダーのネタを必死に1週間くらい前から頑張って探した結果
何も見つからなかったのでHaskellで証明を書きます。

みなさんHaskellで証明を書くのはつらいと思うかもしれませんが
実はEquational Reasoningも使えるし
最近バージョンが上がって少し賢くなったコンパイラの強力なサポートも受けられるので
意外とマシです。(当社比)

さてHaskellで証明をすることについてですが、
ここでは定理証明界のFizzBuzzとも名高い*1、リストのreverse関数が2回やると元に戻ることを示します。

Leanで書いた同じ証明も置いとくので、ぜひ見比べてみてください↓
Leanバージョン

ポイントをいくつか解説します。

cong :: a == b -> f a == f b
cong Refl = Refl

-- fを具体化
congAppend :: Sing x -> a == b -> a ++ Cons x Nil == b ++ Cons x Nil
congAppend _ Refl = Refl

congは上で定義していますが、証明中ではほとんど使っていません。
どうもcongはこの形だとfの曖昧性が残るのでいちいちfを具体的にした命題を置いて使います。

これは、TypeFamiliesで定義した(Reverseとか)type functionはGHC的にはk -> kカインドの関数とは違う(type functionに対しては部分適用を認めない)ようで、fにTypeApplications拡張で直接代入しようとしても引数の数が足りないというエラーになるためです。
ここは型コンストラクタへの部分適用ができるようになればTypeApplicationsでなんとかなるはずです。

--

data instance Sing (typ :: List a) where
  SNil :: Sing Nil
  SCons :: Sing x -> Sing xs -> Sing (Cons x xs)

singleton typeです。

Listカインドの型を保持したままListの項と同型な構造を持つデータを定義します。
これは帰納法を回すときに"xsの内部の項"を引数でとるために使っています。

Haskell依存型プログラミングでは頻出のテクニックであり、
この辺はsingeltonsパッケージあたりを使うとちょっと楽になれます多分。

--

(===) :: Sing a -> Sing b -> Sing (Mk2 a b)
(===) a b = STuple a b

infixl 3 `by`
by :: Sing (Mk2 a b) -> a == b -> b == c -> a == c
by _ = trans

qed :: forall a. a == a
qed = refl

ex :: Sing a -> Sing b -> Sing c -> Sing d -> a == b -> b == c -> c == d -> a == d
ex a b c d ab bc cd =
  a === b `by`ab $
  b === c `by` bc $
  c === d `by` cd $ qed

Equational Reasoningです。
大体Agdaのと同じようなノリで定義しました。

個人的には左辺が右辺と等しい時にそれを省略できる記法を考えたかったですが
めんどくさいので実装が楽なtransをそのまま持ってくる方法を採用しました。
でも証明は同じことをなんども書くので超面倒になります。

あとは証明を読んでもらえばわかると思います。
というわけでHaskellでも比較的楽に証明が書けるよっていうアレでした。

(いや本当は全然楽ではない)
(めっちゃつらかった)
(つらいと思った人はすぐにIdrisかAgdaに助けを求めましょう)

--

*1:今考えた

λ→のtyping & unification algorithm

この記事のunification algorithmは間違っているので
λμのTypeCheckerの実装 - Just $ A sandboxを参考にしてください

λ→のtypingアルゴリズム.
variableとabstractionは型が一意に決まるので, 問題はapplication.
MN:aからM:?x -> aの?xをどうやって決定するかという問題になる.

holeの導入

型変数とは別に, hole(goal)を導入する.
holeは確定していない型で, どんな型も入ることができる. さらにtypingが下から上に, 左から右に進む関係上, typingが進むにつれて段々確定していく.

例:

|- λf. λx. f x : ??
-> f:?0, x:?1 |- f x : ??  <-- abstractionした
-> f:?0, x:?1 |- f:?0  f:?0, x:?1 |- x:?1  <-- application
-> f:?1 -> ?2, x:?1 |- f x :?2  <-- fは関数型なので{?0 = ?1 -> ?2}を代入した
-> |- λ(f: ?1 -> ?2). λ(x: ?1). f x : (?1 -> ?2) -> ?1 -> ?2  <-- abstractionした

applicationの時にholeの代入が必要になる.
この時, holeの等式を代入するという操作をするが, これはbase(|-の左側)と現在確定している型の中身にも代入する必要がある.
このように, 等式が与えられるとそれらに含まれるような最大の型を取ってくるという操作が必要になり, これをunificationという.

unificationは失敗することもある.

x:?0 |- x x : ??
-> x:?0 |- x:?0  x:?0 |- x:?0  <-- {?0 = ?0 -> ?1}はunification不可能

typing algorithm

実際のtyping algorithmは次のような感じになるはず.

-- var
G |- x : ??
-> G |- x : G(x)

-- abs
G |- λx. e : ??
-> G, x:?n |- e : Type(e)
-> G |- λx. e : ?n -> Type(e)

-- app
G |- M N : ??
-> G |- M : Type(M)  G |- N : Type(N)
-> unify {Type(M) = Type(N) -> ?n}
-> G |- M N : ?n

unification algorithmは必要な部分で左辺を右辺に置き換える処理を書くだけのはず.

data Typ = TVar String | TArr Typ Typ | Hole Int
data Untyped = Var String | App Untyped Untyped | Abs String Untyped
type Base = [(String, Typ)]

data Checking = Checking {
  _base :: Base,
  _freshHole :: Int,
  _holes :: [(Int, Typ)]
  }

makeLenses ''Checking

fresh :: (Monad m) => StateT Checking m Int
fresh = do
  n <- use freshHole
  freshHole += 1
  return n

typing :: Untyped -> Either String Typ
typing t = flip evalStateT (Checking [] 0 []) $ go t where
  go :: Untyped -> StateT Checking (Either String) Typ
  go (Var v) = do
    gs <- use base
    case lookup v gs of
      Just t -> return t
      Nothing -> lift $ Left $ "Not in scope: " ++ v ++ " in " ++ show gs
  go (Abs x e) = do
    n <- fresh
    base <>= [(x, Hole n)]
    t <- go e
    hs <- use holes
    return $ apply hs $ TArr (Hole n) t
  go (App e1 e2) = do
    t1 <- go e1
    t2 <- go e2
    n <- fresh
    unify t1 (TArr t2 (Hole n))
    hs <- use holes
    return $ apply hs (Hole n)

  apply :: [(Int, Typ)] -> Typ -> Typ
  apply bs (Hole n) = case lookup n bs of
    Just t -> apply bs t
    Nothing -> Hole n
  apply bs (TVar a) = TVar a
  apply bs (TArr t1 t2) = TArr (apply bs t1) (apply bs t2)

  replace :: Int -> Typ -> Base -> Base
  replace n typ = fmap (second go) where
    go :: Typ -> Typ
    go (TVar a) = TVar a
    go (Hole m)
      | m == n = typ
      | otherwise = Hole m
    go (TArr t1 t2) = TArr (go t1) (go t2)

  allHoles :: Typ -> [Int]
  allHoles (Hole n) = [n]
  allHoles (TArr x y) = allHoles x ++ allHoles y
  allHoles _ = []

  unify :: Typ -> Typ -> StateT Checking (Either String) ()
  unify (Hole n1) t = if n1 `elem` allHoles t
    then lift $ Left $ "Unification failed: " ++ show (Hole n1) ++ " in " ++ show t
    else base %= replace n1 t >> holes <>= [(n1,t)]
  unify t1 (Hole n) = unify (Hole n) t1
  unify (TVar a) (TVar b)
    | a == b = return ()
    | otherwise = lift $ Left $ "Type mismatch: " ++ a ++ " /= " ++ b
  unify (TArr t1 t1') (TArr t2 t2') = unify t1 t2 >> unify t1' t2'
  unify (x@(TArr _ _)) y = lift $ Left $ "Unification failed: " ++ show x ++ " and " ++ show y

動かす

なんかこんな感じになる.

λx. x : Right ?0 -> ?0
λx. λy. y x : Right ?0 -> (?0 -> ?2) -> ?2
λf. λg. λx. f (g x) x : Right (?3 -> ?2 -> ?5) -> (?2 -> ?3) -> ?2 -> ?5
λx. x x : Left "Unification failed: ?0 in ?0 -> ?1"
λx. x y : Left "Not in scope: y in [(\"x\",?0)]"
λf. λx. f (x x) : Left "Unification failed: ?1 in ?1 -> ?2"

はたして

で上のアルゴリズムで本当に合っているのかはよく分からない.
TaPLにこのアルゴリズムについての説明があるらしいので気になる人はどうぞ.

データ型のCPS変換について

HaskellでCPS変換とか調べているとデータ型のCPS変換というのが出てくる.

関数のCPS変換は継続を引数に追加して末尾再帰の形にすればだいたいOKなのでまあわかるのだけど, データ型のCPS変換というのは何なんだという話.
継続は何を継続しているのかがいまいち分からないので何故そのデータ型はCPS変換するとその型になるんだと不思議に思っていたのがちょっと解決したのでそれについて書く.

関数 is っょぃ

パフォーマンスのことを考えれば, 関数型と基本型(ground type)が型の中では圧倒的に偉い.
基本型というのはまぁproductとかrecursionとかdependent typeとかを含まない基本的な型のこと. 例えばIntとか(Haskellのような言語ではIntというのは計算機の都合上特別扱いされているので, ここでのIntはN×Nにring構造を入れたもののことではない).

基本型は基本的にコンパイラのサポートが受けられるので特別な形で処理されるから処理は速い.
関数型は作ったり壊したり(introしたりelimしたり)が速いので速い.
その他の型, つまりproductとかcoproductとかなんかそういうのが遅いのはコンストラクタに対するパターンマッチを何度も繰り返すからで, パターンマッチをさせない書き方ができれば処理が速くなる可能性がある.

そこでデータ型を関数型と基本型の組み合わせでそれと同型なものに変換できない？ という発想になる.

Cont iso

初めに, 次が成り立つ:

型Aに対し, Aと∀P. (A -> P) -> Pはiso.
(Prf) a:A ==> λ(f:A->P). f(a):P, h:(A->P)->P ==> h(id:A->A):A は同型を与える.

この対応は(名前があるのか知らないけど)至るところに現れる.
例えばP=bottomの時は右辺の型は¬¬Aのことだし, ContモナドはCont r a = (a -> r) -> rだったし, そもそもA -> (A -> P) -> Pは単なる関数適用のflip版のことだった. さらに言えば, この同型はyoneda lemmaのId functorに適用した形になっているとも言える.
Contモナドの名前的に明らかにこのことは継続とかそういうのと関係しているのだけどこれだけでは何のことかはわからない. わからないのでもう少し話を進めてみることにする.

直和型

A+Bの直和型を特徴づけるものといえば当然elim ruleになる.(何故かは下で分かる) というのも, 直和型のelim ruleはちょうどcoproduct図式のUMPをもつ射に対応する.

A+Bのelim rule: ∀P. (A -> P) -> (B -> P) -> (A+B -> P)

これは次と同値: A+B -> ∀P. (A -> P) -> (B -> P) -> P

偶然(要出典), 最初にやった同型と同じ * -> (∀P. (..) -> P) の形が出てきた.
で, coproductはup to isoに決まるので∀P. (A -> P) -> (B -> P) -> PはそもそもA+Bと同型になる. これによって次のことがわかる.

A+B = (∀P. (A -> P) -> (B -> P) -> P) と定義してよい. 右辺はパターンマッチが起こらないので速い.

elim ruleとは何か

で, このelim ruleとは何なのかという話だけど, これは次のようにして導出される:

A+B = ∀P. (A+B -> P) -> P    : 最初の同型
= ∀P. hom(A+B, P) -> P
= ∀P. hom(A,P) × hom(B,P) -> P    : homはcoproductをproductに変える
= ∀P. (A -> P) × (B -> P) -> P
= ∀P. (A -> P) -> (B -> P) -> P    : 直積と冪の随伴(curry化)

一般に, inductive datatypeというのはelim ruleが本質的に効いてくる.
(これはinductionがelim ruleになってるということを表している)
その場合は上のような変換で簡単な形に変形できる.

直積型

直積は上の双対なのでintro ruleが対応するけれど, こちらは上のようなほしい形と一致しない.
けれど, なんと直積はCCCでは(後で補足する)左随伴なのでいい感じに変形ができる.

A×B = ∀P. (A×B -> P) -> P
= ∀P. (A -> B -> P) -> P    : 直積と冪の随伴(curry化)

例: List

あとは上のことを使って機械的に変形するだけで単純な形のデータ型なら大体いい感じの型が作れる.

例) List

[a] = 1 + a × [a]
= ∀P. ((1 + a × [a]) -> P) -> P
= ∀P. ((1 -> P) -> (a × [a] -> P) -> P) -> P    : coproductのPR変換
= ∀P. ((1 -> P) -> (a -> [a] -> P) -> P) -> P    : productのPR変換
= ∀P. (P -> (a -> [a] -> P) -> P) -> P    : CCCならhom(1,P)=P

この定義でhead, tailなどは簡単に実装できる.

まとめ

以上により, データ型はパターンマッチを含まないより速い形に書き換えられることがわかった.
このようにして書き換えたものの中で, 継続渡しっぽさを含むものをCPS変換されたデータ型と呼ぶっぽい.
(ちなみに, (... -> P) -> Pが割と継続渡しっぽさがある)

ちなみにこのようなぽさを含むもの全体が上で変換された全体と一致するかどうかは私は知らない.

軽いまとめ:

• 直積とか直和はいい感じに変形できて便利.
• 関数型がめっちゃ偉い.
• 上の記述はだいたいHaskellとかで考えていたけれど, CCCな型システムを持つ言語なら同じことが出来ると思う

Haskellの型システムってCCCじゃないですよね？？？？*1

ﾔ,ﾔﾒﾛｫ〜〜〜(今回はundefinedとかいう邪悪なものは考えてない)

はじめに

初めに書きたかったことを書く.
CPS変換でググると, CPS変換とは継続をうんたらかんたらとかいう文章がヒットしまくるけど何の説明にもなっていないということがすでに人生で5億回くらいあった.

一応自分の中では「関数の」CPS変換と「データ型の」CPS変換という2種類の言葉があり, 前者はContモナドを使った書き方で後者は今回説明したようなことに対応しているのだろうという理解でいる.
本来のCPS変換は前者で, 前者は主に末尾再帰とかそういう話だと思うんだけど, HaskellとCPS変換の話をググると(他の言語でもそうかも？)後者のCPS変換も結構ちょくちょく出てくる.

とりあえずCPS変換の言語に依らないちゃんとした定義を発見するか自分で作ることができれば, この腑に落ちない感じも少しは改善するのかも.

あと, 上のことはCPS変換と何の関係もないかもしれない.
(CPS変換の定義が分からないので関係があるかどうかもわからない)
でも上の操作でパターンマッチは確実に減るので, まあ誰かの役に立てばいいなと思いました.

参考文献

• http://www.brics.dk/RS/01/49/BRICS-RS-01-49.pdf 読んでないけどたぶんCPS変換の真面目な定義が書いてありそう？

*1:https://wiki.haskell.org/Hask#Hask_is_not_Cartesian_closed