7.6.1. 의존 타입🔗

의존 타입은 함수 호출이나 일반적인 데이터 생성자 같은 비타입 코드를 타입이 포함하는 경우로, 타입 시스템의 표현력을 크게 증가시킵니다. 인자의 value로부터 타입을 compute할 수 있다는 것은 함수의 반환 타입이 어떤 인자가 제공되는지에 따라 달라질 수 있음을 의미합니다. 예를 들어, 이를 활용하면 쿼리 결과에 대해 실패할 가능성이 있는 캐스트 연산을 필요로 하지 않으면서, 데이터베이스 쿼리의 결과 타입이 데이터베이스의 스키마와 실행된 특정 쿼리에 의존하도록 만들 수 있습니다. 쿼리가 변경되면 그것을 실행한 결과로 나오는 타입도 함께 변경되므로, 즉각적인 컴파일 시점 피드백이 가능해집니다.

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

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

7.6.2. 유니버스 패턴🔗

의존 타입을 다룰 때 흔히 쓰이는 패턴은 타입 시스템의 일부 부분집합을 구획하는 것입니다. 예를 들어, 데이터베이스 쿼리 라이브러리는 가변 길이 문자열, 고정 길이 문자열, 또는 특정 범위 내의 숫자를 반환할 수 있지만, 함수나 사용자 정의 데이터 타입, 또는 IO 액션을 반환하는 일은 결코 없습니다. 타입 시스템의 도메인 특화 부분집합은, 원하는 타입들의 구조와 일치하는 생성자를 가진 데이터타입을 먼저 정의한 다음, 이 데이터타입의 값을 실제 타입으로 해석하는 함수를 정의함으로써 정의할 수 있습니다. 이 생성자는 문제가 되는 타입들에 대한 코드라고 불리며, 전체 패턴은 때로는 타르스키식 유니버스라고 불리거나, Type 3 또는 Prop과 같은 유니버스를 의미하는 것이 아니라는 점이 문맥상 명확할 때는 그냥 유니버스라고 불리기도 합니다.

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

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

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

• 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 자체 사이의 역할 분담을 나타냅니다. 정의적 동치는 단순하지만 자동으로 이루어지는 반면, 명제적 동치는 수동적이지만 표현력이 있습니다. 명제 동등성은 그렇지 않았다면 타입 내에서 막혀 있었을 프로그램을 다시 진행시키는 데 사용할 수 있습니다.

하지만 타입 수준 계산의 진행을 막힌 상태에서 풀어내기 위해 명제적 동치를 빈번하게 사용하는 것은 일반적으로 코드 스멜(code smell)에 해당합니다. 이는 일반적으로 우연의 일치가 잘 설계되지 않았음을 의미하며, 필요한 불변량을 강제하려면 대개 타입과 인덱스를 재설계하거나 다른 기법을 사용하는 것이 더 나은 방법입니다. 명제적 동등성이 프로그램이 명세를 만족함을 증명하는 데 사용되거나 서브타입의 일부로 사용되는 경우에는 의심할 이유가 더 적습니다.