8
7

More than 5 years have passed since last update.

thihの解析に進捗があります

Last updated at Posted at 2015-12-16

この記事は、この記事は言語実装 Advent Calendar 2015ML Advent Calendar 2015の 17日目の記事です。
(なんか、2つのカレンダーにダブル投稿をしてたので真似してみた)

Haskellみたいな型クラス作りたい。Haskellをstrictにしたような言語が欲しいらしい。Tyiping Haskell in Haskell[1](thih)はHaskellの型推論部分を解説した論文です。thihを参考にすれば型クラスは分かるのです。でもですよ、Haskellの型クラス、、、。難しいんです。酷い英語翻訳[2]してみてたですよ、、、。クソの山を作って力付きましたよ、、、。英語辛いですよ。

そんな中、Mokkosuの作者さんはMokkosuである程度分かりやすく噛み砕いた記事を書いています。[3]

ちょっと理解が進みました。でも、、、まだ、オラわからねぇだ。そう、分かる人は分かったと言ってコンパイラを作ったり作らなかったりして去って行くのです。うう、分かるようにしてくれ、、、って思うけども簡単じゃないのです。という事で鳥人にしかいけない普通の人間に取って難攻不落なHaskellの型クラスに普通の人間がまたちょっと格闘して登ろうとしてみているわけです。

何が分からないのか

ああ、分からん。何が分からないのか、、、。何が欲しいのか。私はHaskell分からないのに、Haskellの型推論部分を理解しようという奇特な方なのであります。ウワー駄目だ駄目だっ!!!

まぁ、落ち着け。

Haskellのワンソースバージョンを移植したOCamlバージョン[4]があり、Scalaに移植[5]してみたりもしました。でも、動かしかたが良くわからんのでした。

何が分からないのかというと、、、全体的な使い方が分からんのです。thihのソース[4]を見ると、ソース分割されたソースコードやらpreludeのテストコードが大量にあります。テストデータあるのでこれを動かしてみればいいんだよなぁ。

テスト切り出してみた

大量のテストデータは邪魔なので、とりあえず1個動かしましょうってことで取り出してみました。
うーん。これ動くのかなぁ、、、。

let tOrdering = TCon (Tycon("Ordering", Star))

let ap  = fold_left1 (fun b a -> Ap(b, a))
let evar v          = (Var v)
let elit l          = (Lit l)
let econst c        = (Const c)

let toBg (g:(id * scheme option * alt list) list) : bindGroup =
  List.fold_right(fun g (a,b) ->
                        match g with
                        | (v, Some t, alts) -> ((v,t,alts)::a, b)
                        | (v, None, alts) -> (a, [(v,alts)]::b)
                      ) g  ([],[])

let (^->) = fn

let assumps : assump list
 = [ Assump("_concmp",
       Forall([Star],
         Qual([], 
          TGen 0 ^->  TGen 0 ^-> tOrdering))) ]

let _ = assert(assumps =
[Assump ("_concmp",
    Forall ([Star],
     Qual ([],
      TAp
       (TAp (TCon (Tycon ("(->)", Kfun (Star, Kfun (Star, Star)))), TGen 0),
       TAp
        (TAp (TCon (Tycon ("(->)", Kfun (Star, Kfun (Star, Star)))), TGen 0),
        TCon (Tycon ("Ordering", Star)))))))])

let classEnv:classEnv = exampleInsts initialEnv

let prelude : program
 = List.map toBg
   [[("flip",
      Some (Forall ([Star; Star; Star],
             Qual([],
              ( (TGen 0 ^-> TGen 1 ^-> TGen 2) ^-> TGen 1 ^-> TGen 0 ^-> TGen 2)))),
      [([PVar "f"; PVar "x"; PVar "y"],
        ap [Var "f"; Var "y"; Var "x"])])]]

let test1 (): assump list = tiProgram classEnv assumps prelude

let _ =
  assert (TGen 0 ^-> TGen 1 ^-> TGen 2 = TAp (
    TAp (TCon (Tycon ("(->)", Kfun (Star, Kfun (Star, Star)))), TGen 0),
    TAp (TAp (TCon (Tycon ("(->)", Kfun (Star, Kfun (Star, Star)))), TGen 1), TGen 2)))

let _ = test1 ()

バグッっとる。。。

うっ。最初の1個目でエラーが出る。困ったぞ。Haskellの動きを見たい。
しかし、デバッグの仕方が分からない。私はHaskellの使い方が分からない奇特な、、、ってのは置いておいて、、、

ghciのデバッガを使ってみる

ghciは素晴しい事に、メインのソースを指定するだけで、依存解析を行って必要なソースコードを読み込んでくれます。

TypingHaskellInHaskell.hsに以下のソースを加えます。

tOrdering = TCon (Tycon "Ordering" Star)

ap              = foldl1 Ap
evar v          = (Var v)
elit l          = (Lit l)
econst c        = (Const c)
elet e f        = foldr Let f (map toBg e)

toBg           :: [(Id, Maybe Scheme, [Alt])] -> BindGroup
toBg g          = ([(v, t, alts) | (v, Just t, alts) <- g ],
                   filter (not . null) [[(v,alts) | (v,Nothing,alts) <- g]])

assumps :: [Assump]
assumps
 = [ "_concmp" :>: 
       (Forall [Star]
         ([] :=> 
          (TGen 0 `fn` TGen 0 `fn` tOrdering))) ]

classEnv :: ClassEnv
Just classEnv = exampleInsts initialEnv

prelude :: Program
prelude
 = map toBg
   [[("flip",
      Just (Forall [Star, Star, Star]
             ([] :=>
              ((TGen 0 `fn` TGen 1 `fn` TGen 2) `fn` TGen 1 `fn` TGen 0 `fn` TGen 2))),
      [([PVar "f", PVar "x", PVar "y"],
        ap [Var "f", Var "y", Var "x"])])]]

test1 :: () -> [Assump]
test1 () = tiProgram classEnv assumps prelude

そして、ghciで読み込みます。

$ ghci TypingHaskellInHaskell.hs
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling TypingHaskellInHaskell ( TypingHaskellInHaskell.hs, interpreted )
Ok, modules loaded: TypingHaskellInHaskell.
*TypingHaskellInHaskell>

ここで:listコマンドを使って関数名を指定すると、、、

*TypingHaskellInHaskell> :list tiExpl
550  tiExpl :: ClassEnv -> [Assump] -> Expl -> TI [Pred]
551  tiExpl ce as (i, sc, alts)
552          = do (qs :=> t) <- freshInst sc
553               ps         <- tiAlts ce as alts t
554               s          <- getSubst
555               let qs'     = predsApply s qs
556                   t'      = typeApply s t
557                   fs      = assumpsTv (assumpsApply s as)
558                   gs      = typeTv t' \\ fs
559                   sc'     = quantify gs (qs':=>t')
560                   ps'     = filter (not . entail ce qs') (predsApply s ps)
561               (ds,rs)    <- split ce fs gs ps'
562               if sc /= sc' then
563                   fail "signature too general"
564                 else if not (null rs) then
565                   fail "context too weak"
566                 else
567                   return ds
568
*TypingHaskellInHaskell>

関数の中味を見る事が出来ます。

*TypingHaskellInHaskell> :break 559
Breakpoint 0 activated at TypingHaskellInHaskell.hs:559:28-49

とすると、ブレークポイントを付ける事が出来ます。:breakは:bだけでもいけるようです。実行してみましょう:

*TypingHaskellInHaskell> test1 ()
Stopped at TypingHaskellInHaskell.hs:559:28-49
_result :: Scheme = _
gs :: [Tyvar] = [Tyvar "v5" Star,Tyvar "v4" Star,Tyvar "v7" Star]
qs' :: [Pred] = _
t' :: Type = TAp
               (TAp (TCon ...) (TAp ...)) (TAp (TAp ...) (TAp ...))

ブレイクポイントで止まって変数がある程度表示されます。ここで、t'の中味を詳しく見たい場合は以下のようにします:

[TypingHaskellInHaskell.hs:559:28-49] *TypingHaskellInHaskell> t'
TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "v5" Star))) (TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "v4" Star))) (TVar (Tyvar "v7" Star))))) (TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "v4" Star))) (TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "v5" Star))) (TVar (Tyvar "v7" Star))))

さらに詳しい情報が見れました。gsとすれば、gsの中味を見れます。

[TypingHaskellInHaskell.hs:559:28-49] *TypingHaskellInHaskell> gs
[Tyvar "v5" Star,Tyvar "v4" Star,Tyvar "v7" Star]

gsの内容が、違ったのです。

原因見つけた

リストのunionの処理結果の順番が変わっていたのが原因でエラーになっていました。unionの処理を以下のように書き換える事でエラーは解消出来ました。

let union xs ys = xs @ filter (fun x -> not (mem x xs)) ys

移植の際には、原因の絞り込みが辛い所です。モチベーションが、、、進捗スピードががた落ちすることがあります。
でも諦めずにコツコツと進むのです。徐々に絞り込んで行けば必ず原因は分かります。

ふっふっふ。分からない事が分かって、問題点を洗い出し、絞り込んで1つ解決し分からない事がわかるようになりました!!!

次にやろうとしてる事

  1. 大量のテストデータをScalaに移植する予定です。OCamlにも移植します。HaskellのプリティプリンタライブラリText.PrettyPrint.HughesPJを使って一気に出力するつもりです。

  2. パーサをOCamllexとOCamlYaccで書きます。オフサイドルールのないバージョンのHaskellのパーサを作ります。thihのソース内にはhatchetという実装があるので、参考にします。HaskellのAltJSも沢山ありますがPureScriptがより単純化されているようですので参考にすると良いかもしれません。

  3. リファレンスで書き直します。Haskellは純粋な関数型言語なので、参照透明性を確保するために一工夫必要です。OCamlやScalaはmutableな変数が使えます。素直にリファレンスを使って書き直せばもっと分かりやすく、そして高速になるはずです。環境が関数お化けになってる箇所も只のデータのリストにすると簡単なるかもしれません。

Haskellを作りたいわけではないのに作らないと理解出来なさそうだ。

このあたりに葛藤があります。少なくともオフサイドルールのないHaskellを作らないと行けないようです。Haskell作りたい訳じゃないのに、一度Haskellのパーサ作ったほうが良さそうなので辛い。
大体葛藤があるとみんな悩み苦しむのです。そういう場合は、葛藤を見つけて辛さを認識し、次に出来るなら、その葛藤を解消してやればいいのです。解消出来ないなら諦めればいい。この挑戦は葛藤があって辛いので、徐々に進める必要がありそうです。ストレスに耐えぬいて一気に解決できるのが一番いいのですが、ちょっと進めばそれでもいいじゃないですか。大変なんだもん。

だから、辛いけど、型推論出来て、パーサ作れたら、後はもうこっちの世界です。もう処理系作れてしまう。きっと、頑張れば素晴しい世界が待っているのです。それを夢みて頑張るのであります。

Haskellを作りたいわけではないのに作らないと理解出来なさそうだ。だけど理解してしまえば素晴しい世界が待っている。

そう考えてこの先の作業を進めて行こうと思います。

まとめ

Haskellの型システムの理解は難しいのですが、分からない点を洗い出し、解消するコードを書いて、バグを取り除き、一歩前進しました。

まだまだ課題はありますが、リストアップする事で明確にしました。

Haskellの型推論はHaskellを理解しないと難しい現状があります。でも、一度こちらの世界に引きずり込んでしまえば色々とあんな事やこんな事を高速に出来るようになるはずです。

参考文献

8
7
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
8
7