Haskell
λ計算では自然数やデータ型をも表現できるが,プログラムが常に意味のある結果になるとは限らない(行き詰まり状態.例えば true + 1 とは?).式を実際に評価することなしに,プログラムの振る舞いをできる限り保証したいというのは自然な動機である. 項の…
定理証明支援系に興味を持ったが,特に証明したい定理があるとか数学に生かしたいといった目的はないので,仕組みを知るためにゼロから作ってみる.定理証明支援系といっても様々だが,ここでは主にCoqを念頭において話を進める.
この記事では GHC 8.0.1 を用いています. STG言語 STG(Spinless Tagless G-machine)とは,遅延評価で高階関数をサポートする関数型言語のための抽象機械である. STG(Shared Term Graph*1)言語はSTG機械のための言語で,GHCでは Haskellソース → Core言…
前回は基本的なデータ型を定義し,テトリスのフィールドを表示させた. 入力 キー入力によって動作が変わるようにしたい. 一旦テトリスを離れる. newtype Input = Get Char inputEvent :: IO (Event Input) echo :: Event Input -> Event Output echo i = …
FRP(Functional Reactive Programming)というスタイルがある.入力から出力を得る(あらゆる)プログラムを関数風に表現する手法らしい.遅延ストリームは純粋関数型言語にぴったりだと感じるが,あまり流行っていないような気がする.HaskellではFRPのラ…