RanolP

나: 건전한 육신에 건전한 정신이 깃든다(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 님을 초대했다 히히

이런 면에서 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 스터디를 하지 않을까 싶네요.

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

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

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

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

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

2022년 논문이면 very new thingy죠

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

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

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

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

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

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

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

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