7.6.1. Dependent Types🔗

함수 호출과 일반 데이터 생성자처럼 타입이 아닌 코드를 포함하는 종속 타입은 타입 시스템의 표현력을 크게 높인다. 인자의 값에서 타입을 계산할 수 있으므로 어떤 인자가 주어지는지에 따라 함수의 반환 타입이 달라질 수 있다. 예를 들어 질의 결과에 실패할 수 있는 캐스팅 연산을 사용하지 않고 데이터베이스 질의의 결과 타입이 스키마와 특정 질의에 의존하게 할 수 있다. 질의가 바뀌면 실행 결과의 타입도 바뀌므로 컴파일 시점에 즉시 피드백을 얻는다.

함수의 반환 타입이 값에 의존하면 그 값을 패턴 매칭으로 분석할 때 타입이 정제될 수 있다. 값을 나타내는 변수가 패턴의 생성자로 대체되기 때문이다. 함수의 타입 서명은 반환 타입이 인자 값에 의존하는 방식을 기록하고, 패턴 매칭은 가능한 각 인자에 대해 반환 타입을 어떻게 충족하는지 설명한다.

타입에 들어 있는 일반 코드는 타입 검사 중 실행되지만 무한 루프를 돌 수 있는 partial 함수는 호출되지 않는다. 대부분 이 계산은 이 책 맨 앞에서 소개한 일반 평가 규칙을 따른다. 최종 값이 나올 때까지 표현식을 값으로 차례로 바꾼다. 타입 검사 중 계산은 실행 시점 계산과 중요한 차이가 있다. 타입의 일부 값은 아직 값이 알려지지 않은 변수일 수 있다. 이 경우 특정 생성자가 선택될 때까지(예를 들어 패턴 매칭으로 선택될 때까지) 패턴 매칭이 “막혀” 진행되지 않는다. 타입 수준 계산은 부분 평가의 일종으로 볼 수 있다. 충분히 알려진 프로그램 부분만 평가하고 나머지는 그대로 둔다.

7.6.2. The Universe Pattern🔗

종속 타입을 다룰 때 흔히 타입 시스템의 일부를 떼어 내는 패턴을 사용한다. 예를 들어 데이터베이스 질의 라이브러리는 길이가 다양한 문자열, 고정 길이 문자열, 특정 범위의 수는 반환할 수 있지만 함수나 사용자 정의 데이터 타입, IO 동작은 절대 반환하지 않을 수 있다. 원하는 타입의 구조에 맞는 생성자를 가진 데이터 타입을 먼저 정의하고 이 데이터 타입의 값을 실제 타입으로 해석하는 함수를 정의하면 도메인 특화 타입 시스템 부분집합을 만들 수 있다. 생성자를 해당 타입의 코드라고 하며, 전체 패턴을 타르스키식 유니버스라고 한다. Type 3이나 Prop 같은 유니버스를 뜻하지 않음이 문맥상 분명할 때는 그냥 유니버스라고도 한다.

사용자 정의 유니버스는 관심 있는 각 타입에 인스턴스를 제공하는 타입 클래스를 정의하는 대안이다. 타입 클래스는 확장 가능하지만 확장이 항상 바람직한 것은 아니다. 타입을 직접 사용하는 것보다 사용자 정의 유니버스를 정의하면 다음과 같은 장점이 있다:

• 동등성 검사와 직렬화처럼 유니버스의 모든 타입에서 작동하는 일반 연산을 코드 재귀로 구현할 수 있다.

• 외부 시스템이 허용하는 타입을 정확히 표현할 수 있고 코드 데이터 타입의 정의가 허용되는 것을 문서화한다.

• Lean의 패턴 매칭 완전성 검사기는 코드를 빠뜨리지 않게 하는 반면 타입 클래스 기반 해법은 누락된 인스턴스 오류를 클라이언트 코드로 미룬다.

7.6.3. Indexed Families🔗

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

인덱싱된 패밀리는 데이터 사이의 복잡한 관계를 표현하고 이를 모두 컴파일러가 검사하게 한다. 데이터 타입의 불변식을 직접 인코딩하므로 잠시라도 이를 위반할 방법이 없다. 컴파일러에 불변식을 알려 주면 이를 충족하기 위해 무엇을 해야 하는지 컴파일러가 프로그래머에게 알려 주는 큰 이점이 있다. 컴파일 시점 오류, 특히 밑줄에서 생기는 오류를 전략적으로 사용하면 프로그래밍 사고의 일부를 Lean에 맡기고 다른 일에 집중할 수 있다.

인덱싱된 패밀리로 불변식을 인코딩하면 어려움이 생길 수 있다. 먼저 불변식마다 자체 데이터 타입이 필요하고, 이에 따라 지원 라이브러리도 필요하다. 결국 List.zip과 Vect.zip은 서로 바꿔 쓸 수 없다. 이는 코드 중복으로 이어질 수 있다. 둘째, 인덱싱된 패밀리를 편리하게 사용하려면 타입에서 사용되는 함수의 재귀 구조가 타입 검사 중인 프로그램의 재귀 구조와 맞아야 한다. 인덱싱된 패밀리 프로그래밍은 올바른 우연의 일치를 마련하는 기술이다. 동등성 증명을 사용해 일치하지 않는 부분을 우회할 수도 있지만 어렵고, 암호 같은 정당화가 가득한 프로그램이 된다. 셋째, 타입 검사 중 큰 값에서 복잡한 코드를 실행하면 컴파일이 느려질 수 있다. 복잡한 프로그램에서 이런 느려짐을 피하려면 특수한 기법이 필요할 수 있다.

7.6.4. Definitional and Propositional Equality🔗

Lean의 타입 검사기는 때때로 두 타입을 서로 바꿔 쓸 수 있는지 검사해야 한다. 타입은 임의의 프로그램을 포함할 수 있으므로 임의의 프로그램이 같은지도 검사할 수 있어야 한다. 그러나 임의의 프로그램이 완전히 일반적인 수학적 의미에서 같은지 검사하는 효율적인 알고리즘은 없다. 이를 해결하기 위해 Lean에는 두 가지 동등성 개념이 있다:

• 정의적 동등성(definitional equality)은 계산과 바인딩된 변수의 이름 변경을 고려한 구문적 표현의 동등성만 검사하는 동등성의 과소 근사(underapproximation)다. Lean은 필요한 상황에서 정의적 동등성을 자동으로 검사한다.

• 명제적 동등성(propositional equality)은 프로그래머가 명시적으로 증명하고 명시적으로 호출해야 한다. 그 대신 Lean은 증명이 유효하고 호출이 올바른 목표를 달성하는지 자동으로 검사한다.

두 동등성 개념은 프로그래머와 Lean 사이의 역할 분담을 나타낸다. 정의적 동등성은 단순하지만 자동이고, 명제적 동등성은 수동이지만 표현력이 있다. 명제적 동등성을 사용하면 타입 안에서 달리 막혀 있는 프로그램을 풀 수 있다.

그러나 타입 수준 계산을 풀기 위해 명제적 동등성을 자주 사용하는 것은 보통 코드 냄새다. 대개 우연의 일치를 잘 설계하지 않았다는 뜻이므로 타입과 인덱스를 다시 설계하거나 필요한 불변식을 강제할 다른 기법을 사용하는 편이 낫다. 반대로 명제적 동등성을 프로그램이 명세를 만족함을 증명하거나 서브타입의 일부로 사용한다면 의심할 이유가 적다.