의존형

의존형(dependent type) 또는 종속유형은 컴퓨터 과학 및 논리학에서 정의가 값에 따라 달라지는 유형이다. 이는 유형 이론과 유형 시스템이 겹치는 특징이다. 직관주의적 유형 이론에서는 의존형을 사용하여 "모두에게" 및 "존재합니다"와 같은 논리 수량자를 인코딩한다. Agda, ATS, Coq, F*, Epigram, Idris 및 Lean과 같은 함수형 프로그래밍 언어에서 의존형은 프로그래머가 가능한 구현 세트를 더욱 제한하는 유형을 할당할 수 있도록 하여 버그를 줄이는 데 도움이 된다.

의존형의 두 가지 일반적인 예는 종속 함수와 종속 쌍이다. 종속 함수의 반환 유형은 해당 인수 중 하나의 값(유형뿐만 아니라)에 따라 달라질 수 있다. 예를 들어 양의 정수 n을 사용하는 함수는 길이가 n인 배열을 반환할 수 있다. 여기서 배열 길이는 배열 유형의 일부이다. (이는 유형을 인수로 포함하는 다형성 (컴퓨터 과학) 및 제네릭 프로그래밍과는 다르다.) 종속 쌍은 첫 번째 값에 따라 유형이 달라지는 두 번째 값을 가질 수 있다. 배열 예제를 고수하면 종속 쌍을 사용하여 형식이 안전한 방식으로 배열과 길이를 쌍으로 연결할 수 있다.

의존형은 유형 시스템에 복잡성을 추가한다. 프로그램에서 의존형의 동등성을 결정하려면 계산이 필요할 수 있다. 의존형에 임의의 값이 허용되는 경우 유형 동등성을 결정하는 것은 두 임의의 프로그램이 동일한 결과를 생성하는지 여부를 결정하는 것을 포함할 수 있다. 따라서 유형 검사의 결정 가능성은 주어진 유형 이론의 동등 의미, 즉 유형 이론이 의도적인지 확장적인지 여부에 따라 달라질 수 있다.^[1]