7. Programming with Dependent Types🔗

대부분의 정적 타입 프로그래밍 언어에서는 타입의 세계와 프로그램의 세계 사이에 단단한 경계가 있다. 타입과 프로그램은 문법이 다르고 서로 다른 시점에 사용된다. 타입은 보통 컴파일 시점에 프로그램이 특정 불변식을 지키는지 검사하는 데 사용된다. 프로그램은 실제 계산을 수행하기 위해 실행 시점에 사용된다. 둘이 상호작용할 때는 대개 “instance-of” 검사와 같은 타입 분기 연산자나, 타입 검사기에 없던 정보를 제공하여 실행 시점에 검증하게 하는 캐스팅 연산자의 형태를 띤다. 즉 타입이 프로그램의 세계에 삽입되어 제한적인 실행 시점 의미를 얻는 방식으로 상호작용한다.

Lean은 이런 엄격한 분리를 강제하지 않는다. Lean에서는 프로그램이 타입을 계산할 수 있고 타입이 프로그램을 포함할 수 있다. 프로그램을 타입에 넣으면 컴파일 시점에 프로그램의 계산 능력을 온전히 사용할 수 있으며, 함수가 타입을 반환할 수 있으므로 타입은 프로그래밍 과정의 일급 참여자가 된다.

종속 타입(dependent type)은 타입이 아닌 표현식을 포함하는 타입이다. 종속 타입의 흔한 원천은 함수의 이름 있는 인자다. 예를 들어 natOrStringThree 함수는 전달받은 Bool에 따라 자연수나 문자열을 반환한다:

def natOrStringThree (b : Bool) : if b then Nat else String :=
  match b with
  | true => (3 : Nat)
  | false => "three"

종속 타입의 다른 예는 다음과 같다:

다형성 입문 절의 posOrNegThree는 인자 값에 따라 반환 타입이 달라진다.
OfNat 타입 클래스는 사용된 특정 자연수 리터럴에 의존한다.
검증기 예제에서 사용한 CheckedInput 구조체는 검증이 수행된 연도에 의존한다.
서브타입은 특정 값을 가리키는 명제를 포함한다.
배열 인덱싱 표기법의 유효성을 결정하는 명제를 비롯해, 흥미로운 명제는 거의 모두 값을 포함하는 타입이므로 종속 타입이다.

종속 타입은 타입 시스템의 능력을 크게 높인다. 인자 값에 따라 분기하는 반환 타입의 유연성 덕분에 다른 타입 시스템에서는 쉽게 타입을 부여할 수 없는 프로그램도 작성할 수 있다. 동시에 종속 타입은 함수가 반환할 수 있는 값을 타입 서명이 제한하게 하여 강한 불변식을 컴파일 시점에 강제한다.

그러나 종속 타입을 사용한 프로그래밍은 상당히 복잡할 수 있으며 함수형 프로그래밍을 넘어서는 여러 기술이 필요하다. 표현력 있는 명세는 충족하기 어려울 수 있고, 스스로 복잡한 상황에 빠져 프로그램을 완성하지 못할 위험도 있다. 반면 이 과정에서 새로운 이해를 얻고, 이를 충족할 수 있는 정제된 타입으로 표현할 수도 있다. 이 장에서는 종속 타입 프로그래밍의 표면만 다루지만, 그 자체로 한 권의 책을 쓸 만한 깊은 주제다.