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에 문자열의 리스트가 주어졌기 때문입니다.