LiftIO 2022 오프닝 발표 | 기초 탄탄 함수형 프로그래밍

Published in

HappyProgrammer

12 min readDec 11, 2022

지난 12월 3일 토요일, 역삼동 마루180에서 두 번째 LiftIO 콘퍼런스가 열렸고, 전 작년에 이어 또 발표자로 나섰습니다. LiftIO는 함수형 프로그래밍 콘퍼런스로, 작년 첫회 때에는 온라인으로 진행했고, 약 150명의 참가자가 마지막까지 열띤 참여를 해주어 주최 측에게 큰 힘이 되었고, 올해에는 그 탄력을 이어받아 오프라인으로 진행했으며 약 90명이 참석하였습니다.

함수형 프로그래밍이라는 마이너한 주제로도 이렇게 많은 분들이, 황금 같은 주말 시간을 내어가며 발표하고, 자원봉사를 하고, 참석을 해주신다는 점이 놀라울 따름입니다.

이번에는 첫 번째 발표자로 나섰고, 약 20분의 짧은 시간 동안 발표를 할 수 있었는데요, 아쉽게도 좋은 호응을 받지는 못한 것 같습니다. 주제 욕심이 앞섰거나, 제 준비나 역량이 부족했거나, 아니면 그 모두 다에 해당한 것 같습니다. 많은 아쉬움은 남지만, 다음에 더 잘하기 위한 정리본을 공유합니다.

발표를 요약하면, 함수형 프로그래밍에서 추구하는 “참조 투명성”을 활용해서 등식 추론이 가능하다는 점을 보이고, 탄탄한 프로그래밍을 통해 두 다리 뻗고 편히 잘 수 있도록 하자는 주장이었습니다. 그러면, 전체 자료를, 간단한 설명과 함께 덧붙입니다. 아래에, 각각의 슬라이드에 요약 정리를 붙이는 형태로 정리하겠습니다.

기초 탄탄 함수형 프로그래밍

프로그래밍은 어떤 문제를 해결하기 위해, 개발자가 어떤 의도를 갖고, 프로그램 코드를 작성해서, 컴파일러나 인터프리터, VM 등이 해당 코드를 머신 코드로 변환해서 컴퓨터가 실행하게 하는 일입니다.

컴퓨터는 대단히 신속정확하고, 컴파일러나 인터프리터 등의 소프트웨어 제품의 완성도는 대단히 높으며, 상대적으로 우리가 일상적으로 작성하는 프로그램의 완성도는 낮습니다. 그럼 프로그램에서 문제가 될 만한 부분은, 대부분의 경우 우리가 작성하는 코드에 있습니다.

잘 작동할지 확신이 들지 않는 코드를 작성하고 나면, 불안해서 잠을 푹 잘 수가 없습니다.

그런 개발자의 불안을 해소할 수 있는 도구와 방법들로, 이런 것들이 있으며, 유닛 테스트를 가장 범용적으로 널리 권장하며, 실무에서도 많이 쓰고 있습니다. 아직 널리 쓰이지는 않는 것 같지만, 함수의 정의역을 다양하게 생성해서 자동으로 테스트를 진행해 주는 속성 기반 테스트도 있습니다. 속성 기반 테스트는 마침 오늘 마지막 세션에 발표해주시는 것 같습니다. 그 밖에도 또 하나의 불안 해소 방법이 있으니, 그게 오늘 말씀드릴 내용입니다.

영화 이미테이션 게임의 주인공, 알란 튜링을 아시나요? 현대의 명령형 프로그래밍의 기원은 튜링 머신이라고 볼 수 있고, 이 튜링 머신은 기본적으로 어떤 메모리 값을 읽어서 계산을 한 뒤, 다시 메모리에 값을 엎어 쓰는 방식으로 계산 과정을 진행합니다.

튜링에 조금 앞서, 알론조 처치가 “람다 칼큘러스”로 어떤 기계적인 계산을 할 수 있다는 이론을 발표했습니다. 함수형 프로그래밍 패러다임은, 람다 대수의 처리방식을 기반으로 하는데, 람다 대수는 어떤 변치 않는 x값을 받아서, 변치 않는 y값을 치환하는 과정을 반복해서 일을 처리합니다.

그 오래전에 튜링이, 이 둘이 할 수 있는 일(계산)이 서로 같다는 점을 설명해 주었고, 따라서, 오늘날 명령형 프로그래밍으로 할 수 있는 일과, 함수형 프로그래밍이 할 수 있는 일은 서로 같다고 볼 수 있겠습니다.

처리할 수 있는 일은 서로 같지만, 우리에게 중요한 차이점이 있으니, 튜링 머신은 기계로 구현하기가 좋고, 람다 대수는 사람이 이해하기 좋다는 특징이 있습니다.

한 가지 예를 들어보겠습니다. 드라마 우영우에서 나온 단어들처럼, 앞에서부터 읽어도 뒤에서부터 읽어도 같은 단어나 구를 팰린드롬이라고 합니다. 아래는 어떤 문자열이 팰린드롬인지 아닌지 확인하는 함수입니다. 명령형 사고로 처리한다면, 이런 식이겠지요. 어떤 문자열 인덱스 i, j를 두고, 반복문을 돌면서, 맨 앞 문자와 뒷 문자가 서로 같은지를 비교해 나가고, 중간지점까지 서로 같으면 참을 반환하는 식이죠.

같은 함수를, 함수형 스타일로 풀어본다면 이렇게 접근할 수 있습니다. 주어진 문자열 전체를 뒤집은 새 문자열을 구하고, 그 둘이 서로 같은지를 확인하면 됩니다. 저는 이 방식이 더 사람이 풀고자 하는 문제에 더 직결돼 이해하기 좋다고 생각하고, 이 점이 함수형 프로그래밍의 장점이라고 생각합니다.

어떤 스타일로 작성했든, 해당 함수가 잘 작동하는지, 단위 테스트로 확인을 해보고, 잘 작동하는지 안심하고 넘어갈 수 있습니다.

함수형 프로그래밍의 또 다른 강점을 소개하기 위해, 초등학교 시절 배웠던 산술 법칙을 떠올려 볼게요. 자연수 사칙 연산에 성립하는 규칙들을 나열했는데요, 이 중에서, 결합 법칙을 더 설명해 보겠습니다.

예를 들어, 우리가 1에서 12까지의 자연수를 모두 더하는 계산을 한다고 합시다. 이때 차례로 더하면, 총 11번을 더하게 되며, 한 번 더하는데 필요한 시간 t를 11번 곱해서, 11t만큼의 시간이 걸리겠습니다.

이를, 프로그램 코드로 작성해보면, 명령형 스타일로 구현하면, 반복문을 돌면서 누적 값을 증가하는 방식으로 풀 수 있고, 함수형 프로그래밍 언어들에서는 foldLeft 등의 함수를 써서 총합을 구할 수 있습니다.

하지만, 우리는 자연수의 덧셈에 대해 결합 법칙이 성립하기 때문에, 12까지 차례로 더한 결과와, 1부터 6까지 더한 다음, 7부터 12까지 더한 값을 마지막으로 한 번 더 해도, 그 결괏값이 같다는 걸 압니다.

더하는 횟수는 11회로 같지만, 앞 뒤를 나누어 여러 코어에 일을 나눠주면, 두 작업을 병렬로 처리할 수 있고, 결과적으로는 6t 만큼의 시간에 전체 작업을 완료할 수 있습니다.

다만, 이렇게, 한 머신 안에서 여러 코어에 일을 나누든, 아니면, 분산 컴퓨팅으로 여러 머신에 일을 나누든, 결합 법칙이 성립해야, 일을 나눠서 리듀스 작업을 할 수 있습니다.

앞서 보인 클로저 코드에서 사용한 fold라는 함수의 설명서입니다. 영문 텍스트에 있는 주요 문구를 추려보면, “잠재적으로 병렬 처리”, “여러 그룹으로 나눠서(기본 512개씩)”, “combinef는 결합 법칙이 성립해야”라는 문구가 눈에 띕니다. clojure에서는 fold 함수가 기본적으로 병렬 처리가 가능한 구조이고, 대신 우리 개발자가 결합 법칙이 성립하는 “결합(combinef)” 함수를 넘겨야 합니다. 그래야 병렬로 처리하든, 직렬로 처리하든 같은 결과를 얻을 수 있습니다.

이미, 초등학교 때 배운, 이 결합 법칙이 성립하는 연산과 그 도메인을 일컬어, 세미그룹(Semigroup)이라고 부릅니다. 여기에 항등원까지 포함하면 모노이드(Monoid)라고 부르는 용어가 있습니다. 즉, 우리가 병렬 처리를 하려면, 이 모노이드를 자주 활용하고 있는 셈입니다.

여기서 한 단계 더 나아가, 자연수 덧셈에 “교환 법칙”이 성립한다는 것도 알고 있으니, 같은 계산 작업을 이렇게 할 수도 있습니다. 맨 앞의 수와, 맨 뒤의 수를 쌍지어 보면, 각 쌍의 합이 13으로 같고, 그 13을 6번 더하면, 총합이 됩니다. 즉, 1부터 n까지의 총합을 일일이 더할 필요 없이, n(n+1)/2 라는 계산 식으로 얻을 수 있는 거죠. 그러면 병렬 처리를 할 필요도 없이, 덧셈 1회 + 곱셈 1회 + 나눗셈 1회로 전체 계산을 빠르게 끝낼 수 있습니다.

이 계산식이, 1부터 12까지의 총합뿐 아니라, 모든 자연수에 대해 참인지를 어떻게 보장할 수 있을까요? 혹시나 더 큰 자연수에 대해서는 틀리지 않을까 하는 불안을 없애냐는 말씀이죠.

고등학교 수학 시간에 배운 “수학적 귀납법”을 통해서, 이 식이 참이라고 증명할 수 있습니다.

최초 값에 대해 참이라는 걸 보이고, 어떤 n에 대해 성립하고 가정한 다음, 마지막으로 (n+1)에 대해서도 성립하는 걸 보이면, 도미노 효과로 모든 자연수에 대해 성립한다고 밝히게 되는 거죠.

P(1)은 1이라는 점은 명확하고, P(n+1)을 풀어보면, P(n) + (n+1)이라는 식을 유도해 낼 수 있습니다.

따라서, P(n+1)이 P(n)에 (n+1)을 더한 값인데, P(n)이 참이는 가정에 의해, p(n+1)까지도 참이 됩니다. 여기에 최초 값 1부터 차례로 다 참이 되어 모든 값이 참이 된다는 증명입니다.

이 얘기를 왜 한 거냐면, 참조 투명성을 활용해, 프로그램 코드에도 수학적 귀납법을 적용할 수 있기 때문입니다.

함수형 프로그램에서 추구하는 “참조 투명성”은 어떤 함수나 식이 그 값과 서로 같고, 상호 치환 가능하다는 성질입니다. 이 참조 투명성을 활용하면, 마치 수학적 귀납법으로 수식을 증명하듯, 프로그램 코드도 올바른지 증명할 수 있습니다.

예를 들어, 어떤 리스트의 원소 수가 몇 개 인지 구하는 함수를 작성해 볼게요. 리커전(재귀)로 구하는 함수입니다.

왼쪽 하스켈 코드를 이해하시기 좋게 오른쪽에 자바 코드로 번역해 두었습니다. 하스켈 코드를 눈여겨보면, 함수의 정의 부분과 계산 본문 사이에 등호(=)가 있는데요, 이게 일반적인 프로그래밍 언어의 시선으로만 보자면, 단순한 문법 같지만, 참조 투명한 함수의 관점에서 바라보면, 양측의 값이 서로 같다는 정의가 되기도 합니다.

그 둘을 서로 문제없이 치환 가능한 것이죠.

함수 하나를 더 만들어 보겠습니다. 똑같은 원소 x를 n개 만큼 담은 리스트를 만드는 replicate라는 함수입니다.

이 두 함수를 올바르게 작성했다면, replicate로 x를 n개 만큼 담은 리스트를 만들고, 그 리스트의 길이를 length로 구하면, 당연히 n이 나와야 합니다.

정말 그런지 확인해보죠.

먼저 P(0)에 대해 참인지 확인합니다. (replicate 0 x)는 replicate 함수 정의에 의해 []라는 빈 리스트 값으로 치환할 수 있습니다. 그러면 결국 전체 식이 length []가 되고, 이는 length 함수의 정의에 따라 0이 나옵니다. 그러면, P(0) = 0임을 쉽게 알 수 있습니다.

그다음 P(n)이 참이라고 가정합니다. 즉, length (replicate n x)가 n이 맞다고 가정하는 거죠.

마지막으로 P(n+1)을 참조 투명성을 활용해서 치환해나가면, 결국 n+1과 같은 값이라는 걸 알 수 있어서, 모든 음이 아닌 자연수 n에 대해 해당 length (replicate n a) = n임을 증명할 수 있는 거죠.

자연수에 대한 증명 뿐 아니라, 임의의 모든 리스트에 대해서도 어떤 명제가 참인지 아닌지 증명할 수 있습니다.

모든 리스트 [a]에 대해 어떤 명제가 참인지 증명하는 방법을 “구조적 귀납법”이라고 부릅니다. “수학적 귀납법”과 그 원리가 동일합니다.

예를 하나 더 들어보겠습니다. 리스트 xs와 리스트 ys를 차례로 잇는 함수 concat(++)을 작성했습니다. 하스켈에 익숙치 않으신 분은, 아래 자바로 번역한 코드를 참고해 주세요.

이 concat(++) 함수에 대해 “결합 법칙”이 성립할까요? 성립한다면, 모든 리스트에 대해 다 성립하는지 어떻게 확인하나요?

구조적 귀납법을 활용해서, 함수 정의를 치환해 나가면, 참이라는 걸 증명할 수 있습니다.

결국, 소프트웨어 시스템의 최종 보스는 “복잡성”인데, 이 복잡성을 다루기 위해, 현대의 프로그래밍 환경에서는 단위 테스트 수준에 머물러 있습니다만, 여기에 속성 기반 테스트나 오늘 설명드린 등식 추론까지 더한다면, 그 복잡성이라는 보스를 잡는 데에 큰 힘이 된다고 생각합니다.

사실 단위 테스트는 대단히 헐거운 형태의 증명입니다. 모든 경우까지는 아니더라도 일부의 경우에 대해 맞는지 틀리는지 확인하는 방법인 거죠. 그보다 더 촘촘한 확인법이 속성 기반 테스트인 거고, 논리적으로 맞는지 증명하는 방법이 등식 추론인 셈입니다.

모든 코드를 증명하면서 작성할 수는 없겠지만, 증명이 가능할 정도로 추론이 쉬운 “참조 투명성”을 활용하면, 부분 부분의 코드들부터 추론, 파악, 검증이 쉽다는 점을 말씀드리고 싶습니다. 꼭 증명까지는 아니더라도, 코드의 가독성부터 큰 차이가 나는 거죠.