나는 카테고리 이론에서 모나드에 대해 읽었습니다. 모나드의 한 정의는 한 쌍의 인접 펑터를 사용합니다. 모나드는 이러한 펑터를 사용하는 왕복으로 정의됩니다. 명백하게 부속은 범주 이론에서 매우 중요하지만, 부속 펑터 측면에서 Haskell 모나드에 대한 설명은 보지 못했습니다. 누군가 그것에 대해 생각 했습니까?
답변
편집 : 그냥 재미로, 나는 이것을 올바르게 할 것입니다. 아래에 보존 된 원래 답변
현재 카테고리 추가 코드는 부속 패키지에 있습니다. http://hackage.haskell.org/package/adjunctions
저는 상태 모나드를 명확하고 간단하게 살펴볼 것입니다. 이 코드는 Data.Functor.Compose
Transformers 패키지에서 사용하지만 자체 포함되어 있습니다.
f (D-> C)와 g (C-> D) 사이의 부속, f-| g는 다양한 방법으로 특성화 될 수 있습니다. 우리는 counit / unit (epsilon / eta) 설명을 사용하여 두 가지 자연스러운 변형 (펑터 간의 형태)을 제공합니다.
class (Functor f, Functor g) => Adjoint f g where
counit :: f (g a) -> a
unit :: a -> g (f a)
counit의 “a”는 실제로 C의 identity functor이고 unit의 “a”는 실제로 D의 identity functor입니다.
counit / unit 정의에서 hom-set adjunction 정의를 복구 할 수도 있습니다.
phiLeft :: Adjoint f g => (f a -> b) -> (a -> g b)
phiLeft f = fmap f . unit
phiRight :: Adjoint f g => (a -> g b) -> (f a -> b)
phiRight f = counit . fmap f
어쨌든 우리는 이제 다음과 같이 unit / counit adjunction에서 Monad를 정의 할 수 있습니다.
instance Adjoint f g => Monad (Compose g f) where
return x = Compose $ unit x
x >>= f = Compose . fmap counit . getCompose $ fmap (getCompose . f) x
이제 우리는 (a,)와 (a->) 사이에 고전적인 부속물을 구현할 수 있습니다.
instance Adjoint ((,) a) ((->) a) where
-- counit :: (a,a -> b) -> b
counit (x, f) = f x
-- unit :: b -> (a -> (a,b))
unit x = \y -> (y, x)
그리고 이제 유형 동의어
type State s = Compose ((->) s) ((,) s)
그리고 이것을 ghci에로드하면 State가 정확히 우리의 고전적인 상태 모나드임을 확인할 수 있습니다. 반대 구성을 사용하여 Costate Comonad (일명 상점 comonad)를 얻을 수 있습니다.
이 방식으로 모나드로 만들 수있는 다른 부가 물이 많이 있지만 (예 : (Bool,) Pair) 이상한 모나드입니다. 안타깝게도 하스켈에서 독자와 작가를 직접 유쾌하게 유도하는 부속물을 할 수는 없습니다. 우리는 할 수 있습니다 계속 수행하지만, copumpkin 설명으로 실제로 약간의 화살표를 반전은 “수반 행렬”typeclass의 다른 “형태”를 사용하므로, 즉, 반대 카테고리에서 adjunction이 필요합니다. 이 양식은 adjunctions 패키지의 다른 모듈에서도 구현됩니다.
이 자료는 The Monad Reader 13-Calculating Monads with Category Theory : http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf의 Derek Elkins의 기사에서 다른 방식으로 다룹니다 .
또한, 프로그램 최적화 용지 HINZE의 최근 칸 확장 사이의 adjunction에서 목록 모나드의 건설을 통해 산책 Mon
과 Set
: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
이전 답변 :
두 개의 참조.
1) Category-extras는 항상 그렇듯이 부속물의 표현과 그로부터 모나드가 발생하는 방식을 제공합니다. 평소와 같이 생각하는 것이 좋지만 문서에 대해서는 꽤 가볍습니다 : http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html
2) -Cafe는 또한 부가의 역할에 대해 유망하지만 간단한 토론을 제공합니다. 일부는 카테고리 확장을 해석하는 데 도움이 될 수 있습니다. http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html
답변
Derek Elkins는 최근 저녁 식사 중에 Cont Monad (_ -> k)
가 자체적으로 반 변성 펑터 를 구성 할 때 발생하는 방식을 보여주었습니다 . 그것이 당신이 (a -> k) -> k
그것을 벗어나는 방법 입니다. 그러나 그것의 counit은 Haskell에서 쓸 수없는 이중 부정 제거로 이어집니다.
이를 설명하고 입증하는 Agda 코드는 http://hpaste.org/68257을 참조 하십시오 .
답변
이것은 오래된 스레드이지만 질문이 흥미로워 서 직접 계산을했습니다. 바라건대 Bartosz가 아직 거기에 있고 이것을 읽을 수도 있습니다 ..
사실, Eilenberg-Moore 구조는이 경우에 매우 명확한 그림을 제공합니다. (나는 구문과 같은 Haskell과 함께 CWM 표기법을 사용할 것입니다)
하자 T
목록 모나드 수 < T,eta,mu >
( eta = return
와 mu = concat
)과 T-대수를 고려 h:T a -> a
.
(그것은 T a = [a]
free monoid <[a],[],(++)>
, 즉 identity []
와 multiplication (++)
입니다.)
정의에 h
만족해야 h.T h == h.mu a
하고 h.eta a== id
.
이제 몇 가지 간단한 다이어그램 추적은 h
실제로 a (로 정의 됨 x*y = h[x,y]
) 에 모노 이드 구조를 유도 h
하고이 구조에 대한 모노 이드 동형이 된다는 것을 증명합니다 .
반대로 < a,a0,* >
Haskell에서 정의 된 모든 모노 이드 구조 는 자연스럽게 T- 대수로 정의됩니다.
이러한 방법으로 ( h = foldr ( * ) a0
함수는 ‘대체한다’고 (:)
와 (*)
, 및 매핑 []
에 a0
, 신원).
따라서이 경우 T- 대수 범주는 Haskell, HaskMon에서 정의 할 수있는 모노 이드 구조 범주 일뿐입니다.
(T-algebras의 형태가 실제로 monoid homomorphism인지 확인하십시오.)
또한 Grp의 무료 제품, CRng의 다항식 링 등과 같이 HaskMon의 범용 개체로 목록을 특성화합니다.
위의 구성에 해당하는 조정은 < F,G,eta,epsilon >
어디
F:Hask -> HaskMon
, 유형 a를 ‘에 의해 생성 된 자유 모노 이드a
‘, 즉[a]
,,G:HaskMon -> Hask
, 건망증 펑터 (곱하기는 잊어 버리세요),eta:1 -> GF
,에 의해 정의 된 자연스러운 변형\x::a -> [x]
,epsilon: FG -> 1
, 위의 접는 함수에 의해 정의 된 자연 변형 (자유 모노 이드에서 몫 모노 이드로의 ‘정규 추정’)
다음으로, 또 다른 ‘Kleisli 카테고리’와 그에 상응하는 부속물이 있습니다. a -> T b
소위 ‘Kleisli composition’으로 구성되어있는 형태가있는 Haskell 유형의 범주인지 확인할 수 있습니다 (>=>)
. 전형적인 Haskell 프로그래머라면이 카테고리가 더 친숙하다는 것을 알게 될 것입니다.
마지막으로, CWM에 예시 된 바와 같이, T- 대수 범주 (각각 Kleisli 범주)는 적절한 의미에서 목록 모나드 T를 정의하는 조정 범주에서 터미널 (각각 초기) 객체가됩니다.
이진 트리 펑터 T a = L a | B (T a) (T a)
에 대해 유사한 계산을 수행 하여 이해를 확인 하는 것이 좋습니다 .
답변
Eilenberg-Moore의 모나드에 대한 부속 펑터의 표준 구성을 찾았지만 문제에 대한 통찰력을 추가하는지 확실하지 않습니다. 구성의 두 번째 범주는 T- 대수 범주입니다. AT 대수학은 초기 범주에 “제품”을 추가합니다.
그렇다면리스트 모나드는 어떻게 작동할까요? 목록 모나드의 펑 터는 예를 들어 유형 생성자 Int->[Int]
와 함수 매핑 (예 : 목록에 대한지도의 표준 적용)으로 구성됩니다. 대수는 목록에서 요소로의 매핑을 추가합니다. 한 가지 예는 정수 목록의 모든 요소를 더하거나 곱하는 것입니다. functor F
는 Int와 같은 모든 유형을 취하여 Int 목록에 정의 된 대수에 매핑합니다. 여기서 제품은 모나 딕 조인으로 정의됩니다 (또는 그 반대의 경우 조인은 제품으로 정의 됨). 건망증 펑 터는 G
대수를 받고 제품을 잊어 버립니다. 그런 다음 인접 펑터 쌍 F
, G
을 사용하여 일반적인 방법으로 모나드를 구성합니다.
나는 내가 더 현명하지 않다고 말해야한다.
답변
관심이 있으시다면, 프로그래밍 언어에서 모나드와 부속물의 역할에 대한 비전문가의 생각이 있습니다.
우선, 주어진 모나드 T
에 대해 Kleisli 범주의 T
. Haskell에서 모나드의 사용은 주로이 범주의 연산에 국한됩니다 (본질적으로 자유 대수의 범주이며 몫이 없음). 사실, Haskell Monad로 할 수있는 모든 것은 새로운 형태를 만들기 위해 a->T b
do 표현식 (>>=)
등을 사용하여 Kleisli 형태의 유형 을 구성하는 것입니다 . 이 맥락에서 모나드의 역할은 단지 표기법의 경제성에 국한되어 있는데, 하나는 형태론의 연관성을 이용하여 [0,1,2]
대신에 쓸 수 있도록 (예를 들어) (Cons 0 (Cons 1 (Cons 2 Nil)))
트리가 아닌 시퀀스로 시퀀스를 작성할 수 있습니다.
현재 Haskell 유형 시스템은 데이터 캡슐화 (기존 유형)를 실현할 수있을만큼 강력하기 때문에 IO 모나드의 사용조차 필수가 아닙니다.
이것은 귀하의 원래 질문에 대한 제 대답이지만 Haskell 전문가가 이것에 대해 뭐라고 말 해야할지 궁금합니다.
반면에 우리가 언급했듯이 모나드와 (T-) 대수에 대한 부속물 사이에는 1-1 대응이 있습니다. MacLane의 용어로 Adjoint는 ‘카테고리의 동등성을 표현하는 방법’입니다. adjunctions의 일반적인 설정에서는 ‘무료 대수 발생기 및 G는’증 펑 ‘의 일종이며, 해당 모나드 (T-대수의 사용을 통해)의 대수 구조 방법 (때)을 설명 할 것이다 에 구성되고 의 객체 .<F,G>:X->A
F
A
X
Hask와 list monad T의 경우 T
소개 하는 구조 는 monoid 의 구조이며, 이것은 monoids 이론이 제공하는 대수적 방법을 통해 코드의 속성 (정확도 포함)을 설정하는 데 도움이 될 수 있습니다. 예를 들어, 함수 foldr (*) e::[a]->a
는 <a,(*),e>
monoid 인 한 연관 연산으로 쉽게 볼 수 있습니다. 이는 컴파일러가 계산을 최적화하기 위해 이용할 수있는 사실입니다 (예 : 병렬 처리). 또 다른 응용은 ‘함수 프로그래밍의 고토’, Y (임의의 재귀 결합 자)를 (부분적으로) 처리하기 위해 범주 적 방법을 사용하여 함수형 프로그래밍에서 ‘재귀 패턴’을 식별하고 분류하는 것입니다.
분명히 이러한 종류의 응용 프로그램은 범주 이론 (MacLane, Eilenberg 등)을 만든 사람의 주요 동기 중 하나입니다. 즉, 범주의 자연스러운 동등성을 설정하고 한 범주에서 잘 알려진 방법을 다른 범주로 이전하려는 것입니다 (예 : 위상 공간에 대한 상동 적 방법, 프로그래밍에 대한 대수적 방법 등). 여기서 adjoint와 모나드는 이러한 카테고리 연결을 활용하는 데 없어서는 안될 도구입니다. (부수적으로, 모나드 (및 이중, 코 모나드)의 개념은 너무 일반적이어서 하스켈 유형의 ‘동질 학’을 정의하는 데까지 갈 수 있지만 아직 생각하지 않았습니다.)
당신이 언급 한 비 결정적 함수에 관해서는 할 말이 훨씬 적습니다. <F,G>:Hask->A
일부 카테고리에 대한 부속 A
이 목록 monad를 정의하는 T
경우 고유 한 ‘비교 펑터’ K:A->MonHask
(Haskell에서 정의 할 수있는 모노 이드 카테고리) 가 있어야합니다 . CWM을 참조하세요. 즉, 목록 모나드를 정의하려면 관심 범주가 제한된 형식의 모노 이드 범주 여야합니다 (예 : 일부 몫이 부족할 수 있지만 자유 대수가 아닐 수 있음).
마지막으로, 몇 가지 언급 :
지난 포스팅에서 언급 한 바이너리 트리 펑 터는 임의의 데이터 유형으로 쉽게 일반화됩니다
T a1 .. an = T1 T11 .. T1m | ...
. 즉, Haskell의 모든 데이터 유형은 자연스럽게 모나드를 정의합니다 (대수학의 해당 범주 및 Kleisli 범주와 함께). 이는 Haskell의 모든 데이터 생성자가 합계 인 결과입니다. 이것이 내가 Haskell의 Monad 클래스가 신택스 슈가에 불과하다고 생각하는 또 다른 이유입니다 (물론 실제로는 꽤 중요합니다).
답변
