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 구조체는 검증이 이루어진 연도에 의존합니다.
서브타입은 특정 값을 가리키는 명제를 포함합니다.
배열 인덱싱 표기법의 유효성을 결정하는 명제를 포함하여, 사실상 흥미로운 명제는 모두 값을 포함하는 타입이며, 따라서 의존 타입입니다.

의존 타입은 타입 시스템의 표현력을 크게 높입니다. 인자 값에 따라 달라지는 반환 타입의 유연성 덕분에 다른 타입 시스템에서는 타입을 붙이기 어려운 프로그램도 작성할 수 있습니다. 또한 의존 타입을 사용하면 타입 시그니처로 함수가 반환할 수 있는 값을 제한할 수 있으므로 강력한 불변 조건을 컴파일 시점에 강제할 수 있습니다.

하지만 의존 타입을 사용한 프로그래밍은 상당히 복잡할 수 있으며, 함수형 프로그래밍을 훨씬 넘어서는 일련의 기술을 필요로 합니다. 표현력이 풍부한 명세는 충족하기가 복잡할 수 있으며, 스스로 옭아매여 프로그램을 완성하지 못하게 될 위험이 실제로 존재합니다. 반면에 이 과정은 새로운 이해로 이어질 수 있으며, 이러한 이해는 충족 가능한 정제된 타입으로 표현될 수 있습니다. 이 장에서는 의존 타입 프로그래밍의 겉면만 살짝 다루지만, 이는 그 자체로 책 한 권을 할애할 만한 깊은 주제입니다.