let rec을 결국 구현했고 타입 젠이 영 이상하지만 일단 코드젠이 얼추 되고 있다.... (TS Output)

isEven(S(O)) == false
isEven(S(S(O)) == true

!!!!!

장고 끝에 결론은 Lumo IR에 let-rec을 추가해야 한다는 것이다.

으어어 드 브루인 인덱스 안해서 망했다

이제 Lumo (GitHub)에서 fixpoint를 바탕으로 상호 재귀 가능한 함수 묶음을 정의할 수 있다. 슬슬 MVP의 끝이 보인다. 다음 스텝은 코드젠이다.

오늘의 진전

fixpoint <- (
    fn[A](f: thunk (A -> produce A)): produce A {
        g <- produce (thunk (
            fn(x: μX. thunk (X -> produce A)): produce A {
                ret <- (force unroll x)(x);
                (force f)(ret)
            }
        ));
        (force g)(roll g)
    }
);
fixpoint_ <- fixpoint[Unit];
(force fixpoint_)(thunk (fn(m: _): _ {
    `Unit/unit {}
}))

는 이제 타입 검사기를 통과한다!

@bglbgl gwyng termination을 보장하려면 occurs check가 필수적이라고 들었어요.

occurs check를 안 짜서 코딩을 잘못하면 컴파일러가 무한 루프를 돈다. unification 어렵네...

unification이 global로 돌아야 한다는 이유를 어느정도 이해하다 구와악 Algorithm W 나와

실제로 파서를 짜고 있다.

Y = forall A. λf.
    let g = thunk (λx. (force f) ((force (unroll x)) x)) : thunk ((μX. thunk (X -> A)) -> A)
    in g (roll g : μX. thunk (X -> A))

를 타입 검사한 게 지난 일이었다.

(Y[λ⟨ isEven: nat -> bool, isOdd: nat -> bool ⟩]) (λm.
    λ⟨
        isEven: λn. match n {
            Nat.zero as n => return true
            Nat.succ as n => return (force m::isOdd) (n.0)
        }
        isOdd: λn. match n {
            Nat.zero as n => return false
            Nat.succ as n => return (force m::isEven) (n.0)
        }
    ⟩
)

이제 위 코드를 대충 타입 검사할 수 있는 거 같다.

이제 시맨틱은 필요한 만큼 구현했으니 드디어 신택스나 코드젠으로 넘어갈 수 있겠다.

재귀 구현을 위해 Y combinator를 올바른 항으로 선언할 수 있게 타입 검사기를 고쳤으나 TyApp이 구현되어 있지 않아 안타깝게도 실행할 수 없다. 슬픈 일이다.

match 짜면서 unification 구현했는데 이거 잘 짜기 어렵긴 해보인다

thunk (fn(x : Nat): MaybeNat {
  match(unroll(x)) {
    case Nat.zero as x -> return MaybeNat.nothing
    case Nat.succ as x -> let y = x.0 in return MaybeNat.just(y)
  }
})

를 Lumo로 타입 검사할 수 있게 되었다. sub1이라는 이름을 붙일 수 있는 함수다.

@bglbgl gwyng 맞아요 compiled to c/js 언어가 목표에요

dup, drop 삽입을 위한 IR → IR 번역은 별개 스텝으로 분리하는 게 낫나...

평가 규칙이 점점 이상해지고 있다.

결국 AST를 짜고 Name Resolution을 한 다음에 AST Lowering을 해서 IR을 만들어야 할 운명인가보다

Perceus 논문을 다시 읽고 있다. 다 읽으면 요약 정리해서 해커스펍에 글 한번 올릴 듯 하다.

생각해보니 variant/record 규칙 저게 아니잔아

형식화 너무 어렵다

람다 함수의 Introduction Rule까지 작성했다.

지금 타입 검사 되는 거:

• () : ()
• Nat.zero
• Nat.succ(Nat.zero)
• Nat.succ(Nat.succ(Nat.zero))
• Nat.zero : Nat
• thunk (λx. return ()) : thunk (() -> ())

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지