해당하는 모나드 변환기 (IO 제외)가없는 모나드가 있습니까?

해당하는 모나드 변환기 (IO 제외)가없는 모나드가 있습니까?

---

지금까지 내가 만난 모든 모나드 (데이터 유형으로 나타낼 수 있음)에는 해당하는 모나드 변환기가 있거나 하나를 가질 수 있습니다. 가질 수없는 모나드가 있습니까? 아니면 모든 모나드에 해당하는 변환기가 있습니까?

A로 변압기 t모나드 대응m 그 뜻 t Identity동형이다 m. 그리고 물론 그것은 모나드 변환기 법칙을 만족하며 t n모든 모나드의 모나드 n입니다.

모든 모나드가 하나를 가지고 있다는 증명 (이상적으로는 건설적인 것)이나 하나가없는 (증거가있는) 특정 모나드의 예를보고 싶습니다. 나는 더 많은 Haskell 지향적 답변과 (범주) 이론적 답변에 관심이 있습니다.

후속 질문으로, 모나드가 m두 가지 변압기가 t1와 t2? 즉, t1 Identity동형입니다 t2 Identity및에 m있지만, 모나드가 n같은 t1 n동형되지는 t2 n.

( IO그리고 ST특별한 의미가 있으므로 여기서는 고려하지 않고 완전히 무시하겠습니다. 데이터 유형을 사용하여 구성 할 수있는 "순수한"모나드에만 집중하겠습니다.)

---

나는 @Rhymoid와 함께하고 있으며 모든 Monads에는 두 개의 (!!) 변압기가 있다고 생각합니다. 내 구성은 약간 다르며 훨씬 덜 완성됩니다. 이 스케치를 증거로 삼고 싶지만 기술 / 직관이 부족하거나 상당히 관련이있을 수 있다고 생각합니다.

Kleisli으로 인해 모든 모나드 ( m) 두 펑로 분해 될 수 F_k및 G_k그러한 F_k행 왼쪽 수반 행렬이고 G_k그리고 그 m동형이다 G_k * F_k(여기 *펑 조성물이다). 또한 F_k * G_k부속물 때문에 코 모나드를 형성합니다.

나는 그것이 모나드 변환기 라고 t_mk정의 했다고 주장합니다 t_mk n = G_k * n * F_k. 분명히 t_mk Id = G_k * Id * F_k = G_k * F_k = m. 정의하기 return때문에,이 펑위한 어렵지 않다 F_k은 "날카로운"펑이며, 정의 join때문에 가능해야 extractcomonad부터 F_k * G_k유형의 값을 감소 시키는데 사용될 수있는 (t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a유형의 값에 G_k * n * n * F_k추가 한 후 비아 감소 join에서 n.

우리는 이후 조금 조심해야 할 F_k및 G_kHask에 endofunctors 수 없습니다. 따라서 표준 유형 Functor클래스의 인스턴스 가 아니며 n위에 표시된대로 직접 구성 할 수도 없습니다 . 대신 우리는 n작곡 전에 Kleisli 카테고리로 "투영"해야 하지만, 저는 그 "투영" return을 m제공 한다고 믿습니다 .

나는주고, 당신은 또한 Eilenberg - 무어 모나드 분해와 함께이 작업을 수행 할 수 있다고 생각 m = G_em * F_em, tm_em n = G_em * n * F_em그리고 유사한 구조 lift, return및 join에 비슷한 의존성과 extractcomonad에서 F_em * G_em.

---

여기에 손으로 흔들리는 대답이 있습니다.

모나드는 명령형 언어의 인터페이스로 생각할 수 있습니다. return순수한 가치를 언어에 주입하는 >>=방법이며 언어의 일부를 결합하는 방법입니다. 모나드 법칙은 언어의 "리팩토링"부분이 예상대로 작동하도록합니다. 모나드가 제공하는 추가 작업은 "작업"으로 생각할 수 있습니다.

모나드 트랜스포머는 "확장 효과"문제에 접근하는 한 가지 방법입니다. Monad를 변환하는 Monad Transformer t가 있다면를 통해 사용할 수있는 추가 작업으로 언어 가 확장되고 m있다고 말할 수 있습니다 . 적용 할 수 있도록 모나드는, 효과 / 작업과 언어 로하는 당신에게가 제공하는 유일한 작업과 언어를 얻을 것이다 . mtIdentitytIdentityt

따라서 "주입, 스플 라이스 및 기타 작업"모델의 관점에서 모나드를 생각하면 Free Monad Transformer를 사용하여 이들을 재구성 할 수 있습니다. 이런 식으로 IO 모나드도 트랜스포머로 바뀔 수 있습니다. 유일한 문제는 언젠가 트랜스포머 스택에서 해당 레이어를 벗겨 낼 수있는 방법을 원한다는 것이며,이를 수행하는 유일한 현명한 방법 IO은 스택 맨 아래에있는 작업을 수행 할 수 있도록하는 것입니다.

---

업데이트 : 아래의 진술 1과 2는 대부분 정확하지 않습니다. 이 경우에 모나드 변환기를 찾은 것 같습니다. 나는 아직 필요한 계산을 완료하지 않았지만 유망 해 보인다. 진술 3과 4는 여전히 유효합니다. 두 개의 다른 변환기가있는 모나드의 예를 보여주기 위해 Statement 5를 추가했습니다.

의 변환기 Either a (z -> a)는 (거의 가능성이 높음) n (Either a (z -> m a), 여기서는 m임의의 외부 모나드입니다. 용 변압기 (a -> n p) -> n aIS는 (대부분) (a -> t m p) -> t m a곳 t m모나드의 변압기입니다 n.

1. 적어도 하나의 반례를 찾았다 고 생각 합니다. 단순하고 명시적인 모나드 변환기가없는 단순하고 명시적인 모나드입니다.

L이 반례 의 모나드 유형 생성자 는 다음과 같이 정의됩니다.

  type L z a  = Either a (z -> a)

이 모나드의 목적은 일반 독자 모나드 z -> a를 명시적인 pure값 ( Left x) 으로 꾸미는 것 입니다 . 일반 리더 모나드의 pure값은 상수 함수 pure x = _ -> x입니다. 그러나 유형 값이 주어지면 z -> a이 값이 상수 함수인지 여부를 확인할 수 없습니다. 를 사용 L z a하면 pure값이로 명시 적으로 표시됩니다 Left x. 이제 사용자는 패턴 일치를 설정 L z a하고 주어진 모나드 값이 순수하거나 효과가 있는지 확인할 수 있습니다 . 그 외에 모나드 L z는 독자 모나드와 똑같은 일을합니다.

모나드 인스턴스 :

  instance Monad (L z) where
     return x = Left x
     (Left x) >>= f = f x
     (Right q) >>= f = Right(join merged) where
        join :: (z -> z -> r) -> z -> r
        join f x = f x x -- the standard `join` for Reader monad
        merged :: z -> z -> r
        merged = merge . f . q -- `f . q` is the `fmap` of the Reader monad
        merge :: Either a (z -> a) -> z -> a 
        merge (Left x) _ = x
        merge (Right p) z = p z

이 모나드는 L z보다 일반적인 건설, 특정 사건 (Monad m) => Monad (L m)곳 L m a = Either a (m a). 이 구성 m은 명시 적 pure값 ( Left x) 을 추가하여 주어진 모나드 를 장식 하므로 사용자는 이제 L m값이 순수한지 여부를 결정하기 위해 패턴 일치를 사용할 수 있습니다 . 다른 모든 방법에서는 L m모나드와 동일한 계산 효과를 나타냅니다 m.

위한 모나드 인스턴스 L m이외에는, 상기 예와 거의 동일 join하고 fmap모나드로 m사용할 필요가 있고 도우미 함수 merge에 의해 정의 된

    merge :: Either a (m a) -> m a
    merge (Left x) = return @m x
    merge (Right p) = p

나는 모나드의 법칙이 L m임의 의 모나드로 유지되는지 확인했다 m.

그래서, 나는 생각 L m일반에 대한 중, 더 모나드 변압기가없는 m또는 간단한 모나드를 위해 m = Reader. L z위에서 정의한대로 고려하면 충분합니다 . 단순한 모나드조차도 변압기가없는 것 같습니다.

모나드 변압기의 부존재의 (휴리스틱)이 모나드 이유가있다이다 Reader 내부 를 Either. Either모나드 변환기는 그베이스가 외부 모나드 내부 구성 할 필요 모나드 EitherT e m a = m (Either e a)모나드 변환기가 탐색을 사용하여 동작하기 때문에. Either데이터 유형에 를 포함하는 모나드는 모나드 변환기가 작동하려면 순회가 필요하므로 변환기에 "내부"구성이 있어야합니다. 그러나 Reader모나드 변환기는 기본 모나드가 외부 모나드 외부 에서 구성되어야 ReaderT r m a = r -> m a합니다. 모나드L내부 구성 변환기와 구성 외부 변환기를 요구하는 모나드를 요구하는 데이터 유형의 구성이며, 두 번째 모나드는 첫 번째 모나드 내부에있어 조정이 불가능합니다. L- 트랜스포머를 어떻게 정의하려고해도 LT모나드 트랜스포머의 법칙을 만족시킬 수없는 것 같습니다.

유형 생성자를 정의 LT할 수 있는 한 가지 가능성은 LT z m a = Either a (z -> m a). 결과는 합법적 인 모나드이지만, morphism에는 m a -> LT z m a보존하지 않습니다 m'들 return때문에 return x에 매핑되는 Right (\z -> return x)하지 않은는 L의 return(항상 Left x).

또 다른 가능성은 LT z m a = z -> Either a (m a). 결과는 모나드하지만 다시 m집 return으로 매핑되는 \_ -> Right (...)대신의 Left (...)모나드에 필요한 z -> Either a (m a).

사용 가능한 유형 생성자를 결합 할 수있는 또 다른 가능성은 LT z m a = Either a (m (z -> a) )이지만 이것은 임의의 모나드에 대한 모나드가 아닙니다 m.

나는 확실히 그 엄격하게 증명하는 방법을 모르겠습니다 L더 모나드 변압기하지만, 타입 생성자들의 조합이 없습니다 Either, ->그리고 것이 m제대로 작동하는 것 같다.

따라서 모나드 L z와 일반적으로 양식의 모나드 L m는 명시 적 유형 생성자 ( Either, ->및 의 조합)가되는 간단하고 사용하기 쉬운 모나드 변환기가없는 것 같습니다 m.

2. 명시 적 모나드 변환기가없는 것처럼 보이는 모나드의 또 다른 예 :

type S a = (a -> Bool) -> Maybe a

이 모나드는 여기 "검색 모나드"의 맥락에서 나타났습니다 . Jules Hedges 의 논문 에서는 검색 모나드에 대해 언급하며보다 일반적으로 다음 형식의 "선택"모나드를 언급합니다.

 type Sq n q a = (a -> n q) -> n a

주어진 모나드 n및 고정 유형에 대해 q. 검색 모나드는 상기와 선택 모나드 특정 사건 n a = Maybe a과 q = (). 그러나 Hedges의 논문 (내 생각에는 잘못 Sq보임)은 모나드의 모나드 변환기 라고 주장합니다 (a -> q) -> a.

내 의견은 모나드 에 "외부 구성"유형 (a -> q) -> a의 모나드 변환기 가 있다는 것 (m a -> q) -> m a입니다. 이것은 펑터의이 속성이 모나드보다 강합니까? 질문에서 살펴본 "강성"의 속성과 관련 이 있습니다. 즉, (a -> q) -> a리지드 모나드는 "composed-outside"유형의 모나드 변환기를 가지고 있습니다.

그러나 (a -> n q) -> n a모나드 n가 고정 되지 않으면 고정되지 않습니다 . 모든 모나드는 딱딱한 것은 아니기 때문에 (예를 들어 Maybe, Cont딱딱하지 않은), 모나드 (a -> n q) -> n a는 "composed-outside"유형의 모나드 변환기를 가지지 않을 것 (m a -> n q) -> n (m a)입니다. 또한 "구성된 내부"변환기 m((a -> n q) -> n a)도 없습니다.-이것은 임의의 모나드를위한 모나드가 아닙니다 m. 가지고 m = Maybe반례를 위해. 유형 (a -> m (n q)) -> m (n a)은 유사하게 임의의 모나드 m및 n. 유형 m(a -> n q) -> n a은 모나드 m이지만 임의의 모나드로 래핑 된 일부 값만 m a -> m (a -> n q) -> n a계산할 수 없기 때문에 리프팅을 허용하지 않습니다 .n am

모두 S와 Sq합법적 인 모나드는 (I 수동으로 확인)하지만 둘 중은 합법적 인 모나드 변압기를 갖고있는 것 같아요 없습니다.

다음은 모나드 변환기가 존재하지 않는다는 휴리스틱 주장입니다. (a -> n q) -> n a모든 모나드 에 대해 작동 하는 모나드 변환기에 대한 n데이터 유형 정의가있는 경우 해당 데이터 유형 정의는 rigid에 대한 "composed-outside"변환기 n와 non-rigid에 대한 다른 변환기를 산출했을 것 n입니다. 그러나 이러한 종류의 선택은 n자연스럽고 매개 변수 적으로 사용하는 유형 표현식 (즉, 모나드 인스턴스가있는 불투명 유형 생성자) 에서는 불가능합니다 .

3. Generally, transformed monads don't themselves automatically possess a monad transformer. That is, once we take some foreign monad m and apply some monad transformer t to it, we obtain a new monad t m, and this monad doesn't have a transformer: given a new foreign monad n, we don't know how to transform n with the monad t m. If we know the transformer mt for the monad m, we can first transform n with mt and then transform the result with t. But if we don't have a transformer for the monad m, we are stuck: there is no construction that creates a transformer for the monad t m out of the knowledge of t alone and works for arbitrary foreign monads m.

4. @JamesCandy's answer suggests that for any monad (including IO?!), one can write a (general but complicated) type expression that represents the corresponding monad transformer. Namely, you first need to Church-encode your monad type, which makes the type look like a continuation monad, and then define its monad transformer as if for the continuation monad. But I think this is incorrect - it does not give a recipe for producing a monad transformer in general.

Taking the Church encoding of a type a means writing down the type

 type ca = forall r. (a -> r) -> r

This type ca is completely isomorphic to a by Yoneda's lemma. So far we have achieved nothing other than made the type a lot more complicated by introducing a quantified type parameter forall r.

Now let's Church-encode a base monad L:

 type CL a = forall r. (L a -> r) -> r

Again, we have achieved nothing so far, since CL a is fully equivalent to L a.

Now pretend for a second that CL a a continuation monad (which it isn't!), and write the monad transformer as if it were a continuation monad transformer, by replacing the result type r through m r:

 type TCL m a = forall r. (L a -> m r) -> m r

This is claimed to be the "Church-encoded monad transformer" for L. But this seems to be incorrect. We need to check the properties:

• TCL m is a lawful monad for any foreign monad m and for any base monad L
• m a -> TCL m a is a lawful monadic morphism

The second property holds, but I believe the first property fails, - in other words, TCL m is not a monad for an arbitrary monad m. Perhaps some monads m admit this but others do not. I was not able to find a general monad instance for TCL m corresponding to an arbitrary base monad L.

Another way to argue that TCL m is not in general a monad is to note that forall r. (a -> m r) -> m r is indeed a monad for any type constructor m. Denote this monad by CM. Now, TCL m a = CM (L a). If TCL m were a monad, it would imply that CM can be composed with any monad L and yields a lawful monad CM (L a). However, it is highly unlikely that a nontrivial monad CM (in particular, one that is not equivalent to Reader) will compose with all monads L. Monads usually do not compose without stringent further constraints.

A specific example where this does not work is for reader monads. Consider L a = r -> a and m a = s -> a where r and s are some fixed types. Now, we would like to consider the "Church-encoded monad transformer" forall t. (L a -> m t) -> m t. We can simplify this type expression using the Yoneda lemma,

 forall t. (x -> t) -> Q t  = Q x

(for any functor Q) and obtain

 forall t. (L a -> s -> t) -> s -> t
 = forall t. ((L a, s) -> t) -> s -> t
 = s -> (L a, s)
 = s -> (r -> a, s)

So this is the type expression for TCL m a in this case. If TCL were a monad transformer then P a = s -> (r -> a, s) would be a monad. But one can check explicitly that this P is actually not a monad (one cannot implement return and bind that satisfy the laws).

Even if this worked (i.e. assuming that I made a mistake in claiming that TCL m is in general not a monad), this construction has certain disadvantages:

• It is not functorial (i.e. not covariant) with respect to the foreign monad m, so we cannot do things like interpret a transformed free monad into another monad, or merge two monad transformers as explained here Is there a principled way to compose two monad transformers if they are of different type, but their underlying monad is of the same type?
• The presence of a forall r makes the type quite complicated to reason about and may lead to performance degradation (see the "Church encoding considered harmful" paper) and stack overflows (since Church encoding is usually not stack-safe)
• The Church-encoded monad transformer for an identity base monad (L = Id) does not yield the unmodified foreign monad: T m a = forall r. (a -> m r) -> m r and this is not the same as m a. In fact it's quite difficult to figure out what that monad is, given a monad m.

As an example showing why forall r makes reasoning complicated, consider the foreign monad m a = Maybe a and try to understand what the type forall r. (a -> Maybe r) -> Maybe r actually means. I was not able to simplify this type or to find a good explanation about what this type does, i.e. what kind of "effect" it represents (since it's a monad, it must represent some kind of "effect") and how one would use such a type.

• The Church-encoded monad transformer is not equivalent to the standard well-known monad transformers such as ReaderT, WriterT, EitherT, StateT and so on.

It is not clear how many other monad transformers exist and in what cases one would use one or another transformer.

5. One of the questions in the post is to find an explicit example of a monad m that has two transformers t1 and t2 such that for some foreign monad n, the monads t1 n and t2 n are not equivalent.

I believe that the Search monad provides such an example.

 type Search a = (a -> p) -> a

where p is a fixed type.

The transformers are

 type SearchT1 n a = (a -> n p) -> n a
 type SearchT2 n a = (n a -> p) -> n a

I checked that both SearchT1 n and SearchT2 n are lawful monads for any monad n. We have liftings n a -> SearchT1 n a and n a -> SearchT2 n a that work by returning constant functions (just return n a as given, ignoring the argument). We have SearchT1 Identity and SearchT2 Identity obviously equivalent to Search.

The big difference between SearchT1 and SearchT2 is that SearchT1 is not functorial in n, while SearchT2 is. This may have implications for "running" ("interpreting") the transformed monad, since normally we would like to be able to lift an interpreter n a -> n' a into a "runner" SearchT n a -> SearchT n' a. This is possibly only with SearchT2.

A similar deficiency is present in the standard monad transformers for the continuation monad and the codensity monad: they are not functorial in the foreign monad.

---

My solution exploits the logical structure of Haskell terms etc.

I looked at right Kan extensions as possible representations of the monad transformer. As everyone knows, right Kan extensions are limits, so it makes sense that they should serve as universal encoding of any object of interest. For monadic functors F and M, I looked at the right Kan extension of MF along F.

First I proved a lemma, "rolling lemma:" a procomposed functor to the Right kan extension can be rolled inside it, giving the map F(Ran G H) -> Ran G(FH) for any functors F, G, and H.

Using this lemma, I computed a monadic join for the right Kan extension Ran F (MF), requiring the distributive law FM -> MF. It is as follows:

Ran F(MF) . Ran F(MF) [rolling lemma] =>
  Ran F(Ran F(MF)MF) [insert eta] =>
  Ran F(Ran F(MF)FMF) [gran] =>
  Ran F(MFMF) [apply distributive law] =>
  Ran F(MMFF) [join Ms and Fs] =>
  Ran F(MF).

What seems to be interesting about this construction is that it admits of lifts of both functors F and M as follows:

(1) F [lift into codensity monad] =>
  Ran F F [procompose with eta] =>
  Ran F(MF).

(2) M [Yoneda lemma specialized upon F-] =>
  Ran F(MF).

I also investigated the right Kan extension Ran F(FM). It seems to be a little better behaved achieving monadicity without appeal to the distributive law, but much pickier in what functors it lifts. I determined that it will lift monadic functors under the following conditions:

1) F is monadic.

2) F |- U, in which case it admits the lift F ~> Ran U(UM). This can be used in the context of a state monad to "set" the state.

3) M under certain conditions, for instance when M admits a distributive law.

참고URL : https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io