함수형 언어와 타입 시스템에 관심 있는 개발자라면 ATS(Applied Type System)라는 이름을 한 번쯤 들어봤을 것이다. 공개된 입문서 'Introduction to Programming in ATS'는 이 언어의 핵심 기능을 한데 모아 소개하는 문서로, ATS가 어떤 지향을 가진 언어인지 비교적 선명하게 보여준다. 저자는 ATS를 '문법이 풍부하고(syntax-rich) 기능이 풍부한(feature-rich)' 언어라고 규정하는데, 이 두 표현은 칭찬인 동시에 경고로 읽힌다. 하나의 언어가 다루는 개념의 폭이 넓다는 것은 그만큼 학습 곡선이 가파르다는 뜻이기도 하기 때문이다.
입문서가 다루는 기능의 스펙트럼
이 책이 소개하겠다고 밝힌 주제의 목록만 봐도 ATS의 야심이 드러난다. 기초적인 함수형 프로그래밍에서 출발해, 단순 타입(simple types), 재귀적으로 정의되는 데이터타입(datatypes), 다형 타입(polymorphic types)으로 이어진다. 여기까지는 현대 함수형 언어를 접해본 사람에게 익숙한 영역이다. 그러나 목록은 여기서 멈추지 않고 의존 타입(dependent types), 선형 타입(linear types), 정리 증명(theorem-proving), 그리고 정리 증명을 활용한 프로그래밍(PwTP·programming with theorem-proving), 템플릿 기반 프로그래밍까지 뻗어간다. 하나의 입문서가 이만큼의 개념을 포괄하려 한다는 사실 자체가, ATS가 단일 패러다임의 언어가 아니라 여러 고급 타입 이론을 실제 코드로 녹여내려는 실험적 언어임을 말해준다.
이 개념들이 왜 중요한지는 각각이 해결하려는 문제를 보면 이해가 쉽다. 의존 타입은 타입이 값에 의존할 수 있게 하여, 예컨대 '길이가 n인 리스트'처럼 값의 성질을 타입 차원에서 명시하고 컴파일 단계에서 검증하도록 돕는 계열의 기법이다. 선형 타입은 자원이 정확히 한 번만 사용되도록 추적하는 방식으로, 메모리나 파일 핸들 같은 자원 관리를 타입 시스템에 맡긴다. 정리 증명과 PwTP는 프로그램의 성질을 수학적 증명 수준으로 보장하려는 접근이다. 즉 ATS는 '돌아가는 코드'를 넘어 '옳다는 것이 보장된 코드'를 겨냥한다.
실무자에게 주는 의미와 분명한 한계
한국의 IT 실무자 관점에서 이런 언어가 흥미로운 이유는, 최근 산업계가 안정성과 자원 안전성에 쏟는 관심의 방향과 맞닿아 있기 때문이다. 러스트가 소유권 모델로 메모리 안전성을 주류 개발 현장에 끌어들인 것처럼, ATS가 다루는 선형 타입과 의존 타입은 버그를 런타임이 아니라 컴파일 시점에, 혹은 설계 시점에 걸러내려는 같은 흐름 위에 있다. 서버 저수준 코드, 임베디드, 안전이 중요한 시스템을 다루는 엔지니어라면 이런 개념 자체를 익혀두는 것이 특정 언어 채택 여부와 무관하게 자산이 된다.
다만 저자 스스로 분명히 밝힌 한계를 가볍게 넘겨선 안 된다. 책은 독자가 프로그래밍 일반에 익숙하다고 전제하지는 않는다고 하면서도, 상당한 프로그래밍 경험이 없는 사람에게는 상당히 밀도가 높게 느껴질 것이라고 못 박는다. 이는 흔한 겸양이 아니라, 앞서 나열한 개념들을 한 권에 압축해 담은 구성의 필연적 귀결로 보는 편이 정확하다. 입문서라는 이름을 달고 있지만, 실제로는 함수형 프로그래밍과 타입 이론에 대한 기본기를 어느 정도 갖춘 독자를 위한 안내서에 가깝다.
결국 이 문서는 ATS를 당장 실무에 도입하라고 권하는 자료라기보다, 타입 시스템이 어디까지 프로그램의 정확성을 책임질 수 있는가를 탐색하는 하나의 참고 지점으로 받아들이는 편이 낫다. 문서는 개인적 용도의 인쇄만을 허용한다고 명시하고 있어 배포 시에는 라이선스 조건을 확인할 필요가 있다. 새로운 언어 하나를 당장 습득하기보다, 의존 타입과 선형 타입, 증명 기반 프로그래밍이라는 개념이 제시하는 문제의식을 자신의 현재 작업에 비춰보는 것이 이 입문서를 가장 실용적으로 읽는 방법일 것이다.