부가 물로서의 모나드

부가 물로서의 모나드

---

저는 카테고리 이론에서 모나드에 대해 읽었습니다. 모나드의 한 정의는 한 쌍의 인접 펑터를 사용합니다. 모나드는 이러한 펑터를 사용하는 왕복으로 정의됩니다. 명백히 부속은 범주 이론에서 매우 중요하지만, 부속 펑터 측면에서 Haskell 모나드에 대한 설명은 보지 못했습니다. 누군가 그것에 대해 생각 했습니까?

---

편집 : 그냥 재미로, 나는 이것을 올바르게 할 것입니다. 아래에 보존 된 원래 답변

현재 카테고리 확장에 대한 부가 코드는 부가 패키지에 있습니다 : http://hackage.haskell.org/package/adjunctions

저는 상태 모나드를 명확하고 간단하게 살펴볼 것입니다. 이 코드는 Data.Functor.ComposeTransformers 패키지에서 사용하지만 자체 포함되어 있습니다.

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는 또한 adjunction의 역할에 대해 유망하지만 간단한 토론을 제공합니다. 일부는 카테고리 확장을 해석하는 데 도움이 될 수 있습니다. http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

---

Derek Elkins는 최근 저녁 식사 시간에 Cont Monad (_ -> k)가 자체적으로 contravariant functor 를 구성 할 때 어떻게 발생하는지 보여주었습니다 . 그것이 당신이 (a -> k) -> k그것을 벗어나는 방법 입니다. 그러나 그것의 counit은 Haskell에서 쓸 수없는 이중 부정 제거로 이어집니다.

이를 설명하고 증명하는 일부 Agda 코드는 http://hpaste.org/68257을 참조 하십시오 .

---

이것은 오래된 스레드이지만 질문이 흥미로워 서 직접 계산을했습니다. 바라건대 Bartosz가 아직 거기에 있고 이것을 읽을 수도 있습니다 ..

사실, Eilenberg-Moore 구조는이 경우에 매우 명확한 그림을 제공합니다. (나는 구문과 같은 Haskell과 함께 CWM 표기법을 사용할 것입니다)

Let T be the list monad < T,eta,mu > (eta = return and mu = concat) and consider a T-algebra h:T a -> a.

(Note that T a = [a] is a free monoid <[a],[],(++)>, that is, identity [] and multiplication (++).)

By definition, h must satisfy h.T h == h.mu a and h.eta a== id.

Now, some easy diagram chasing proves that h actually induces a monoid structure on a (defined by x*y = h[x,y] ), and that h becomes a monoid homomorphism for this structure.

Conversely, any monoid structure < a,a0,* > defined in Haskell is naturally defined as a T-algebra.

In this way (h = foldr ( * ) a0, a function that 'replaces' (:) with (*),and maps [] to a0, the identity).

So, in this case, the category of T-algebras is just the category of monoid structures definable in Haskell, HaskMon.

(Please check that the morphisms in T-algebras are actually monoid homomorphisms.)

It also characterizes lists as universal objects in HaskMon, just like free products in Grp, polynomial rings in CRng, etc.

The adjuction corresponding to the above construction is < F,G,eta,epsilon >

where

• F:Hask -> HaskMon, which takes a type a to the 'free monoid generated by a',that is, [a],
• G:HaskMon -> Hask, the forgetful functor (forget the multiplication),
• eta:1 -> GF , the natural transformation defined by \x::a -> [x],
• epsilon: FG -> 1 , the natural transformation defined by the folding function above (the 'canonical surjection' from a free monoid to its quotient monoid)

Next, there is another 'Kleisli category' and the corresponding adjunction. You can check that it is just the category of Haskell types with morphisms a -> T b, where its compositions are given by the so-called 'Kleisli composition' (>=>). A typical Haskell programmer will find this category more familiar.

Finally,as is illustrated in CWM, the category of T-algebras (resp. Kleisli category) becomes the terminal (resp. initial) object in the category of adjuctions that define the list monad T in a suitable sense.

I suggest to do a similar calculations for the binary tree functor T a = L a | B (T a) (T a) to check your understanding.

---

I've found a standard constructions of adjunct functors for any monad by Eilenberg-Moore, but I'm not sure if it adds any insight to the problem. The second category in the construction is a category of T-algebras. A T algebra adds a "product" to the initial category.

So how would it work for a list monad? The functor in the list monad consists of a type constructor, e.g., Int->[Int] and a mapping of functions (e.g., standard application of map to lists). An algebra adds a mapping from lists to elements. One example would be adding (or multiplying) all the elements of a list of integers. The functor F takes any type, e.g., Int, and maps it into the algebra defined on the lists of Int, where the product is defined by monadic join (or vice versa, join is defined as the product). The forgetful functor G takes an algebra and forgets the product. The pair F, G, of adjoint functors is then used to construct the monad in the usual way.

I must say I'm none the wiser.

---

If you are interested,here's some thoughts of a non-expert on the role of monads and adjunctions in programming languages:

First of all, there exists for a given monad T a unique adjunction to the Kleisli category of T. In Haskell,the use of monads is primarily confined to operations in this category (which is essentially a category of free algebras,no quotients). In fact, all one can do with a Haskell Monad is to compose some Kleisli morphisms of type a->T b through the use of do expressions, (>>=), etc., to create a new morphism. In this context, the role of monads is restricted to just the economy of notation.One exploits associativity of morphisms to be able to write (say) [0,1,2] instead of (Cons 0 (Cons 1 (Cons 2 Nil))), that is, you can write sequence as sequence, not as a tree.

Even the use of IO monads is non essential, for the current Haskell type system is powerful enough to realize data encapsulation (existential types).

This is my answer to your original question, but I'm curious what Haskell experts have to say about this.

On the other hand, as we have noted, there's also a 1-1 correspondence between monads and adjunctions to (T-)algebras. Adjoints, in MacLane's terms, are 'a way to express equivalences of categories.' In a typical setting of adjunctions <F,G>:X->A where F is some sort of 'free algebra generator' and G a 'forgetful functor',the corresponding monad will (through the use of T-algebras) describe how (and when) the algebraic structure of A is constructed on the objects of X.

In the case of Hask and the list monad T, the structure which T introduces is that of monoid,and this can help us to establish properties (including the correctness) of code through algebraic methods that the theory of monoids provides. For example, the function foldr (*) e::[a]->a can readily be seen as an associative operation as long as <a,(*),e> is a monoid, a fact which could be exploited by the compiler to optimize the computation (e.g. by parallelism). Another application is to identify and classify 'recursion patterns' in functional programming using categorical methods in the hope to (partially) dispose of 'the goto of functional programming', Y (the arbitrary recursion combinator).

Apparently, this kind of applications is one of the primary motivations of the creators of Category Theory (MacLane, Eilenberg, etc.), namely, to establish natural equivalence of categories, and transfer a well-known method in one category to another (e.g. homological methods to topological spaces,algebraic methods to programming, etc.). Here, adjoints and monads are indispensable tools to exploit this connection of categories. (Incidentally, the notion of monads (and its dual, comonads) is so general that one can even go so far as to define 'cohomologies' of Haskell types.But I have not given a thought yet.)

As for non-determistic functions you mentioned, I have much less to say... But note that; if an adjunction <F,G>:Hask->A for some category A defines the list monad T, there must be a unique 'comparison functor' K:A->MonHask (the category of monoids definable in Haskell), see CWM. This means, in effect, that your category of interest must be a category of monoids in some restricted form (e.g. it may lack some quotients but not free algebras) in order to define the list monad.

Finally,some remarks:

The binary tree functor I mentioned in my last posting easily generalizes to arbitrary data type T a1 .. an = T1 T11 .. T1m | .... Namely,any data type in Haskell naturally defines a monad (together with the corresponding category of algebras and the Kleisli category), which is just the result of any data constructor in Haskell being total. This is another reason why I consider Haskell's Monad class is not much more than a syntax sugar (which is pretty important in practice,of course).

참고URL : https://stackoverflow.com/questions/4697320/monads-as-adjunctions