定理証明支援系ができるまで(1)単純型付きλ計算

単純型付きλ計算

λ計算では自然数やデータ型をも表現できるが，プログラムが常に意味のある結果になるとは限らない(行き詰まり状態．例えば true + 1 とは？)．式を実際に評価することなしに，プログラムの振る舞いをできる限り保証したいというのは自然な動機である．
項の種類を表すものとして型を導入し，評価前に型検査を行う．

定理証明支援系ができるまで(0)型無しλ計算

定理証明支援系に興味を持ったが，特に証明したい定理があるとか数学に生かしたいといった目的はないので，仕組みを知るためにゼロから作ってみる．定理証明支援系といっても様々だが，ここでは主にCoqを念頭において話を進める．

目次

(0)型無しラムダ計算 <<
(1)単純型付きラムダ計算

型無しλ計算

お馴染みのλ計算である．型はまだ無い．

以下の実装はIdrisで書かれている(ほぼHaskellと思って問題ない)．パーサ・表示部分は省略する．

HaskellのSTG言語

この記事では GHC 8.0.1 を用いています．

STG言語

STG（Spinless Tagless G-machine）とは，遅延評価で高階関数をサポートする関数型言語のための抽象機械である．
STG（Shared Term Graph*1）言語はSTG機械のための言語で，GHCでは Haskellソース → Core言語 → STG言語 → C-- → アセンブラ，LLVM というコンパイル過程で中間言語として現れる．

STG言語は，ghcで --ddump-stg オプションをつけてコンパイルすると出力される．

*1:GHCのSTGに関するまとめ - あどけない話

Haskellの型システムを書く(1)

Haskell Advent Calendar 2017 3日目の記事です．

Haskellの型推論器を実装し，型システムへの理解を深める．

GHC拡張には型に関するものも多いが，今回は触れず標準のHaskellに従う．

Hindley-Milner 型推論

シンプルなλ式に対する多相型推論器を考える．

Functional Reactive Programming でテトリスを書いてみる(2) [Haskell]

前回は基本的なデータ型を定義し，テトリスのフィールドを表示させた．

入力

キー入力によって動作が変わるようにしたい．
一旦テトリスを離れる．

newtype Input = Get Char

inputEvent :: IO (Event Input)

echo :: Event Input -> Event Output
echo i = (\(Get c) -> Put c) <$> i

main = do
    hSetEcho stdin False
    input <- inputEvent
    run $ echo input

インターフェースとしては，inputEventから得た入力イベントを出力イベントに変換する形にする．

Functional Reactive Programming でテトリスを書いてみる(1) [Haskell]

FRP（Functional Reactive Programming）というスタイルがある．入力から出力を得る（あらゆる）プログラムを関数風に表現する手法らしい．遅延ストリームは純粋関数型言語にぴったりだと感じるが，あまり流行っていないような気がする．

HaskellではFRPのライブラリが複数あるそうだが，よく分からないのでボトムアップに自作してみよう．ゲームといえば入出力と内部状態の塊，楽しそうなのでCUIで動くテトリスを題材とする．

基本

FRPにはEventとBehaviorという概念がある．
Eventは，時間と値の組のリストで，離散的なイベントを表す．例えば，キーが押されたというイベント，画面が更新されたというイベントなど．
Behaviorは時間の関数で，連続的な値を表す．例えば，経過時間や現在のスコアなど．

type Time = Double
newtype Event a = Event [(Time, a)]
newtype Behavior a = Behavior (Time -> a)

ブログはじめました

ゆるくやっていこうと思います．