type check는 왜 필요한가?

geeknews 보다가 재밌는 글 발견해서 요약

원글 링크

『프로그래밍 언어 속 타입』 책 소개 | GeekNews

불편하고 딱딱하기만 한 타입 검사는 왜 필요할까?

버그란 프로그램이 의도와 다르게 동작하는 경우를 뜻한다. 그렇다면 버그가 없는 프로그램을 만들어야 할 텐데 그건 불가능하다.

버그를 고치는 것도 어렵지만 찾는 게 더 어려울 때도 있다. 도대체 어디서 이 버그가 발생하는 거지? 찾지 못해서 고치지 못하는 버그도 많다.

그럼 어떻게 하면 버그를 잘 찾을 수 있나?

버그를 이해할 필요가 있다. 버그의 가장 흔한 원인 중 하나는 type error다. 타입 오류가 뭔가? 그걸 알려면 타입이 뭔지 먼저 답해야 한다.

타입은 프로그램에 존재하는 값을 그 종류에 따라 분류한 것이다. 값은 변수에 저장되거나 함수가 반환할 수 있는 true, 1, "string" 같은 것을 뜻한다.

프로그램에는 다양한 값이 존재하며, 제각각 다른 역할을 가지고 있으니 값을 분류하는 행위는 당연히 필요하다.

예를 들어 정수는 사칙연산에 사용할 수 있다. 문자열은 문자열 나름의 기능이 있다. 불리언도 마찬가지.

그러므로 정수는 정수라는 타입으로 묶고, 문자열은 문자열이라는 타입, 불리언은 불리언이라는 타입으로 묶는다.

만약 어떤 타입의 값을, 그 타입이 가지고 있지 않은 능력이 필요한 자리에 사용한다면 프로그램 실행에 문제가 생길 수 있다. "abc" * "b" 같은 상황을 떠올리면 된다. 이게 타입 오류의 한 예다.

타입의 능력을 벗어나는 일을 시키면 프로그램은 멈춘다.  이런 상황을 의도할 개발자는 없다. 그럼 이런 버그를 찾아서 잡기 가장 쉬운 방법은 무엇일까? 직접 실행해보는 것이다. 만약 타입 오류가 발생하면 프로그램이 실행 중에 오류 메시지를 뿜으며 종료될 것이다. 하지만 이 방법은 프로그램이 커질 수록 점점 더 불가능에 가까워진다. 어떻게 그 모든 기능을 테스트 해볼 수 있나?

그래서 사람들은 프로그램의 코드를 입력받아 프로그램이 타입 오류를 일으키는지 자동으로 판단해주는 프로그램인 type checker를 사용한다. 이상적인 타입 검사기는 주어진 프로그램이 타입 오류를 절대 일으키지 않는다면 통과시키고, 하나라도 타입 오류를 일으킨다면 통과시키지 않고 오류가 어디서, 왜 일어나는지 출력한다. 이건 실제 오류가 아니라 타입 오류로 인해 오류가 날 가능성이 있다는 경고다.

이런 타입 체커가 있다면 타입 오류를 걱정할 필요가 없다. 타입 체커가 타입 오류를 모두 검사해주니까. 하지만 그런 이상적인 타입 체커는 존재하지 않는다. 그런 타입 검사기를 만드는 것은 매우 어렵기 때문이 아니라 그것을 만들 수 없다는 사실을 이미 튜링이 1930년에 논리적으로 증명(halting problem)했다.

완전한 타입 체커는 불가능하지만, 그래도 설렁설렁하는 타입 체커는 가능하다. 프로그램이 타입 오류를 일으키는 경우의 수가 단 하나라도 있다면 '거부'라고 출력해야 한다. 이건 이상적 타입 체커와 같다. 대신 실제로 타입 오류가 없는데도 '거부'라고 출력하는 경우가 생긴다. 다시 말해 주어진 프로그램이 타입 오류를 절대로 일으키지 않는다면 통과하지만, 간혹 가다 거부라고 출력할 때도 있다는 것이다. 그러니까 조금 이상하게 동작할 가능성도 있는 타입 체커가 현실세계의 타입 체커다.

현실세계의 타입체커만 있어도 어쨌거나 타입 오류로부터 안전해지는 것이다. '타입 오류를 하나라도 일으킨다면 무조건 통과하지 못한다'는 성질이 타입 체커에 가장 중요한 성질이다.

그런데 문제가 없는데도 통과하지 못한다면? 이때는 언제 어디서 왜 일어났는지 타입 체커가 친절하게 알려주기 때문에 인간이 개입해서 판단해야 한다. 그리고 타입 체커가 알아차릴 수 있도록 약간의 수정이 필요하다.

이처럼 타입 검사는 버그를 자동으로 찾아준다는 가치를 가진다. 그 대가로 약간의 불편함을 감수해야 하긴 하지만, 그게 없어서 올 재앙보다 낫다. 버그는 타입 오류 뿐만 아니라 무수히 많고 그 중 하나인 타입 에러만 해결해도 큰 이득이다. 그래서 타입 검사가 우리에게 필요한 것.