---
# System prepended metadata

title: Dependent Type

---

# _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