関数型プログラミング
主な言語
Haskell
Clojure
Erlamg
Agda
定理証明器、すなわち数学的な証明を検証するコンピュータプログラム
Clean
Scala
など
依存型
長さを型レベルで持っている
強い制約
積極評価
多い
遅延評価
必要になるまで評価されない
評価待ちの状態を多く作ると遅くなる
群論
圏論
関数型言語は命令型に比べ最適化の伸びしろが大きい？