Scala의 given - using을 사용한 Effect 모사는 아마 Capability Passing Style에 가까우니까 Effekt의 해석을 따를 거로 본다.

(위 트윗의 koka 코드도 그렇고 이 트윗의 effekt 코드도 그렇고 귀찮아서 대충 Gemini 시켰다. 틀려도 양해 바란다)

반면 Effekt의 Capability Passing Style 멘탈 모델로 생각하면 약간 양상이 달라지는데, Capability는 값 주입의 관점으로 보기 때문에 Effect를 it happens가 아니라 it requires로 본다. 그래서 named handler 같은 코드를 이렇게 쓴다. 걍 computation을 받는 함수인 것.

fun swap[A]() {h1: State[A]} {h2: State[A]}: Unit = {
  val a = h1.get();
  val b = h2.get();
  h1.set(a);
  h2.set(b);
}

koka는 happens지만 effekt는 requires다. 하지만 named handler에서는 둘 다 그냥 computation을 인자로 넘기는 모양새에 수렴했다.

swap :: State a (State a ()) 같은 함수를 algebraic effect로 기술하려면 같은 효과가 두번 나오기에 koka는 named handlers를 실험하고 있다. 옳은 방향이라고 생각한다. 기존에 koka는 masked effect라는 복잡한 개념을 사용해 outer effect에 접근했다.

fun swap-with-mask() : <state<a>, state<a>> () {
  val inner-val = get() // innermost
  val outer-val = mask<state<a>> { get() } // skip the innermost
  set(outer-val) // innermost
  mask<state<a>> { set(inner-val) } // skip the innermost
}

하지만 named handler와 함께라면 이렇게 쓸 수 있다

fun swap-with-named-handlers(h1, h2) : <state<a>> () {
  val val1 = perform get() at h1
  val val2 = perform get() at h2
  perform set(val2) at h1
  perform set(val1) at h2
}

seealso: https://dl.acm.org/doi/10.1145/3563289

Call-by-Push-Value를 다시 방문하고 있는데 의문이 떠나지 않음... 왜 tag를 일급 시민으로 만들고 소비 방법을 (1) 의존함수 Π_i∈I Bᵢ (2) 구분 합 Σ_i∈I Aᵢ 이렇게 2개나 만들게 했지

타입 검사기 출력을 개선했다. 아직 Introduction Rule밖에 없기 때문에 Pfenning Recipe를 따라서 모두 check 규칙이다.

x : A면 inl x는 임의의 B에 대해 A + B로 검사될 수 있다

흠

v : unroll τ ⟹ roll v : τ 뭔가 당연하다면 당연하긴 한데 흠 재밌네

모든 노드에 고유 식별자를 부여하고 외부에 거대한 해시맵 Expr → Type을 만드는 수밖에 없나?

이제 타입 검사기 짜는 데에는 익숙해지고 있는데 검수 이후에 타입 정보를 어떻게 코드 생성 과정에서 유용화하는지 모르겠다

Higher-Rank Polymorphism이 있어야 하는가에 대해 고민하는 중 있으면 unification 구현이 귀찮아진다는 거 같은데

해커스펍에 페이지 맨 위로 버튼이 있으면 좋겠다

Higher-Order Abstract Syntax가 왜 유용한지 살펴보고 있는데 아직은 잘 모르겠다 메타 언어와 대상 언어가 있다부터 기기묘묘한데

‘앞/전’과 ‘뒤/후’의 비대칭성은 한국어 학습자들에게 지옥을 선사할 것이다.

참고로 이거 다 국립국어원의 잘못이 아니라 한국어의 잘못임. 이건 표준국어대사전이 그냥 현실을 반영했을 뿐이다. 즉 이 글을 읽고 있는 당신도 0.000001% 정도 잘못이 있다.

- ‘앞일’은 미래인데(예: 앞일을 예측하다), ‘뒷일’도 미래다(예: 뒷일을 부탁하네). 맞죠?

- 마찬가지로, ‘앞길’은 미래다(예: 앞길이 창창한 젊은이). 그런데 ‘뒷길’도 미래다(예: 자식의 뒷길을 생각하면 걱정이 앞선다).

- ‘뒷날’도 미래고(예: 우리는 뒷날 또 만나게 되었다), ‘훗날’도 미래다(예: 훗날을 기약하다). 그런데 ‘앞날’도 미래다(예: 앞날이 창창하다). 희한하게 ‘전날’만 과거이다.

- 그런데 ‘앞날’은 간혹 과거를 가리킬 수도 있다(예: 일찍이 앞날의 폭군은 있었고…).

- 관형사형에 ‘뒤’나 ‘후’를 붙여서 시점을 나타낼 수 있다(예: “고친 뒤의 모습” 또는 “고친 후의 모습”). 그런데 반대로 하려면 관형사형이 아니라 명사형을 써야 한다(예: “고치기 전의 모습”). 그리고, ‘전’만 쓸 수 있다. ‘앞’은 여기서 아예 쓸 수 없다.

- ‘후일’은 미래의 아무 날이나 다 가리키며, 특정한 날을 가리킬 수 없다. 반면 ‘전일’은 직전, 즉 인접한 과거의 1일만 가리킨다.

- 그런데 또 ‘전날’은 인접한 과거의 1일을 가리킬 수도 있고, 과거의 아무 날을 가리킬 수도 있다.

- 그런데 또 ‘훗날’은 미래의 아무 날을 뜻하며, 인접한 미래의 1일을 가리킬 수 없다.

- ‘전년’과 ‘후년’은 각각 과거의 아무 해, 또는 미래의 아무 해를 가리킬 수 있다. 대, 대칭인가?!

- 하지만 특정한 해를 가리키는 경우, ‘전년’은 인접한 과거의 해를 가리킨다. 반면 ‘후년’은 ‘올해의 다음다음 해’이다.

- …뭐라고? 왜냐하면 미래의 해들은 순서대로 ‘내년’-‘후년’-‘내후년’이기 때문이다. 책상 엎어버리고 싶죠?

- 참고로 ‘내후년’은 동음이의어이다. 올해가 2025년이라면 내후년은 2027년을 가리킬 수도 있고 2028년을 가리킬 수도 있다. (이게 언어냐?)

- ‘후년’이 ‘올해의 다음다음 해’가 되는 이 원리는 오직 ‘년’에만 적용된다. 예를 들어 ‘후일’, ‘후주’, ‘후월’ 등에는 그런 의미가 없다.

- ‘후일’은 미래의 아무 날이다. 하지만 ‘후주’와 ‘후월’은 인접한 미래의 것 하나만 가리킨다.

- ‘전년’은 인접한 과거의 해이지만, 과거의 모든 해를 다 가리킬 수도 있다(예: 우리는 전년의 기록들을 검토하여 그 사람의 행적을 조사해 보기로 했다).

- 반면 ‘전일’, ‘전주’, ‘전월’은 오직 인접한 과거의 하나만 가리킬 수 있다.

- ‘전달’과 ‘훗달’도 비대칭이다.

도대체 이걸 어떻게 배워서 쓰라는 것인지. 생각해 보면 나도 실제로 이렇게 쓰고 있다는 것도 기가 찬다.

그밖에:

- ‘지난날’에는 특정한 날을 가리키는 뜻이 전혀 없다. 반면 ‘지난주’, ‘지난달’, ‘지난해’는 모두 과거의 인접한 하나만 가리킨다.

- ‘다음 날’과 ‘다음날’은 의미가 완전히 다르다. ‘다음날’은 ‘정하여지지 아니한 미래의 어떤 날’이다. 따라서 인접한 미래의 1일을 가리킬 때에는 ‘다음 날’만 쓸 수 있다. (도저히 못 외우시겠으면 그냥 ‘이튿날’로 피신하시라…)

정보 리터러시 관련 의견을 보존하러 왔다. 우리는 흔히 영어 자료가 한국어 자료보다 낫다는 문화사대주의적 의견에 공감하곤 한다. 하지만 여기엔 숨은 의견이 여럿 있다. 하나씩 까보며 음미해보자.

영어 자료는 한국어 자료보다 낫다. => 왜 나을까? 도움이 되기 때문에. 왜 도움이 될까? => (진실에 가깝기 때문에, 다양한 경험이 전시되어 있기 때문에). 왜 진실에 가까울까? => 1차 출처에 가깝기 때문에. 왜 1차 출처에 가까울까? => 사용자가 다수이기 때문에 직접 사용하거나 번역되어 2차 출처로 기능하기 때문에. 왜 다양한 경험이 있을까? => 생산자가 자료 작성 시 영어를 선택할 확률이 한국어보다 높기 때문에.

그렇다면 우리는 영어 자료가 나은 이유를 구체적으로 표현할 수 있다.

• (일반적으로) 한국어 웹보다 영어 웹이 더 크기 때문에 원하는 자료를 구할 확률이 더 높다.
• (일반적으로) 한국어 웹보다 영어 웹에서 1차 출처에 가까운 자료를 구할 확률이 더 높다.

탐색 공간을 넓히고, 정보 전파 과정에서의 왜곡을 줄이기 위해서 영어 웹 탐색이 효과적이다. 다만 영어 웹이 "언제나" 좋은 건 아니다. 한컴오피스 자료가 미국에 많겠는가, 아니면 한국에 많겠는가? 1차 출처에 가까운 곳을 향해 왜곡을 줄이고, 그 안에서 탐색 공간을 최대한 효율적으로 넓혀야 한다.

영어 검색이라는 피상적인 행위에서 벗어나 정보 탐색의 본질을 좇는 것이 좋다.

오랜만에 프로그래밍 언어 이야기하러 왔다. 오늘 주제는 타입스크립트의 핵심 가치다.

많은 사람들이 정적 타입 언어를 도입하는 이유로 안전성(Soundness)를 이야기한다. 맞는 말이다. 하지만 타입스크립트에서 안전성은 2등 가치다. 그럼 1등 가치는 뭘까?

바로 개발 경험 개선이다. 구체적으로, 오류 나기 쉬운 구문을 적당히 줄이고 자동 완성을 개선하며 큰 규모 리팩토링 시 심리적(그리고 any 같은 기능을 안 썼다는 가정하에 런타임에도 유의미한 수준의) 안정성을 얻겠다는 거다.

타입스크립트 공식 위키 문서에도 안전성은 목표가 아니라고 나와있다 (#). 우리는 때때로 도구의 목적에 들어맞지 않는 불필요한 기대를 하곤 한다. 하지만 도구 개발자와 싸우는 건 사용자로서 좋은 전략이 아니다.

조건부 타입과 재귀 타입, 템플릿 문자열 타입, infer 등을 보라. 정적 분석 난이도가 지수적으로 올라가는 희한한 기능들이 언어에 계속 추가되는 이유가 무엇인가. 추론을 포기하고 any가 나오곤 하는 이유가 무엇인가.

그들이 추구하는 게 안전한 세계가 아닌 실용적인 세계이기 때문이다.

JS에서 Promise는 await으로 값을 읽는 것 외에, 현재 pending 상태를 읽는 등의 동작을 허용하지 않는다. 이거 왜 안되냐고하면 Promise의 의미론과 배경 철학이 어쩌구저쩌구하는 대답이 돌아온다. 내 생각에 그건 틀렸다. 이유는

간단한 대답: 가능하면서 왜 안해줌?

약간더 복잡한 대답

그 제약 조건은 Promise가 callback과 같은 의미의 다른 표현일때는 성립한다. callback이 전달하는 값은 특정시점 = t에 존재하는 것이다. t이후에 그 값을 사용하기위해선 따로 저장을 해놓던가해서 값의 존재시기를 >= t 로 바꾸어야한다.

그런데 Promise는 await을 여러번 하는걸 허용한다. await x; await x; 이런식으로. 값이 없으면 기다리고, 값이 한번 들어오면 그걸 계속해서 돌려준다. 여기서 Promise가 callback이랑 다른게 드러난다. 그리고 실제로 callback과 다르게 동작하기위해 값의 여부 등을 내부 상태로 갖고있을수 밖에 없다.

요약하면, callback과 완전히 상호호환될때 정당화되는 제약을 callback이 아니면서 강요하니까 문제란 얘기다.

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

@hongminhee洪 民憙 (Hong Minhee) 조금 길지만 제거 예정(예문: Features deprecated / 제거 예정인 기능)이 그럭저럭 쓸만한 번역어인 거 같고요. Gemini를 굴려보니 재밌는 번역어를 몇 제시해주네요.

• 폐기 예정 / 폐지 예정
• 비권장 / 지원 중단 예정
• 구식 / 낡은 / 노후화된 / 대체될
• 사양길의 / 저물어가는 / 쇠퇴한

다만 여전히 제게는 '제거 예정/제거할'이 가장 와닿네요.

• This is a deprecated feature / 제거할 기능이야.
• Have you marked it as deprecated? / 제거 예정이라 적어놨어?
• Removed recently deprecated features / 최근 제거 예정이었던 기능을 지웠습니다
• Don't use deprecated features / 제거될 기능은 사용하지 마

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

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

나: 아 짜증나

에디터가 하스켈의 타입 에러메시지를 보여줄땐 호버링으로 뜨는 창으로는 부족한거 같다. 별도의 뷰를 만들어서 크게 보여주고 또 rich한 기능(메시지에 포함된 심볼로의 navigation 등)을 제공하면 좋겠다.

와, 해커스펍에서 summary, detail 태그 지원되는거 방금 처음봤어

뭐라는 거시여

We eventually end up with constraints of the shape “$\tau_\text{con} \leq \tau_\text{dis}$” and there always exists a $\tau_i \in \tau_\text{con}$ and $\tau'_j \in \tau_\text{dis}$ such that we can reduce the constraint to an equivalent constraint $\tau_i \leq \tau'_j$.” (Parreaux and Chau, 2022, p. 10)

아 Ctrl + Enter로 올리기 되니까 너무 편하다 이게 SNS지

MLstruct 읽고 있는데 다행스럽게도 Simple-sub 기반이라고 한다. MLsub 기반이었으면 MLsub 읽으러 가야 해서 울었음

@cog25 님을 초대했다 히히

@hongminhee洪 民憙 (Hong Minhee) 최고예요

이런 면에서 KDL이 아주 훌륭하다고 느꼈던 게 /- 주석이란 게 있다. AST 노드 하나를 주석 처리하는 거.

#자기소개 를 해볼까요.

• @ranolpRanol☆P 와 동일인입니다...만 해당 계정은 근시일 내에 살릴 계획이 없습니다.
• @ranolp 계정은 프로그래밍 언어론/해커스펍 사용기 위주 계정입니다.
• 다시 말하자면 그 외 일상적인 내용은 트위터에서 이야기한다는 뜻입니다...
• TypeScript와 얼추 호환되면서 제정신인 타입 추론 규칙을 가진 언어를 만들려고 타입 이론을 공부하고 있습니다.
  • 좀 많이 전에는 Bidirectional Typing (J. Dunfield, N. Krishnaswami)을 읽었었고,
  • 독일에 있는 튀빙겐 대학 내에서 연구하는 대수적 효과 언어 Effekt도 간단히 살펴보았었습니다.
  • 최근에는 힌들리-밀너-다마스 타입 추론 위에 얹은 부타입 확장을 살펴보고 있습니다.
    • 캠브릿지 대학 연구인 MLsub (S. Dolan and A. Mycroft)...
    • 을 단순화한 Simple-sub (L. Parreaux)을 시작으로 MLstruct, Ultimate Conditional Syntax 등 홍콩대 연구를 많이 보고 있습니다
    • MLscript가 정말 흥미로운 언어에요 ReScript but more Kotlin처럼 생겼음
• 올해 들어서 An Infinitely Large Napkin으로 군론과 군의 작용, 위상수학과 대수 위상(호모토피만), 그리고 범주론을 배웠습니다.
• 형식적 증명 보조기에도 관심이 많습니다.
  • Software Foundation을 통해 Coq (현 Rocq)를 약간 배웠습니다.
  • Lean 4도 약간 맛보기를 했습니다.
  • 의존 타입/마틴 뢰프 타입(MLTT)/호모토피 타입(HoTT) 등을 배워 간단한 증명 보조기도 만들어보고 싶네요.
    • 아마 An Infinitely Large Napkin 스터디가 끝나면 HoTT 스터디를 하지 않을까 싶네요.

#툿친소 #연친소 #핵친소

함수형 언어는 뭐 사실 역사와 전통의 리스프 방언에서 시작해야 하지 않나 (웃음)

모바일 웹은 그냥 새로 디자인하는 걸 개인적으로 선호한다. 내비게이션 방법이 꽤나 달라서 (바텀 탭 내비게이션 등)

@hongminhee洪 民憙 (Hong Minhee) 뭔가 구조적 한계나 표준의 강압은 아니었군요! 항상 연합우주 웹 클라이언트들 쓰면서 스레드 탐색이 불편했는데 구현을 바꾸면 제 기준 약간은 편해질 거 같네요 각 보고 신 클라이언트 기여해야지...

자기소개 각잡고 쓰기 귀찮앙

생각해보면 연합우주류 UX가 다 그랬던 거 같은데 이유가 있는 건가

~분전 부분을 눌러야 스레드 위로 탐색이 가능한데 그냥 트위터식 UX로 위쪽 트윗 영역 전체가 스레드 위로 탐색 기능이면 안되나

2022년 논문이면 very new thingy죠

드디어 기본 타입 추론 아이디어를 염탐할 수 있다

MLstruct 논문을 읽어야 하는데 너무 귀찮다... Simple-sub 논문은 Scala 코드 줘서 읽고 구현하기 쉬웠단 말야

트위터는 트친소고 블루스카이는 블친소니까 해커스펍은 해친소 내지는 햌친소겠군

@kodingwarriorJaeyeol Lee 바로 이슈 만들었습죠

사람 프사/닉네임에 호버했을 때 호버 카드 안나오는 거 은근 불편하다 초기 팔로우 관계 빌딩할 땐 타임라인 보면서 재밌어보이는 사람 보이면 즉시 호버 카드에서 팔로하면 편한데

왜 ctrl + enter 눌러도 안 올라가지....

벨로그에 draft로 남겨두던 논문 요약+번역 포스트를 살려서 여기다가 올리면 괜찮으려나

@saschanazKAGAMI🏳️‍🌈🏳️‍⚧️ Firefox Nightly를 사용하고 있어요. 파폭 애들이 PWA 구현을 하다 말았을 가능성도 높긴 한데...

해커스펍을 PWA로 설치하니까 뒤로가기하면 앱을 이탈해버려서 곤란하다

여기선 프로그래밍 언어론 이야기나 해야겠다