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이 힙에 할당된 객체를 가리키는 포인터가 아니라 상수 값임을 의미합니다.

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