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:今考えた

Programming in Scalaを読んでいる時のメモ

Programming in Scala: A Comprehensive Step-by-Step Guide, Third Edition (English Edition)

を読んでいる時に気になったことをメモします.
2nd Editionなので若干内容が古いやつっぽいのと本文はかなり飛ばし読みしてるので変なことを言っているかも.

疑問が解決したらちゃんと補足していく予定.

Chapter9以前

• 関数はブロック内の最後の値が戻り値になるっぽい. 慣れないと若干気持ち悪い.
• (a:A, b:B) => { c:C }はラムダ式みたいなものかな？ 便利だしdefとかあんまり要らなさそう.
• objectはただの名前空間みたいなものだと思って気軽に使っていいのかな？
• x.f(y)をx f yとかけるから中置記法が使えるらしい. 面白いし変なsyntaxと間違う余地がなければかなり便利っぽい.
• Scalaでは0引数関数と定数の区別が曖昧になっている箇所がある(defの定義のところとか). 要確認.
• for-exprはforM関数とリスト内包表記を混ぜたみたいな感じ.

Chapter10

• abstract classは実装もかけるのか.
• classのパラメータ書くところにprivateとかつけられるの魔剤ﾝｺﾞ！？ 内部ではパラメータは全部ただのvalに置き換わってるからかなあ.
• classのoverrideとか(おそらくメソッド名等々)の解決はコンパイル時に行われるっぽい
• finalを付けるとそれを継承したclassやoverrideしたmethodを定義できなくなる. どこで使うのこれ？

Chapter11

• Javaきもこわちかよらんとこ
• nullはNull型になっていてValueTypeとはcompatibleじゃない
• Nothingがbottom

Chapter12

• traitはそれ自体の値も作れるし継承してクラスを作ることもできる
• traitはパラメータをもてないのとsuperが動的に解決されるのに注意
• classより使い勝手よさそう
• 複数のtraitを継承してmethodが衝突した場合は最後のやつだけが有効
• reusableならtrait それ以外はabstract classみたいな感じでいいらしい

Chapter15

• case classというのが作れるらしい. closure conditionをコンパイラに伝えるためのものかな？
• pattern matchingだ！これで勝つる！
• valの中身がconstantかどうかまでmatchingの時に判定するので注意
• _*でワイルドカード任意個の意味になる
• Anyで受け取ったものをtypeでmatchingもできるらしい. 最高に気持ち悪い.
• @でmatchした項全体を変数で受け取れる
• case [pat] if [cond]でpattern guardも使える つよい
• valの定義やfor-exprの変数定義でpatternを使った束縛もできる

Chapter16

• List concatは:::
• foldが/:と:\なのは流石にヤバくない？？？

Chapter19

• subtyping特有のあれこれがあって注意が必要そう
• S <: T ~> K[S] <: K[T]のようにsubtyping relationを保つときKはこの引数についてcovariantという. 関係が逆になるものをcontravariantという.
• 型パラメータがcovariant/contravariantであるべきという性質を+A/-Aで要求できる.
• T >: UでTはUのsupertype, UはTのlower boundであることを要求できる.
• 「あるクラスを含む全てのクラス」「あるクラスに含まれる全てのクラス」に対する実装を書く(そんなことが本当にあれば)ことができるようになるんだと思う

Chapter20

• traitの中にはtype/def/val/varをメンバーとして含めることができる
• member_=でmemberのsetterを定義する. Agdaのmixfix operatorみたいな感じ(完全にmixfixできるの？ 多分そんなことはないよね？).
• lazyを付けると変数の初期化と生成を遅延できる

Chapter21

• implicit危険なので気をつけよう
• implicit coercionとimplicit parameterがある
• <:をimplicit coercion込みで解決してくれるやつは<%とかく
• この辺使いまくるとコンパイルに時間かかりそう

Chapter28

• 異なる型の比較とかをうまくやろうとするとそりゃあ大変だよねって話. そもそもそういうことが起こること自体なんか変なのでは？と思うけど
• subtypingの事情があるのは分かるけど、そんなに何でもかんでも同一視することが大事なのかはよく分からない

Chapter30

• actor便利かよ〜〜〜
• ここだけ別の資料なりなんなりでちゃんと勉強したほうがよさそう

λ→の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にこのアルゴリズムについての説明があるらしいので気になる人はどうぞ.