8.7. Special Types🔗

메모리에서 데이터가 표현되는 방식을 이해하는 것은 매우 중요하다. 보통 데이터 타입의 정의에서 표현 방식을 알 수 있다. 각 생성자는 태그와 참조 횟수를 포함한 헤더가 있는 메모리 객체에 대응한다. 생성자의 각 인자는 다른 객체를 가리키는 포인터로 표현된다. 즉 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은 힙 객체를 가리키는 포인터가 아니라 상수값이다.

다음 타입은 특별한 표현을 가진다: