7. 의존 타입을 사용한 프로그래밍🔗

대부분의 정적 타입 프로그래밍 언어에서는 타입의 세계와 프로그램의 세계 사이에 밀폐된 경계가 존재합니다. 타입과 프로그램은 서로 다른 문법을 가지며 서로 다른 시점에 사용됩니다. 타입은 일반적으로 컴파일 시점에 프로그램이 특정 불변 조건을 준수하는지 검사하는 데 사용됩니다. 프로그램은 실행 시점에 실제 계산을 수행하기 위해 사용됩니다. 이 둘이 상호작용할 때는 대개 "instance-of" 검사나 캐스팅 연산자와 같은 타입 케이스 연산자의 형태를 취하며, 이는 타입 검사기에 그렇지 않으면 알 수 없었을 정보를 제공하여 실행 시점에 검증되도록 합니다. 다시 말해, 이러한 상호작용은 타입이 프로그램의 세계에 삽입되어 제한적인 런타임 의미를 얻는 형태로 이루어집니다.

Lean은 이러한 엄격한 분리를 강제하지 않습니다. Lean에서는 프로그램이 타입을 계산할 수 있으며, 타입이 프로그램을 포함할 수 있습니다. 프로그램을 타입 안에 배치하면 컴파일 시점에 그 완전한 계산 능력을 활용할 수 있으며, 함수에서 타입을 반환할 수 있는 능력은 타입을 프로그래밍 과정의 일급 참여자로 만듭니다.

의존 타입은 타입이 아닌 표현식을 포함하는 타입입니다. 의존 타입의 흔한 원천 중 하나는 함수에 대한 이름 붙은 인자입니다. 예를 들어, 함수 natOrStringThree는 전달받은 Bool이 무엇인지에 따라 자연수나 문자열 중 하나를 반환합니다:

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

의존 타입의 추가 예시는 다음과 같습니다:

다형성에 대한 소개 절에는 posOrNegThree가 있으며, 여기서 함수의 반환 타입은 인자의 값에 따라 달라집니다.
OfNat 타입 클래스는 사용되는 특정 자연수 리터럴에 따라 달라집니다.
검증기 예제에서 사용된 CheckedInput 구조체는 검증이 이루어진 연도에 의존합니다.
서브타입은 특정 값을 가리키는 명제를 포함합니다.
배열 인덱싱 표기법의 유효성을 결정하는 것을 포함하여 사실상 모든 흥미로운 명제는 값을 포함하는 타입이며, 따라서 의존 타입입니다.

의존 타입은 타입 시스템의 표현력을 크게 향상시킵니다. 인자 값에 따라 분기하는 반환 타입의 유연성 덕분에, 다른 타입 시스템에서는 타입을 부여하기 쉽지 않은 프로그램도 작성할 수 있습니다. 동시에, 의존 타입은 타입 시그니처가 함수에서 반환될 수 있는 값을 제한할 수 있도록 해주며, 이를 통해 강력한 불변 조건을 컴파일 시점에 강제할 수 있습니다.

하지만 의존 타입을 사용한 프로그래밍은 상당히 복잡할 수 있으며, 함수형 프로그래밍을 넘어서는 별도의 기술 전반을 요구합니다. 표현력이 풍부한 명세는 충족하기 복잡할 수 있으며, 스스로 얽매여 프로그램을 완성하지 못하게 될 실질적인 위험이 있습니다. 반면, 이 과정은 새로운 이해로 이어질 수 있으며, 이는 충족될 수 있는 정련된 타입으로 표현될 수 있습니다. 이 장에서는 의존적으로 타입이 지정된 프로그래밍의 표면만을 다루고 있지만, 이는 그 자체로 한 권의 책 전체를 할애할 만한 깊이 있는 주제입니다.