Stateモナドの例の式のトレース

SEさんは、トレース得意なので
書く必要が無いかもしれませんが
老婆心から。

計算してみると、結構タイヘン。
計算が得意でない人で、初心者ならば
consを3回もしない例で、やった方が良いかも。
こういう計算の支援系はないのかな、自動計算はできなくても
計算ステップの前後でチェックができたり、適用可能な変形の候補を
プログラムの補完機能みたいに、ポップアップで表示するなりできる
ツールは世の中に存在しないのだろうか?
coqは、興味深いけど、ツールの特性に合わせるのがタイヘンだから
この場合の候補には、ならないと思われる。

お題
下記式の簡約のトレース
>run (cons0 "a" Nil >>= cons0 "b" >>= cons0 "c") 0
>→ (Cons "c" (Cons "b" (Cons "a" Nil)),3)

以下トレース実施
(なお、計算順序は、適用の仕方が可笑しくなければ
たぶん、チャーチロッサー性で担保できると思っている)
run (cons0 "a" Nil >>= cons0 "b" >>= cons0 "c") 0
{
　　cons0の定義より
　　∵cons0 :: a -> List a -> Monadic (List a)
　　cons0 x xs = Monadic $ \cnt -> (Cons x xs, cnt + 1)
}
→run ( (Monadic $ \cnt1 -> (Cons "a" Nil, cnt1 + 1))
　　>>= Monadic (\xs -> \cnt2 -> (Cons "b" xs, cnt2 + 1))
　　　>>= Monadic (\xs -> \cnt3 -> (Cons "c" xs, cnt3 + 1))) 0
→run (Monadic f >>= Monadic g >>= Monadic h) 0
　f:(\cnt0 -> (Cons "a" Nil, cnt0 + 1))
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
{
　モナドのbind(>>=)の定義より「Monadic f >>= Monadic g」を展開すると
　Monadic f >>= g
　　= Monadic (\cnt0 ->
　　　　let (result1, cnt1) = f cnt0
　　　　　in run (g result1) cnt1)
}
→run (Monadic (\cnt0 -> let (result1, cnt1) = f cnt0
　　　　　　　in run (Monadic g result1) cnt1)
　　　　　　　　>>= Monadic h) 0
　f:(\cnt0 -> (Cons "a" Nil, cnt0 + 1))
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→run (Monadic k >>= Monadic h) 0
　k:(\cnt0 ->
　　　let (result1, cnt1) = f cnt0
　　　　in run (Monadic g result1) cnt1)
{
　モナドの定義を変形した下記を使用して展開すると
　Monadic k >>= (Monadic h)
　　= Monadic (\cnt3 ->
　　　　　　　　let (result4, cnt4) = k cnt3
　　　　　　　　　in run ( (Monadic h) result4) cnt4)
}
→run (Monadic (\cnt3 ->
　　　　　　　　let (result4, cnt4) = k cnt3
　　　　　　　　　in run (h result4) cnt4)) 0
　k:(\cnt0 ->
　　　let (result1, cnt1) = f cnt0
　　　　in run (Monadic g result1) cnt1)
→run (Monadic (\cnt3 ->
　　let (result4, cnt4) = ((\cnt0 ->
　　　　let (result1, cnt1) = f cnt0
　　　　　in run (Monadic g result1) cnt1) cnt3)
　　　in run ( (Monadic h) result4) cnt4)) 0
{
　runの定義より
　run (Monadic func) initCnt = func initCnt
}
→(\cnt3 ->
　　let (result4, cnt4) = ( (\cnt0 ->
　　　　let (result1, cnt1) = f cnt0
　　　　　in run (Monadic g result1) cnt1) cnt3)
　　　in run ( (Monadic h) result4) cnt4)) 0
→(\0 ->
　　let (result4, cnt4) = ( (\cnt0 ->
　　　　let (result1, cnt1) = f cnt0
　　　　　in run (Monadic g result1) cnt1) cnt3)
　　　in run ( (Monadic h) result4) cnt4))
→let (result4, cnt4) = ( (\cnt0 ->
　　　let (result1, cnt1) = f cnt0
　　　　in run (Monadic g result1) cnt1) 0)
　　in run ( (Monadic h) result4) cnt4)
{
　runの定義より
　run (Monadic func) initCnt = func initCnt
}
→let (result4, cnt4) = ( (\cnt0 ->
　　　let (result1, cnt1) = f cnt0
　　　　in (g result1) cnt1) 0)
　　in run ( (Monadic h) result4) cnt4)
　f:(\cnt0 -> (Cons "a" Nil, cnt0 + 1))
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ( (\cnt0 ->
　　　let (result1, cnt1) = (\cnt0 -> (Cons "a" Nil, cnt0 + 1)) cnt0
　　　　in (g result1) cnt1) 0)
　　in run ( (Monadic h) result4) cnt4)
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ( (\cnt0 ->
　　　let (result1, cnt1) = (Cons "a" Nil, cnt0 + 1)
　　　　in (g result1) cnt1) 0)
　　in run ( (Monadic h) result4) cnt4)
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ( (\cnt0 ->
　　　let (result1, cnt1) = (Cons "a" Nil, cnt0 + 1)
　　　　in (g (Cons "a" Nil)) cnt0 + 1) 0)
　　in run ( (Monadic h) result4) cnt4)
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ((\cnt0 -> g (Cons "a" Nil) cnt0 + 1) 0)
　　in run ( (Monadic h) result4) cnt4)
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ( (\0 -> g (Cons "a" Nil) cnt0 + 1) 0)
　　in run ( (Monadic h) result4) cnt4)
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = (g (Cons "a" Nil) 0 + 1)
　　in run ( (Monadic h) result4) cnt4)
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = (g (Cons "a" Nil) 1)
　　in run ( (Monadic h) result4) cnt4)
　g:(\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1))
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ((\cnt2 -> \xs -> (Cons "b" xs, cnt2 + 1)) (Cons "a" Nil) 1)
　　in run ( (Monadic h) result4) cnt4)
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ( (\(Cons "a" Nil) -> \1 -> (Cons "b" xs, cnt2 + 1)) (Cons "a" Nil) 1)
　　in run ( (Monadic h) result4) cnt4)
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = ( (\(Cons "a" Nil) -> \1 -> (Cons "b" (Cons "a" Nil), 1 + 1)) (Cons "a" Nil) 1)
　　in run ( (Monadic h) result4) cnt4)
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 1 + 1)
　　in run ( (Monadic h) result4) cnt4)
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 2)
　　in run ( (Monadic h) result4) cnt4)
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 2)
　　in run ( (Monadic h) (Cons "b" (Cons "a" Nil))) 2)
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
{
　runの定義より
　run (Monadic func) initCnt = func initCnt
}
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 2)
　　in h (Cons "b" (Cons "a" Nil))) 2)
　h:(\cnt3 -> \ys -> (Cons "c" ys, cnt3 + 1))
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 2)
　　in (\cnt3 -> \ys ->
　　　　　　(Cons "c" ys, cnt3 + 1))) (Cons "b" (Cons "a" Nil))) 2)
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 2)
　　in (\2 -> \(Cons "b" (Cons "a" Nil))) ->
　　　　　　(Cons "c" ys, cnt3 + 1))) (Cons "b" (Cons "a" Nil))) 2)
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 2)
　　in (\2 -> \(Cons "b" (Cons "a" Nil))) ->
　　　　　　(Cons "c" (Cons "b" (Cons "a" Nil))), 2 + 1))) (Cons "b" (Cons "a" Nil))) 2)
→let (result4, cnt4) = (Cons "b" (Cons "a" Nil), 2)
　　in (Cons "c" (Cons "b" (Cons "a" Nil))), 3)))
→(Cons "c" (Cons "b" (Cons "a" Nil))), 3)))

大筋こんな感じ ?

間違いを見つけて後で書き直すかもしれない。
→修正した。たぶんあっている。
以上です。