8.7. 특수 타입🔗

메모리에서 데이터가 어떻게 표현되는지 이해하는 것은 매우 중요합니다. 일반적으로 그 표현은 데이터 타입의 정의를 보면 이해할 수 있습니다. 각 생성자는 메모리상의 객체 하나에 대응하며, 이 객체에는 태그와 참조 카운트를 담은 헤더가 있습니다. 생성자의 각 인자는 다른 객체를 가리키는 포인터로 표현됩니다. 다시 말해, List는 실제로 연결 리스트이며, structure에서 필드를 꺼내는 일은 실제로 포인터 하나를 따라가는 것에 불과합니다.

그러나 이 규칙에는 몇 가지 중요한 예외가 있습니다. 여러 타입이 컴파일러에 의해 특별하게 취급됩니다. 예를 들어, UInt32 타입은 Fin (2 ^ 32)로 정의되지만, 런타임에는 머신 워드에 기반한 실제 네이티브 구현으로 대체됩니다. 마찬가지로, Nat의 정의는 List Unit과 유사한 구현을 암시하지만, 실제 런타임 표현은 충분히 작은 수에 대해서는 즉시 머신 워드를 사용하고 더 큰 수에 대해서는 효율적인 임의 정밀도 산술 라이브러리를 사용합니다. Lean 컴파일러는 패턴 매칭을 사용하는 정의를 이 표현에 맞는 적절한 연산으로 변환하며, 덧셈과 뺄셈 같은 연산 호출은 하부 산술 라이브러리의 빠른 연산으로 대응됩니다. 결국, 덧셈이 피가수의 크기에 선형적으로 비례하는 시간이 걸려서는 안 됩니다.

일부 타입이 특수한 표현을 가진다는 사실은 이러한 타입을 다룰 때 주의가 필요하다는 의미이기도 합니다. 이러한 타입 대부분은 컴파일러가 특별하게 취급하는 structure로 이루어져 있습니다. 이러한 구조체에서 생성자나 필드 접근자를 직접 사용하면 효율적인 표현과 증명에 사용하도록 설계된 표현 사이에 비용이 큰 변환이 일어날 수 있습니다.

예를 들어 배열은 연결 리스트를 감싸는 구조체로 정의됩니다. 컴파일된 코드에서 배열은 효율적인 동적 배열로 표현되며, 리스트에 생성자 Array.mk를 적용하면 그 리스트가 이러한 효율적인 배열로 변환되는데, 이 변환에는 선형 시간이 걸립니다. 필드 접근자 toList는 배열을 다시 연결 리스트로 변환하며, 이 역시 선형 시간이 걸립니다. 이러한 Array의 정의는 오로지 배열에 관한 성질을 더 쉽게 증명하기 위해 존재하며, 실제로 실행될 코드에서는 이러한 변환을 피해야 합니다. 마찬가지로 String은 바이트 배열과 그 바이트들이 유효한 UTF-8이라는 증명을 함께 담은 구조체로 정의되지만, 런타임 표현에는 문자열의 문자 수를 캐시하는 필드가 추가로 포함됩니다. 생성자는 바이트 배열이 유효할 때만 적용할 수 있으므로 바이트들이 실제로 UTF-8 시퀀스인지 확인할 필요는 없지만, 문자 수는 선형 시간에 계산됩니다. 접근자 toByteArray는 새 바이트 배열 객체를 할당하고 내부 바이트를 복사하므로 선형 시간과 선형 공간이 듭니다. 문자열에 대한 기본 연산 중 상당수는 컴파일러에 의해 효율적인 버전으로 대체되며, 이 버전은 가능한 경우 새 문자열을 할당하는 대신 런타임 문자열을 직접 변경합니다.

타입 자체와 명제의 증명은 모두 컴파일된 코드에서 완전히 지워집니다. 다시 말해, 이들은 공간을 전혀 차지하지 않으며, 증명의 일부로 수행되었을 수 있는 모든 계산 역시 마찬가지로 지워집니다. 이는 증명이 배열을 귀납적으로 정의된 리스트로 다루는 편리한 인터페이스를 활용할 수 있다는 뜻이며, 여기에는 귀납법을 사용하여 배열에 관한 사실을 증명하는 것도 포함됩니다. 그러면서도 프로그램이 실행되는 동안 느린 변환 단계를 거치지 않습니다. 이러한 내장 타입의 경우, 데이터를 편리한 논리적 표현으로 나타낸다고 해서 프로그램이 느려야 하는 것은 아닙니다.

구조체 타입에 타입도 증명도 아닌 필드가 단 하나만 있다면, 실행 시점에는 생성자 자체가 사라지고 그 하나뿐인 인자로 대체됩니다. 다시 말해, 서브타입은 추가적인 간접 참조 계층 없이 기반 타입과 똑같이 표현됩니다. 마찬가지로 Fin은 메모리상에서 그저 Nat일 뿐이며, 단일 필드 구조체를 만들어 Nat이나 String의 서로 다른 용도를 구분하더라도 성능상의 손해가 없습니다. 생성자에 타입도 증명도 아닌 인자가 하나도 없다면, 그 생성자 역시 사라지고 원래 포인터가 쓰였을 자리에 상수 값이 대신 들어갑니다. 따라서 true, false, none은 힙에 할당된 객체를 가리키는 포인터가 아니라 상수 값입니다.

다음 타입들은 특별한 표현을 가집니다.