# _dependent type_

## 定義
- (Type Theory)：一種型別(type)，其內容取決於屬於該型別之值(value)。
- 包含 Pi-type、Sigma-type等

## 語源

- dependent：
- *Webster's New College dictionary*：influenced, controlled, or determined by something else（被其他事物影響、控制或定義）
- 可以理解為：依靠的、關聯的、受影響的（遠東《新時代英漢詞典》），是independent（獨立）的反義詞。
- type：臺灣通常的翻譯為「型別」，簡中圈為「類型」

## 既有翻譯
- 依值型別：
- 用例：[中研院FLOLAC研習營相關網頁](https://flolac.iis.sinica.edu.tw/flolac14/dtp.html)

## 翻譯提案

- 暫無
- 以下為東亞的漢字翻譯：
- 簡中圈稱為「依賴類型」。
- 日文漢字稱為「依存型」（用例：[東京工業大学情報理工学院数理・計算科学系プログラミング研究室 - 依存型とエフェクト](https://prg.is.titech.ac.jp/ja/projects/typesystem/dependent-types-and-effects/)）
- 韓文漢字稱為「從屬類型」(종속 유형, *jongsok yuhyeong*)（用例：[韓文Wiki - 증명 보조기(證明 補助機)](https://ko.wikipedia.org/wiki/%EC%A6%9D%EB%AA%85_%EB%B3%B4%EC%A1%B0%EA%B8%B0)）

## 另請參考
- 型別論 (type theory)
- typing

## 參考資料
- 遠東《新時代英漢詞典》
- Webster’s New College dictionary