"AI^[1] 덕분에 ***가 민주적이 된다"는 말이 자주 나오고는 한다. 나는 이에 매우 회의적이다. 다른 것은 다 받아들여서 AI가 많은 사람들이 어떤 일을 매우 싸게 (거의 공짜로) 할 수 있게 해준다고 쳐도, AI로 만들어내기 힘든 수준의 "고급" 결과물은 여전히 존재하고, 이는 특정 직군의 고경력 전문가에게 넘어가게 된다. 문제는 이 "경력"을 어떻게 쌓느냐이다. 해당 직군의 초보자들은 AI에 밀려 경쟁력을 잃기 십상이고, 그들을 위한 여러 자리를 (AI를 활용하여 생산성을 높인) 전문가 한 명이 대체하기도 한다. 어떤 직군을 가질 수 있는 조건이 말하자면 이미 엄청난 실력을 가질 것이 되는 환경의 조성을 "민주적이다"라고 할 수 있을까?

원숭이가 키보드를 쳐도 수 억번 치면 확률상 실제 동작하는 프로그램이 나오는데, LLM이 로컬에서 브루트포스를 할 수 있는 때가 오면, 테스트 통과 조건만 깔짝대면 완성된 프로그램이 나오는 때가 얼마 안남았네요.

@ailrunAilrun (UTC-5/-4) LLM 요약 대신 글 앞 부분을 보여주는 옵션을 설정에 만들어 보도록 하겠습니다. 😅

생각보다 훨씬 자세하게 명문화된 규칙이 있군요.! 공부하면서 이 예시 저 예시 보다 보면, 버전이 널뛰고, 그러다 보면 HLS 지원이 오락 가락하게 되어, 사실 각 잡고 프로젝트에 쓰는 것 아니면, 의존도가 높지 않게 되어버리더라고요. 그 이유가 버전 지원 때문이란 생각에, 미리 HLS 친화적인 버전을 골라낼 수 있나 했는데, 그러긴 어려울 것 같네요.

각 버전대의 최신 버전인가 보네요.

HLS의 윙맨 같은 기능을 전면에 특징으로 내세우는 건가요? @ailrunAilrun (UTC-5/-4) @bglbgl gwyng

@ailrunAilrun (UTC-5/-4) @lionhairdino 아 이거 찾는중이었습니다ㅋㅋ hegel로 아무리 검색해도 안나왔는데 hazel이었네요.

에디터와 언어 문법 관계 얘기를 보다보니, parinfer 가 생각나네요. 이런 게 좀만 더 일찍 나왔더라면, 제가 Lisp를 지금보다는 잘하고 있었을지도 모르겠습니다. @bglbgl gwyng

@ailrunAilrun (UTC-5/-4) 정말 좋은 글 정말 감사합니다. 아직도 CS관련 글을 보다가 가로로 긴 직선만 나오면 "이거 내가 읽어도 되나?" 싶은 생각이 들면서 읽기를 포기하곤 하는데 기초적인 부분부터 너무 잘 설명해주셔서 끝까지 읽을 수 있었습니다. (사실 두번 읽었습니다.)

자연 연역의 E/I 룰에서는 항상 가정의 목록이 유지되거나 줄어들어 "가정의 소비(?)"된 정도를 기준으로 증명을 순차적으로 구성하거나 파악하는게 유리한 대신 전건과 후건을 다루는데 있어서 그 대칭성이 보이지 않는다. 대신 이와 동등한 논건대수에서는 추론 규칙에 전건과 후건 사이의 대칭성을 명백히 드러냄으로써 추론 시스템 자체의 특정 구조적인 성질을 이해하는데 유리할 수 있다.

라는 생각이 들었는데 이게 올바른 관찰일까요?

"이 내용들이 2 편에서 다룰 본격적인 논리와 자료 표현의 관계에 대해 흥미를 불러일으켰기를 바라며" -> 2편 정말 기대됩니다. ㅎ

"여론에 따라" 함수형 추상 기계 관련 글을 쓰고 있었는데, 쓰다 보니 논리와 low-level data representation 이 보였다는 핑계 말씀이지요? 생각할 엄두조차 내지 못했던 주제들, 다 이해는 못하지만 감사히 보고 있습니다. SPJ, 와들러 교수님 등의 교양 수준 강의 활동들을 보다 보면, 왜 국내 교수님(고인물-댓가없이 입문자들에게 도움을 준다는 의미)들은 없나 아쉬운데, 엘룬님 글로 조금 달래지네요. @ailrunAilrun (UTC-5/-4)

ㅋㅋㅋ 뭔가 “답정너" 느낌이 있는데요. 댓글 여론과 다른 ... 농담입니다. 전혀 불만 없이 기다리고 있겠습니다.@ailrunAilrun (UTC-5/-4)

@bglbgl gwyng 자연 연역, 즉 함수형 언어에서 (치환을 통해) "더 간단한 증명"을 해서 본문에 등장하는 문제를 피할 수 있는 것처럼 논건(論件) 대수에서도 (cut이 없는) "더 간단한 증명"을 할 수 있다는 이야기였습니다. 본문에서 설명이 조금 부족했던 것 같네요.

@ailrunAilrun (UTC-5/-4) 좋은 글 감사합니다!

저런 식의 증명 대신 L에서 x가 등장하는 자리에 M을 치환해넣고, y가 등장하는 자리에 N을 치환해넣은 증명 또한 가능하기 때문이다. 이 직관을 구체화한 것이 바로 다음의 cut 제거 정리이다.

요부분이 좀 헷갈리는데요, 글에서 소개된 Sequent Calculus에서는 치환에 대한 설명이 없는 것으로 보입니다. 함수형 언어에서의 치환에 해당하는 Sequent Calculus에서의 규칙이 추가로 필요한데 생략하신 걸까요, 아니면 글의 내용만으로 설명가능한데 제가 뭔가 놓친걸까요?

에디터의 플러그인도 Nix로 관리하고 싶다. 에디터 쪽에서 지원을 해야하는데, 누군가 총대매고 해줄법도 한데...

논리와 low-level data representation을 다뤄볼지, 아니면 함수형 추상 기계들(Turing Machine같은 것이지만 함수형을 위한 것들)을 다뤄볼지$\ldots$ 딱 결론이 나질 않는다 ☠️

완전한 검정 배경에 하얀 글자는 대비가 높아, 눈에 잔상이 남습니다. 눈의 피로를 덜기 위해 다크 모드를 주 톤으로 선택했다면, 대비를 적당 수준으로 낮춰야 합니다. 나이가 올라갈 수록 영향을 받습니다. 모르시는 분들이 많은 것 같습니다.

9.6 전에는 실수로 허용되던 것이란 말이 나와, 학문적 정 부 의 가치가 있는 줄 알았습니다. @ailrunAilrun (UTC-5/-4) @bglbgl gwyng

답 댓글이 아니라, 질문 댓글입니다. 레코드 업데이트 하는 동안에 반드시 레코드 타입을 먼저 알아야 한다는 게 "정상"이라는 거지요?

bar :: T Int
-- bar = emptyT --- 허용
bar = emptyT { x = [3] } --- 레코드 업데이트 중에는 타입 specialize를 못하니 불가

@bglbgl gwyng

@ailrunAilrun (UTC-5/-4) 말씀하신대로 저 변경사항이 오류랑 관련이 없는거 같아 아리송한 와중에, 저게 9.4 -> 9.6의 컴파일러 변경 사항이 저거밖에 없어서 오리무중에 빠졌네요. 빨리 재현 코드를 만들어봐야겠습니다.

https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.6#superclass-expansion-is-more-conservative

내가 9.4 -> 9.6 마이그레이션에서 겪고 있는 문제가 이거랑 관련이 있는거 같은데(확실치 않음)... 9.4에서는 c :: Type -> Constraint 일때 forall c. c Int 뭐 이런 조건이 있으면, 모든 c에 대해 c Int가 존재하는게 말이 안되는데도 실제로 c Int 꼴로 쓰이는 c만 고려해서 타입체크를 통과시켜줬던거 같다(이것도 확실하지 않음). 근데 9.6에선 당연히 거부당한다.

위의 내 이해가 맞다면 9.4의 constraint solving 완전 무근본이었단건데, 이건 또 믿기 어렵다(하스켈의 설계 결정에 대한 신뢰 유지한다고 하면). 어디서 내가 잘못 파악한거지.

adjoint도 두 개가 짝을 이뤄 뭔가를 완성하는 느낌이 있었는데, dual도 뭔가 시스템이 완성?안정?된 느낌도 들고 그러네요.
아직 콕 짚지는 못하지만, 프로그램 설계할 때, 기계적으로 따르기만 해도 도움이 될 것 같은 요소가 있을 것만 같아서, 가끔 이해하고 싶은 욕구가 생기는데, "화살표를 싹다 뒤집으면 듀얼"이야 같은 말로는 응용할 수 있을만한 이해에 도달을 못하고 있습니다. 인문학스런 해석 질문은 그만 드려야겠지요. @ailrunAilrun (UTC-5/-4)

아하!하고 답 달려고 고민했는데, 역시나 어렵네요. 둘이 서로 반쪽같은 것들로, 둘을 가지고 있으면 뭔가 되는 그런 "느낌"이라고 뿐이 감이 안오네요. 0에서 +1로 갔다가 -1로 오면 "역"이지만, 0에서 +1로 가고, 0에서 -1로 가는 건 듀얼로 볼 수 있겠지요? 똑 떨어지지 않는 인문학 같아요. @ailrunAilrun (UTC-5/-4)

거의 15년 전에 야심 넘치게 Benjamin C. Pierce의 Types and Programming Languages를 한 권 장만했지만 아직도 아주 깨끗하다. 앞으로도 읽을 일이 없을 것 같다… ㅋㅋㅋ

듀얼은 일반인이 이해하게, 간단한 문장으로 똑 떨어지게 설명하기 어렵네요 (관련 전공자 아님)

@lionhairdino @domatdo도막도 다른 글에서 CBPV의 컴파일에 대해 다룬다면 이야기하겠지만 CBPV의 경우 jump와 연관된 건 thunk에 더 가깝습니다.

@lionhairdino @domatdo도막도 함수의 경우에는 그냥 완전히 다른 해석을 하고 있기 때문이라고 보시면 됩니다. 원래의 람다 함수를 기계 수준에서 이해하려고 한다면 함수 정의로 jump하는 개념을 항상 포함하고 있다고 볼 수 있습니다. 이와는 다르게 CBPV는 값과 계산을 나눔으로서 람다 함수를 그냥 빼내기 연산(Pop) 이후 다른 연산을 이어하는 것으로 바꾼 거지요.

(비전공자가 볼 내용은 아닌 것 같긴 한데요.) 취미 공부하는 사람의 질문입니다.
"인자를 받는다"는 행위를
"인자를 스택에 넣는다" 와 "인자를 스택에서 빼낸다" 둘 로 쪼개어
보는 아이디어에서 시작하는 것으로 보면 되나요?
그래서 adjoint란 용어가 아른 거리는 건가 싶습니다.

람다식을, 인자가 아직 들어오지 않아 reduce할 게 없는 값으로 볼 때는
[1.인자를 스택에 push ---2.인자를 스택에서 pop] 이 없어 reduce할 게 없는 상태로 봤는데,
CBPN에선 [2.인자를 스택에서 pop]은 있고, 이 걸로 reduce할 게 있는 상태.
로 본다는 얘기인가요?

위 설명에서 질문하고 싶은 것도 한 가득이고, @domatdo도막도 님의 이어지는 질문도 어렵긴 한데, 뭔가 전부는 아니더라도 "제가 필요한 정도"의 것은 건져갈 게 보이는 것 같아 질문드립니다.
@ailrunAilrun (UTC-5/-4)

@ailrunAilrun (UTC-5/-4) (force . thunk) m = m이라 볼 수 있지 않았나요?

@ailrunAilrun (UTC-5/-4) 아, thunk . force라고 해야 했는데 force . thunk라 했네요..! 그리고 다시 생각하니 thunk . force도 항등 사상이 맞군요…

@domatdo도막도 그 둘이 사실 수반 함자(Adjoint Functor)의 구현입니다. 강한 형 CBPV를 사용하면 thunk(-)는 Up -의 생성자고 return은 Down -의 생성자인데요, 이 두 함자 Up과 Down이 수반 함자 쌍을 이룹니다.

@ailrunAilrun (UTC-5/-4) 재밌게도 force . thunk랑 return . thunk 모두 항등 사상이 못 되네요. 이건 값이 ‘~인 것‘이기 때문일까요? ~인 것을 갖고 무언가를 더 하기 위해서 return과 to가 있는 것인가 싶어졌어요.

@ailrunAilrun (UTC-5/-4) 재밌게도 force . thunk랑 return . thunk 모두 항등 사상이 못 되네요. 이건 값이 ‘~인 것‘이기 때문일까요? ~인 것을 갖고 무언가를 더 하기 위해서 return과 to가 있는 것인가 싶어졌어요.

@ailrunAilrun (UTC-5/-4) 연구하고 계신 체계는 어떤 체계인가요?

@ailrunAilrun (UTC-5/-4) 람다 대수 스펙이 있다면 축약 방법은 Unspecified behavior라고 볼 수 있겠네요. 이곳저곳에서 Call-By-Push-Value를 자주 언급해서 궁금하던 찰나였는데 친절하게 설명해주신 덕분에 편하게 이해할 수 있었습니다. 늘 감사합니다.

Hackers' Pub의 문제는 아니고 Firefox랑 Linux 한글 입력기랑 JS기반 입력기의 환장의 콜라보같은데, 긴 글을 치다보면 한글 입력을 가끔 씹는다. 이를테면 "우주로 가자."고 치는데 "우주로 가." 같이 쳐지는 상황$\ldots$ 써진 걸 확인하면 될 일이지만 약간 "Zone"에 들어가서 정신없이 치다가 한 서너줄 전에 글자 하나 빠진 거 발견하면 아주 돌아버린다$\ldots$

함수형을 공부하기 전, 함수 작업?의 대상을 {함수, 인자}로만 인식했었는데, {함수, 인자, 적용}으로 인식하기 시작하면서 편해지는 게 많아졌습니다. 그런데 이게 편한 이유가 다른 배경 지식이 생겨서 그런 건지, 이 길로 가는게 쉬운 길이어서 그런 건지는 잘 모르겠습니다. 여기서 시작하면 $와 <$>가 자연스러워 보였습니다. 혼자 결론에 도달하고는, 누군가가 처음 공부할 때 알려줬으면 좋았겠는데 싶었습니다. 그냥 혼자 생각입니다.

꾸벅 꾸벅 조는 건 완전 동의입니다. 제가 혼자 그 공부하면서 졸았습니다. @xtjuxtapose

@curry박준규 더 primitive한 의미론을 포착해서 문법 요소로 만들고 그걸로 다양한 정의를 하게 하는게 낫다는 점에선 동의하는데요. 말씀하신 기준을 그대로 적용해버리면, 모든 언어들이(하스켈도 포함) 발전할수록 점점 키워드가 추가되는데, 그때마다 점점 더 안 좋아졌다고 하면 좀 이상하죠.

@bglbgl gwyng 이게 생각해보니 ‘문법이 복잡하다’, ‘문법 요소가 적다’라는 표현이 구체적이지 않은 것 같습니다. 갑자기 언어 확장이 떠오르면서 ‘문법 안 복잡한 거 맞나?’ 싶네요. 그래서 표현을 좀 바꾸면 저는 사전에 정의된 키워드가 적을 수록 좋다고 생각합니다.

@lionhairdino :%!foo가 파일의 전체 내용을 foo의 출력으로 대체하는 방식이다 보니 그런 것 같습니다.