定義 (Type Theory)：一種型別(type)，其內容取決於屬於該型別之值(value)。 包含 Pi-type、Sigma-type等 語源 dependent：Webster's New College dictionary：influenced, controlled, or determined by something else（被其他事物影響、控制或定義） 可以理解為：依靠的、關聯的、受影響的（遠東《新時代英漢詞典》），是independent（獨立）的反義詞。 type：臺灣通常的翻譯為「型別」，簡中圈為「類型」

語源 co-（共同、一起） routine維基詞典：設計來辦理特別任務的指令之集合 A set of instructions designed to perform a specific task; a subroutine.(http://en.wiktionary.org/wiki/routine) 臺灣以前有人翻成「子程式；常式」（參資訊學會用詞表） 常式用例：曾建超，1994：分散式記憶體多處理機的平行編譯系統(II) 國家教育研究院樂詞網收錄常程式 既有翻譯 共常式co-（共）+routine（常式）