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

• 8
Like
• 0
Comment
Edited at
3
More than 1 year has passed since last update.

（なんか、２つのカレンダーにダブル投稿をしてたので真似してみた）

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

まぁ、落ち着け。

## テスト切り出してみた

うーん。これ動くのかなぁ、、、。

```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 ()
```

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

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

```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
```

ここで: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> :break 559
```

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

```*TypingHaskellInHaskell> test1 ()
_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
```

でも諦めずにコツコツと進むのです。徐々に絞り込んで行けば必ず原因は分かります。

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

## 次にやろうとしてる事

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

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