Haskell 프로그래밍의 Monad 대 범주 이론의 Monad
Haskell 프로그래밍과 수학 범주 이론에서 사용되는 모나드의 개념에 대한 질문이 있습니다.
Haskell에서 모나드는 다음 구성 요소로 구성됩니다.
해당 모나드 유형을 얻는 방법을 각 기본 유형에 대해 정의하는 유형 생성자입니다. 이 유형 생성자의 이름은 종종 전체 모나드와 동의어로 사용됩니다. 만약$M$ 모나드의 이름이고 $t$ 임의의 고정 데이터 유형이면 $M t$ 해당하는 모나드 유형입니다.
기본 유형의 값을 해당 모나드 유형의 값에 매핑하는 단위 함수입니다. 결과는 원래 값에서 얻을 수있는 해당 유형의 "가장 단순한"값입니다. Haskell에서는이 함수를 return이라고합니다. 단위 함수에는 다형성 유형이 있습니다.$t → M t$
모나드 연산의 조합을 설명하는 하나 이상의 추가 연산입니다.
반면에 범주 이론에서 모나드는 트리플입니다 $(T, \eta, \mu)$ 카테고리 $C$ 어디
$T: C \to C$ 펑터이다
$\eta: 1_K \to T$ 범주 이론의 의미에서 자연스러운 변화
$\mu: T^2 \to T$ 자연스러운 변화
이러한 개체는 다음 다이어그램을 충족해야합니다. https://en.wikipedia.org/wiki/Monad_(category_theory)
질문 : Haskell의 모나드는 추상 범주 이론과 어떤 관련이 있습니까? Haskell의 모나드 구조는 범주 이론의 의미에서 자연스러운 "모나드 구조"를 가지고 있습니까?$M$ 위에서 설명한 것과 같은 표준 트리플?
답변
Haskell의 모나드는 유형 이론이 유형 이론 내부에서 수행 될 때 유형 범주에 대한 모나드가됩니다. Haskell 및 유사 언어의 기능은 다소 제한적이므로 범주 이론에는 수행 할 수없는 기본 구성이 많이 있지만 합리적으로 인코딩 할 수있는 구조는 많습니다.
M :: * → *펑터의 객체 매핑입니다. 대신 이름을 지정했습니다. $T$ 나중.- 펑터의 화살표 매핑 부분은 fmap
- $η$Haskell이 호출하는 단위 함수입니다 return(또는 pure좀 더 일반적입니다)
- $μ$에 의해 주어집니다 join.
Monad인스턴스에 예상되는 요구 사항 은 범주 이론에서 모나드가 되는 요구 사항 과 동일합니다.
본질적으로 이것은 카테고리의 모나드에 대해 구체적으로 말하는 것과 크게 다르지 않습니다. $\mathsf{Set}$, Haskell / etc에 대한 이전 언급을 제외하고. 세트 이론이 가지고있는 일부 구조가 누락되었습니다. 당신은 모나드에 대해서만 생각할 수 있습니다.$\mathsf{Set}$, 왜냐하면 추상 / 보편 대수의 많은 구조가 하나를 생성하고 그렇게 표현할 수 있기 때문입니다.
다양한 프로그래밍 언어의 유형이 기술적으로 좋은 속성 / 구조를 가진 범주를 형성하지 않는다고 불평 할 수 있지만 대신 시스템과 같이 더 잘 작동하는 것에 대해 이야기하는 수단으로 사용하고 있다고 상상할 수 있습니다. $F_ω$, 그리고 흥미로운 방식으로 답을 바꾸지는 않을 것입니다.