1.2. Types
타입은 프로그램이 계산할 수 있는 값에 따라 프로그램을 분류한다. 타입은 프로그램에서 다음과 같은 여러 역할을 한다.
-
컴파일러가 값의 메모리 표현을 결정할 수 있게 한다.
-
함수의 입력과 출력에 대한 가벼운 명세로서 프로그래머의 의도를 다른 사람에게 전달한다. 컴파일러는 프로그램이 이 명세를 따르는지 보장한다.
-
문자열에 수를 더하는 것 같은 여러 잠재적 실수를 방지해 프로그램에 필요한 테스트 수를 줄인다.
-
Lean 컴파일러가 반복적인 코드를 줄여 주는 보조 코드를 자동으로 생성하도록 돕는다.
Lean의 타입 시스템은 유난히 표현력이 높다. 타입은 “이 정렬 함수는 입력의 순열을 반환한다”와 같은 강한 명세나 “이 함수는 인수의 값에 따라 반환 타입이 다르다”와 같은 유연한 명세를 표현할 수 있다. 타입 시스템은 수학 정리를 증명하는 완전한 논리로 사용할 수도 있다. 하지만 이러한 최첨단 표현력이 더 단순한 타입을 불필요하게 만들지는 않으며, 고급 기능을 사용하려면 먼저 이 단순한 타입을 이해해야 한다.
Lean의 모든 프로그램에는 타입이 있어야 한다. 특히 모든 표현식은 평가되기 전에 타입이 있어야 한다. 지금까지의 예제에서는 Lean이 스스로 타입을 알아낼 수 있었지만, 때로는 타입을 직접 제공해야 한다. 이는 괄호 안에서 콜론 연산자를 사용해 다음과 같이 한다:
#eval (1 + 2 : Nat)
여기서 Nat은 임의의 정밀도를 가진 부호 없는 정수인 자연수의 타입이다.
Lean에서 Nat은 음이 아닌 정수 리터럴의 기본 타입이다.
하지만 이 기본 타입이 항상 최선의 선택은 아니다.
C에서는 뺄셈 결과가 0보다 작아질 때 부호 없는 정수가 표현할 수 있는 가장 큰 수로 언더플로한다.
그러나 Nat은 임의로 큰 부호 없는 수를 표현할 수 있으므로 언더플로할 가장 큰 수가 없다.
따라서 Nat의 뺄셈은 결과가 원래 음수가 되었을 경우 zero를 반환한다.
예를 들어,
#eval (1 - 2 : Nat)
-1이 아니라 0으로 평가된다.
음의 정수를 표현할 수 있는 타입을 사용하려면 이를 직접 제공한다:
#eval (1 - 2 : Int)
이 타입을 사용하면 예상대로 결과는 -1이다.
표현식을 평가하지 않고 타입을 확인하려면 #eval 대신 #check을 사용한다. 예를 들면 다음과 같다:
#check (1 - 2 : Int)
실제로 뺄셈을 수행하지 않고 1 - 2 : Int를 보고한다.
프로그램에 타입을 부여할 수 없으면 #check과 #eval 모두 오류를 반환한다. 예를 들면 다음과 같다:
#check String.append ["hello", " "] "world"다음과 같이 출력된다.
String.append의 첫 번째 인수에는 문자열이 필요하지만 문자열 목록이 제공되었기 때문이다.