Hyunjoon Kim

@d01c2@hackers.pub · 32 following · 28 followers

Yet another PL enthusiast a.k.a. Hyunjoon Kim, d01c2 plz read my nickname as 'dolce'.

Hyunjoon Kim shared the below article:

How to pass the invisible

洪 民憙 (Hong Minhee) @hongminhee@hackers.pub

This post explores the enduring challenge in software programming of how to pass invisible contextual information, such as loggers or request contexts, through applications without cumbersome explicit parameter passing. It examines various approaches throughout history, including dynamic scoping, aspect-oriented programming (AOP), context variables, monads, and effect systems. Each method offers a unique solution, from the simplicity of dynamic scoping in early Lisp to the modularity of AOP and the type-safe encoding of effects in modern functional programming. The post highlights the trade-offs of each approach, such as the unpredictability of dynamic scoping or the complexity of monad transformers. It also touches on how context variables are used in modern asynchronous and parallel programming, as well as in UI frameworks like React. The author concludes by noting that the art of passing the invisible is an eternal theme in software programming, and this post provides valuable insights into the evolution and future directions of this critical aspect of software architecture.

Read more →
11
1
0
9

오늘 발견한 흥미로운 링크들: Matt 타입스크립트 선생님은 종종 Effect 에 대해 트윗하는데 주로 이펙트를 찍먹해보시고 이걸 강의로 만들까말까 만들까말까 하신다. Michael EffectTS 의 BDFL 은 종종 맷 선생의 트윗에 답글을 달아 이펙트 얘기를 풍부하게 가꿔주신다.

오늘은 이펙트의 굿파츠에 대한 얘기로 스레드가 열렸다. https://x.com/mattpocockuk/status/1936083553483157714

나도 EffectTS 도입을 하고 싶지만 여러모로 기존 바닐라JS 스펙과 다른 모양의 코드가 나와서 여러모로 망설이고 있다. (내 기준 이펙트는 실행 코드를 작성하기 보다 실행 계획을 작성하는 개념으로 접근하고 있다) 프로덕션 코드를 새로 만든다면 EffectTS 도입을 고려하고 있지만 학습 난의도가 있어 이를 위해 함께 스터디하고 코드 마이그레이션 계획도 세워야하는데, 그럴 여유는 보통 없는게 현실.

아직은 neverthrow 부터 사용해보는 정도가 지금의 최선이라고 생각한다. 나는 throw 기반의 조건 제어 코드가 불편하다. try catch 안에서 if 절로 throw 하는 코드를 볼 때마다 불만이다. 복구할 수 있는 에러는 throw 하지 않는게 옳다고 생각한다. 물론 언어의 문제도 있지만... 그렇게 스레드를 읽던 중 effectively 라는 애매한 이름의 Alegbraic effects 를 구현한 라이브러리가 공개되어 있다는 것을 발견했다. 작성자 본인도 뻔뻔하게 홍보한다고 어필하고 있다. ;) effectively

EffectTS 라는 이름도 애매하지만 Effectively 는 더 애매하다. 인기가 많아지기 전에 그럴듯 한 이름으로 브랜딩되면 좋겠다. 아, 그렇게 생각하는 이유는 TS 씬에 이런 라이브러리/프레임워크가 자주 거론되면 좋겠다는 생각 때문이다.

얘기하고 싶은 것은, 아이러니하게 이 effectively 의 readme 가 매우 간결하고 읽기 쉽게 EffectTS 에 대해 소개하고 있기 때문이다. effect.website 의 문서는 뭔가 개선이 필요하다. 없는게 없이 다 있지만 실제 읽다보면 어려운 부분이 많고 더 많은 설명이나 예제가 필요한 경우가 생긴다. 미카엘 본인도 문서 개선 필요는 공감하는 것 같다. (해당 스레드 발언 추정) 그리고 또 다른 유저가 포스트를 안내해주셨는데, Effect-like code without Effect 짧게 읽기 좋다. 게다가 이 포스트가 담긴 사이트의 프로덕트도 유용해 보인다.

시작부터 Result 나 Optional 을 제공하는 언어가 많은 소프트웨어 엔지니어들에게 높은 선호도를 가지는 이유가 있다고 본다.

5

나: 건전한 육신에 건전한 정신이 깃든다(Sound body ⇒ Sound mind) ⇔ 건전하지 않은 정신이라면 육신도 건전하지 않다 (¬Sound mind ⇒ ¬Sound body)

@: 당신은 명제와 대우의 참값이 같다는 주장을 하며 배중률을 가정하고 말았습니다!!

나: 아 짜증나

5

@kodingwarriorJaeyeol Lee 님에게 들킨 김에 써보는

  • 퍼리입니다. 언젠간 해커스 펍을 털로 뒤덮으려는 아름다운 마음을 품고 있습니다.
  • 재작년 부터 web3 쪽으로 전향했고 주로 코어 쪽을 건들고 있습니다. 하지만 여전히 블록체인은 잘 모릅니다.
  • 언어 만드는걸 좋아하고 관련 프로젝트들에 기여를 하고 있습니다
  • 좋아하는 언어는 러스트와 OCaml인데 안 쓴지 오래되서 조만간 까먹을거 같네요
  • 파서나 상태머신, 정적분석을 좋아합니다. - 관련해서 요즘은 개발하고 있는 언어에 린터를 만들고 있습니다
  • 활자 중독입니다. 해커스펍은 읽을게 많아 좋네요. 책은 주로 철학이나 건축 쪽을 읽고 있습니다.
  • 의외로 백엔드나 프론트엔드를 해본적이 없어서 항상 애매한 포지션에 있는 것 같습니다.
  • 밴드활동도 하고 있습니다. 원래 대충 모여서 술마시는 것에 의의를 뒀었는데 올해는 공연 뛸 일이 많아졌네요.
  • 20대 중반이고 서울에서 거주 중입니다

여러모로 잘 부탁드립니다. 추가로 깃헙 프로필은 https://github.com/notJoon입니다.

낫준 배상

9
1
0

새로 오신 분들도 많이 계시니, 한 번 해 볼까요? 저부터 해보겠습니다.

  • Hackers' Pub을 만들고 운영하고 있습니다. (Hackers' Pub은 저희 집 홈 서버에서 돌아가고 있습니다… 😂)
  • 연합우주(fediverse)와 ActivityPub에 관심이 많고, 또 관련된 소프트웨어(@fedifyFedify: an ActivityPub server framework, @holloHollo :hollo:, @botkitBotKit by Fedify :botkit:, Hackers' Pub…)를 만듭니다.
  • 좋아하는 언어는 Haskell인데 자주 쓰는 언어는 TypeScript입니다. 예전에는 Python을 좋아하고 자주 썼습니다.
  • 함수형 프로그래밍을 좋아합니다만, 좋아하는 만큼 잘 다루는지는 잘 모르겠습니다.
  • 옛날에는 덕 타이핑 언어를 좋아했는데, 나이가 들고 협업을 많이 하게 되면서 정적 타이핑 언어를 선호하게 되었습니다. 그래도 여전히 덕 타이핑 언어가 제공하는 특별한 생산성이 있다고 생각합니다.
  • 자유 소프트웨어와 오픈 소스를 좋아합니다. GPL을 좋아하지만, 트랜스젠더 배제적인 행보를 보인 적 있는 자유 소프트웨어 재단이나 여러 성추행 전적이 있는 Richard Stallman은 좋아하지 않습니다.
  • 소프트웨어 문서화에도 관심이 많습니다. 문서화가 소프트웨어 개발의 중요한 부분이라고 생각합니다. 문서화 도구들에도 관심이 많습니다.
  • 원래는 백엔드 개발자였는데 바로 전 직장이 블록체인 회사여서 백엔드 개발에서 손을 놓은 지 좀 되니까 이제는 잘 모르게 됐습니다. 재활이 필요합니다.
  • 현재는 일 안 하고 쉬고 있습니다.
  • 30대 후반, 기혼, 자녀는 없습니다. 서울에서 살고 있습니다.

아무쪼록 잘 부탁드립니다.

17
0
0

Hyunjoon Kim shared the below article:

데이터 효율성으로 본 AI와 인간의 비교

bgl gwyng @bgl@hackers.pub

이 글은 AI와 인간의 능력 비교에서 데이터 효율성의 중요성을 강조하며 시작합니다. 현재 AI는 인간에 비해 데이터 효율성이 떨어지지만, 일단 학습된 능력은 복제 가능하다는 점을 지적하며 콜센터 직원과 같은 직업군에 대한 위협은 여전하다고 설명합니다. 데이터 효율성이 중요한 경영인과 연구자는 AI를 유용한 도구로 활용할 수 있지만, 인간의 데이터 효율성이 정말 높은지에 대한 의문을 제기합니다. Yann Lecun의 주장을 인용하여 인간이 받아들이는 데이터 양이 AI 학습에 쓰이는 양보다 적지 않음을 언급하며, 인간은 데이터를 있는 그대로 학습하지 않고 편향에 기반하여 학습한다는 흥미로운 주장을 제시합니다. 마지막으로, AI에게 인간처럼 무모한 결론을 내리도록 가르치는 것이 옳은지에 대한 질문을 던지며, 압도적인 양의 데이터를 통해 더 많은 진실을 알아낼 수 있는지에 대한 고민으로 마무리합니다. 이 글은 AI 개발 방향에 대한 새로운 시각을 제시하며 독자에게 깊은 생각거리를 제공합니다.

Read more →
8
4

Hyunjoon Kim shared the below article:

논리와 메모리 - 논리와 저수준(Low-level) 자료 표현(Data representation) (2 편 중 2 편)

Ailrun (UTC-5/-4) @ailrun@hackers.pub

이 글은 "논리적"이 되는 두 번째 방법인 논건 대수를 재조명하며, 특히 컴퓨터 공학적 해석에 초점을 맞춥니다. 기존 논건 대수의 한계를 극복하기 위해, 컷 규칙을 적극 활용하는 반(半)공리적 논건 대수(SAX)를 소개합니다. SAX는 추론 규칙의 절반을 공리로 대체하여, 메모리 주소와 접근자를 활용한 저수준 자료 표현과의 커리-하워드 대응을 가능하게 합니다. 글에서는 랜드(∧)와 로어(∨)를 "양의 방법", 임플리케이션(→)을 "음의 방법"으로 구분하고, 각 논리 연산에 대한 메모리 구조와 연산 방식을 상세히 설명합니다. 특히, init 규칙은 메모리 복사, cut 규칙은 메모리 할당과 초기화에 대응됨을 보여줍니다. 이러한 SAX의 컴퓨터 공학적 해석은 함수형 언어의 저수준 컴파일에 응용될 수 있으며, 논리와 컴퓨터 공학의 연결고리를 더욱 강화합니다. 프랭크 페닝 교수의 연구를 바탕으로 한 SAX는 현재도 활발히 연구 중인 체계로, ML 계열 언어 컴파일러 개발에도 기여할 수 있을 것으로 기대됩니다.

Read more →
12

Hyunjoon Kim shared the below article:

논리적이 되는 두 가지 방법 - 논리와 저수준(Low-level) 자료 표현(Data representation) (2 편 중 1 편)

Ailrun (UTC-5/-4) @ailrun@hackers.pub

이 글은 어떤 문장이 "논리적"이라고 할 수 있는지에 대한 심도 있는 탐구를 시작합니다. 일상적인 오용을 지적하며, 진정으로 논리적인 주장은 증명 가능성과 체계의 무모순성이라는 두 가지 핵심 조건을 충족해야 한다고 주장합니다. 특히, "좋은 가정 아래" 논리성을 증명하는 두 가지 방법, 즉 함수형 언어와 유사한 구조를 가진 자연 연역과, 약간의 "부정행위"를 통해 무모순성을 쉽게 보일 수 있는 논건 대수를 소개합니다. 글에서는 명제와 판단의 개념을 명확히 정의하고, 자연 연역을 통해 논리적 증명을 구축하는 방법을 상세히 설명합니다. 특히, 자연 연역과 함수형 언어 간의 놀라운 유사성, 즉 커리-하워드 대응을 통해 논리적 사고와 프로그래밍 언어 이해 사이의 연결고리를 제시합니다. 또한, 자연 연역의 한계를 극복하고 무모순성을 보다 쉽게 증명할 수 있는 논건 대수를 소개하며, 자연 연역과의 구조적 차이점을 강조합니다. 이 글은 논리적 사고의 깊이를 더하고, 프로그래밍 언어와 논리 간의 관계에 대한 흥미로운 통찰을 제공합니다. 특히, 커리-하워드 대응을 통해 논리와 프로그래밍이 어떻게 연결되는지 이해하고 싶은 독자에게 유익할 것입니다.

Read more →
12
3
4

Hyunjoon Kim 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(nlog⁡n)O(n\log{n})같다.

등이 있다. 이렇게 어떤 두 대상이 같은지에 대해서 이야기를 하다보면 반대로 어떤 두 대상이 같지 않은지에 대해서도 이야기하게 된다. 즉,

  • x+4x + 422로 나눈 나머지는 x+1x + 122로 나눈 나머지와 같지 않다.
  • 연결 리스트(Linked List)와 배열(Array)은 같지 않다.
  • 함수 λ x→x\lambda\ x \to x와 정수 55같지 않다.

같은 것과 판정 문제(Decision Problem)

이제 컴퓨터 과학(Computer Science)과 프로그래밍(Programming)에 있어 자연스러운 의문은 "두 대상이 같은지 아닌지와 같은 답을 주는 알고리즘(Algorithm)이 있나?"일 것이다. 다시 말해서 두 대상 aabb를 입력으로 주었을 때

  • 알고리즘이 참 값(True\mathtt{True})을 준다면 aabb가 같고
  • 알고리즘이 거짓 값(False\mathtt{False})을 준다면 aabb가 같지 않은

알고리즘이 있는지 물어볼 수 있다. 이런 어떤 명제가 참인지 거짓인지 판정하는 알고리즘의 존재 여부에 대한 질문을 "판정 문제"("Decision Problem")라고 하며, 명제 PP에 대한 판정 문제에서 설명하는 알고리즘이 존재한다면 "PP는 판정 가능하다"("PP is decidable")고 한다. 즉, 앞의 질문은 "임의의 aabb에 대해 aabb가 같은지 판정 가능한가?"라는 질문과 같은 의미라고 할 수 있다.

이 질문에 대한 대답은 당연하게도 어떤 대상을 어떻게 비교하는지에 따라 달라진다. 예를 들어 우리가 32 비트(bit) 정수에 대해서만 이야기하고 있다면 "임의의 32 비트 정수 aabb에 대해 aabb가 각 비트별로 같은지 판정 가능한가?"라는 질문에 대한 답은 "그렇다"이다. 반면 우리가 비슷한 질문을 자연수를 받아 자연수를 내놓는 임의의 함수에 대해 던진다면 답은 "아니다"가 된다.[1]

그렇다면 어떤 대상의 어떤 비교에 대해 판정 문제를 물어보아야할까? 프로그래머(Programmer)로서 명백한 대답은 두 프로그램(Program)이 실행 결과에 있어서 같은지 보는 것일 것이다. 그러나 앞서 자연수를 받아 자연수를 내놓는 함수에 대해 말했던 것과 비슷하게 두 프로그램의 실행 결과를 완벽하게 비교하는 알고리즘은 존재하지않는다. 이는 우리가 두 프로그램의 같음을 판정하고 싶다면 그 같음을 비교하는 방법에 제약을 두어야 함을 말한다. 여기서는 다음의 두 제약을 대표로 설명할 것이다.

  1. 문법적 비교(Syntactic Comparison)
  2. β\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);

두 프로그램 모두 x5라는 값을 할당하고 5를 콘솔에 출력하나, 첫번째 프로그램은 = 5;를, 두번째 프로그램은 = 3 + 2을 사용하여 5를 할당하고 있기 때문에 문법적으로 다르다.

문법적 비교는 이렇게 문법만 보고서 쉽게 판정할 수 있다는 장점이 있으나, 두번째 예시처럼 쉽게 같은 행동을 함을 이해할 수 있는 프로그램에 대해서도 "같지 않음"이라는 결과를 준다는 단점을 가진다. 혹자는

3 + 2같은 계산은 그냥 한 다음에 비교하면 안돼? 컴파일러(Compiler)도 상수 전파(Constant Propagation) 최적화라던지로 3 + 25로 바꾸잖아?

라는 생각을 할 수도 있을 것이다. 이 제안을 반영한 방법이 바로 β\beta 동등성이다.

2. β\beta 동등성

바로 앞의 소절에서 단순 계산의 추가에 의해 같음같지 않음으로 변하는 것을 보았다. 이런 상황을 피하기 위해서는 같음을 평가할 때 프로그램의 실행을 고려하도록 만들어야 한다. 가장 대표적인, 대부분의 프로그래밍 언어(Programming Language)에 존재하는 프로그램의 실행은 함수 호출이다. 따라서 함수 호출을 고려한 같음의 비교는 f(c)와 함수 f의 몸체 b 안에서 인자 xc로 치환한 것을 같다고 취급해야한다. 예를 들어

let f = (x) => x + 3;

이 있다면, f(5)5 + 3 혹은 8을 같은 프로그램으로 취급해야한다. 이 비교 방법의 큰 문제는 함수가 종료하는지 알지 못한다는 것이다. 두 프로그램 ab를 비교하는데, a가 종료하지 않는 함수 l을 호출한다면, 이 알고리즘은 "같음"이나 "같지 않음"이라는 결과를 낼 수조차 없다. 즉, 올바른 판정법이 될 수 없다.

더 심각한 문제는 아직 값을 모르는 변수가 있는 "열린 프로그램"("Open Program")에 대해서도 이런 계산을 고려해야한다는 것이다. 다음의 JavaScript 예시를 보자.

let g = (x) => f(x) + 3;
let h = (x) => (x + 3) + 3;

gh는 같은 프로그램일까? 우리가 gh가 같은 프로그램이기를 원한다면 f(x)x + 3을 같은 프로그램으로 보아야한다. 대부분의 프로그램은 함수 안에서 쓰여지기 때문에 프로그램의 비교는 거의 항상 gh의 몸체와 같은 열린 프로그램들의 비교이다. 따라서 gh를 다른 프로그램으로 본다면 계산을 실행하여 두 프로그램을 비교하는 의미가 퇴색되고 만다. 그렇기 때문에 우리는 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 + 35로 계산하면 되잖아?"

그렇다. 이런 의존 형에 β\beta 동등성을 적용하면 우리가 원하는 형을 바로 얻어낼 수 있다. Vector (2 + 3) aVector 5 a같은 형이기 때문이다. 더욱이, 의존 형의 경우 종료하지 않는 부속 프로그램이 잘못된 형을 줄 수 있기 때문에 많은 경우 종료하지 않는 부속 프로그램을 어차피 포함하지 않는다. 다시 말해, 앞서 말한 제약 조건 즉 모든 부속 프로그램이 종료해야만 한다는 제약조건은 의존 형의 경우 상대적으로 훨씬 덜 심각한 제약조건이 되는 것이다.

이런 의존 형에 있어서의 β\beta 동등성 검사를 "변환 검사"("Conversion Check")라고 하며, 두 형이 β\beta 동등일 경우 이 두 형이 서로 "변환 가능하다"("Convertible")라고 한다. 이 변환 검사는 의존 형이론 구현에 있어서 가장 핵심인 기능 중 하나이며, 가장 잦은 버그를 부르는 기능 중 하나이기도 하다.

마치며

이 글에서는 같음과 같지 않음의 판정 문제에 대해 간략히 설명하고 프로그램의 같음을 판정하는 법에 대해서 단순화하여 다루어보았다. 구체적으로는 문법 기반의 비교와 β\beta 동등성을 통한 비교로 프로그램의 같음을 판정하는 법을 알아보았고, 이 중 β\beta 동등성이 적용되는 가장 중요한 예시인 의존 형이론을 β\beta 동등성을 중점으로 짤막하게 설명하였다. 마지막 문단에서 언급했듯 의존 형이론의 구현에 있어서 β\beta 동등성을 올바르게 구현하는 것은 가장 중요한 작업 중 하나이기에, 최근 연구들은 β\beta 동등성의 구현 자체를 의존 형이론 안에서 함으로서 검증된 β\beta 동등성의 구현을 하기 시작하고 있다. 이 글이 같음과 같지 않음과 판정 문제 그리고 β\beta 동등성에 있어 유용한 설명을 내놓았기를 바라며 이만 줄이도록 하겠다.


  1. 두 함수가 같다라고 보는 방법에 따라 다르나, 두 함수가 항상 같은 값을 가진다면 같다고 하자. 이때 함수의 판정 문제는 정지 문제(Halting Problem)와 동일하다. 임의의 튜링 기계(Turing Machine) ff가 입력 nn을 받았을 때 종료하면 g(n)=1g(n) = 1, 아니면 g(n)=0g(n) = 0이라고 하면 이 함수 gg와 상수 함수 c(n)=1c(n) = 1가 같은 함수임을 보이는 것은 ff가 항상 종료한다는 것을 보이는 것과 동등하다. ↩︎

Read more →
5
2
2