AI가 짠 코드의 테스트코드를 AI한테 짜게하고 있으니 Who watches the watchman? 이 떠오르는 것이다.
notJoon
@joonnot@hackers.pub · 51 following · 63 followers
Uncertified Quasi-pseudo dev
Hackers' Pub에 글 올릴 때 도표를 Graphviz로 그리면 좋은 점: 도표 안의 글자도 함께 번역된다!
바이브 코딩
(이상한 생각 하지 마세욧)
Get back to work
My agent is coding
Hmm go ahead
xkcd.com/303/
notJoon shared the below article:
업자를 위한 아주 인포멀한 모나드 설명

lionhairdino @lionhairdino@hackers.pub
1.
함수형에선, 스트림 [1,2,3]
에
(+1)
을 map
해서 [2,3,4]
를 만들고,
(+2)
를 map
해서 [3,4,5]
를 만드는 작업을,
(+2) ∘ (+1)
를 [1,2,3]
에 map
하는 걸로 표현할 수 있어야 한다.
(+1)
, (+2)
, ((+2) ∘ (+1))
함수들은 모두 Int -> Int
함수를 원하는 곳에 넣어 줄 수 있는 함수들이다.
위와 같이, 완벽하게 정보를 유지하진 않지만, 같은 "류"의 작업을 두 번 하는 것을, 한 번 작업하는 것으로 표현할 수 있는 경우도 있다. 예를 들어,
첫 번째 작업으로, "hello"
를 로그로 남기고,
두 번째 작업으로, " world"
를 로그로 남기는데,
이를 한 번의 작업으로, "hello world"
를 로그로 남기는 작업으로 표현할 수 있다.
여기는 로그를 남기는 횟수 정보는 필요 없고, 최종 로그만 필요하다는 인위적 정보 선택이 들어가 있다. 이 인위적 선택(여기선 로그 문자열을 합치는 것)을 수긍해야만 가능하다.
로그를 남기는 작업을 m
이라 부를 때, m a
를 받는 곳에 m (m a)
를 넘길 방법이 생긴다는 뜻이다. 달리 말하면, m (m a)
로 표현되는 작업을 인위적인 절차를 거쳐 m a
로 만들어도, 내가 필요한 정보는 사라지지 않는다는 뜻이다.
2.
무언가가 하나인데, 유심히 보면 하나가 아닌 경우, 이게 바로 모노이드다. mono
는 하나를 뜻하고, ~oid
는 "척"하는 걸 말한다. (예. 인간인 척 하는 휴머노이드) 하나인척 하는 게 모노이드다. 수학 책 앞 부분에서 이항 연산, 결합 법칙, 항등원이 있으면 모노이드라는 설명을 하는데, 그래서 모노이드가 뭐에 쓰는 물건인지는 한참 공부해야 알 게 된다.
(아래는 혼자만의 생각입니다.)
모노이드를 바라 보는 눈 중 하나로, "모든 대상을 이항 연산으로 표현"을 들 수 있다.
0
을 포함한 자연수들 0,1,2,3,...
들은, +
이항 연산과, 이 연산의 항등원 0
이 있으면, 모두 ○ + ○
한 가지 모양으로 표현할 수 있게 된다.
0
-> 0+0
1
-> 0+1
2
-> 0+(1+1) = 1+1
...
모노이드 구조이기에, 어딘가에서 ○ + ○
모양을 원한다면, 0,1,2,3,...
을 모두 넣어 줄 수 있다.
3.
"어딘가에서 m a
를 원한다면, m a, m (m a), m (m (m a)), ...
를 모두 넣어 줄 수 있다."를 위와 비교하며 보자.
위에서 얘기한 인위적 선택 작업을 join
으로 표현하면,
m (m a)
--join--> m a
m (m (m a))
--join--> m (m a)
--join--> m a
...
m
반복 작업을 모두 ○ --join--> ○
모양으로 표현할 수 있을 것만 같다. 그런데, 딱 하나는 표현하지 못한다. join
은 m
이 두 개 있는 걸, 하나로 만드는 작업이라, m
하나를 ○ --join--> ○
로 표현하지 못한다. m
을 join
이 들어간 모양으로 표현하려면, 자연수, +
에서 처럼 0
에 대응하는 것이 필요하다. m
하나를, m
두 개로 만들되, 최종 결과에 영향을 미치지 않는 pure
라는 작업을 만든다. 위 로그 작업을 예로 들면, 로그로 빈문자 ""
을 추가하는 작업을 pure
로 만든다. 그러면 이제야 비로소, 모든 반복된 m 을 join으로 표현할 수 있게 된다
m a
--pure--> m (m a)
--join--> m a
m (m a)
--join--> m a
m (m (m a))
--join--> m (m a)
--join--> m a
...
이제, join
절차가 항상 있는 m a
를 원하는 곳에 m a
도 m (m (m a))
도 넣어 줄 수 있게 되었다.
"hello"와 " world"를 남기던 두 개의 작업 합쳐, "hello world"를 남기는 하나의 작업으로 표현할 수 있게 되었다.
※ 지금 눈에 명확히 보이진 않지만, m 둘을 합성하는 연산을 .
이라 하면, .
만으론 모노이드 이항 연산 역할을 못하지만, join
의 도움을 받고, id 만으론 항등원 역할을 못하지만, pure
의 도움을 받아 모노이드 구조를 이룬다.
결론.
당연히 모든 내용이 담겨 있진 않고, 모나드를 무엇의 모노이드로 보는 내용을 비수학적으로 풀어 봤다. 모노이드는 모두를 하나의 모양으로 표현 할 수 있다는 걸, 보증해주는 거대한 개념이지만, 업자인 나에겐 "그렇게 해도 된다"는 정도의 느낌만 있다. (결합 법칙이 빠졌는데, 나중에 코드를 모듈화 하는 것과 연관지어 보면, 명확한 대응을 알 수 있다.)
모나드는, 조금 다르게 생긴 것을, 당장 필요한 요소만 잘 관리한다면 "같은 걸로 치자"를 멋지게(,어렵게) 형식화한 이론이다.
사족.
저와 대화를 나눠본 분들은 아시겠지만, 제가 비전공자라 용어 선택이나 개념 정의가 매우 인포멀해서 인상을 찌푸리는 경우도 자주 만듭니다. PL 전공자분들처럼 깊숙히 이론을 파고 싶은 게 아니라, 현실에 적용할 수 있을 만큼의 눈만 가지고 싶습니다. 현실을 모델링할 때, "인위적 정보 선택"을 해서 필요한 정보를 남길 수 있는 경우를 알아채는 눈을 길러야 되는데, bind
또는 flatmap
, return
또는 pure
가 있는 구조가 모나드라고만 배우면, 이런 눈을 가지는데 매우 오래 걸리는 것 같습니다.
비전공 업자분이 보셨다면, 얻어 가시는 아이디어가 있었으면 좋겠고, 전공자분이 보셨다면, 인포멀한 부분에 너무 인상 찌푸리지 마시고, 틀린 개념이 있다면, 부드럽게 조언을 해주시면 좋겠습니다.
※ 모나드 용어는 mono
와 triad
에 온 게 아닐까 의심한다는 설이 있습니다.(검색해 보면 근거는 미약해 보입니다.) 모나드는 join
, return
그리고 위에서 명시적 언급은 안했지만, 펑터의 fmap
, 이렇게 세 개 triad의 도움을 받아 모노이드로 만들 수 있는 구조입니다.
※ "정교한" 내용이 아님을 강조하고 선입견이 생기지 않기 위해, 일부러 제목을 달지 않고, 반말(혼잣말)투로 썼습니다.
제목은
- 함수형
- 모노이드
- 모나드
순서 입니다.
@bglbgl gwyng 네 러스트로 구현 중이에요
@joonnotnotJoon 약간 초치는거 같아서 죄송한데, 파싱 후에도 AST가지고 해야할 잡다구리한 일들이 있단 말이죠. 대표적으로 포매터? 본격적으로 언어를 위한 툴링을 만들려면 그런것들을 만들어야하는데, space/comment preserving을 지원하도록 업그레이드하는게 필요이상으로 고단할수 있습니다. 그래서 파서 컴비네이터 자체가 아니라 언어 개발이 목적이라면 type_sitter 요런걸 고려해보시는걸 추천드립니다. 제가 Rust를 할줄 몰라서 저걸 못썼는데 늘 부러웠어요.
러스트가 어렵다는 이야기에는 러스트의 특징을 이질적으로 느끼는 경우가 많아서도 있겠지만…어렵다는 말의 재생산이 어렵다는 이미지를 더 굳히는 것 같기도 합니다. 일종의 악순환이라고도 생각하는 게…어렵다는 이미지를 가지고 보면 개념 익히는 것도 어렵고 컴파일 에러를 해결하는 과정도 좀 더 고되게 느낄 수 있거든요. 러스트에 대한 이미지를 어렵다고 생각할수록, 갖고있는 배경지식이 러스트와 이질적일수록 어렵다고 느끼는 사람들이 많은듯합니다
notJoon shared the below article:
논리적이 되는 두 가지 방법 - 논리와 저수준(Low-level) 자료 표현(Data representation) (2 편 중 1 편)

Ailrun (UTC-5/-4) @ailrun@hackers.pub
이 글은 어떤 문장이 "논리적"이라고 할 수 있는지에 대한 심도 있는 탐구를 시작합니다. 일상적인 오용을 지적하며, 진정으로 논리적인 주장은 증명 가능성과 체계의 무모순성이라는 두 가지 핵심 조건을 충족해야 한다고 주장합니다. 특히, "좋은 가정 아래" 논리성을 증명하는 두 가지 방법, 즉 함수형 언어와 유사한 구조를 가진 자연 연역과, 약간의 "부정행위"를 통해 무모순성을 쉽게 보일 수 있는 논건 대수를 소개합니다. 글에서는 명제와 판단의 개념을 명확히 정의하고, 자연 연역을 통해 논리적 증명을 구축하는 방법을 상세히 설명합니다. 특히, 자연 연역과 함수형 언어 간의 놀라운 유사성, 즉 커리-하워드 대응을 통해 논리적 사고와 프로그래밍 언어 이해 사이의 연결고리를 제시합니다. 또한, 자연 연역의 한계를 극복하고 무모순성을 보다 쉽게 증명할 수 있는 논건 대수를 소개하며, 자연 연역과의 구조적 차이점을 강조합니다. 이 글은 논리적 사고의 깊이를 더하고, 프로그래밍 언어와 논리 간의 관계에 대한 흥미로운 통찰을 제공합니다. 특히, 커리-하워드 대응을 통해 논리와 프로그래밍이 어떻게 연결되는지 이해하고 싶은 독자에게 유익할 것입니다.
Read more →- Zig 라이브러리 짜기
- 이력서 쓰기
Excited to share that we just released ESMeta v0.6.0! Here's two new features that we're really excited about in this release. Since this is my personal account, I won't be introducing the entire toolchain, but if you're curious, check out on https://github.com/es-meta/esmeta/ (1/n)
Show GN: 나만의 연합우주(fediverse) 마이크로블로그 만들기
------------------------------
이 튜토리얼은 [Fedify] 라이브러리를 사용하여 [ActivityPub] 프로토콜 기반의 마이크로블로그 서비스를 구현하는 방법을 설명합니다. ActivityPub은 다양한 소셜 네트워크 서비스들이 서로 연동될 수 있게 해주는 분산형 소셜 네트워킹 프로토콜로, 이를 통해 [Mastodon], [Misskey] 같은 서비스와 상호작용할 수 있는 독…
------------------------------
https://news.hada.io/topic?id=20508&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
인간이 코딩을 얼마나 못하냐면, chatGPT :: String -> String
이 현존하는 가장 비싼 프로그램이다
터미널에 대해 궁금한 점이 생겨 자료를 찾다 보니 Windows Console Team에서 연재한 시리즈물을 발견했는데, 그 내용이 참 유익했다.
Windows Command-Line Series:
- Backgrounder
- The Evolution of the Windows Command-Line
- Inside the Windows Console
- Introducing the Windows Pseudo Console (ConPTY)
- Unicode and UTF-8 Output Text Buffer
콘솔 앱이 터미널과 입출력을 주고 받는 것을 공기처럼 당연하다고 생각했는데, 그 과정에는 커서 이동이나 개행 등과 같은 제어 문자를 렌더링하거나 SIGINT 같은 시그널을 발생시켜주는 처리가 존재했다. 터미널과 콘솔 앱이 서로 분리된 구조가 과거 물리 터미널로부터 비롯된 것도 흥미로웠고 말이다. 사실 이해 못 한 부분이 아직 많아서 다음에 또 읽어볼 생각이다.
와, 이거 진짜 짱이다 cc @joonnotnotJoon
notJoon shared the below article:
웹 접근성이 UI 설계에 중요한 이유
김무훈 @iamuhun@hackers.pub
웹 접근성의 중요성과 WAI-ARIA 표준을 바탕으로 한 의미론적인 UI를 설계한 사례를 블로그에 공개했습니다.
전문성 검증이 필요한 분야이다 보니, 퇴고 과정에 접근성 전문가 @resistan 님의 도움을 받았습니다.
확실히 문서에 잘 정리해놓으니까 AI랑 협업하기가 수월한 것 같음. 개인 프로젝트에도 잘 해놓으면 아주 좋겠구먼
@joonnotnotJoon CONTRIBUTING.md 파일 하나 잘 작성해 두면 사람이랑 협업할 때 뿐만 아니라 LLM이랑 협업할 때도 도움이 많이 되더라고요. Hackers' Pub도 하나 마련해 뒀어요.
확실히 문서에 잘 정리해놓으니까 AI랑 협업하기가 수월한 것 같음. 개인 프로젝트에도 잘 해놓으면 아주 좋겠구먼
...구글은 사업 접어라
notJoon shared the below article:
함수형 언어의 평가와 선택

Ailrun (UTC-5/-4) @ailrun@hackers.pub
함수형 언어(Functional Language)의 핵심
함수형 언어가 점점 많은 매체에 노출되고, 더 많은 언어들이 함수형 언어의 특징을 하나 둘 받아들이고 있다. 함수형 언어, 적어도 그 특징이 점점 대세가 되고 있다는 이야기이다. 하지만, 함수형 언어가 대체 무엇이란 말인가? 무엇인지도 모르는 것이 대세가 된다고 할 수는 없지 않은가?
함수형 언어란 아주 단순히 말해서 함수가 표현식[1]인 언어를 말한다. 다른 말로는 함수가 값이기 때문에 다른 함수를 호출해서 함수를 얻어내거나 함수의 인자로 함수를 넘길 수 있는 언어를 말한다. 그렇다면 이 단순화된 핵심만을 포함하는 언어로 함수형 언어의 핵심을 이해할 수 있지 않을까? 이게 바로 람다 대수(Lambda Calculus)의 역할이다.[2]
람다 대수는 딱 세 종류의 표현식만을 가지고 있다.
- 변수 (xx, yy, …\ldots)
- 매개변수 xx에 인자를 받아 한 표현식 MM(함수의 몸체)을 계산하는 함수 (λx→M\lambda x\to M)
- 어떤 표현식 LL의 결과 함수를 인자 NN으로 호출 (L NL\ N)
이후의 설명에서는 MM 과 NN, 그리고 LL이라는 이름을 임의의 표현식을 나타내기 위해 사용할 것이다. 람다 대수가 어떤 것들을 표현할 수 있는가? 앞에서 말했듯이 람다 대수는 함수의 인자와 함수 호출의 결과가 모두 함수인 표현식을 포함한다. 예를 들어 λx→(λy→y)\lambda x \to (\lambda y \to y) 는 매개변수 xx에 인자를 받아 함수 λy→y\lambda y \to y를 되돌려주는 함수이고, λx→(x (λy→y))\lambda x \to (x\ (\lambda y \to y))는 매개변수 xx에 함수인 인자를 받아 그 함수를 (λy→y\lambda y \to y를 인자로 사용하여) 호출하는 함수이다.
람다 대수(Lambda Calculus)의 평가(Evaluation)
이제 문제는
그래서 람다 대수의 표현식이 하는 일이 뭔데?
이다. 위의 표현식에 대한 소개는 산수로 말하자면 x+yx + y와 같이 연산자(++)와 연산항(xx와 yy)로부터 얻어지는 문법만을 설명하고 있고, 3+53 + 5와 같은 구체적인 표현식을 계산해서 88이라는 결과 값을 내놓는 방식을 설명하고 있지 않다. 이런 표현식으로부터 값을 얻어내는 것을 언어의 "평가 절차"("Evaluation Procedure")라고 한다. 람다 대수의 평가 절차를 설명하는 것은 어렵지 않다. 적어도 표면적으로는 말이다.
- 함수는 이미 값이다.
- 함수 λx→M\lambda x \to M을 NN으로 호출하면 MM에 등장하는 모든 xx을 NN으로 치환(Substitute)하고 결과 표현식의 평가를 계속한다.
이는 겉으로 보기에는 말이 되는 설명처럼 보인다. 하지만 이 설명을 실제로 해석기(Interpreter)로 구현하려고 시도한다면 이 설명이 사실 여러 세부사항을 무시하고 있다는 점을 깨닫게 될 것이다.
- 함수 호출 L NL\ N에서 LL이 (아직) λx→M\lambda x \to M 꼴이 아닐 때는 어떻게 해야하지?
- 함수 호출 (λx→M) N(\lambda x \to M)\ N에서 NN을 먼저 평가하는 게 낫지 않나? xx가 MM에 여러번 등장한다면 NN을 여러번 평가해야 할텐데?
첫번째 문제는 비교적 간단히 해결할 수 있다. LL을 먼저 평가해서 λx→M\lambda x \to M 꼴의 결과 값을 얻어낸 뒤에 호출을 실행하면 되기 때문이다. 반면에 두번째 질문은 좀 더 미묘한 문제를 가지고 있다. 함수 호출의 평가에서 발생하는 이 문제에 구체적인 답을 하기 위해서는 값에 의한 호출(Call-By-Value, CBV)와 이름에 의한 호출(Call-By-Name, CBN)이 무엇인지 이해해야 한다.
값에 의한 호출(Call-By-Value)? 이름에 의한 호출(Call-By-Name)?
앞에서 말한 함수 호출에서부터 발생하는 문제는 사실 함수형 언어에서만 발생하는 문제는 아니다. C와 같은 명령형 언어에서도 함수를 호출할 때 인자를 먼저 평가해야하는지를 결정해야하기 때문이다. 즉 이 문제는 함수를 가지고 있고 함수를 호출해야하는 모든 언어들이 가지고 있는 문제이다.
그렇다면 이 일반적인 문제를 어떻게 해결하는가? 대부분의 언어가 취하는 가장 대표적인 방식은 "값에 의한 호출"("Call-By-Value", "CBV")이라고 한다. 이 함수 호출 평가 절차에서는 함수의 몸체에 인자를 치환하기 전에[3] 인자를 먼저 평가한다. 이 방식을 사용하면 인자를 여러번 평가해야하는 상황을 피할 수 있다.
또 다른 방식은 "이름에 의한 호출"("Call-By-Name", "CBN")이라고 한다. 이 방식에서는 함수의 몸체에 인자를 우선 치환한 후 몸체를 평가한다. 몇몇 언어의 매크로(Macro)와 같은 기능이 이 방식을 사용한다. 얼핏 보기에는 CBN은 장점이 없어보인다. 그러나 함수가 인자를 사용하지 않을 경우는 CBN이 장점을 가진다는 것을 볼 수 있다. 극단적으로 평가가 종료되지 않는 표현식(Non-terminating expression)이 있다면[4] CBV는 종료하지 않고 CBN만이 종료하는 경우가 있음을 다음 예시를 통해 살펴보자. 표현식 (λx→(λy→y)) N(\lambda x \to (\lambda y \to y))\ N이 있다고 할 때, NN이 평가가 종료되지 않는 표현식이라고 하자. 이 경우 CBV를 따른다면 종료하지 않는 NN 평가를 먼저 수행하느라 이 표현식의 값을 얻어낼 수 없지만, CBN을 따른다면 λy→y\lambda y \to y라는 값을 손쉽게 얻어낼 수 있다. 바로 이런 상황 때문에
CBN은 CBV보다 일반적으로 더 많은 표현식들을 평가할 수 있다
고 말한다.
모호한 선택을 피하는 방법
두 방식의 장점을 모두 가질 수는 없을까? 다시 말해서, 어떤 상황에서는 이름에 의한 호출을 사용하고, 어떤 상황에서는 값에 의한 호출을 사용할 수 없을까? 이 질문에 답한 수많은 선구자들 가운데 폴 블레인 레비(Paul Blain Levy)가 내놓은 답인 "값 밀기에 의한 호출"("Call-By-Push-Value", "CBPV")은 함수형 언어의 평가를 기계 수준(Machine level)에서 이해하는데에 있어 강력한 도구를 제공한다. CBPV는 우선 "계산"("Computation")과 "값"("Value")을 구분한다.
- 계산 MM, NN, LL, …\ldots = 함수 λx→M\lambda x \to M 또는 함수 호출 L VL\ V
- 값 VV, UU, WW, …\ldots = 변수 xx
잠깐, 앞서서 함수형 언어에서 함수는 값이라고 하지 않았던가? 이는 값 밀기에 의한 호출에서 함수와 함수 호출을 종전과 전혀 다르게 이해하기 때문이다. 함수 λx→M\lambda x \to M는 스택(Stack)에서 값을 빼내어(Pop) xx라는 이름을 붙인 후 MM을 평가하는 것이고, 함수 호출 L VL\ V는 스택에 값 VV를 밀어넣고(Push)[5] LL을 평가하는 것이다. 따라서 함수 λx→M\lambda x \to M는 평가의 결과가 아닌 추가적인 평가가 가능한 표현식이 된다. 이 구분을 간결하게 설명하는 것이 다음의 CBPV 표어이다.
값은 "~인 것"이다. 계산은 "~하는 것"이다.
그렇지만 함수형 언어이기 위해서는 함수를 값으로 취급할 수 있어야 한다고 했지 않은가? 그렇다. 이를 위해 CBPV는
계산을 강제한다면(force\mathbf{force}) 계산 MM를 하는 지연된 계산인 값 thunk(M)\mathbf{thunk}(M)
을 추가로 제공한다. 이 둘 (force(V)\mathbf{force}(V)와 thunk(M)\mathbf{thunk}(M))을 다음과 같이 문법에 추가할 수 있다.
- 계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V)
- 값 = xx 또는 thunk(M)\mathbf{thunk}(M)
CBPV를 완성하기 위해 필요한 마지막 조각은 계산을 끝내는 법이다. 현재까지 설명한 λx→M\lambda x \to M와 L VL\ V 그리고 force(V)\mathbf{force}(V) 는 모두 다음 계산을 이어서 하는 표현식이고, 계산을 끝내는 방법을 제공하지는 않는다. 예를 들어 λx→M\lambda x \to M의 평가는 스택에서 값을 빼내고 계산 MM의 평가를 이어한다. 그렇다면 계산의 끝은 무엇인가? 결과 값을 제공하는 것이다. 이를 위해 return(V)\mathbf{return}(V)를 계산에 추가하고, 이 결과 값을 사용할 수 있도록 M to x→NM\ \mathbf{to}\ x \to N (계산 MM을 평가한 결과 값을 xx라고 할 때 계산 NN을 평가하는 계산) 또한 계산에 추가하면 다음의 완성된 CBPV를 얻는다.
- 계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V) 또는 return(V)\mathbf{return}(V) 또는 M to x→NM\ \mathtt{\mathbf{to}}\ x \to N
- 값 = xx 또는 thunk(M)\mathbf{thunk}(M)
이제 CBPV를 얻었으니 원래의 목표로 돌아가보자. 어떻게 CBV 호출과 CBN 호출을 CBPV로 설명할 수 있을까?
- CBV 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를 return(thunk(λx→M))\mathbf{return}{(\mathbf{thunk}(\lambda x \to M))}과 L to x→N to y→force(x) yL\ \mathbf{to}\ x \to N\ \mathbf{to}\ y \to \mathbf{force}(x)\ y로 표현할 수 있다. 즉, CBPV의 관점에서 CBV의 함수는 지연된 원래 계산 λx→M\lambda x \to M을 값으로 되돌려주는 계산으로 이해할 수 있고, 함수 호출 L NL\ N은 함수 부분 LL을 먼저 평가하고 NN을 평가한 뒤 NN의 계산 결과 yy를 스택에 밀어넣고 지연된 계산인 함수 부분 xx의 계산을 강제하는(force(x)\mathbf{force}(x)) 것으로 이해할 수 있다.
- CBN 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를 λx→M\lambda x \to M(단, 변수 xx의 모든 사용을 force(x)\mathbf{force}(x)로 치환함)과 L thunk(N)L\ \mathbf{thunk}(N)로 표현할 수 있다. 즉, CBPV의 관점에서 함수 호출은 L NL\ N은 지연된 NN을 스택에 밀어넣은 뒤 LL의 계산을 이어가는 것으로 볼 수 있다. 이 지연된 NN은 이후에 스택에서 빼내어져 어떤 이름 xx가 붙은 뒤, 이 변수가 사용될 때에야 비로소 계산된다.
다소 설명이 복잡할 수 있으나, 단순하게 말해서 CBPV는 CBV에 따른 상세한 평가 순서와 CBN 따른 상세한 평가 순서를 세부적으로 설명할 수 있는 충분한 기능을 모두 갖추고 있으며, 이를 통해 CBV 함수 호출과 CBN 함수 호출을 모두 설명할 수 있다는 이야기이다.
기계 수준(Machine level)에서의 Call-By-Push-Value의 장점
앞에서는 CBPV가 CBV와 CBN를 모두 설명할 수 있음을 다뤘다. 그러나 CBPV는 프로그래머(Programmer)가 직접 사용하기에는 과도하게 자세한 세부사항들을 포함하고 있기에, 프로그래머가 직접 CBPV를 써서 CBV와 CBN의 구분을 조율하기에는 적합하지 않다. 그렇다면 어느 수준에서 CBV와 CBN을 혼합해 사용할 때 도움을 줄 수 있을까? 바로 람다 대수를 기계 수준으로 컴파일(Compile)할 때이다. 이때는 CBPV가 가진 자세한 세부사항의 표현력이 굉장히 유용해진다.
예를 들어 람다 대수를 기계 수준으로 변환할 때 흔히 필요한 것 중 하나인 항수 분석(Arity analysis)에 대해 이야기해보자. 항수 분석은 함수가 하나의 인자를 받은 뒤 실행되어야 하는지, 혹은 두 인자를 모두 받아 실행되어야 하는지 등을 확인하여 이후에 그에 걸맞는 최적화된 기계어(Machine language)를 생성할 수 있게 도와주는 분석 작업이다. 평범한 람다 대수에서는 항수 분석의 결과를 직접적으로 표현하기 어렵다. 예를 들어 람다 대수의 λx→(λy→y)\lambda x \to (\lambda y \to y)의 경우 이 함수가 xx와 yy를 모두 받아 yy를 되돌려주는 함수인지 (항수가 2인 함수인지), 혹은 xx를 받아 λy→y\lambda y \to y라는 함수를 되돌려주는 함수인지 (항수가 1인 함수인지) 구분할 수 없다. 그러나 이를 CBPV로 변환한 λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))나 λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는 각각이 무엇을 뜻하는지 분명히 이해할 수 있다.
- λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))는 두 변수 xx와 yy를 스택에서 빼낸 뒤 yy의 값을 되돌려주는 함수(항수가 2인 함수)이다.
- λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는 변수 xx를 스택에서 빼낸 뒤 지연된 계산 λy→return(y)\lambda y \to \mathtt{return}(y)를 돌려주는 함수(항수가 1인 함수)이다.
이런 장점을 바탕으로 CBPV를 더 발전시킨 "언박싱한 값에 의한 호출"("Call-By-Unboxed-Value")을 GHC 컴파일러의 중간 언어(Intermediate language)로 구현하는 것에 대한 논의가 현재 진행되고 있으며 앞으로 더 많은 함수형 컴파일러들이 관련된 중간 언어를 채용하기 시작할 것으로 보인다.
마치며
이 글에서는 함수형 언어의 핵인 람다 대수를 간단히 설명하고 람다 대수를 평가하는 방법에 대해서 다루어보았다. 특히 그 중 값 밀기에 의한 평가(Call-By-Push-Value, CBPV)가 무엇이며 CBPV가 다른 대표적인 두 방법(CBV, CBN)을 어떻게 표현할 수 있는지, 그리고 CBPV의 장점이 무엇인지에 대해서도 다루어 보았다. 이 글에서 미처 다루지 못한 중요한 주제는 CBPV를 기계에 가까운 언어로 번역해보는 것이다. 여기에서는 글이 너무 복잡해지는 것을 피하기 위해 제했으나, CBPV의 장점에서 살펴봤듯 이는 CBPV에 있어 핵심 주제 중 하나이기 때문에 이후에 다른 글을 통해서라도 이 주제를 소개할 기회를 가지고자 한다. 이 글이 CBPV에 대한 친절한 소개글이었기를 바라며 이만 줄이도록 하겠다.
결과 값(Value)을 가지는 언어 표현을 말한다. 예를 들어 1+11 + 1은 22라는 값을 가지는 표현식이지만 (JavaScript의)
let x = 3;
나 (Python의)def f(): ...
은 그 자체로는 값이 없기 때문에 표현식이 아니다. ↩︎다만 실제 역사에서는 람다 대수의 이해와 발견이 함수형 언어의 개발보다 먼저 이루어졌다. 이런 역사적 관점에서는 (이미 많은 수학자들이 이해하고 있던) 람다 대수에 여러 기능을 추가한 것이 바로 함수형 언어라고 볼 수 있다. ↩︎
프로그래밍 언어(Programming Language)는 실제로는 치환을 사용하지 않고 환경(Environment)을 사용하는 경우가 더 많지만 설명의 편의를 위해 다른 언어들 또한 환경 대신 치환에 기반해 평가한다고 가정하겠다. ↩︎
앞서 설명한 람다 대수에서는 이를 쉽게 얻을 수 있다. 오메가(Ω\Omega)라고 부르는 표현식인 (λx→x x) (λx→x x)(\lambda x \to x\ x)\ (\lambda x \to x\ x)의 평가는 값에 의한 호출을 따르든 이름에 의한 호출을 따르든 종료되지 않는다. ↩︎
바로 이 함수 호출을 값 밀기에 기반해 해석하는 데에서 CBPV의 이름이 유래했다. ↩︎
2025年 오픈소스 컨트리뷰션 아카데미 參與型 멘토團 募集 公告가 떴다. Fedify 프로젝트의 메인테이너로서 멘토團에 志願하고자 한다. 志願書가 .hwp 파일이기에 큰 맘 먹고 한컴오피스 한글 for Mac도 購入했다. (아무래도 앞으로 .hwp 파일 다룰 일이 많을 것 같다는 豫感이 들어서…)
notJoon shared the below article:
같은 것을 알아내는 방법

Ailrun (UTC-5/-4) @ailrun@hackers.pub
이 글은 일상적인 질문에서부터 컴퓨터 과학의 핵심 문제에 이르기까지, '같음'이라는 개념이 어떻게 적용되고 해석되는지를 탐구합니다. 특히, 두 프로그램이 '같은지'를 판정하는 문제에 초점을 맞춰, 문법적 비교와 $\beta$ 동등성이라는 두 가지 접근 방식을 소개합니다. 문법적 비교는 단순하지만 제한적이며, $\beta$ 동등성은 프로그램의 실행을 고려하지만, 계산 복잡성으로 인해 적용이 어렵습니다. 이러한 어려움에도 불구하고, 의존 형 이론에서의 형 검사(변환 검사)는 $\beta$ 동등성이 유용하게 활용될 수 있는 중요한 사례임을 설명합니다. 이 글은 '같음'의 개념이 프로그래밍과 타입 이론에서 어떻게 중요한 역할을 하는지, 그리고 이 개념을 올바르게 이해하고 구현하는 것이 왜 중요한지를 강조하며 마무리됩니다.
Read more →notJoon shared the below article:
Hacker's Pub에 입문한 한국어권 여러분을 위한 안내서

Jaeyeol Lee @kodingwarrior@hackers.pub
Hacker's Pub은 소프트웨어 업계 종사자들이 자유롭게 생각을 공유하고 소통할 수 있는 소셜 네트워크 서비스이자 블로깅 플랫폼입니다. ActivityPub 프로토콜을 지원하여 Mastodon, Misskey 등 다른 SNS 서비스 사용자들과도 연결되어 플랫폼 경계를 초월한 소통이 가능합니다. 이 글에서는 Hacker's Pub의 의미와 ActivityPub 프로토콜에 대한 간략한 소개, 그리고 커뮤니티에 기여할 수 있는 다양한 방법을 제시합니다. 오픈 소스로 개발되는 Hacker's Pub 생태계에 참여하여 함께 서비스를 발전시키고, 우리만의 클라이언트를 만들어 Hashnode와 같은 블로그 템플릿을 구축하는 미래를 기대해 볼 수 있습니다. Hacker's Pub은 상호 존중과 신뢰를 바탕으로 모든 이들이 자유롭게 의견을 나누고 함께 만들어가는 공간입니다.
Read more →버그의 입장에서 보면, 개발자가 하는 일이란 하나의 커다란 버그를 여러개의 작은 버그들로 끝없이 바꾸는 작업이다. 언제까지? 사용자 눈에 띄지 않을 때까지.