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

Coq 定理証明支援系型システム Idris Haskell

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

2018-06-19

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

Coq 定理証明支援系型システム Idris Haskell

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

2017-12-30

HaskellのSTG言語

Haskell STG GHC

この記事では GHC 8.0.1 を用いています． STG言語 STG（Spinless Tagless G-machine）とは，遅延評価で高階関数をサポートする関数型言語のための抽象機械である． STG（Shared Term Graph*1）言語はSTG機械のための言語で，GHCでは Haskellソース → Core言…

2017-12-26

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

Haskell Advent Calendar 2017 3日目の記事です． Haskellの型推論器を実装し，型システムへの理解を深める．GHC拡張には型に関するものも多いが，今回は触れず標準のHaskellに従う． Hindley-Milner 型推論シンプルなλ式に対する多相型推論器を考える．

2017-11-09

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

Haskell FRP

前回は基本的なデータ型を定義し，テトリスのフィールドを表示させた．入力キー入力によって動作が変わるようにしたい．一旦テトリスを離れる． newtype Input = Get Char inputEvent :: IO (Event Input) echo :: Event Input -> Event Output echo i = …