Chapter 04

型を考えるプログラム

Nobuo Yamashita
Nobuo Yamashita
2021.12.03に更新

Toy.toy の実装 (toy03)

toy はプログラムのソースコードをメモリにロードして、初期状態を構成し、それに eval を適用して状態遷移列を得て、そこから出力を抽出します。

toy :: SourceCode -> Interactive
toy prog = map output . eval . initState (load prog)

load はソースコードからメモリイメージを生成します。ここでは型シグネチャだけ、実装はとりあえず、undefined としておきます。

load :: SourceCode -> Memory
load = undefined

initState はプログラムをロードしたメモリと入力列で初期状態を構成します。

initState :: Memory -> [Input] -> ToyState
initState = undefined

実装はとりあえず、undefined にしておきましょう。メモリMemoryも詳細は後ほどにして、ここでは仮に () としておきます。

type Memory = ()

型を考えるプログラム

ここでは、

まず、型にプログラムの意図を載せ、次に、その意図を実現するように実装を与える

という流儀でプログラミングしていきます。この流儀は Haskell と相性がとてもよいのです。

いままでのコードを流儀にそって読みなおしてみましょう。

toy :: SourceCode -> Interactive となっていますから、toy はソースコード SourceCode から対話型プログラム Interactive を生成するという意図です。

この toy をソースコード prog に適用した式の型は toy prog :: Interactive であるといいことでもあります。toy の定義は toy prog という適用を定義するかたちであたえています。定義等式の右辺の式が、意図どおり、対話的プログラムになっているか、すなわち、Interactiveという型になるのかを確認してみましょう。

toy の定義右辺式は、

map output . eval . initState (load prog)

です。この式が正しく Interactive 型に型付けされていなければなりません。Interactive :: [Input] -> [Output] でしたから、

map output . eval . initState (load prog) :: [Input] -> [Output]

と型付けされるということです。このことから、

map output            :: b -> [Output]
eval                  :: a -> b
initState (load prog) :: [Input] -> a

であることが要請されます。前の章で eval :: ToyState -> [ToyState] としました。
したがって、上の aToyState であり、b[ToyState] ですので、

map output            :: [ToyState] -> [Output]
initState (load prog) :: [Input]    -> ToyState

となることが要請されます。2つめの型付けについて見てみると

initState :: c -> ([Input -> ToyState])

であることが要請されています。

load :: SourceCode -> Memory

としているので、

load prog :: Memory

となり、cMemory になりますので、

initState :: Memory -> ([Input] -> ToyState)

が要請であり、これが、機能から考えた initState の型シグネチャと一致していることがわかります。

map output :: [ToyState] -> [Output] のほうは確認は簡単ですね。

コード

ここまでの `Toy` モジュール全体
src/Toy.hs
module Toy where

type SourceCode  = String
type Interactive = [Input] -> [Output]
type Input  = String
type Output = String

drive :: Interactive -> (String -> String)
drive f = unlines . f . lines

toy :: SourceCode -> Interactive
toy prog = map output . eval . initState (load prog)

output :: ToyState -> Output
output = undefined

load :: SourceCode -> Memory
load = undefined

initState :: Memory -> [Input] -> ToyState
initState = undefined

type Memory   = ()
type ToyState = ()

eval :: ToyState -> [ToyState]
eval state = state : rests
    where
        rests | isFinal state = []
              | otherwise     = eval (step state)

isFinal :: ToyState -> Bool
isFinal = undefined

step :: ToyState -> ToyState
step = undefined