一個外行對依值型別的理解

依值型別 (dependent type) 是型別理論 (type theory) 的重要概念，也是FP的進階概念。因為概念很抽象，而且還要會點型別概念，方好入手。雖此係函數式程式語言的重要概念，但是許多程式人，會仰之彌高，進而生畏，降低學習意願，遑論相關係的定理證明了。

身為一個外行，之前筆者亦如是。對型別理論感到興趣之際，面對依值型別還是一頭霧水，不知何以理解。然最近稍理解些，所以做了這份筆記。

但是因為內文牽涉許多數學符號，為利閱讀，以Typst排版軟體製成PDF版：[下載連結]