Type-Driven Development with Idris 리뷰

2017-10-23

요약

Type-Driven Development with Idris에서는 타입을 중심으로 하는 소프트웨어 개발 방식을 소개합니다. 기존에는 타입이 데이터가 올바른지 확인하는 정도의 역할을 수행했지만 이 방식에서는 타입이 보다 많은 역할을 수행합니다. 예를 들면 함수 실행 전과 후의 상태를 타입을 사용해서 표현하거나 함수와 데이터가 준수해야하는 계약(contract)을 타입으로 정의할 수 있습니다. 이를 통해 프로그래머가 정한 계약이나 약속을 프로그램이 컴파일 타임에 준수하도록 강제하며, 소프트웨어가 올바르게 작성되었는지를 다른 소프트웨어 개발 방식보다 더 확실하게 보장해줄 수 있습니다.

이 책에서는 타입 주도 개발(TDD: Type-driven Development)을 이드리스(Idris) 프로그래밍 언어를 사용해서 소개합니다. 이드리스는 범용 순수 함수형 프로그래밍 언어로 이 책의 저자이기도 한 에드윈 브레이디(Edwin Brady)가 만들었습니다. 이드리스는 하스켈과 ML의 영향을 받은 언어로, TDD에 적합한 최신형 타입 시스템을 사용합니다. 이 책에서는 TDD와 함께 이드리스 언어의 기본도 배우게 됩니다.

대상 독자

소프트웨어가 올바르게 작성되었는지를 타입 시스템을 적극적으로 활용해서 확신하고 보장하는데 관심이 있으신 분들께 이 책을 추천합니다. 불변성, 클로저, 고차 함수 등 함수형 프로그래밍의 기본 개념에 익숙해야 하며, 하스켈, 오캐멀, 스칼라 등 다른 함수형 언어를 이미 알고 있다면 훨씬 수월하게 책을 읽을 수 있을 것입니다. 책 자체에서도 새로운 개념을 많이 소개하기 때문에 이를 배우는 와중에 펑터가 뭔지도 배워야하는 상황은 가급적 피하는 것이 좋다고 봅니다.

정적 타입 시스템에 관심이 없거나, 당장 실무에 적용할 수 있는 개념과 언어에만 관심이 있는 실용주의자라면 이 책은 잘 맞지 않을 것입니다. 또한 함수형 프로그래밍에 관해 상당히 많은 배경지식을 가지고 있다는 것을 전제로 하기 때문에 관련 경험이 별로 없으면 책이 너무 빠르게 진도를 나가는 것처럼 느껴질 수도 있습니다.

이 책만의 장점

일단 이 책에서 가장 마음에 드는 점은 저자가 TDD를 소개한다는 주 목적에 집중한다는 점입니다. 저자가 자신이 관심 있는 주제에 대해 책을 쓸 경우 책의 집필 목적에서 벗어나는 내용도 담겨 있는 경우가 자주 발생합니다. 하지만 이 책은 TDD를 소개한다는 목적에 충실한 구성을 갖추고 있어 모든 내용이 매끄럽게 이어집니다. 저자는 먼저 기본 개념을 소개하고 개발 환경을 설정한 뒤, TDD의 예시를 간단한 것부터 시작해서 점점 더 복잡한 것을 제시합니다. 마지막 다섯 챕터에서는 파일 IO나 동시성 프로그래밍 등 조금 더 실무에서 볼만한 예시를 제공합니다.

저자가 개념을 체계적으로 가르친다는 것도 마음에 드는데, 기술적인 주제를 다루는 사람 중에선 드문 경우입니다. 저자는 책의 도입부에 다음과 같은 표어를 TDD 개발 절차로 소개합니다. “타입, 정의, 개선: 타입을 적고, 해당 타입을 만족하는 함수를 구현하고, 문제를 더 잘 이해하게 될수록 타입 또는 정의를 계속 개선해나간다.” 책 전체에 걸쳐 이 과정을 적용하는데, 매번 조금씩 다른 상황에서 어떻게 응용해야 할지 보여줍니다. 이런 식으로 조금씩 다른 상황에서 같은 과정을 적용하는 방법을 반복하는 것은 매우 효과적인 교수법인데 저자는 이를 적극적으로 활용하고 있습니다.

또한 새로운 개념을 소개할 때에도 튜토리얼 형태로 설명하는데, 먼저 바탕이 되는 코드를 제공하고 여기에 “타입, 정의, 개선” 과정을 적용하는 것을 독자가 각 단계별로 따라하도록 시킵니다. 다음은 3장에 나온 간단한 예시입니다.

-- 예를 들어 XOR 연산자를 정의하려면 다음과 같은 단계를 거치면 됩니다.

-- 1. 타입 - 먼저 타입을 지정합니다.
xor : Bool -> Bool -> Bool

-- 2. 정의 - xor 위에 커서를 두고 Ctrl-Alt-A 를 눌러서 기본적인 정의를 추가합니다.
xor : Bool -> Bool -> Bool
xor x y = ?xor_rhs

-- 3. 정의 - x 위에서 Ctrl-Alt-C 를 눌러서 x의 두 가지 가능한 값을 기준으로 쪼갭니다.
xor : Bool -> Bool -> Bool
xor False y = ?xor_rhs_1
xor True y = ?xor_rhs_2

-- 4. 개선 - 우변을 채워넣어서 함수 정의를 완료합니다.
xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

마지막으로 각 장마다 적절한 연습문제가 제공됩니다. 새로 소개된 개념을 완전히 이해해야만 풀 수 있을 정도로 어려운 연습문제를 제공하는 책도 있지만, 이 책은 독자가 개념을 이해하도록 돕는 직관적이고 간단한 연습문제를 제공합니다. 책을 보면서 혼자 배우는 상황이라면 이런 연습문제가 더 낫다고 생각합니다.

타입 주도 개발 (TDD: Type-Driven Development)

함수형 프로그래밍 패러다임에서는 프로그램이란 데이터를 한 형태에서 다른 형태로 변환하는 과정이라고 봅니다. 이 때 데이터 형태나 구조는 타입으로 표현하고, 변환 과정은 입력값 및 결과값이 있는 함수로 표현합니다. TDD는 타입을 사용해서 프로그램의 전반적인 구성과 구조를 표현하는데 중점을 둡니다. 앞서 말했듯이 TDD의 핵심이 되는 개발 절차는 “타입, 정의, 개선”입니다.

그 이름에서 알 수 있듯이 TDD에서는 타입을 먼저 적습니다. 프로그램을 작성하려고 할 때에는 보통 머리 속에 대략적인 구조도를 그리고 있을 텐데, 타입을 사용해서 이를 명시적으로 표현합니다. 예를 들어 물질의 상태를 표현하려 한다고 합시다. 먼저 data Matter = Solid | Liquid | Gas 타입을 정의하고, 상태 변화를 phaseTransition : Matter -> Matter 함수로 표현할 수 있습니다.

기본이 되는 타입과 함수를 정의했으면 소프트웨어가 우리 머릿속 구조도를 더 정교하게 반영하도록 정의를 개선해나갑니다. 예를 들어 플라즈마 상태도 추가하려 한다고 해봅시다. 그러면 data Matter = Solid | Liquid | Gas | Plasma와 같이 타입을 개선합니다. 최종적으로 만족스러운 프로그램을 완성할 때까지 이 “타입, 정의, 개선” 과정을 반복합니다.

TDD는 완전히 새로운 개발 방식이라기보다는 하스켈 같은 정적 타입 함수형 언어를 사용하는 커뮤니티에서 자생적으로 나타난 소프트웨어 개발 방법론을 정리하고 다듬은 것이라고 생각합니다. 생각해보면 저도 하스켈 프로그램을 읽거나 작성할 때는 일단 정의된 타입과 함수의 타입 표기를 살펴보곤 합니다. TDD는 그런 접근법을 정리하고 발전시킨 방식이라고 봅니다.

이드리스(Idris) 언어

하지만 이 책에 소개된 TDD는 제가 하스켈을 배우면서 경험한 것보다 훨씬 강력한 형태인데, 이는 이드리스 특유의 기능 덕분입니다. 그 중 핵심적인 몇 가지를 살펴봅시다.

퍼스트 클래스 타입

이드리스는 퍼스트 클래스 타입을 지원하여 함수에 타입을 인자로 줄 수 있습니다. 퍼스트 클래스 함수가 처음 도입되었을 때의 패러다임 변화를 경험해보셨다면 퍼스트 클래스 타입도 그만큼 큰 변화를 의미한다는 것을 미루어 짐작할 수 있을 것입니다. 퍼스트 클래스 함수 때와 마찬가지로 퍼스트 클래스 타입을 사용하면 완전히 새로운 방식으로 코드를 작성할 수 있습니다.

퍼스트 클래스 타입의 간단한 예를 들자면 이드리스에서는 List 타입이 data List : (elem : Type) -> Type이라고 정의되어 있습니다. 이는 인터페이스 형식의 기능을 언어 차원에서 특별히 제공하는 것이 아니라, 타입을 인자로 받는 일반적인 타입입니다. 다만 이런 단순한 예시를 통해서 퍼스트 클래스 타입이 가지는 의미를 제대로 보여주기는 어렵습니다. 이드리스에서는 이 기능을 보통 디펜던트 타입과 함께 사용하므로 디펜던트 타입에 대해서 살펴보도록 합시다.

디펜던트 타입(Dependent Type)

디펜던트 타입이야말로 이드리스의 꽃이라 할 수 있는데, 다른 값을 바탕으로 연산되는 타입을 정의할 수 있도록 해줍니다. 개인적으로는 타입 수준에 정의된 함수라고 보는 편이 가장 이해하기 쉽다고 생각합니다.

예를 들어 Vector 4 String 타입이 있습니다. 이는 String 타입의 요소를 정확히 4개 가지고 있는 리스트의 타입입니다. 이 때 리스트의 길이로 다른 값을 넣으면 Vector 0 String, Vector 1 String, Vector 2 String 등등 비슷한 타입을 계속 만들어낼 수 있습니다. 이를 일반화하면 Vector n String 타입이라고 표현할 수 있는데, 이는 실질적으로 n이라는 값을 입력값으로 받아서 어떤 타입을 결과값으로 반환하는 함수입니다. 이 함수가 연산하는 결과값은 n의 값에 의존(dependent)하는 타입이기 때문에 이런 함수를 디펜던트 함수(dependent function)이라고 합니다. 그리고 이런 함수의 타입을 디펜던트 함수 타입(dependent function type), 혹은 줄여서 디펜던트 타입(dependent type)이라고 부릅니다.

디펜던트 타입을 사용하면 코드로 더 많은 것을 표현할 수 있고, 프로그램에 대한 정보를 타입 시스템에 더 많이 포함시킬 수 있는데, 두 가지 용례가 가장 흥미로웠습니다. 첫째, 기존에 런타임에만 확인 가능했던 데이터 관련 구체적인 정보를 컴파일 타임에 확인할 수 있게 됩니다. 예를 들어 Integer 타입은 해당 타입을 가지는 값이 정수라고만 알려줍니다. 하지만 그 값이 양수인지, 음수인지, 혹은 0인지는 런타임에만 확인 가능합니다. 디펜던트 타입을 사용하면 “3의 배수인 양수”나 “-50보다 크고 9953보다는 작은 홀수” 같이 더 정확한 타입을 정의할 수 있습니다. 앞서 Vect n String 타입에 대해 이야기했는데 이 타입도 “n개의 String 요소를 담은 리스트”를 나타낸다고 풀이할 수 있습니다. 타입 시스템에 담긴 이러한 정보를 컴파일 타임에 보장할 수 있기 때문에 예상 못한 값이 런타임에 나타나지 않을까 걱정하지 않아도 됩니다.

둘째, 올바른 프로그램의 정의를 타입 시스템에 포함시킬 수 있습니다. 은행 업무를 예로 들면 Withdrawl 디펜던트 타입을 정의하고, 출금할 액수 외에도 “올바른 인증 정보”와 “출금 요청액 이상의 잔고를 보유한 은행 계좌”라는 인자를 받도록 할 수 있습니다. 그러면 Withdrawl 타입을 제대로 정의했다면 Withdrawl 타입을 가진 모든 값은 항상 올바른 은행 업무를 나타낸다고 확신할 수 있게 됩니다.

이런 정보는 전통적으로 UML이나 소스 코드 내 주석 등 외부 문서, 혹은 더 끔찍한 경우엔 개발자의 머리 속에만 담겨있는 정보였습니다. 하지만 이드리스에서는 디펜던트 타입을 사용해서 이를 소스 코드에 직접 넣어서 컴파일러가 이 정보에 접근할 수 있고, 덕분에 프로그램의 정의와 구현체가 서로를 자동적으로 참조하도록 할 수 있습니다. 그러면 소프트웨어 사양이 바뀌는 즉시 이를 프로그램의 정의에 반영할 수 있고, 컴파일러는 새로운 정의를 바탕으로 프로그램이 올바르게 작성되었는지 다시 검사할 수 있습니다. 소스 코드와 문서를 번갈아가며 보면서 새로운 명세가 제대로 반영되었는지 수동적으로 확인할 필요가 없어진다는 말입니다.

책에서 저자는 디펜던트 타입의 용례를 몇 개 소개하는데, 여기서는 앞서 간단히 언급한 물질의 상태 변화 예시를 확장해보겠습니다. 디펜던트 타입 안에 상태 변화의 입력상태와 출력상태 정보를 포함시킨 예시를 봅시다.

data Matter = Solid | Liquid | Gas

data PhaseTransition : Type -> Matter -> Matter -> Type where
    Melt : PhaseTransition () Solid Liquid
    Vaporize : PhaseTransition () Liquid Gas
    Condense : PhaseTransition () Gas Liquid
    Freeze : PhaseTransition () Liquid Solid
    Sublime : PhaseTransition () Solid Gas
    Deposit : PhaseTransition () Gas Solid

    Pure : ty -> PhaseTransition ty state state
    (>>=) : PhaseTransition a state1 state2 ->
            (a -> PhaseTransition b state2 state3) ->
            PhaseTransition b state1 state3

PhaseTransition 디펜던트 타입은 물질의 상태 변화를 표현하며, 마지막 두 인자는 입력상태와 출력상태를 나타냅니다. 예를 들어 Melt 컨스트럭터를 사용해 만들어진 PhaseTransition 타입의 값은 Solid 입력 상태와 Liquid 출력 상태를 가져야만 합니다. 이를 사용해서 다음과 같이 연속적인 상태 변화를 표현할 수 있습니다.

vaporizeIce : PhaseTransition () Solid Gas
vaporizeIce = do Melt
                 Vaporize

vaporizeIceThenFreezeAgain : PhaseTransition () Solid Gas
vaporizeIceThenFreezeAgain = do Melt
                                Vaporize
                                Deposit

freezeSteam : PhaseTransition () Gas Solid
freezeSteam = do Freeze
                 Freeze

이 때 마지막 함수는 올바르지 않다는 것을 알 수 있습니다. 기체를 고체로 만들려면 일단 액화시키고 나서 고체화시켜야 하는데, freezeSteam 함수는 고체화 작업만 두 번 합니다. 무엇보다도 컴파일러도 freezeSteam에서 표현한 상태 변화가 올바르지 않다는 것을 인지하고 컴파일 타임에 오류를 표시하며, 이는 디펜던트 타입 덕분에 가능한 일입니다.

뛰어난 REPL

이드리스의 REPL은 매우 강력합니다. 앞서 제시했던 XOR 예시를 다시 살펴봅시다.

-- 예를 들어 XOR 연산자를 정의하려면 다음과 같은 단계를 거치면 됩니다.

-- 1. 타입 - 먼저 타입을 지정합니다.
xor : Bool -> Bool -> Bool

-- 2. 정의 - xor 위에 커서를 두고 Ctrl-Alt-A 를 눌러서 기본적인 정의를 추가합니다.
xor : Bool -> Bool -> Bool
xor x y = ?xor_rhs

-- 3. 정의 - x 위에서 Ctrl-Alt-C 를 눌러서 x의 두 가지 가능한 값을 기준으로 쪼갭니다.
xor : Bool -> Bool -> Bool
xor False y = ?xor_rhs_1
xor True y = ?xor_rhs_2

-- 4. 개선 - 우변을 채워넣어서 함수 정의를 완료합니다.
xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

여기서 ?xor_rhs, ?xor_rhs_1, ?xor_rhs_2 처럼 ?로 시작하는 것들은 구멍(hole)이라고 부릅니다. 아직 프로그램에서 완성되지 않은 부분을 대신하는 것인데, 이드리스 REPL에서는 이런 구멍을 다루는 명령을 많이 지원합니다. 위 코드에서 주석 부분에 나온 지시문에서는 자동으로 케이스 문을 만들거나, 해당 구멍이 어떤 타입을 가져야하는지 표시하는 등 기본적인 명령 몇 가지를 언급하고 있습니다. 지시문을 실제로 따르는 모습을 아래 gif에서 볼 수 있습니다. 이드리스 REPL은 번거롭게 하는 관리자라기보다는 꼼꼼한 조수와 같은 느낌을 주어 매우 사용하기 편합니다.

기타 상념

전반적으로 책을 읽으면서 많은 것을 배울 수 있었습니다. 워낙 독특한 개념을 많이 소개하고 있어서 제가 읽은 프로그래밍 언어 관련 서적 중에서는 가장 어려운 책이었습니다. 예를 들어 1 + k와 k + 1이 동일한 타입이라고 이드리스 컴파일러를 납득시켜야 타입 체크를 통과할 수 있다는 내용을 읽었을 때는 많이 당혹스러웠습니다. 다른 언어에서는 아직 한 번도 보지 못한 개념이었거든요.

이드리스는 기존 프로그래밍 모델의 근본적인 문제를 해결하려 하는 꽤나 미래지향적인 언어입니다. 하지만 언어로서는 마음에 들지만 주류 언어로 부상할 것 같지는 않습니다. 무엇보다도 하스켈보다도 더 많은 배경지식을 필요로 한다는 것이 걸립니다. 게다가 이드리스 타입 시스템은 일반적인 프로그램에 쓰기에는 너무 우수합니다. 주류 언어는 보통 “일단 돌아가기는 하면 되는” 언어인데 이드리스는 “정말 뛰어난” 언어를 추구하기 때문에 맞지 않습니다. 예를 들어 일반적인 쇼핑몰 재고 관리 소프트웨어에 쓰기에 이드리스는 좀 오버스펙이라고 봅니다. 또한 이드리스는 오히려 너무 표현력이 좋기 때문에 협업할 때 안 좋을 것 같다는 생각도 듭니다. 어떤 것을 표현하는 방법이 너무 많기 때문에 팀원들이 각자 자신만의 방식으로 프로그램을 작성할텐데 이는 협업에 악영향을 미칩니다. 구글이 계속되는 비판에도 불구하고 Go 언어를 단순하게 유지하는 것에도 다 이유가 있습니다.

하지만 그렇기 때문에 원자로 제어 시스템처럼 중요한 소프트웨어를 작성해야한다면 이드리스를 선택할 것입니다. 이드리스로 작성한 프로그램만큼 신뢰감이 가는 프로그램은 없을 것 같기 때문이죠.