@hongminhee@hackers.pub · 626 following · 411 followers
Hi, I'm who's behind Fedify, Hollo, BotKit, and this website, Hackers' Pub!
Fedify, Hollo, BotKit, 그리고 보고 계신 이 사이트 Hackers' Pub을 만들고 있습니다.
Website
GitHub
Hollo
DEV
velog
Qiita
Zenn
Matrix
X🗨️Discuss: How should MoonBit handle effect polymorphism (allow one single higher order function to work over callback with/without error or async)?
1. Error + Async
2. Error only
3. No polymorphism, dup code
4. Hybrid/Other solution
⬇️Download: https://aka.moonbitlang.com/vsm
👥Community: https://discord.gg/5d46MfXkfZ
h1 태그의 기본 스타일이 변경됩니다
------------------------------
- 주요 브라우저들이 <h1> 태그의 기본 스타일(UA 스타일)을 변경하는 업데이트를 진행 중임
- 특히 중첩된 section, article, nav, aside 등의 내부에서 사용된 <h1>에 영향을 줌
- 개발자들은 이 변경으로 인해 사이트에 예기치 않은 스타일 변화나 Lighthouse 경고가 발생할 수 있으므로 주의가 필요…
------------------------------
https://news.hada.io/topic?id=20275&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
2025年 오픈소스 컨트리뷰션 아카데미 參與型 멘토團 募集 公告가 떴다. Fedify 프로젝트의 메인테이너로서 멘토團에 志願하고자 한다. 志願書가 .hwp 파일이기에 큰 맘 먹고 한컴오피스 한글 for Mac도 購入했다. (아무래도 앞으로 .hwp 파일 다룰 일이 많을 것 같다는 豫感이 들어서…)
본문에 “< center > 태그 안 된다는 얘길 듣고” 라고 썼는데 … 글에 적용되어버림…
RE: https://hackers.pub/@diarapin/019622df-6d0d-7651-a0a6-3fd0ad97fe25
최근에 추천사를 썼던 책이 있는데요. 이 교재를 활용해서 LLM AI 에이전트를 개발해볼까합니다. 제가 자원봉사(?)를 하고 있는 곳에서 컨텐츠 팀을 담당하고 있는데, 거기서 하는 일 중 하나가 뉴스레터 발행입니다.
TLDR 뉴스레터처럼 링크들을 오마카세처럼 모아서 양질의 콘텐츠를 제공하는게 목표인데, 그런 데이터를 모으기 위해서 최대한 아티클들을 모아서 요약해주는 봇을 만들어야겠다는 판단이 들었습니다. 언어 LLM 관련된 리소스도 많은 파이썬을 쓰게 될 것 같고, 서버 프레임워크는 컨텐츠 관리(어드민페이지)의 수월함을 위해서 Django를 쓰게 될 것 같습니다.
https://product.kyobobook.co.kr/detail/S000216210672
RE: https://hackerspub-ask-bot.deno.dev/message/01962280-fc29-748e-9ba8-fad032795e0d
이 글을 작성한 이후로 바로 Ask 봇을 만들었는데, 생각보다 오래 걸리지 않았다.
이렇게 하니까 1시간 컷 찍음
RE: https://hackers.pub/@kodingwarrior/0196222c-4b5a-783e-9dd8-8dc5f3e90202
# Ask Hackers Pub : 이번 주말에 뭐 하시나요?
이번 주말에 뭘 하려고 계획 중인지 편하게 얘기해 보아요.
읽을 책, 가볼 곳, 해볼 것.. 어떤 것이든 좋습니다.
도움 요청이나 피드백 요청도 좋습니다.
물론! 아무것도 하지 않고 쉬는 것도 훌륭합니다.
* 지난 주말에 계획하셨던 일의 회고도 한 번 남겨보면 좋을 것 같아요.
Hello, World!
Want to create a #bot for the #fediverse? #BotKit by 
With BotKit, you can:
Check out our documentation at https://botkit.fedify.dev/ and start building your fediverse bot today!
#연합우주(#fediverse)를 위한 봇을 만들고 싶으신가요? #BotKit by Fedify를 사용하면 몇 줄의 코드만으로 독립형 #ActivityPub 봇을 구축할 수 있습니다! 일반적인 Mastodon 또는 Misskey 봇과 달리, BotKit은 플랫폼 제약 없이 완전한 ActivityPub 서버를 만들 수 있게 도와줍니다.
BotKit으로 할 수 있는 것:
문서는 https://botkit.fedify.dev/에서 확인하시고 지금 바로 연합우주 봇을 만들어 보세요!
PL을 체계적으로 공부하는걸 회피하고 그때그때 좋아보이는 개념을 찍먹만하며 살아왔더니, 그냥 현존하는 프로그래밍 언어에 불평불만만 많은 사람이 되고말았다;;
해커즈 퍼브에서 "사용자"에 해당하는 부분에 스타일시트 적용 전후 비교
생각해 보니 에모지 반응 찍을 때 게시물이 Mastodon에서 작성된 경우에는 선택지를 없애는 게 나으려나…? Like 액티비티로 표현되는 ❤️ 이외에는 모두 Mastodon이 받아들이지 않는 EmojiReact 액티비티로 표현되기 때문에, 게시물 작성자가 어차피 에모지 반응을 볼 수 없으므로…
@hongminhee@hackers.pub洪 民憙 (Hong Minhee) 우리.인생 같은 포크에선 읽기 전용으로 리액션을 볼 수 있는 경우가 있어요
'악플'이라는 말이 그 자체로 암시하는 바가 있다. 악글, 악메시지 같은 황당한 조어는 없다. 그러나 '악플'은 아주 당당하게 한국어 언중의 삶에서 확고한 위상을 점유하고 있다. 이 근본 없는 신조어가 뉴스 헤드라인에 박혀 있어도 아무도 토를 달지 않을 정도다.
오직 댓글만이 이럴 수 있다. 오직 댓글만이 사람을 자살로 몰고 가는 죄악의 주범으로 번번이 지목될 수 있고, 오직 댓글만이 정치 여론 조작의 혐의로 관계자들을 징역에 처할 수 있다. 자기 블로그에 글 썼다고 이렇게까지 지탄을 받거나 처벌을 받는 일은 없다. 이것은 의미심장하다. 이것은 개개인의 품성 문제가 아니다. 댓글이라는 시스템이 갖는 구조적 원인이 분명히 있는 것이다.
그런 의미에서 트위터 역사상 가장 훌륭한 기능 추가도 "댓글 안 받기" 기능이라고 생각한다. 그러므로 해커즈 퍼브에 댓글 안 받기 기능이 생기기만 기다리는 중...
협업을 할 때 미묘하게 거슬리는 것들
쿠버네티스는 컴포즈만으로는 할 수 없는 HA (네트워킹 포함) 까지 책임져주는 솔루션 중 de-facto 라서 쓴다고 생각해요
앵간한 상황 다 대응되고
복잡하고 어려운 이유는 "앵간한 상황 다 대응"되기 때문이 아닐까 싶음... 컨테이너만 띄울거면 이렇게 복잡해질 이유가 없었음 - 사실 그 부분만 보면 컴포즈랑 비슷하기도 하고
여기에서는 트위터보다 조금 더 편하게 글을 써보려고 합니다. 해커스펍 가입해놓고 글 하나 안 올렸었네요.
흠...... 모르는 사이에 oci가 탈탈 털렸었어요?
@meWoojin Kim 헐 오라클 클라우드 털렸는데 증거 인멸 시도까지...
https://www.perplexity.ai/search/e54ef60b-306a-4631-a9df-99a97b206605
k8s의 인터페이스는 .yaml 보다는 API로 평가받아야 한다. .yaml도 사실 API payload 그대로 쓰라고하는거고, 딱히 사람이 직접 작성하는걸 염두한거 같지 않다. 뭐 어차피 다들 kustomize 같은걸로 템플릿화 시키니까 괜찮다.
근데 내가 알기로 k8s에서는 이미지를 업로드하고 바로 Pod으로 실행시키는 API가 없다. 그래서 무조건 레지스트리에 준비시켜놓고 주소를 줘야한다. 심지어 이미지 레지스트리 자체는 플러그인으로 다양한 방식으로 확장가능한데 말이다. 이게 맞습니까?
CJK 언어는 음절문자를 사용하는 특성상 아무데서나 끊어서 개행(改行)할 수 있고, 라틴 문자(키릴･그리스 문자도 마찬가지.)처럼 단어 단위 끊기와 음절단위 하이프네이션 원칙이 적용되지 않습니다. 따라서 CJK 텍스트는 어디서나 워드브레이크가 일어나도 괜찮도록 엔진 단위에서 처리를 달리하기 때문에 텍스트랩 설정 때문에 CJK 언어로 쓰인 문단의 텍스트플로가 달라지면 그게 더 큰일입니다.
RE: https://bsky.app/profile/did:plc:v2ob6je7otkaffdktzdaywzp/post/3lmfb5z66622e
이제 이중(?)배포 안 해도 되는건가
【拡散希望】
Hackers' Pub（ハッカーズ・パブ）は現在開発中の、ソフトウェアエンジニアと技術愛好家の為のActivityPub対応ソーシャルネットワークです。現在は韓国語中心のコミュニティが形成されていますが、日本のエンジニアの方々にも参加していただきたいと考えています。
Hackers' Pubは短文の投稿[1]と長文の記事[2]の両方をサポートしています。日常的な会話や簡単な質問は短文投稿で、詳細な技術解説やチュートリアルなどは長文記事で表現できます。QiitaやZennのような技術ブログ機能と、MastodonやMisskeyのようなタイムライン機能を兼ね備えた一つのプラットフォームで、両方の利点を享受できます。何よりもActivityPubプロトコルに対応している為、Mastodon、Misskey、Akkoma等と連携可能です。（このアカウントもHackers' Pubから投稿しています！）
技術的な特徴として、拡張Markdownによるテーブル、脚注、警告ボックス、ダイアグラム、数式などの多様な記法をサポートし、構文ハイライト、行ハイライト、差分表示などの強力なコードブロック機能も備えています。また、様々な言語での投稿が可能で、将来的には自動翻訳機能も予定しています。
Hackers' PubはAGPL-3.0ライセンスの下で開発されているオープンソースプロジェクトです。コードの貢献や機能提案も歓迎しています。
現在はまだ開発段階のため招待制となっています。Hackers' Pubに興味がある方は、DMや返信でメールアドレスをお知らせいただければ、招待状をお送りします。技術コミュニティの一員として、ぜひご参加をお待ちしております。よろしくお願いいたします。
Of which name do you think, when you think of “invention of the web”?
If it's a man, this site is for you to study: https://nowebwithoutwomen.com/
Or this book, Broad Band: https://www.penguinrandomhouse.com/books/545427/broad-band-by-claire-l-evans/
If you give talks, these are especially great resources for getting history straight.
홈서버는 괜히 SBC로 하지 말고
걍 컴퓨터 업글하고 남은 데스크탑/랩탑을 서버로 굴리거나
SBC를 쓸 거면 앗싸리 싼걸 여러개 사서 클러스터링을 하는게 나은 것 같아요
다음 글은 CBPV에 대해서 써볼까 합니다. CBV(Call-By-Value)나 CBN(Call-By-Name)은 전공자라면 한번쯤은 들어봤을 이름이지만, CBPV는 특정 분야 석박사가 아니면 들어본 적 없을 것 같네요. 하지만 실제 컴파일러 구현(GHC지만...)도 논의되고 있는 만큼 앞으로 유명해지지 않을까 싶어 미리 다뤄보려고 합니다.
어이쿠, CBPV가 무엇의 약자인지 써놓지를 않았네요. Call-By-Push-Value의 약자입니다. "Push"가 들어가는 걸로 CBV랑은 완전히 다른 것이 되는데요, 어찌 다른지는 글에서 다뤄보도록 하겠습니다.
다음 글은 CBPV에 대해서 써볼까 합니다. CBV(Call-By-Value)나 CBN(Call-By-Name)은 전공자라면 한번쯤은 들어봤을 이름이지만, CBPV는 특정 분야 석박사가 아니면 들어본 적 없을 것 같네요. 하지만 실제 컴파일러 구현(GHC지만...)도 논의되고 있는 만큼 앞으로 유명해지지 않을까 싶어 미리 다뤄보려고 합니다.
좀 쓰다 급하게 마무리하고 자러 갑니다. Hacker's Pub 가입 이후 처음이라 올리긴 하는데요…
옥텟 규칙으로 본 IETF RFC 9110 “HTTP Semantics” https://eonj.github.io/trouble.log/2025-04-09.an-octet-aspect-to-ietf-rfc-9110/
리) 드디어 자체적으로 플로우를 생산하기 시작한 해커스펍. 응원합니다.
한번 k8s 를 써보고 나니 지금 있는 시스템을 도커 컴포즈로 기운 시스템에서 k8s 로 이전하고 싶어지긴 하덥니다
특히 컨테이너 바깥 호스트에 있는 nginx 하고는 바이바이 하고 싶긴 함 이제는
k8s를 제대로 공부안하고 있는 이유는 딱 봤을때 k8s의 primitive 위에서 조화롭고 아름다운 뭔가가 만들어질거같은 느낌이 들지 않기 때문이다. 하스켈 튜토리얼 챕터1만 봐도 제대로 공부해봐야겠다 생각이 드는거랑 반대의 이유.
...인데 사실 저 느낌이 완전 틀렸을수 있다. 애초에 ops를 아름답게 하는 방법을 우리가 모르는 걸수도 있고. 또는 ops 자체가 현실의 지저분한 일임을 알기에 그걸 마주하지 않으려고 핑계대는 걸수도 있고. 약간의 상상의 나래를 펼쳐보자면, Pod 2개를 합성하는 연산을 정의하는 방식으로 쌓아올려나가면 어떨까 싶다. 지금은 Pod의 합성이란건 암시적으로 이루어지는데, 한 Pod의 노출된 ip:port를 다른 Pod이 보고 있으면 그게 합성이다;;
쿠버네티스도 간단하게 쓸 수 있죠. 요즘 k3s 같은거 쓰면 구성도 쉽고, 사용도 그냥 kubectl apply -f deployment.yaml 하면 끝인데. 이렇게만 쓰면 도커컴포즈랑 그렇게 다르지 않습니다.
근데도 쿠버를 쓰지 말라는 이유는, '잘못 쓸 여지'가 많기 때문입니다
쿠버를 쓰다 보면, 괜히 GitOps 하고 싶어서 ArgoCD 깔고, 서비스 메시 한다고 Istio 깔고, prometheus 깔고, thanos 셋업하고, EFK 스택 만들고, 이러다보면 아무도 유지보수 못하는 쿠버네티스 클러스터가 완성됩니다. 아니면 옵스 엔지니어가 주 40시간 전체를 이거를 간신히 존속시키는데에만 다 쓰고 나머지 아무것도 못 합니다.
이런거 다 참을 수 있고 k3s로 깔고 kubectl apply -f 만 치고 살거면 쿠버 쓰셔도 됩니다.
첨부한 사진이 무슨 링크드인에 '2025년 쿠버네티스 표준 구성' 이라고 돌아다니던데, 제발 이러지 마세요.
도커컴포즈 쓰면 이런걸 아예 못 하게 되니까 오히려 장점인거죠. 잘못 쓸 여지가 없음.
쿠버세란 옵스 엔지니어 연봉을 뜻한다
내가 k8s 자체를 딱히 좋아하느건 아닌데(어차피 잘 몰라서 좋고 싫고 할것도 없음), 근데 요즘은 처음부터 k8s 쓰는게 오버엔지니어링은 아니게 되었다.
k3s같은 것도 있고(NixOS로 하면 5분이면 띄운다), 어차피 머신 적을때는 별로 설정할것도 없을 것이다. 혹시 뭔가 +알파로 해줘야할게 있을때 helm install로 날먹 할수 있다는 여지도 있다. 그 다음에 서비스 운영은 이제 docker-compose up하냐, kubectl apply -f deployment.yaml 하냐의 차이가 된다.
근데 또 복잡하지 않은 인프라라면, 때가되서 k8s로 옮기는 것도 크게 어렵지 않을 것이다. 나는 '옮기는' 종류의 일을 매우 하기 싫어/두려워하기 때문에(DB 마이그레이션 처럼) 그냥 service.k3s.enabled = true 해버린다.
RE: https://hackers.pub/@ujuc/0196189f-1c95-7120-831b-27d7c51e8f38
똑같은 얘기를 닉스, 닉스오에스, 닉스옵스로도 할 수 있어요. "아 이거 걍 선언형으로 파일 작성하고 nixops deploy --check 하나만 때리면 알아서 이것저것 다 뜨고 다 설정될 텐데 괜히 귀찮게 왜 쿠버네티스를"
근데 현실적으로는 그냥 도커 컴포즈가 제일 삽질의 총량이 적죠...
📣 Exciting news! Fedify CLI is now available via Homebrew!
If you're using #Homebrew on macOS or #Linuxbrew on Linux, you can now install our CLI toolchain with a simple command:
서버메이드 깐프 brew install fedify
This makes it even easier to get started with building your federated server app. Try it out and let us know what you think!
똑같은 얘기를 닉스, 닉스오에스, 닉스옵스로도 할 수 있어요. "아 이거 걍 선언형으로 파일 작성하고 nixops deploy --check 하나만 때리면 알아서 이것저것 다 뜨고 다 설정될 텐데 괜히 귀찮게 왜 쿠버네티스를"
근데 현실적으로는 그냥 도커 컴포즈가 제일 삽질의 총량이 적죠...
쿠버는 마세라티 문제가 맞음! 제발 쿠버 섣불리 쓰지마!
어케어케 쿠버를 쓰기로 결정했다면
istio 같은거 제발 쓰지마!!!!!!
(도커도 쓰기 싫고 그냥 샌드박스된 바이너리 하나 돌리면 전부 알잘딱 돌아갔으면 좋겠어요)
RE: https://hackers.pub/ap/notes/01961970-a29f-78ff-baaf-1db2056a78e1
@saschanazKAGAMI🏳️🌈🏳️⚧️ 그게 제일 바람직하다는 것에 저도 동의해요. 다만 현실적으로는 아무래도 DB라든지 MQ라든지 이것저것 같이 띄워야 하다 보니, 서비스 운영을 하려다 보면 그런 전체 형상 관리를 위한 추상화 계층이 있기는 있어야 하는 것 같아요. 물론 도커 컴포즈를 안 쓰고 앤서블로 그런 모든 것을 관리할 수도 있고, 아예 닉스나 닉스오에스를 써서 더 아름답게 할 수도 있겠습니다만... 도커 컴포즈 정도면 타협 가능한 것으로...
개인적으로 쿠버네티스를 편하게 쓰기 위한 공부를 어느 정도 마친 상태에서 보면 "아 이거 쿠버 하나만 떠 있으면 편하게 이것저것 띄우고 할 수 있는데 괜히 귀찮게 세팅해야 하네"라는 생각이 들기도 하지만 😅 쿠버네티스 잘 모르는 상태에서는 참 막막하겠다 싶긴 합니다....
RE: https://hackers.pub/@xt/01961970-a29f-78ff-baaf-1db2056a78e1
(도커도 쓰기 싫고 그냥 샌드박스된 바이너리 하나 돌리면 전부 알잘딱 돌아갔으면 좋겠어요)
RE: https://hackers.pub/ap/notes/01961970-a29f-78ff-baaf-1db2056a78e1
저, 저도 90% 이상의 경우 도커 컴포즈 정도가 적당한 추상화 수준이라고 생각해요...
실제로 쿠버네티스 쓰는 팀에서 일해 본 경험도 그렇고, 주변 이야기 들어 봐도 그렇고, 도입하면 도입한 것으로 인해 증가하는 엔지니어링 코스트가 분명히 있다는 점은 누구도 부인하지 않는 것 같은데요. 쿠버네티스를 제대로 쓰는 것 자체도 배워야 할 것도 많고, 엔지니어가 유능해야 하고, 망치도 들여야 하고... 웬만하면 전담할 팀이 필요하지 않나 싶어요. (전담할 '사람' 한 명으로 때우기에는, 그 사람 휴가 가면 일이 마비되니까.)
엔지니어만 100명이 넘는 곳이라면 확실히 도입의 이득이 더 크겠지만, 반대로 혼자 하는 프로젝트라면 도무지 수지타산이 안 나올 것이라고 생각합니다. 따라서 쟁점은 그 손익분기점이 어디냐일 텐데... "대부분의" 서비스는 대성공하기 전까지는 도입 안 해도 되지 않나, 조심스럽게 말씀드려 봅니다. 즉 쿠버네티스가 푸는 문제는 마세라티 문제인 것이죠...
특히 클라우드 남의 컴퓨터 를 쓰지 않고 베어메탈 쓰는 경우는 더더욱...
RE: https://hackers.pub/@hongminhee/019618b4-4aa4-7a20-8e02-cd9fed50caae
하.. S3는 글로벌하게 네임스페이스를 구분하지 않았으면 좋겠다... 이름 짓기 너무 힘들다ㅠ.ㅠ.
@ailrunAilrun (UTC-5/-4) 재밌게 잘 읽었습니다. 걱정하신 것과 다르게 저에게는 쓰신 글이 술술(?) 잘 읽혔어요. 이제 다음 글은 Dependent Haskell인가요!
@curry박준규 Dependent Haskell은 흥미로운 내용을 다루기에는 아직 너무 갈 길이 멀고... 그렇다고 동기만 다루자니 좀 심심하네요. 아마 Agda나 Coq등을 조금 다뤄보지 않을까 싶습니다. 관련 내용으로 Dependent Haskell을 좀 언급할 수는 있겠습니다.
Jira, Linear 등 일정 관리 앱이 풀어야할 가장 어려운 문제는, 사용자 중 상당수는 애초에 일정 관리를 하기 싫어하는 사람이라는 것이다. 안타깝게도 나도 거기 포함되는데, 문제는 그런 사람일 수록 일정 관리가 꼭 필요하다. 나중에 프로젝트가 복잡해지면 일정 관리 앱을 켜는 거 자체를 꺼리게 된다. 이걸 어쩌면 좋지.
洪 民憙 (Hong Minhee) shared the below article:
Ailrun (UTC-5/-4) @ailrun@hackers.pub
국밥 두 그릇의 가격이 얼마인가? KTX의 속력이 몇 km/h인가? 내일 기온은 몇 도인가? 일상에서 묻는 이런 질문은 항상 같음의 개념을 암시적으로 사용하고 있다. 앞의 예시를 보다 명시적으로 바꾼다면 아래와 같이 (다소 어색하게) 말할 수 있다.
이런 질문들의 추상화인 이론들은 자연스럽게 언제 무엇과 무엇이 같은지에 대해서 답하는 데에 초점을 맞추게 된다. 예를 들면
등이 있다. 이렇게 어떤 두 대상이 같은지에 대해서 이야기를 하다보면 반대로 어떤 두 대상이 같지 않은지에 대해서도 이야기하게 된다. 즉,
이제 컴퓨터 과학(Computer Science)과 프로그래밍(Programming)에 있어 자연스러운 의문은 "두 대상이 같은지 아닌지와 같은 답을 주는 알고리즘(Algorithm)이 있나?"일 것이다. 다시 말해서 두 대상 aa와 bb를 입력으로 주었을 때
알고리즘이 있는지 물어볼 수 있다. 이런 어떤 명제가 참인지 거짓인지 판정하는 알고리즘의 존재 여부에 대한 질문을 "판정 문제"("Decision Problem")라고 하며, 명제 PP에 대한 판정 문제에서 설명하는 알고리즘이 존재한다면 "PP는 판정 가능하다"("PP is decidable")고 한다. 즉, 앞의 질문은 "임의의 aa와 bb에 대해 aa와 bb가 같은지 판정 가능한가?"라는 질문과 같은 의미라고 할 수 있다.
이 질문에 대한 대답은 당연하게도 어떤 대상을 어떻게 비교하는지에 따라 달라진다. 예를 들어 우리가 32 비트(bit) 정수에 대해서만 이야기하고 있다면 "임의의 32 비트 정수 aa와 bb에 대해 aa와 bb가 각 비트별로 같은지 판정 가능한가?"라는 질문에 대한 답은 "그렇다"이다. 반면 우리가 비슷한 질문을 자연수를 받아 자연수를 내놓는 임의의 함수에 대해 던진다면 답은 "아니다"가 된다.[1]
그렇다면 어떤 대상의 어떤 비교에 대해 판정 문제를 물어보아야할까? 프로그래머(Programmer)로서 명백한 대답은 두 프로그램(Program)이 실행 결과에 있어서 같은지 보는 것일 것이다. 그러나 앞서 자연수를 받아 자연수를 내놓는 함수에 대해 말했던 것과 비슷하게 두 프로그램의 실행 결과를 완벽하게 비교하는 알고리즘은 존재하지않는다. 이는 우리가 두 프로그램의 같음을 판정하고 싶다면 그 같음을 비교하는 방법에 제약을 두어야 함을 말한다. 여기서는 다음의 두 제약을 대표로 설명할 것이다.
이 방법은 말 그대로 두 프로그램이 문법 수준에서 같은지를 보는 것이다. 예를 들어 다음의 두 JavaScript 프로그램은 문법적으로 같은 프로그램이다.
// 1번 프로그램
let x = 5;
console.log(x);
// 2번 프로그램
let x = 5;
console.log( x );공백문자의 사용에서 차이가 있으나, 그 외의 문법 요소는 모두 동일함에 유의하자. 반면 다음의 두 JavaScript 프로그램은 동일한 행동을 하지만 문법적으로는 다른 프로그램이다.
// 1번 프로그램
let x = 5;
console.log(x);
// 2번 프로그램
let x = 3 + 2;
console.log(x);두 프로그램 모두 x에 5라는 값을 할당하고 5를 콘솔에 출력하나, 첫번째 프로그램은 = 5;를, 두번째 프로그램은 = 3 + 2을 사용하여 5를 할당하고 있기 때문에 문법적으로 다르다.
문법적 비교는 이렇게 문법만 보고서 쉽게 판정할 수 있다는 장점이 있으나, 두번째 예시처럼 쉽게 같은 행동을 함을 이해할 수 있는 프로그램에 대해서도 "같지 않음"이라는 결과를 준다는 단점을 가진다. 혹자는
3 + 2같은 계산은 그냥 한 다음에 비교하면 안돼? 컴파일러(Compiler)도 상수 전파(Constant Propagation) 최적화라던지로3 + 2를5로 바꾸잖아?
라는 생각을 할 수도 있을 것이다. 이 제안을 반영한 방법이 바로 β\beta 동등성이다.
바로 앞의 소절에서 단순 계산의 추가에 의해 같음이 같지 않음으로 변하는 것을 보았다. 이런 상황을 피하기 위해서는 같음을 평가할 때 프로그램의 실행을 고려하도록 만들어야 한다. 가장 대표적인, 대부분의 프로그래밍 언어(Programming Language)에 존재하는 프로그램의 실행은 함수 호출이다. 따라서 함수 호출을 고려한 같음의 비교는 f(c)와 함수 f의 몸체 b 안에서 인자 x를 c로 치환한 것을 같다고 취급해야한다. 예를 들어
let f = (x) => x + 3;이 있다면, f(5)와 5 + 3 혹은 8을 같은 프로그램으로 취급해야한다. 이 비교 방법의 큰 문제는 함수가 종료하는지 알지 못한다는 것이다. 두 프로그램 a와 b를 비교하는데, a가 종료하지 않는 함수 l을 호출한다면, 이 알고리즘은 "같음"이나 "같지 않음"이라는 결과를 낼 수조차 없다. 즉, 올바른 판정법이 될 수 없다.
더 심각한 문제는 아직 값을 모르는 변수가 있는 "열린 프로그램"("Open Program")에 대해서도 이런 계산을 고려해야한다는 것이다. 다음의 JavaScript 예시를 보자.
let g = (x) => f(x) + 3;
let h = (x) => (x + 3) + 3;g와 h는 같은 프로그램일까? 우리가 g와 h가 같은 프로그램이기를 원한다면 f(x)와 x + 3을 같은 프로그램으로 보아야한다. 대부분의 프로그램은 함수 안에서 쓰여지기 때문에 프로그램의 비교는 거의 항상 g와 h의 몸체와 같은 열린 프로그램들의 비교이다. 따라서 g와 h를 다른 프로그램으로 본다면 계산을 실행하여 두 프로그램을 비교하는 의미가 퇴색되고 만다. 그렇기 때문에 우리는 x와 같이 값이 정해지지 않은 변수가 있을 때에도 f(x)을 호출하여 비교해야만 한다. 이는 우리가 단순히 모든 함수가 종료하는지 여부를 떠나서, 함수의 몸체에 등장하는 모든 부속 프로그램(Sub-program)이 종료하는지 아닌지를 따져야만 한다는 이야기이다.
이런 강한 제약조건으로 인해 β\beta 동등성을 통해서 프로그램 비교의 판정 문제를 해결 가능한 곳은 매우 제한적이지만, β\beta 동등성이 매우 유용한 한가지 경우가 있다. 바로 의존 형이론(Dependent Type Theory)의 형검사(Type Checking)이다.
의존 형이론은 형(Type)에 임의의 프로그램을 포함할 수 있도록 하는 형이론(Type Theory)의 한 종류이다. 예를 들어 명시적인 길이(n)를 포함한 벡터(Vector) 형을 Vector n Int과 같이 쓸 수 있다. 이 형은 n개의 Int값을 가진 벡터를 표현하는 형이다. 이제 append라는 두 벡터를 하나로 연결하는 함수를 만든다고 해보자. 대략 다음과 같은 형을 쓸 수 있을 것이다.
append : Vector n a -> Vector m a -> Vector (n + m) a즉, append는 길이 n짜리 a 형의 벡터와 길이 m짜리 a 형의 벡터를 합쳐서 길이 n + m짜리 a 형의 벡터를 만드는 함수이다. 이 함수를 사용해서 길이 5의 벡터를 길이 2와 길이 3짜리 벡터 x, y로부터 만들고 싶다고 하자.
append x y : Vector (2 + 3) a안타깝게도 우리는 길이 2 + 3짜리 벡터를 얻었지, 길이 5짜리 벡터를 얻진 못했다. 여기서 앞서의 질문이 다시 돌아온다.
아니,
2 + 3를5로 계산하면 되잖아?"
그렇다. 이런 의존 형에 β\beta 동등성을 적용하면 우리가 원하는 형을 바로 얻어낼 수 있다. Vector (2 + 3) a과 Vector 5 a는 같은 형이기 때문이다. 더욱이, 의존 형의 경우 종료하지 않는 부속 프로그램이 잘못된 형을 줄 수 있기 때문에 많은 경우 종료하지 않는 부속 프로그램을 어차피 포함하지 않는다. 다시 말해, 앞서 말한 제약 조건 즉 모든 부속 프로그램이 종료해야만 한다는 제약조건은 의존 형의 경우 상대적으로 훨씬 덜 심각한 제약조건이 되는 것이다.
이런 의존 형에 있어서의 β\beta 동등성 검사를 "변환 검사"("Conversion Check")라고 하며, 두 형이 β\beta 동등일 경우 이 두 형이 서로 "변환 가능하다"("Convertible")라고 한다. 이 변환 검사는 의존 형이론 구현에 있어서 가장 핵심인 기능 중 하나이며, 가장 잦은 버그를 부르는 기능 중 하나이기도 하다.
이 글에서는 같음과 같지 않음의 판정 문제에 대해 간략히 설명하고 프로그램의 같음을 판정하는 법에 대해서 단순화하여 다루어보았다. 구체적으로는 문법 기반의 비교와 β\beta 동등성을 통한 비교로 프로그램의 같음을 판정하는 법을 알아보았고, 이 중 β\beta 동등성이 적용되는 가장 중요한 예시인 의존 형이론을 β\beta 동등성을 중점으로 짤막하게 설명하였다. 마지막 문단에서 언급했듯 의존 형이론의 구현에 있어서 β\beta 동등성을 올바르게 구현하는 것은 가장 중요한 작업 중 하나이기에, 최근 연구들은 β\beta 동등성의 구현 자체를 의존 형이론 안에서 함으로서 검증된 β\beta 동등성의 구현을 하기 시작하고 있다. 이 글이 같음과 같지 않음과 판정 문제 그리고 β\beta 동등성에 있어 유용한 설명을 내놓았기를 바라며 이만 줄이도록 하겠다.
두 함수가 같다라고 보는 방법에 따라 다르나, 두 함수가 항상 같은 값을 가진다면 같다고 하자. 이때 함수의 판정 문제는 정지 문제(Halting Problem)와 동일하다. 임의의 튜링 기계(Turing Machine) ff가 입력 nn을 받았을 때 종료하면 g(n)=1g(n) = 1, 아니면 g(n)=0g(n) = 0이라고 하면 이 함수 gg와 상수 함수 c(n)=1c(n) = 1가 같은 함수임을 보이는 것은 ff가 항상 종료한다는 것을 보이는 것과 동등하다. ↩︎
해커스펍을 스마트해지기 위한 용도로 쓰고 있다. 대수롭지 않은 생각도 어디안쓰면 쓸데없이 머릿속에서 리플레이된다. flush를 자주 하자...
RE: https://social.silicon.moe/@realgsong/114300412588845941
