아닙니다. Haskell을 이해하기 위해 범주 이론에 관한 책을 집어들 필요는 없습니다.

나는 몇 년 동안 Haskell을 사용해 왔으며 호기심에서 일부 범주 이론을 선택했지만 실제로는 필요하지 않습니다. 한 편으로,이 모든 추상화가 어떻게 “큰 그림”에 어떻게 들어 맞는지 보는 것이 좋지만, 나는 가지 않았다. “오 세상에 나는 이것을 Maybe카테고리에서 []s 로 profunctor로 만들면된다 . 공주님!”.

이제 하스켈 타입 이론으로 무엇을하고 있는지에 따라 울타리가 있습니다.

하스켈을 배우고 있다면 타입 시스템의 모든 뉘앙스를 이해하려고하지 마십시오 . C ++ 템플릿 메타 프로그래밍을 먼저 배우는 것과 같습니다. 팬시 유형은 훌륭한 도구이지만 기능적 프로그래밍을 잘 이해하면 전형적 다형성을 이해하는 것보다 낫습니다.

이제 1 년 또는 2 년의 Haskell 이후에 Haskell의 유형 시스템 작동 방식에 대한 모든 미묘한 부분을 이해하려고한다고 가정 해 봅시다. 그렇다면 일부 유형 이론이 도움이 될 수 있습니다.

일이 어떻게 작동하는지에 대한 논리를 이해하는 데 도움이되며 솔직히 볼만한 가치가있는 컴퓨터 과학 IMO의 멋진 지점입니다. 당신은 당신이 관심있는 부분을 체리 선택하고 여전히 괜찮은 금액을 배울 수 있습니다.

Haskell의 경우 STLC, HM 유형 시스템 (시스템 F) 및 람다 큐브 (Haskell은 시스템 Fw iirc) 및 등 회귀 유형을 살펴 봅니다. 타입과 프로그래밍 언어는이 모든 것들을 시작하고 다루는 훌륭한 자료입니다.

쿨 에이드를 마시고 신진 유형 이론가라는 것을 알고 싶다면 Agda 또는 Coq를 찌르십시오. 이것들은 “종속 형”을 특징으로하며, Haskell보다 람다 큐브에서 한 걸음 더 먼 곳입니다. 종속 유형은 유형 이 용어에 종속 되도록합니다. 이것은 유형이 실제로 이론을 증명할만큼 강력하다는 것을 의미합니다. 호기심을 자극하는 인터넷 검색 “카레 하워드 동 형사상”은 몇 가지 흥미로운 결과를 가져옵니다.

답변