하스켈은 kind가 있어서 Value, Type, Kind 까지는 알아야 하는데
idris는 Type : Type 이라서 kind가 없음.
가령 Functor f도 f : Type -> Type 인데 여기서 화살표가 kind arrow(?)가 아니라 그냥 함수 타입임.
막 수학적으로 깊게 가면 러셀 페러독스가 어쩌고 나올것 같은데 그걸 모르니까 할말이 없네
참고로 Agda는 Value : Set0 : Set1 : ... 처럼 무한히 간다고 알고 있음
하스켈보다 더한 또라이..
(하스켈도 무한히 있다고 생각할 수는 있는데 그걸 직접 다루진 못함)
하스켈은 Kind까지밖에 없는 거 아님? 무한한 건 아닐 텐데. Kind 위에 있는 게 없자너. - dc App
그니까 있는것처럼 생각할 수 있다고. 예를 들어서 모든 kind의 모임인 sort가 있는데, 하스켈에서 그걸 명시적으로 다루지 않는것 뿐임.
아 그래요? ㅈㅅ kind의 모임을 sort라 하구나 - dc App
https://jozefg.bitbucket.io/posts/2014-02-10-types-kinds-and-sorts.html
정확히는 BOX라는 sort가 하스켈에 있는 모든 kind의 모임이라고 해야 맞을듯
그니까 coq나 agda같은걸 하면 무한한 Universe(U0=Type, U1=Kind, U2=Sort, ...) 들을 다뤄야 하는거.. 시발
이것은 타입 레벨 프로그래밍! 너무 무섭다 ㄷㄷ - dc App
Coq도 배워야 하는데 ㅇㅅㅇ - dc App
V 랭 해봄?
ㄴㄴ.. 좀 찾아보니 스펙 개쩔긴 하네
하스켈에서 타입레벨 깊게 팔것 아니면 kind까지는 몰라도 되지 않음? 이드리스는 타입레벨이 필수라... - dc App
몰라도 되긴 하지. 언어의 기능을 최대한 활용 하려면 알아야 된다고
러스트처럼 HKT 없는거임?
없긴 한데 러스트랑 비슷하진 않음. Type이 자기 자신에 속해서 kind가 필요 없는거지. 대신 inconsistency가 생긴다고 들었던것 걑은데, 인터넷 찾아봐도 확실하게 선언된게 없어서 잘 모르겠다.