RanolP

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가 왜 유용한지 살펴보고 있는데 아직은 잘 모르겠다 메타 언어와 대상 언어가 있다부터 기기묘묘한데

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

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

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

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

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

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

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

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

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

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

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

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

@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)

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

나: 아 짜증나

뭐라는 거시여

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로 위쪽 트윗 영역 전체가 스레드 위로 탐색 기능이면 안되나