Haskell Kind 시스템으로 보는 타입의 타입 분류 체계

Haskell 아이디어가 주류 언어로 더 많이 퍼질수록 세상이 좋아질 거라고 봄. 고수준 추상화가 여러 개념을 묶어주는 게 진짜 멋있음.

나는 Haskell을 연구용 언어로 보는 쪽임. 좋은 아이디어가 많은데 실무에선 덜 다듬어져 있어서 다른 언어로 옮겨가서야 성숙해지더라.

에이전트가 코드를 짜는 시대에는 언어 재미가 줄어들 것 같음. 결국 형식론으로 에이전트를 몰게 될 듯.

모나드가 어려운 이유는 Kind를 코드에서 다룰 수 있는 언어가 거의 없어서임. type->type 같은 걸 추상화할 수 있다고 먼저 설명하면 훨씬 수월해짐.

모나드가 어려운 건 모나드 트랜스포머 때문임. 세계를 모듈식으로 표현하려다 보니 복잡해짐. 그래서 나는 그냥 C++로 돌아가더라.

모나드는 순수 함수형 언어가 만든 문제를 푸는 도구임. 불순한 언어에선 애초에 그 문제가 없음. 큰 게임을 Haskell로 짜다가 모나드 때문에 포기함.

모나드 설명이 어려운 건 IO 모나드 때문인 듯. IO를 빼면 꽤 단순한데 넣는 순간 멘탈 모델이 깨짐.

이 글의 terms 정의는 틀린 것 같음. terms는 문법 표현이고 values는 런타임 개념임. 1+2는 term이고 실행하면 3이 됨.

타입 이론 맥락에서는 terms가 표준 용법임. MathWorld도 1+2를 term으로 정의함. 컴파일러 관점만 정답인 건 아님.

하스켈은 의존 타입을 끝까지 받아들이지 않고 확장만 계속 붙여서 복잡해진 것 같음. Lean, Agda, Idris 2는 처음부터 의존 타입을 넣어서 훨씬 깔끔함.

그 언어들 실무에 쓸 만함?