@curry박준규 all을 다음과 같이 정의하면 문제가 무엇일까요?

all p [] = False
all p [x] = p x
all p (x:xs) = p x && all xs

이 질문에 대한 대답 중 all의 의미에 관한 것이 있을 겁니다. 논리적으로 "모든 ...에 대해"를 어떻게 이해해야 하는냐에 대한 것 말이지요.

공집합을 직접 사용하는 것이 가장 간단한 예시겠지만, 좀 더 논리학에서 자주 사용되는 예시로는 "20세기의 모든 프랑스 왕은 대머리다"가 있겠습니다. 이는 무의미하게 (Vacuously) 참인데요, 왜냐면 19세기를 마지막으로 프랑스에는 더 이상 왕이 없기 때문이지요. 즉, 일반적으로 "모든 ...에 대해"에서 "..." 부분이 (결과적으로) 공집합일 경우 "모든 ..."에 의해 수식된 본문이 어떤 문장인지와는 상관 없이 참이라고 이해한다는 것이지요.

살짝 다른 차원에서 확장해서 바라보는 얘기이긴 한데 그냥 첨언하자면 언어학의 하위 분야인 화용론에서 전제(Presuppositions)라는 주제랑 연결되는 것 같네요. 댓글에 프랑스 왕은 머머리다 예문도 써주신 걸 보니 더욱 더 그런 것 같고요. 간단하게 설명드리자면, 일단 한국어 예문으로 하면 살짝 오해의 소지가 있어^[1] 영어 예문을 갖고 쓰면 다음과 같이 생각해볼 수 있습니다.

• P: The King of France is bald.^[2]
• Q: There exists an entity that is King of France.

이 때 P의 명제가 참일 수 있는 이유는 Q를 전제로 깔고 가기 때문입니다. 이렇게 Q를 전제로 갖고 가면 P에 부정을 넣어도 (The King of France is not bald 혹은 ¬(The King of France is bald)) 여전히 그 명제는 참입니다. 하지만 실제 현실에서 Q는 거짓입니다. 왜냐하면 오늘날 프랑스는 군주국가가 아니니깐요. 그럼에도 불구하고 P는 여전히 참을 진리값으로 가지죠.

따라서 실제로 전제를 이렇게 정의하기도 합니다 (Levinson, 1983, p. 175).

• A sentence P sematically presupposes a sentence Q iff:
• (a) P ⊨ Q
• (b) ~P ⊨ Q

참고로 여기서 "⊨"는 "함의한다"를 지칭하는 기호입니다 (예: "하스켈은 함수형 언어다."란 문장은 "하스켈은 언어다"란 걸 함의하죠.).

그렇다면 Q가 전제되는 건 알겠는데, 이 진리값이 무엇이느냐에 대한 질문이 생길 수 있습니다. 이에 대해서 언어학자들은 보통 크게 두 가지로 봅니다. 하나는 참으로 간주하는 거고, 다른 하나는 참도 거짓도 아니다라고 보는 거죠. 전자같은 경우엔 어떻게 보면 기계적으로 바라보는 거고, 후자의 경우엔 참/거짓이라는 기존 이치논리(two-valued logic) 혹은 1 또는 0으로 하는 불 논리에서 확장해서 Kleene의 삼치논리(three-valued logic)로 가게 되죠.

참고로 전제 성립 여부 포함 화용론 전체에서 깔고 가는 가장 큰 가정이 하나 있는데, 이 경우에는 바로 해당 발화(utterance) P, 즉 '프랑스왕은 머머리다'라는 명제가 이루어질 때 화자와 청자가 프랑스에는 왕이란 개체가 존재한다(=Q)라고 암묵적으로 서로 동의한다라는 가정입니다.

발음이 재밌는데요. 우리말로 하면 뽀ㄹ겠다에 가깝나 본데요. 언젠가 퀘백가면, 같이 뽀겠다와 흑맥주 달릴까요? @ailrunAilrun (UTC-5/-4)

뭔가 족발 식감 같은 건가요? @ailrunAilrun (UTC-5/-4)

오호, D는 그냥 Day라 하는데, T는 뭘까요? @ailrunAilrun (UTC-5/-4)

해커스 퍼블릭 D-30분..이 아니라 H-30
D Day는 하루 단위로만 쓴다네요.

GHCup 오랜만에 다시 설치하는데 못보던 게 생겼다.

GHCup provides different binary distribution "channels". These are collections of tools
and may differ in purpose and philosophy. First, we select the base channel.

[S] Skip  [D] Default (GHCup maintained)  [V] Vanilla (Upstream maintained)  [?] Help (default is "Skip").

https://well-typed.com/blog/2025/08/standard-chartered-supports-haskell-ecosystem/
제일은행을 먹은 SC(Standard Chartered)가 하스켈 생태계에 돈을 보태겠다네요. SC가 하스켈을 프로덕트에 조금씩 쓰고 있다는 얘기는 들은 적 있는데... 뭐 얼마나 후원하는지는 자세히는 안나와 있습니다만, 대기업 돈이 들어오면, 긍부정적 변화가 생기긴 하는데.. 툴체인이 정돈된다든지 해서 입문자한테 도움이 되는 변화가 생기면 좋겠습니다. 하스켈을 JS로 트랜스파일링 하는 컴파일러도 있는데, 막상 쓰려고 보면, 난이도가 너무 높아요.

시장 조사 중인 거지요? SMT solver?는 좀 더 전공자용 같고, Lens는 업자도 자주 쓰는 것 같습니다. 언제나 둘 다 쓰자에 한 표지만, 시간 관계상 하나만 쓴다면, Lens에 한 표 던지겠습니다. @ailrunAilrun (UTC-5/-4)

@ailrunAilrun (UTC-5/-4) 고쳐놓도록 하겠습니다!

웬일이래유... 엘룬님이 다른 분 초대를 다하고.ㅎ @ailrunAilrun (UTC-5/-4)

문법 강조가 바뀔 때가 한참 지난 것 같은데, AI가 별의별 걸 다하는 세상에 아직도 눈에 보이는 소식들이 없네요. 예를 들면, 식별자(변수), 함수, 등 문법 요소에 따라 색을 입힌다거나 하는 게 아닌,
전역이냐, 로컬이냐로 색을 달리 한다든지,
오른쪽 우선 결합 연산자면 빨간색, 왼쪽 우선 결합이면 파란색 한다든지,
시맨틱 문법 강조가 일반화 될 때가 된 것 같은데, 혹시 저만 모르고 있는 건가요?

a = f a 일 때, a를 f의 고정점이라 하니
m a = m (m a) 가 된다면, m a를 m의 고정점이라 할 수 있다.
모나드는 m a = m (m a)가 안되는 것을 join, return의 도움을 받아 성립하게 만든다.
그래서 m의 고정점을 바로 m a라 할 순 없지만, join, return의 도움으로 고정점처럼 동작하게 할 수 있다.
처럼 설명해도 되나 싶습니다.

여러 번 작업 한 걸, 한 번의 작업으로 표현한다.
반대에서 출발해서 보면, 한 번의 작업을 여러 번의 작업으로 인수 분해한다.

이런 목적 측면에서 보면, 고정점도 모나드도 하나의 궤로 설명할 수 있지 않을까 싶습니다.

그냥 상상입니다.

주의: 프로그래머에게도 수학도에게도 쓸모 있지 않은 그저 생각 놀이로, 어제 모임에서 제가 떠들었던 잡담입니다.

튜링 완전한 프로그램은 따로 메모리를 두어 관리하며 돌아가는데, 람다 산법은 이런 메모리가 없는데도 불구하고, 튜링 완전이 할 수 있는 일은 모두 할 수 있다고 합니다. 왜 그럴 수 있는지, 시작 아이디어가 뭘까 생각해 봤습니다. (슬쩍 보기엔, 학문적으로 긴 여정이 있는데, 그 걸 모두 따라가기엔 벅찬 일이라, 절대 따라가고 싶진 않고, 그저 아이디어 정도만 알고 싶습니다.)

함수형에선, 정보를 "기억memory"하는 역할도 역시 함수가 담당합니다. 기억이 필요할 땐 함수 구조를 주어, 기억 공간을 만든다고 볼 수 있습니다. 함수 합성에서 다음 함수의 인자로 새로 바인딩하며 기억의 역할을 합니다. 애초 메모리 모델이 없는 게 아니라, 다른 구조로 메모리 모델을 구현했다고 볼 수 있는 것 아닌가 싶습니다. (이렇게 말하는 곳은 없습니다.)

람다 함수는, "따로 호출할 일이 없어 이름 없는 함수로 정의한다" 쯤으로 넘어가기엔, 숨어 있는 의미가 너무 큽니다. 분명, 이렇게 넘어갈 일이 아닌데, 역시나 친절히 설명해주는 자료를 아직은 못봤습니다. (많이 찾아 보 거나, 깊게 공부한 건 아니라서, 어딘가에는 있지 않을까 싶어요)

람다 함수로 만들어,

• 실행 시점 제어
• 함수 합성 체인 참여
• 필요한 정보들을 모아 두는 단위
• 외부와 소통하는 길을 만들어 둘 수 있고, ...

여기에 기억이라는 중요한 역할도 담당하게 합니다.

람다 산법은 매개 변수, 함수 몸체, 적용, 이렇게 3가지 요소만으로 모든 걸 해결합니다. 알론조 처치 아저씨는 어찌 이런 구조를 떠올렸을까 싶습니다. 애초에 위와 같은 식으로 볼 수 있는 함수 통찰의 눈이 먼저 있었던 상태에서 만든 거겠지요?

"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를 한 권 장만했지만 아직도 아주 깨끗하다. 앞으로도 읽을 일이 없을 것 같다… ㅋㅋㅋ

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