프로그래밍 언어 '엘릭서' 1.20 공개...타입 표기 없이도 모든 코드 자동 검사해 '확정 버그' 잡아낸다...개발자가 따로 손댈 일 없이 오탐도 적어, 4년 연구의 첫 결실

[한국정보기술신문] 함수형 프로그래밍 언어 엘릭서(Elixir)가 코드에 별도의 타입 표시를 달지 않고도 프로그램 전체를 자동으로 검사해 오류를 찾아내는 기능을 갖췄다. 엘릭서 창시자 호세 발림(José Valim)은 6월 3일 공식 블로그를 통해 점진적 타입 시스템을 탑재한 새 버전 '엘릭서 1.20'을 공개했다. 발림은 이번 버전이 모든 엘릭서 프로그램에 대해 타입을 추론하고 점진적으로 검사하는 첫 개발 단계를 완료한 것이라고 설명했다.

엘릭서는 통신 시스템 등에 쓰이는 얼랭(Erlang) 가상머신 위에서 돌아가는 프로그래밍 언어로, 안정성과 동시 처리 능력이 강점으로 꼽힌다. 발림은 2022년 엘릭서에 '집합론적 타입(set-theoretic types)'을 도입하겠다고 예고했고, 2023년 관련 설계를 담은 논문을 발표하며 연구를 본격적인 개발 단계로 옮긴 바 있다. 이번 1.20 버전은 그 4년에 걸친 작업의 첫 결실에 해당한다.

프로그래밍에서 타입(type)은 어떤 값이 정수인지 문자열인지처럼 데이터의 종류를 가리킨다. 타입 검사는 코드가 종류에 맞지 않는 값을 다루지 않는지를 미리 점검하는 과정이다. 예를 들어 문자를 다루는 기능에 숫자를 잘못 넣으면 프로그램이 실행 도중 멈출 수 있는데, 타입 검사는 이런 문제를 코드를 실행하기 전에 잡아낸다.

타입을 다루는 방식은 크게 둘로 나뉜다. 코드를 실행하기 전에 타입을 엄격히 따지는 방식을 정적 타입, 실행하면서 그때그때 확인하는 방식을 동적 타입이라 부른다. 엘릭서는 본래 동적 타입 언어였다. 정적 타입은 오류를 일찍 발견할 수 있지만, 개발자가 값마다 종류를 일일이 적어 줘야 하는 번거로움이 따른다.

발림이 택한 방식은 이 둘을 절충한 '점진적 타입(gradual typing)'이다. 발림은 엘릭서 타입 시스템이 세 가지 목표를 지향한다고 밝혔다. 타입 시스템이 추론한 타입이 프로그램의 실제 동작과 어긋나지 않는 '건전성', 실행 중에 확인이 필요한 부분에는 dynamic 타입을 쓰되 그렇지 않으면 정적 타입처럼 작동하는 '점진성', 그리고 합집합·교집합·여집합 같은 기본적인 집합 연산으로 타입을 표현해 오류 메시지를 명확히 하는 '개발자 친화성'이다. 엘릭서의 타입 시스템을 집합론적 타입이라 부르는 것도 이 때문이다. 이는 여러 종류를 하나로 묶거나(합집합), 겹치는 부분만 추리거나(교집합), 특정 종류를 제외하는(여집합) 방식으로 데이터의 종류를 다룬다는 뜻이다.

점진적 타입의 핵심은 개발자가 타입을 직접 적어 넣지 않아도 시스템이 코드를 보고 타입을 스스로 추론한다는 점이다. 엘릭서는 이렇게 추론한 정보를 바탕으로 실행되지 않는 죽은 코드(dead code)와, 실행하면 반드시 실패하는 오류를 찾아낸다. 발림은 이런 오류를 '확정 버그(verified bug)'라고 이름 붙였다. 실행하면 틀림없이 문제를 일으키는, 의심의 여지가 없는 오류라는 의미다.

타입 시스템을 기존 언어에 새로 넣을 때 가장 큰 걸림돌은 '오탐(false positive)', 즉 멀쩡한 코드를 오류라고 잘못 지적하는 일이다. 발림은 엘릭서가 오탐을 너무 많이 내면 개발자가 타입 시스템을 신뢰하지 않게 된다고 보고, 이를 막는 데 공을 들였다고 밝혔다.

그 해법이 'dynamic(다이내믹)'이라는 특수한 타입이다. 다른 언어에도 'any(애니)'처럼 어떤 값이든 받아들이는 타입이 있지만, 이 경우 타입 검사가 사실상 무력화돼 오류를 거의 잡지 못한다. 엘릭서의 dynamic 타입은 두 가지 성질로 이와 차별화된다고 발림은 설명했다.

첫째는 '호환성'이다. 어떤 값이 dynamic 타입일 때, 엘릭서는 그 값이 들어갈 수 있는 종류와 실제로 요구되는 종류가 전혀 겹치지 않을 때에만 오류로 판정한다. 예컨대 어떤 값이 정수나 문자열 중 하나라면, 숫자만 받는 계산에 쓰여도 정수일 가능성이 있으므로 오류로 보지 않는다. 그러나 같은 값을 지도(map)라는 전혀 다른 구조에만 쓰는 기능에 넣으면, 정수도 문자열도 지도가 아니므로 곧바로 확정 버그로 잡힌다.

둘째는 '좁히기(narrowing)'다. dynamic 타입은 코드가 진행되면서 점차 더 구체적인 종류로 좁혀진다. 어떤 값에서 'a'와 'b'라는 항목을 꺼내 더하면, 엘릭서는 그 값이 a와 b를 숫자로 가진 지도라고 범위를 좁힌다. 이 덕분에 항목 하나를 빠뜨리고 값 전체를 숫자처럼 잘못 쓰면 오류로 걸러진다. 발림은 다른 점진적 타입 언어들이 dynamic 타입을 만나면 타입 정보를 모두 버리는 것과 달리, 엘릭서는 이를 일정한 범위로 유지하며 검사한다는 점을 차별점으로 들었다.

이번 작업의 상당 부분은 조건 분기 같은 다양한 코드 구조에 타입 검사와 좁히기를 적용하는 데 들어갔다. 엘릭서는 값의 종류나 크기를 확인하는 조건문을 해석해, 그 안에서 다룰 수 있는 값의 종류를 정확히 추론한다. 예를 들어 어떤 값이 특정 항목을 가진 지도라는 조건을 통과하면, 그 항목이 없을 때를 가정한 코드는 오류로 판정한다.

여러 갈래로 나뉘는 분기 처리에서도 앞선 갈래의 정보를 활용한다. 환경 변수를 읽어 값이 없으면(nil) 한 갈래로, 있으면 다른 갈래로 처리하는 코드에서, 첫 갈래가 '값 없음'을 걸러 냈으므로 두 번째 갈래의 값은 반드시 문자열이라고 시스템이 판단하는 식이다. 이런 방식은 불필요하게 중복된 분기나 죽은 코드를 찾아내는 데도 도움이 된다. 발림은 지도와 묶음(tuple) 등을 다루는 표준 기능 다수에도 타입을 부여했다고 밝혔다.

이번 검사 능력은 객관적 지표로도 확인됐다. 엘릭서는 타입 좁히기 성능을 재는 'If T 벤치마크'의 13개 항목 가운데 12개를 통과했다. 발림은 이 결과가 평범한 엘릭서 코드에서도 정확한 타입 정보를 끌어낼 수 있음을 보여 준다고 해석했다. 이 타입 시스템은 프랑스 국립과학연구센터(CNRS)와 기업 리모트(Remote)의 협력으로 개발됐으며, 현재 프레샤(Fresha)와 타이드웨이브(Tidewave)가 개발을 후원하고 있다.

엘릭서 1.20은 코드를 실행 가능한 형태로 바꾸는 컴파일 속도도 끌어올렸다. 특히 코어 수가 많은 컴퓨터에서 효과가 크다. 발림은 자체 비교 실험에서 엘릭서의 빌드 도구가 얼랭 가상머신 계열 언어 가운데 가장 빠른 것으로 나타났다고 밝혔다. 이번 버전에는 큰 프로젝트의 컴파일 시간을 줄일 수 있는 새 컴파일러 설정도 추가됐다.

발림은 다음 과제로 집합론적 타입을 활용한 '타입 표기(type signature)' 도입을 꼽았다. 다만 이는 아직 연구와 개발이 더 필요한 단계로, 현재 버전의 성능에 만족하고 재귀 타입과 매개변수 타입 등을 효율적으로 구현할 수 있을 때 비로소 도입하겠다는 신중한 입장을 밝혔다. 이 문제들이 풀리면 구조체에 타입을 지정하는 기능과 타입 표기를 차례로 검토할 계획이다. 발림은 사용자들이 1.20 버전을 써 보고 시스템이 무료로 찾아 주는 오류들을 고쳐 보기를 권했다.