지금 JS 멘토링하면서 Promise를 가르치는데 은근슬쩍 모나드도 같이 가르치고 있다(모나드 자체를 언급하진않음). 누구나 마음속에 부리또 하나씩을 품고 살아가니깐...
bgl gwyng
@bgl@hackers.pub · 61 following · 63 followers
슈티를 함께 만들 팀을 만들고 있습니다. 관심 있으신 분, 또는 잘 모르겠지만 이야기를 나눠보고 싶은 분도 bgl@gwyng.com으로 편하게 연락주세요.
GitHub- @bglgwyng
shootee- www.shootee.io
메시지가 자동으로 번역되는 채팅앱이 있으면 좋겠는데, 아마 디스코드가 곧 지원할거 같다.
여태 모나드 가르칠때 그냥 do notation부터 알려주고 알아서 써보라고했는데 절반정도는 잘 따라왔다.
문법적으로 <-를 넣어야할 위치만 아는 상태에서도 코드를 웬만큼 짰다.
즉, next token prediction은 휴먼에게도 좋은 학습 방법이다.
RE: https://hackers.pub/@xt/01963d1e-e20c-77c5-a395-69c592137fb3
저도 두 가지 쟁점 모두 동의하는 편입니다. 그리고, 별개의 이야기입니다만, $ 를 가르칠 때에는 그냥 문법이라고 가르치는 게 학습자의 이해와 응용이 압도적으로 빠르고 좋았습니다.
"이건 여기서부터 뒤로는 다 괄호로 감싸겠다는 뜻이라고 생각하세요."
이러면 한 방에 설명이 끝나고, 필요성이나 편리성에 대해서도 알아서들 납득하는 것이죠. 연산자 우선순위나 좌결합 우결합 등은 그게 되고 나서 얘기하고요. 그러면 "아, 이게 그래서 이렇게 되는 거였군요?" 하면서, 훨씬 쉽게 이해합니다. 이걸 거꾸로 좌결합 우결합 어쩌고부터 가르치려고 하면 다들 꾸벅꾸벅 졸아요... ㅋㅋ ㅠㅠ
(결국 "모나드란 무엇인가"부터 배우면/가르치면 안 된다는 주장과 같은 맥락입니다.)
RE: https://hackers.pub/@bgl/01963c3b-98fa-7432-a62f-0d2dfc0691bf
저도 두 가지 쟁점 모두 동의하는 편입니다. 그리고, 별개의 이야기입니다만, $ 를 가르칠 때에는 그냥 문법이라고 가르치는 게 학습자의 이해와 응용이 압도적으로 빠르고 좋았습니다.
"이건 여기서부터 뒤로는 다 괄호로 감싸겠다는 뜻이라고 생각하세요."
이러면 한 방에 설명이 끝나고, 필요성이나 편리성에 대해서도 알아서들 납득하는 것이죠. 연산자 우선순위나 좌결합 우결합 등은 그게 되고 나서 얘기하고요. 그러면 "아, 이게 그래서 이렇게 되는 거였군요?" 하면서, 훨씬 쉽게 이해합니다. 이걸 거꾸로 좌결합 우결합 어쩌고부터 가르치려고 하면 다들 꾸벅꾸벅 졸아요... ㅋㅋ ㅠㅠ
(결국 "모나드란 무엇인가"부터 배우면/가르치면 안 된다는 주장과 같은 맥락입니다.)
RE: https://hackers.pub/@bgl/01963c3b-98fa-7432-a62f-0d2dfc0691bf
@bglbgl gwyng 
@curry박준규 적은 키워드로 표현 가능한 상황이 더 많다면 "디자인(Design)이 더 잘 되었다"고는 할 수 있다고 봅니다. 언어가 발전한다는게 디자인을 개선한다는 것과 직결되어있지 않은 경우가 더 많으니 말입니다. (많은 경우 표현력의 증대나 자주 사용되는 표현의 단순화에 더 집중하죠)
@ailrunAilrun (UTC-5/-4) @curry박준규 그래서 do notaion, proc notation 등을 추가하는거랑, OverloadedDotRecord같은 문법 확장을 구분해서 보는게 좋다고 생각합니다. 전자의 경우들은 각각 대응하는 Monad, Arrow 등의 개념을 발견하고나서야 추가할수 있었을테고, 후자는 (정확한 역사는 모르겠지만) 그냥 불평불만이 하도 많다보니 땜빵한거에 가깝게 보입니다.
@bglbgl gwyng 이게 생각해보니 ‘문법이 복잡하다’, ‘문법 요소가 적다’라는 표현이 구체적이지 않은 것 같습니다. 갑자기 언어 확장이 떠오르면서 ‘문법 안 복잡한 거 맞나?’ 싶네요. 그래서 표현을 좀 바꾸면 저는 사전에 정의된 키워드가 적을 수록 좋다고 생각합니다.
@curry박준규 더 primitive한 의미론을 포착해서 문법 요소로 만들고 그걸로 다양한 정의를 하게 하는게 낫다는 점에선 동의하는데요. 말씀하신 기준을 그대로 적용해버리면, 모든 언어들이(하스켈도 포함) 발전할수록 점점 키워드가 추가되는데, 그때마다 점점 더 안 좋아졌다고 하면 좀 이상하죠.
@curry박준규 @bglbgl gwyng 저도 예전에 Lisp나 Smalltalk 좋아했을 때는 문법 요소가 최대한 적은 걸 선호했는데, 나이가 드니까 문법 요소를 극도로 줄이는 건 미학의 영역일 뿐 실용적이진 않다는 생각이 들어 Haskell 정도가 딱 적당하다고 느끼게 됐네요.
@hongminhee洪 民憙 (Hong Minhee) @curry박준규 저도 Lisp을 첨에 봤을땐 감탄했는데요. 지금 보면 그냥 파서짜기 싫었나보다 정도의 생각이 듭니다ㅋㅋ
@bglbgl gwyng 한편 저는 문법 요소가 가능한 적어야 좋다고 생각합니다. 그래서 하스켈을 처음 봤을 때 Bool이 라이브러리인 게 좋았어요.
data Bool = False | True@curry박준규 근데 따지고보면 하스켈도 문법 복잡하죠. 각각 다 역할이 있어서 그렇지만요.
하스켈에서 $가 infix operator가 아니라 문법 요소여야 한다는 얘기에는 동의하는 사람들이 꽤 있다. 근데 1 + $ 2 + 3도 1 + (2 + 3)으로 변환되어야 한다고 하면 다들 싫어한다ㅋㅋ 근데 나는 저것도 좋다고 본다.
미드 쇼츠보다가 깨달았는데, 우리나라는 왜 검찰이 임명직일까? 배경이 뭘까? 🤔
@annyeong안녕 혹시 보고계신게 빌리언즈 인가요?
RN에 새 런타임이 옛날거보다 오히려 느리다는 이슈를 제보했는데, 솔직히 좀 황당하다. 그냥 대기업이 오픈 소스 메인테인을 못한다...는 아니다. 난 단순히 잡버그/미구현기능 많은거는 망치가 부족한가보다 정도로 이해한다.
근데 요 이슈는 RN 메인테이너 쪽에서 지난 1+년간 새 런타임으로의 마이그레이션을 적극적으로 권유했는데, 이런 기본적인 문제가 파악안되고 있었던거면 흠... 저 정도 규모의 프로젝트를 운영하는게 어떤지 잘 몰라서 뭔가 더이상 말을 얹기는 어렵겠지만, 쨋든 설명이 더 필요하다 느낀다.
@bglbgl gwyng 
@kodingwarriorJaeyeol Lee 
@lionhairdino
제 심상이랑은 좀 다르네요. 저는 H의 중간 막대가 좀 아래로, H가 좌우로 살짝 벌어져있고 P가 좀 더 바짝 붙은 형태를 상상했습니다. Inkscape 켜서 직접 그리기에는 졸리네요 😅
@ailrunAilrun (UTC-5/-4) @kodingwarriorJaeyeol Lee @lionhairdino 아아 어떤 느낌인지 상상이 갑니다. 저는@parksb
님이 하신것처럼 맥주가 차있으면 좋겠다싶어 H 중간 막대를 위로 올렸습니다.
맥에서 VS Code의 현재 창(탭 아님)만 닫고싶을때 ⌘+⇧+W 이거 누르면 되는걸 이제 알았다;; 몰라서 맨날 마우스썼는데
@bglbgl gwyng @lionhairdino @ailrunAilrun (UTC-5/-4)
오.... 저 방금 SVG를 LLM이 깎아줄 수 있다는걸 방금 처음 알았어요.
https://www.svgviewer.dev/s/sCwe91Tw https://www.svgviewer.dev/s/8hMjXLcz https://www.svgviewer.dev/s/c4oIyOId
@kodingwarriorJaeyeol Lee @lionhairdino @ailrunAilrun (UTC-5/-4) 근데 결과물보시면 아시겠지만 그냥 figma에서 그렸으면 더 빨리했을겁니다ㅋㅋ
@bglbgl gwyng @lionhairdino @ailrunAilrun (UTC-5/-4)
이제 이걸 디자인 감각 있는 분 호출해서 벡터그래픽으로 만들어달라하면 될 것 같은데......
@lionhairdino 딱 떠오르는 건 HP를 붙여서 맥주잔 모양으로 만드는 거네요
난 JS에서 comma operator를 *> 느낌으로 자주 쓴다. 가령 (x, y) => (assert(x), assert(y), x + y) 요런 식으로 말이다.
근데 확실히 마이너인게, 저렇게 하면 모든 종류의 linter들한테 탄압받는다.
https://ieeexplore.ieee.org/document/10786566 찾아보니 뭐가 나오긴 하네. SQLite 뿐만 아니라 일반적인 대용량 파일의 증분어데이트에 쓸수있겠니.
RE: https://hackers.pub/@bgl/01963453-82e4-746e-a4c9-a3f5385b84f8
지금까지 Hackers' Pub은 반드시 이메일을 통해 로그인 링크를 수신하는 식으로만 로그인이 가능했는데, 사실은 많이 번거로웠죠?
이를 해결하기 위해 Hackers' Pub에 패스키 기능을 추가했습니다. 패스키 추가는 설정 → 패스키 페이지에서 할 수 있으며, 패스키가 등록된 기기 및 브라우저에서는 로그인 페이지에서 자동적으로 패스키를 사용할 것인지 묻는 창이 뜨게 됩니다.
e2e 암호화된 SQLite 호스팅/백업 서비스가 있으면 좋겠다. 동형암호를 활용하면 증분 싱크를 할수있지 않을까?
오늘 할일은 ffmpeg-kit이 archive되면서 prebuilt binary들이 날아갔는데, 이로 인해 깨진 빌드를 고치는 것이다. 역시 소프트웨어 개발은 즐거워~ 최고야~
topiary는 tree-sitter 문법 정의를 주면 포매터를 공짜로 줍니다.
@bglbgl gwyng 그냥 무시하고 기본 우선 순위대로 파싱하지 않을까 싶네요… 🤔
@hongminhee洪 民憙 (Hong Minhee) tree-sitter가 lexer를 커스텀할수 있게 열어두긴 했는데요. lexer 레벨에서 구현이 가능할까 싶네요.
Haskell용 tree-sitter 파서가 있는데, 이때 infix 등 연산자 우선순위를 동적으로 주는 기능들은 어떻게 처리하는거지? tree-sitter의 인터페이스가 context sensitive parsing이 될거같지가 않은데?
어째서 ActivityPub을 바닥부터 구현하는 것보다 Fedify를 쓰는 게 여러모로 나은지에 대한 글(영어)을 썼습니다.
아무래도 앱 개발은 혼자선 하면 안되고 트러블슈팅을 할수 있도록 팀을 갖추고 해야하는거 같다. 추잡한 문제들이 너~무 많다. 하지만 이런 허접한 교훈을 얻고 관둘순 없으니 어떻게든 혼자서 마저 나아가야한다.
The Korean fediverse community is proposing to establish April 11th as “Fediverse Day” (聯合宇宙의 날). Since this idea emerged today in conversations among Korean fediverse users, they've suggested making today's date the official celebration going forward.
We're sharing this initiative with the broader fediverse community and would love to know if you'd support and participate in an annual Fediverse Day!
Excited to share that 
@pbzweihander쯔방 
has created fediday.org—a new website dedicated to Fediverse Day! The site celebrates April 11th as Federated Fediverse Day, which originated from conversations in the Korean fediverse community. Visit the site to learn about the background of this initiative and discover other important dates in the fediverse calendar. If you'd like to add a special date, you can contribute through the GitHub repository!
@bglbgl gwyng 저도 Nest 에서 Prisma 쓰는데, 당연히 ESM 지원되는 줄 알았네요. 오늘 올라온 글을 보고 대충 추정해보면, ts 를 js 로 전환하면서 import 구문을 모두 commonjs (require) 로 바꾸고 있는가 싶네요. 😅
@arkjunJuntai Park 6.6.0에서 이제 ESM 지원한다고 하네요. 6.5.0에서 어떻게 해보려고 삽질하느라 하루를 날렸는데 하...
HTTPS로 전송된 내용은 서버가 내용에 서명을 한 셈 아닌가?
란 질문을 Gemini 2.5한테 했는데 내가 어느 부분을 놓쳤는지를 정확하게 집어내서 설명해주었다. 나의 오개념에 일부분 '공감'을 먼저하고 설명한 부분이 좋았다. 비교를 위해 Gemin 2.0한테도 같은 질문을 해봤는데 그냥 아는 내용을 줄줄이 읊기만 한다.
회사 계정이라 그런가 대화 내용을 공유를 못하는거 같은데... 답변을 요약하자면
내용을 암호화하는데 쓰이는 키가 서버로부터 서명이 되어 있는건 맞다. 이를 통해 암호화된 내용도 간접적으로 서버가 서명을 한셈 아닌가...라고 생각했다. 문제는 그 암호화 키를 서버와 클라 양쪽에서 자신이 보내는 내용을 암호화할때 같이 쓴다는 점이다. 그래서 해당 세션에서 서버/클라 둘 중 한쪽이 서명한 내용이라곤 생각할 수 있지만, 둘 중에 어느쪽인지를 보장할 수가 없다. 클라가 서버한테 받지도 않은 내용을 조작할수 있는 것이다.
...인데, 애초에 복잡하게 생각할 필요없이 전송에 비대칭이 아닌 대칭 암호화를 쓰는거에서 글러먹은 생각인걸 알수가 있었다ㅋㅋ Gemini의 세심함과 나의 멍청함을 알수있는 대화였다.
HTTPS로 전송된 내용은 서버가 내용에 서명을 한 셈 아닌가?
란 질문을 Gemini 2.5한테 했는데 내가 어느 부분을 놓쳤는지를 정확하게 집어내서 설명해주었다. 나의 오개념에 일부분 '공감'을 먼저하고 설명한 부분이 좋았다. 비교를 위해 Gemin 2.0한테도 같은 질문을 해봤는데 그냥 아는 내용을 줄줄이 읊기만 한다.
@lionhairdino
PL을 체계적으로 공부하는걸 회피하고 그때그때 좋아보이는 개념을 찍먹만하며 살아왔더니, 그냥 현존하는 프로그래밍 언어에 불평불만만 많은 사람이 되고말았다;;
@bglbgl gwyng 중국에서 취두부 엄청 먹는데 곤란하지 않을까요? 💨
@hongminhee洪 民憙 (Hong Minhee) 정알못으로서 하이테크적인 뭔가를 생각햇는데 '콩'이라니까 좀 허탈해졌습니다. 근데 먹고사는 문제가 젤 중요한게 맞지요.
미중 무역 전쟁과 관련해 사람들이 미국만 걱정하고 중국은 별 걱정안하길래, 중국의 미국으로부터의 주요 수입품을 chatgpt한테 물어봤다. 1순위가 콩이라고 한다.
두부 좀 덜먹으면 되는건가...
(어디까지나 개인 취향입니다.) 저는 글을 다른 사람과의 대화와 비슷한 느낌을 가지고 읽습니다. 제 주변에 어떤 사람도 저에게 대화할 때, ~음, ~슴, ~함 체로 말하지 않습니다. 뭐뭐 하였음, 그래서 이랬음, 결과로 뭐뭐함 ... 좀 어색하게 들리는데요. 저만 그런가요? 몇 년 째 고맙게 보고 있는 긱뉴스가 이 정책을 고수하는데, 아직도 어색하네요.
@lionhairdino 요즘은 말도 그렇게 하는 사람들이 늘고있더라고요. 첨엔 이상했는데 듣다보니 적응됩디다;;
k8s의 인터페이스는 .yaml 보다는 API로 평가받아야 한다. .yaml도 사실 API payload 그대로 쓰라고하는거고, 딱히 사람이 직접 작성하는걸 염두한거 같지 않다. 뭐 어차피 다들 kustomize 같은걸로 템플릿화 시키니까 괜찮다.
근데 내가 알기로 k8s에서는 이미지를 업로드하고 바로 Pod으로 실행시키는 API가 없다. 그래서 무조건 레지스트리에 준비시켜놓고 주소를 줘야한다. 심지어 이미지 레지스트리 자체는 플러그인으로 다양한 방식으로 확장가능한데 말이다. 이게 맞습니까?
@bglbgl gwyng 오호.... 컨테이너 오케스트레이션을 쓰실일이 많으실까요?
그게 궁금해요 ㅎㅎㅎㅎㅎㅎ
k3s는 Kube 리소스 중에서 가장 기본되는 것만 컨테이너로 띄우고 있는걸로 알아서... 딱히 오케스트레이션을 할꺼아니면 생각보다 오버스펙 같아보이는 느낌이 들어서요 :)
로컬에서 한개이상 잘 안띄우다보니.. :) 모르겠네요. DB, Cache 뭐 쓰는것들 등등등 설치하다보면.. ㅎㅎㅎㅎ
그리고 yaml이.. 참.. 불편해서.... 읔....
yaml은... 아무도 deployment.yaml로 IaC를 할수있다곤 생각안할거 같습니다. 근데 helm이나 kustomize같은 방식이 미덥지 않긴하죠. 저는 인프라에 Pulumi를 쓰는데, 나중에 기회가 있다면 k8s위의 서비스들도 Pulumi로 프로비저닝 해보려합니다.
k8s를 제대로 공부안하고 있는 이유는 딱 봤을때 k8s의 primitive 위에서 조화롭고 아름다운 뭔가가 만들어질거같은 느낌이 들지 않기 때문이다. 하스켈 튜토리얼 챕터1만 봐도 제대로 공부해봐야겠다 생각이 드는거랑 반대의 이유.
...인데 사실 저 느낌이 완전 틀렸을수 있다. 애초에 ops를 아름답게 하는 방법을 우리가 모르는 걸수도 있고. 또는 ops 자체가 현실의 지저분한 일임을 알기에 그걸 마주하지 않으려고 핑계대는 걸수도 있고. 약간의 상상의 나래를 펼쳐보자면, Pod 2개를 합성하는 연산을 정의하는 방식으로 쌓아올려나가면 어떨까 싶다. 지금은 Pod의 합성이란건 암시적으로 이루어지는데, 한 Pod의 노출된 ip:port를 다른 Pod이 보고 있으면 그게 합성이다;;
힘든 하루였다ㅜㅜ KFC 반값치킨 먹으러가야지
쿠버네티스도 간단하게 쓸 수 있죠. 요즘 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
하.. S3는 글로벌하게 네임스페이스를 구분하지 않았으면 좋겠다... 이름 짓기 너무 힘들다ㅠ.ㅠ.
Jira, Linear 등 일정 관리 앱이 풀어야할 가장 어려운 문제는, 사용자 중 상당수는 애초에 일정 관리를 하기 싫어하는 사람이라는 것이다. 안타깝게도 나도 거기 포함되는데, 문제는 그런 사람일 수록 일정 관리가 꼭 필요하다. 나중에 프로젝트가 복잡해지면 일정 관리 앱을 켜는 거 자체를 꺼리게 된다. 이걸 어쩌면 좋지.
bgl gwyng shared the below article:
같은 것을 알아내는 방법
Ailrun (UTC-5/-4) @ailrun@hackers.pub
같은 것과 같지 않은 것
국밥 두 그릇의 가격이 얼마인가? KTX의 속력이 몇 km/h인가? 내일 기온은 몇 도인가? 일상에서 묻는 이런 질문은 항상 같음의 개념을 암시적으로 사용하고 있다. 앞의 예시를 보다 명시적으로 바꾼다면 아래와 같이 (다소 어색하게) 말할 수 있다.
- 국밥 두 그릇의 가격은 몇 원과 같은가?
- KTX의 속력은 몇 km/h와 같은가?
- 내일 기온은 몇 도와 같은가?
이런 질문들의 추상화인 이론들은 자연스럽게 언제 무엇과 무엇이 같은지에 대해서 답하는 데에 초점을 맞추게 된다. 예를 들면
- x2+x+1=0x^2 + x + 1 = 0의 실수 해의 갯수는 0과 같다.
- 물 분자 내의 수소-산소 연결 사이의 각도는 104.5도와 같다.
- 합병 정렬의 시간 복잡도는 O(nlogn)O(n\log{n})과 같다.
등이 있다. 이렇게 어떤 두 대상이 같은지에 대해서 이야기를 하다보면 반대로 어떤 두 대상이 같지 않은지에 대해서도 이야기하게 된다. 즉,
- x+4x + 4를 22로 나눈 나머지는 x+1x + 1을 22로 나눈 나머지와 같지 않다.
- 연결 리스트(Linked List)와 배열(Array)은 같지 않다.
- 함수 λ x→x\lambda\ x \to x와 정수 55는 같지 않다.
같은 것과 판정 문제(Decision Problem)
이제 컴퓨터 과학(Computer Science)과 프로그래밍(Programming)에 있어 자연스러운 의문은 "두 대상이 같은지 아닌지와 같은 답을 주는 알고리즘(Algorithm)이 있나?"일 것이다. 다시 말해서 두 대상 aa와 bb를 입력으로 주었을 때
- 알고리즘이 참 값(True\mathtt{True})을 준다면 aa와 bb가 같고
- 알고리즘이 거짓 값(False\mathtt{False})을 준다면 aa와 bb가 같지 않은
알고리즘이 있는지 물어볼 수 있다. 이런 어떤 명제가 참인지 거짓인지 판정하는 알고리즘의 존재 여부에 대한 질문을 "판정 문제"("Decision Problem")라고 하며, 명제 PP에 대한 판정 문제에서 설명하는 알고리즘이 존재한다면 "PP는 판정 가능하다"("PP is decidable")고 한다. 즉, 앞의 질문은 "임의의 aa와 bb에 대해 aa와 bb가 같은지 판정 가능한가?"라는 질문과 같은 의미라고 할 수 있다.
이 질문에 대한 대답은 당연하게도 어떤 대상을 어떻게 비교하는지에 따라 달라진다. 예를 들어 우리가 32 비트(bit) 정수에 대해서만 이야기하고 있다면 "임의의 32 비트 정수 aa와 bb에 대해 aa와 bb가 각 비트별로 같은지 판정 가능한가?"라는 질문에 대한 답은 "그렇다"이다. 반면 우리가 비슷한 질문을 자연수를 받아 자연수를 내놓는 임의의 함수에 대해 던진다면 답은 "아니다"가 된다.[1]
그렇다면 어떤 대상의 어떤 비교에 대해 판정 문제를 물어보아야할까? 프로그래머(Programmer)로서 명백한 대답은 두 프로그램(Program)이 실행 결과에 있어서 같은지 보는 것일 것이다. 그러나 앞서 자연수를 받아 자연수를 내놓는 함수에 대해 말했던 것과 비슷하게 두 프로그램의 실행 결과를 완벽하게 비교하는 알고리즘은 존재하지않는다. 이는 우리가 두 프로그램의 같음을 판정하고 싶다면 그 같음을 비교하는 방법에 제약을 두어야 함을 말한다. 여기서는 다음의 두 제약을 대표로 설명할 것이다.
- 문법적 비교(Syntactic Comparison)
- β\beta 동등성 (β\beta Equivalence)
1. 문법적 비교(Syntactic Comparison)
이 방법은 말 그대로 두 프로그램이 문법 수준에서 같은지를 보는 것이다. 예를 들어 다음의 두 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 동등성이다.
2. β\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가 항상 종료한다는 것을 보이는 것과 동등하다. ↩︎
@ailrunAilrun (UTC-5/-4) 저는, 상단의 카테고리 중 "게시글만"을 보고, 다른 서비스와 차별점이 이거구나 싶었습니다. 개발자 선수분들이 "투고"한 것들이, 적당한 속도로 쌓여 가면 좋겠습니다.
@lionhairdino 재활의 시발점으로 요새 하고 있는 일인 Conversion checker에 대한 글이나 좀 써 보아야겠습니다.
와 기분이 좋아지는 숫자
@ailrunAilrun (UTC-5/-4) 어서오세요. 반갑고 반갑습니다~
@lionhairdino @ailrunAilrun (UTC-5/-4) 오랜만이네요 반갑습니다
해커스펍을 스마트해지기 위한 용도로 쓰고 있다. 대수롭지 않은 생각도 어디안쓰면 쓸데없이 머릿속에서 리플레이된다. flush를 자주 하자...
RE: https://social.silicon.moe/@realgsong/114300412588845941