Dependent type

컴퓨터과학 또는 논리학에서 의존형이란 타입 정의가 값에 의존하는 타입을 말한다. 프로그래밍 언어 중 Lean, Idris, Coq 등이 의존형 시스템을 채택하고 있다.