読もうと思って購入したので，メモを残しておきたい．メモなので，内容について保証はないし，私的な備忘録を公開しているというスタンスです．
- 関数プログラミングは，型で制約条件を表現することで，ドキュメントとそれを作成するために必要なコストを減らすことができる．なぜなら，制約条件を守らなかったらコンパイルエラーとすることができるから，わざわざ注意喚起のために記述する分量が減るからである．
- 命令型言語における関数が特定の命令/手続きにつけられた識別符号であるのに対し，関数型言語のそれは数学的な意味での関数，つまり入力に対して出力が一意に決まる対応関係のことである．
- 状態に触れ，干渉することを副作用と呼ぶ．入出力は外界の状態に干渉するため，副作用である．
- プログラムを，そしてその対象となる問題をどう定義するかという定義を，プログラミングパラダイムと呼ぶ．
- 一般に，関数を第一級の対象とする言語を関数型言語とする．
- 第一級の対象であるということは，プログラムにおいて関数を値と同じように扱えるということである．
- 一般に，手続き型言語は，コンピュータの物理的特性を陽に記述することを強いられる．
- メモリモデル(ここから変数は箱というメタファーが派生する)
- (破壊的)代入は「書き換えられる」というメモリモデルに依拠する操作であるが，なんとなく鵜呑みに受け入れられている．
- 数学における代入とプログラミングにおける(破壊的)代入は異なるものだといえる．
- 型システムは，プログラムに型と呼ばれるものを付け，それによって振舞いを保証しようとする仕組みである．
- 型検査を通過すれば振舞いの安全性が保証されるような型付けを強い型付け，保証されないそれを弱い型付けと呼ぶ．
- 依存型のことはよくわからん
- 証明とかで使えるらしい ふええ怖いよお
- 型に依存する型，値に依存する型が作れる
- 偶数に限った整数とか，0以上の整数とか？
- 適切な抽象化によりプログラムは柔軟に保たれる．関数型言語は数学が持つ強力な抽象化能力にタダ乗りできる
- IEEE754浮動小数点数は結合則を厳密に満たさないので，各ノードで処理して後から足すなどの処理ができかかったりする
- テストじゃなくてプログラム自体の性質を証明しちゃえばいいじゃん -> 形式手法のうちの定理証明
- それってプログラムをまるっと別の方法で再定義しているにすぎないのでは？
- COBOLをリバースエンジニアリングして仕様書にするツールはHaskellが利用されているらしい
- 渋い
