Mercurial > hg > Papers > 2015 > atton-thesis

comparison agda.tex @ 40:470d99799398

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add description functor record
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 13 Feb 2015 11:31:46 +0900
parents 2ff5acb0d2e9
children 8fc2ac1f901f
comparison
equal deleted inserted replaced
39:8a70394e45b4 40:470d99799398
1 \chapter{Agda による証明手法} 1 \chapter{証明支援系言語 Agda による証明手法}
2 \label{chapter:agda} 2 \label{chapter:agda}
3 第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。 3 第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。
4 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。 4 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。
5 functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。 5 functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。
6 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。 6 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。