1.2. 타입🔗

타입은 계산 가능한 값을 기준으로 프로그램을 분류합니다. 타입은 프로그램에서 여러 역할을 수행합니다:

이는 컴파일러가 값의 메모리 내 표현에 대한 결정을 내릴 수 있게 해 줍니다.
타입은 프로그래머가 자신의 의도를 다른 사람에게 전달하는 데 도움이 되며, 함수의 입력과 출력에 대한 경량 명세 역할을 합니다. 컴파일러는 프로그램이 이 명세를 준수하는지 확인합니다.
이는 숫자와 문자열을 더하는 것과 같은 다양한 잠재적 실수를 방지하며, 따라서 프로그램에 필요한 테스트의 수를 줄여줍니다.
이는 Lean 컴파일러가 상용구를 줄여주는 보조 코드의 생성을 자동화하는 데 도움을 줍니다.

Lean의 타입 시스템은 유별나게 표현력이 뛰어납니다. 타입은 “이 정렬 함수는 입력의 순열을 반환한다”와 같은 강력한 명세와 “이 함수는 인자의 값에 따라 서로 다른 반환 타입을 가진다”와 같은 유연한 명세를 표현할 수 있습니다. 타입 시스템은 수학적 정리를 증명하기 위한 완전한 논리 체계로도 사용될 수 있습니다. 그러나 이러한 최첨단 표현력이 있다고 해서 더 단순한 타입들이 불필요해지는 것은 아니며, 이러한 단순한 타입을 이해하는 것은 더 고급 기능을 사용하기 위한 전제 조건입니다.

Lean의 모든 프로그램은 타입을 가져야 합니다. 특히, 모든 식은 평가되기 전에 타입을 가져야 합니다. 지금까지의 예제에서는 Lean이 스스로 타입을 알아낼 수 있었지만, 때로는 타입을 직접 제공해야 할 필요가 있습니다. 이는 괄호 안에서 콜론 연산자를 사용하여 수행됩니다:

3#eval (1 + 2 : Nat)

여기서 Nat은 자연수의 타입으로, 임의 정밀도의 부호 없는 정수입니다. Lean에서 Nat은(는) 음이 아닌 정수 리터럴의 기본 타입입니다. 이 기본 타입이 항상 최선의 선택은 아닙니다. C에서는 뺄셈의 결과가 0보다 작아질 경우, 부호 없는 정수는 표현 가능한 가장 큰 수로 언더플로됩니다. 그러나 Nat은 임의로 큰 부호 없는 수를 표현할 수 있으므로, 언더플로될 대상이 되는 가장 큰 수가 존재하지 않습니다. 따라서 Nat에 대한 뺄셈은 결과가 음수가 될 경우 zero를 반환합니다. 예를 들어,

0#eval (1 - 2 : Nat)

0으로 평가되며, -1으로 평가되지 않습니다. 음의 정수를 표현할 수 있는 타입을 사용하려면 이를 직접 제공하십시오:

-1#eval (1 - 2 : Int)

이 타입을 사용하면 예상대로 결과는 -1입니다.

식을 평가하지 않고 타입을 확인하려면 #eval 대신 #check를 사용하십시오. 예를 들면 다음과 같습니다:

1 - 2 : Int#check (1 - 2 : Int)

실제로 뺄셈을 수행하지 않고도 1 - 2 : Int를 보고합니다.

프로그램에 타입을 부여할 수 없는 경우, #check와 #eval 모두에서 오류가 반환됩니다. 예를 들면:

sorry.append "world" : String#check String.append Application type mismatch: The argument
  ["hello", " "]
has type
  List String
but is expected to have type
  String
in the application
  String.append ["hello", " "]["hello", " "] "world"

출력

Application type mismatch: The argument
  ["hello", " "]
has type
  List String
but is expected to have type
  String
in the application
  String.append ["hello", " "]

String.append의 첫 번째 인자는 문자열이 와야 하는데, 대신 문자열 목록이 제공되었기 때문입니다.