7.6.1. 의존 타입🔗

타입이 함수 호출이나 일반적인 데이터 생성자처럼 타입이 아닌 코드를 포함하는 의존 타입은 타입 시스템의 표현력을 크게 높입니다. 인자의 값으로부터 타입을 계산할 수 있다는 것은 어떤 인자가 주어지느냐에 따라 함수의 반환 타입이 달라질 수 있다는 뜻입니다. 예를 들어, 이를 이용하면 쿼리 결과에 실패할 가능성이 있는 캐스트 연산을 적용하지 않고도 데이터베이스 쿼리의 결과 타입이 데이터베이스의 스키마와 실행한 구체적인 쿼리에 따라 결정되도록 할 수 있습니다. 쿼리가 바뀌면 그 쿼리를 실행한 결과의 타입도 함께 바뀌므로, 컴파일 시점에 즉각적인 피드백을 받을 수 있습니다.

함수의 반환 타입이 값에 의존하는 경우, 패턴 매칭으로 그 값을 분석하면 값을 나타내는 변수가 패턴 속의 생성자로 대체되므로 타입이 정제될 수 있습니다. 함수의 타입 시그니처는 반환 타입이 인자 값에 어떻게 의존하는지를 문서화하며, 패턴 매칭은 가능한 각 인자에 대해 반환 타입을 어떻게 충족할 수 있는지를 설명합니다.

타입 안에 나타나는 일반 코드는 타입 검사 중에 실행됩니다. 다만 무한히 반복될 수 있는 partial 함수는 호출되지 않습니다. 대부분의 경우 이 계산은 이 책의 맨 처음에서 소개한 일반적인 평가 규칙을 따르며, 최종 값이 나올 때까지 표현식이 점차 그 값으로 대체됩니다. 타입 검사 중의 계산은 런타임 계산과 중요한 차이가 하나 있습니다. 타입 안의 일부 값은 아직 값이 알려지지 않은 변수일 수 있다는 점입니다. 이런 경우 패턴 매칭은 “막힌” 상태가 되어, 예를 들어 패턴 매칭을 통해 특정 생성자가 선택되기 전까지는 진행되지 않으며 끝내 선택되지 않으면 계속 진행되지 않습니다. 타입 수준 계산은 일종의 부분 평가로 볼 수 있습니다. 부분 평가에서는 프로그램 중 충분히 알려진 부분만 평가하면 되고 나머지 부분은 그대로 둡니다.

7.6.2. 유니버스 패턴🔗

의존 타입을 다룰 때 흔히 쓰는 패턴 중 하나는 타입 시스템의 일부분을 따로 떼어 내는 것입니다. 예를 들어, 데이터베이스 쿼리 라이브러리는 가변 길이 문자열, 고정 길이 문자열, 특정 범위의 숫자는 반환할 수 있지만, 함수나 사용자 정의 데이터 타입, IO 액션은 결코 반환하지 않습니다. 타입 시스템의 도메인 특화 부분집합을 정의하려면, 먼저 원하는 타입들의 구조에 맞는 생성자를 가진 데이터 타입을 정의한 다음, 이 데이터 타입의 값을 진짜 타입으로 해석하는 함수를 정의하면 됩니다. 이 생성자들을 해당 타입들의 코드라고 부르며, 이 패턴 전체를 타르스키 방식의 유니버스(universe à la Tarski)라고 부르기도 하고, Type 3이나 Prop 같은 유니버스를 뜻하는 것이 아님이 문맥상 분명할 때는 그냥 유니버스라고 부르기도 합니다.

사용자 정의 유니버스는 관심 있는 각 타입마다 인스턴스를 두는 타입 클래스를 정의하는 방식의 대안입니다. 타입 클래스는 확장 가능하지만, 확장성이 항상 바람직한 것은 아닙니다. 사용자 정의 유니버스를 정의하면 타입을 직접 사용하는 것에 비해 여러 가지 장점이 있습니다:

• 동등성 검사나 직렬화처럼 유니버스 안의 모든 타입에 대해 동작하는 제네릭 연산은 코드에 대한 재귀로 구현할 수 있습니다.

• 외부 시스템이 받아들이는 타입을 정확하게 표현할 수 있으며, 코드 데이터 타입의 정의는 무엇을 기대할 수 있는지 문서화하는 역할을 합니다.

• Lean의 패턴 매칭 완전성 검사기는 빠뜨린 코드가 없도록 보장하는 반면, 타입 클래스에 기반한 해법은 인스턴스 누락 오류를 클라이언트 코드로 미룹니다.

7.6.3. 인덱스 족🔗

데이터 타입은 서로 다른 두 종류의 인자를 받을 수 있습니다. 매개변수는 데이터 타입의 모든 생성자에서 동일하지만, 인덱스는 생성자마다 다를 수 있습니다. 인덱스를 특정 값으로 정하면 데이터 타입의 생성자 중 일부만 사용할 수 있습니다. 예를 들어, Vect.nil은 길이 인덱스가 0일 때만 사용할 수 있고, Vect.cons는 어떤 n에 대해 길이 인덱스가 n+1일 때만 사용할 수 있습니다. 매개변수는 보통 데이터 타입 선언에서 콜론 앞에 이름 붙은 인자로 쓰고 인덱스는 콜론 뒤 함수 타입의 인자로 쓰지만, Lean은 콜론 뒤의 인자가 매개변수로 쓰이는 경우를 추론할 수 있습니다.

인덱스 족을 사용하면 데이터 사이의 복잡한 관계를 표현식으로 나타낼 수 있으며, 이는 모두 컴파일러가 검사합니다. 데이터 타입의 불변 조건을 직접 인코딩할 수 있으며, 일시적으로라도 이를 위반할 방법은 없습니다. 데이터 타입의 불변 조건을 컴파일러에게 알려 주면 큰 이점이 있습니다. 이제 컴파일러가 불변 조건을 만족시키려면 무엇을 해야 하는지 프로그래머에게 알려 줄 수 있습니다. 컴파일 타임 오류, 특히 밑줄에서 비롯되는 오류를 전략적으로 활용하면 프로그래밍 사고 과정의 일부를 Lean에 맡길 수 있으며, 그만큼 프로그래머는 다른 문제에 신경 쓸 여유를 얻습니다.

인덱스 족을 사용해 불변 조건을 인코딩하면 어려움이 생길 수 있습니다. 첫째, 불변 조건마다 전용 데이터 타입이 필요하고, 그 데이터 타입에는 다시 전용 지원 라이브러리가 필요합니다. 결국 List.zip과 Vect.zip은 서로 바꿔 쓸 수 없기 때문입니다. 이로 인해 코드 중복이 생길 수 있습니다. 둘째, 인덱스 족을 편리하게 사용하려면 타입에 쓰이는 함수의 재귀 구조가 타입 검사 대상 프로그램의 재귀 구조와 일치해야 합니다. 인덱스 족을 이용한 프로그래밍은 올바른 우연의 일치가 일어나도록 조율하는 기술입니다. 들어맞지 않는 우연은 동등성 증명에 기대어 우회할 수 있지만, 이는 어려운 일이며 프로그램이 이해하기 힘든 정당화로 뒤덮이게 됩니다. 셋째, 타입 검사 중에 큰 값에 대해 복잡한 코드를 실행하면 컴파일 시간이 느려질 수 있습니다. 복잡한 프로그램에서 이러한 속도 저하를 피하려면 특수한 기법이 필요할 수 있습니다.

7.6.4. 정의적 동등성과 명제적 동등성🔗

Lean의 타입 검사기는 때때로 두 타입을 서로 바꿔 쓸 수 있는 것으로 간주해야 하는지 검사해야 합니다. 타입에는 임의의 프로그램이 포함될 수 있으므로, 타입 검사기는 임의의 프로그램이 서로 같은지 검사할 수 있어야 합니다. 그러나 임의의 프로그램이 완전히 일반적인 수학적 의미에서 같은지 검사하는 효율적인 알고리즘은 존재하지 않습니다. 이 문제를 피하기 위해 Lean에는 두 가지 동등성 개념이 있습니다:

• 정의적 동등성은 동등성을 과소 근사한 것으로, 본질적으로 계산과 속박 변수의 이름 변경을 제외하고 구문적 표현이 같은지를 확인합니다. Lean은 정의상 동등성이 필요한 상황에서 이를 자동으로 검사합니다.

• 명제적 동치는 프로그래머가 명시적으로 증명하고 명시적으로 사용해야 합니다. 그 대신 Lean은 증명이 유효한지, 그리고 그 사용이 올바른 목표를 달성하는지를 자동으로 검사합니다.

두 가지 동등성 개념은 프로그래머와 Lean 사이의 역할 분담을 나타냅니다. 정의상 동등성은 단순하지만 자동으로 처리되는 반면, 명제적 동등성은 수동으로 다뤄야 하지만 표현력이 뛰어납니다. 명제적 동등성을 사용하면, 그렇지 않았다면 타입 안에서 막혀 버렸을 프로그램을 다시 진행시킬 수 있습니다.

하지만 막힌 타입 수준 계산을 풀어 주려고 명제적 동등성을 자주 사용한다면 대개 코드 스멜입니다. 이는 보통 우연의 일치가 잘 설계되지 않았다는 뜻이며, 타입과 인덱스를 다시 설계하거나 필요한 불변 조건을 다른 기법으로 강제하는 편이 대체로 더 좋습니다. 반면 프로그램이 명세를 충족함을 증명하는 데 명제적 동등성을 사용하거나 서브타입의 일부로 사용할 때는 의심할 이유가 적습니다.