1.1. Evaluating Expressions
Lean을 배우는 프로그래머가 이해해야 할 가장 중요한 것은 평가가 어떻게 작동하는지다.
평가는 산술에서 하듯 표현식의 값을 찾는 과정이다.
예를 들어 15 - 6의 값은 9이고 2 × (3 + 1)의 값은 8이다.
뒤 표현식의 값을 구하려면 먼저 3 + 1을 4로 바꾸어 2 × 4를 얻고, 이를 다시 8로 줄인다.
때로 수학 표현식에는 변수가 있다. x의 값이 무엇인지 알기 전에는 x + 1의 값을 계산할 수 없다.
Lean에서 프로그램은 무엇보다 표현식이며 계산은 표현식을 평가해 값을 찾는 것으로 생각하는 것이 기본이다.
대부분의 프로그래밍 언어는 명령형이며 프로그램은 결과를 얻기 위해 차례로 실행할 문장들의 시퀀스로 이루어진다. 프로그램은 가변 메모리에 접근하므로 변수가 가리키는 값이 시간에 따라 바뀔 수 있다. 가변 상태 외에도 파일 삭제, 외부 네트워크 연결, 예외를 던지거나 잡는 일, 데이터베이스에서 데이터를 읽는 일도 있다. “부수 효과”는 수학 표현식을 평가하는 모형을 따르지 않는 프로그램상의 일을 가리키는 포괄적인 용어다.
그러나 Lean의 프로그램은 수학 표현식과 같은 방식으로 작동한다.
변수에 값을 주면 다시 대입할 수 없고 표현식을 평가해도 부수 효과가 없다.
두 표현식의 값이 같다면 하나를 다른 것으로 바꾸어도 프로그램이 다른 결과를 계산하지 않는다.
그렇다고 Lean으로 콘솔에 Hello, world!를 쓸 수 없다는 뜻은 아니지만, 입출력은 Lean 사용 경험의 핵심이 아니다.
따라서 이 장에서는 Lean으로 표현식을 대화형으로 평가하는 방법에 집중하고 다음 장에서 Hello, world! 프로그램을 작성·컴파일·실행하는 방법을 설명한다.
Lean에 표현식을 평가하라고 하려면 편집기에서 표현식 앞에 #eval을 쓰면 결과를 알려 준다.
보통 #eval 위에 커서나 마우스 포인터를 두면 결과를 볼 수 있다.
예를 들면 다음과 같다.
#eval 1 + 2다음 값을 낸다.
일반적인 수학 표기와 대부분의 프로그래밍 언어는 함수 적용에 괄호(예: f(x))를 쓰지만 Lean은 함수와 인수를 나란히 쓴다(예: f x).
함수 적용은 가장 흔한 연산 중 하나이므로 간결하게 쓰는 것이 좋다.
다음처럼 쓰는 대신
#eval String.append("Hello, ", "Lean!")
"Hello, Lean!"을 계산하려면 대신 다음과 같이 쓴다.
#eval String.append "Hello, " "Lean!"여기서는 함수의 두 인수를 함수 옆에 공백으로 나란히 쓴다.
산술 연산 순서 규칙이 (1 + 2) * 5에 괄호를 요구하는 것처럼 함수 인수를 다른 함수 호출로 계산할 때도 괄호가 필요하다.
예를 들어 다음에는 괄호가 필요하다.
#eval String.append "great " (String.append "oak " "tree")
그렇지 않으면 두 번째 String.append가 "oak "과 "tree"를 인수로 받는 함수가 아니라 첫 번째 함수의 인수로 해석되기 때문이다.
먼저 안쪽 String.append 호출의 값을 구한 뒤 "great "에 이어 붙여 최종 값 "great oak tree"를 얻는다.
명령형 언어에는 보통 두 종류의 조건문이 있다. 불리언(Boolean) 값에 따라 실행할 명령을 정하는 조건 문장과, 불리언(Boolean) 값에 따라 평가할 두 표현식 중 하나를 정하는 조건 표현식이다.
예를 들어 C와 C++에서는 조건 문장을 if와 else로 쓰고 조건 표현식은 ?와 :로 조건과 분기를 나누는 삼항 연산자로 쓴다.
Python에서는 조건 문장이 if로 시작하고 조건 표현식은 가운데에 if를 둔다.
Lean은 표현식 중심의 함수형 언어이므로 조건 문장은 없고 조건 표현식만 있다.
조건 표현식은 if, then, else로 쓴다.
예를 들면 다음과 같다.
String.append "it is " (if 1 > 2 then "yes" else "no")다음과 같이 평가된다.
String.append "it is " (if false then "yes" else "no")다음과 같이 평가된다.
String.append "it is " "no"
마지막으로 "it is no"로 평가된다.
간결하게 하기 위해 이런 평가 단계의 시퀀스를 때때로 화살표로 연결해 쓴다.
String.append "it is " (if 1 > 2 then "yes" else "no")String.append "it is " (if false then "yes" else "no")String.append "it is " "no""it is no"1.1.1. Messages You May Meet
인수가 빠진 함수 적용을 평가하라고 Lean에 요청하면 오류 메시지가 나온다. 특히 다음 예제는
#eval String.append "it is "상당히 긴 오류 메시지가 나온다:
이 메시지는 인수 일부만 적용한 Lean 함수가 나머지 인수를 기다리는 새 함수를 반환하기 때문에 발생한다. Lean은 함수를 사용자에게 표시할 수 없으므로 표시하라는 요청을 받으면 오류를 반환한다.
1.1.2. Exercises
다음 표현식의 값은 무엇인가? 손으로 계산한 다음 Lean에 입력해 결과를 확인하라.
-
42 + 19 -
String.append "A" (String.append "B" "C") -
String.append (String.append "A" "B") "C"