Functor / Functor / Applicative / Monad가 아닌 좋은 예?

Functor / Functor / Applicative / Monad가 아닌 좋은 예?

---

타입 클래스 X가 무엇인지 누군가에게 설명하면서 정확히 X 인 데이터 구조의 좋은 예를 찾기 위해 고심하고 있습니다.

따라서 다음에 대한 예를 요청합니다.

• Functor가 아닌 타입 생성자.
• Functor이지만 형식이 아닌 형식 생성자입니다.
• Applicative이지만 Monad가 아닌 형식 생성자입니다.
• Monad 인 타입 생성자.

나는 모나드에 대한 많은 예가 있다고 생각하지만, 이전 예와 관련이있는 모나드의 좋은 예가 그림을 완성 할 수 있습니다.

특정 유형 클래스에 속하는 중요한 측면에서만 다른 서로 유사한 예제를 찾습니다.

이 계층 구조의 어딘가에 Arrow의 예제를 적용 할 수 있다면 (응용 프로그램과 Monad 사이입니까?)

---

Functor가 아닌 타입 생성자 :

newtype T a = T (a -> Int)

반공 변 펑터를 (공변량) 펑터로 만들 수는 없습니다. 쓰기를 시도 fmap하면 실패합니다. 반 변형 functor 버전은 반대로되어 있습니다.

fmap      :: Functor f       => (a -> b) -> f a -> f b
contramap :: Contravariant f => (a -> b) -> f b -> f a

functor이지만 형식이 아닌 형식 생성자 :

좋은 예가 없습니다. 이 Const있지만 이상적으로 는 비모 노이드가 아닌 콘크리트를 원하고 생각할 수 없습니다. 모든 유형은 기본적으로 숫자, 열거 형, 곱, 합계 또는 함수입니다. 당신은 아래의 pigworker를 볼 수 있으며, 내가 아닌지 Data.Void에 대해 동의하지 않습니다 Monoid.

instance Monoid Data.Void where
    mempty = undefined
    mappend _ _ = undefined
    mconcat _ = undefined

이후로는 _|_하스켈 법적 값이고, 사실의 유일한 법적 값 Data.Void이는 모노 이드 규칙을 준수합니다. unsafeCoerce프로그램이 더 이상 unsafe함수 를 사용하자마자 Haskell 의미를 위반하지 않도록 보장되지 않기 때문에 관련이 있는지 확실 하지 않습니다 .

하단에있는 기사 ( 링크 ) 또는 안전하지 않은 기능 ( 링크 )에 대해서는 Haskell Wiki를 참조하십시오 .

다양한 확장 기능을 가진 Agda 또는 Haskell과 같은 더 풍부한 유형 시스템을 사용하여 이러한 유형 생성자를 만들 수 있는지 궁금합니다.

응용 프로그램이지만 Monad가 아닌 형식 생성자 :

newtype T a = T {multidimensional array of a}

다음과 같은 방법으로 Applicative를 만들 수 있습니다.

mkarray [(+10), (+100), id] <*> mkarray [1, 2]
  == mkarray [[11, 101, 1], [12, 102, 2]]

그러나 모나드로 만들면 치수 불일치가 발생할 수 있습니다. 나는 이와 같은 예가 실제로 드문 것으로 생각됩니다.

Monad 인 타입 생성자 :

[]

화살표 정보 :

이 계층 구조에서 화살표가 어디에 있는지 묻는 것은 어떤 종류의 "빨간색"인지 묻는 것과 같습니다. 종류의 불일치에 유의하십시오.

Functor :: * -> *
Applicative :: * -> *
Monad :: * -> *

그러나,

Arrow :: * -> * -> *

---

내 스타일이 휴대 전화에 의해 좁아 질 수 있지만 여기로갑니다.

newtype Not x = Kill {kill :: x -> Void}

Functor가 될 수 없습니다. 만약 그렇다면, 우리는

kill (fmap (const ()) (Kill id)) () :: Void

달은 녹색 치즈로 만들어졌습니다.

그 동안에

newtype Dead x = Oops {oops :: Void}

functor입니다

instance Functor Dead where
  fmap f (Oops corpse) = Oops corpse

하지만 적용 할 수는 없습니다.

oops (pure ()) :: Void

그리고 초록색은 문 치즈로 만들어 졌을 것입니다.

(추가 메모 : Void에서와 같이 Data.Void빈 데이터 유형입니다. undefinedMonoid임을 증명하는 데 사용하려고 시도하면 사용 unsafeCoerce하지 않는 것을 증명하는 데 사용 합니다.)

즐겁게

newtype Boo x = Boo {boo :: Bool}

예를 들어 Dijkstra는 다양한 방식으로 적용 할 수 있습니다.

instance Applicative Boo where
  pure _ = Boo True
  Boo b1 <*> Boo b2 = Boo (b1 == b2)

그러나 모나드는 될 수 없습니다. 지속적으로해야합니다 그 반환을 관찰, 왜 안 보려면 Boo True또는 Boo False, 따라서 그

join . return == id

개최 할 수 없습니다.

Oh yeah, I nearly forgot

newtype Thud x = The {only :: ()}

is a Monad. Roll your own.

Plane to catch...

---

I believe the other answers missed some simple and common examples:

A type constructor which is a Functor but not an Applicative. A simple example is a pair:

instance Functor ((,) r) where
    fmap f (x,y) = (x, f y)

But there is no way how to define its Applicative instance without imposing additional restrictions on r. In particular, there is no way how to define pure :: a -> (r, a) for an arbitrary r.

A type constructor which is an Applicative, but is not a Monad. A well-known example is ZipList. (It's a newtype that wraps lists and provides different Applicative instance for them.)

fmap is defined in the usual way. But pure and <*> are defined as

pure x                    = ZipList (repeat x)
ZipList fs <*> ZipList xs = ZipList (zipWith id fs xs)

so pure creates an infinite list by repeating the given value, and <*> zips a list of functions with a list of values - applies i-th function to i-th element. (The standard <*> on [] produces all possible combinations of applying i-th function to j-th element.) But there is no sensible way how to define a monad (see this post).

---

How arrows fit into the functor/applicative/monad hierarchy? See Idioms are oblivious, arrows are meticulous, monads are promiscuous by Sam Lindley, Philip Wadler, Jeremy Yallop. MSFP 2008. (They call applicative functors idioms.) The abstract:

We revisit the connection between three notions of computation: Moggi's monads, Hughes's arrows and McBride and Paterson's idioms (also called applicative functors). We show that idioms are equivalent to arrows that satisfy the type isomorphism A ~> B = 1 ~> (A -> B) and that monads are equivalent to arrows that satisfy the type isomorphism A ~> B = A -> (1 ~> B). Further, idioms embed into arrows and arrows embed into monads.

---

A good example for a type constructor which is not a functor is Set: You can't implement fmap :: (a -> b) -> f a -> f b, because without an additional constraint Ord b you can't construct f b.

---

I'd like to propose a more systematic approach to answering this question, and also to show examples that do not use any special tricks like the "bottom" values or infinite data types or anything like that.

When do type constructors fail to have type class instances?

In general, there are two reasons why a type constructor could fail to have an instance of a certain type class:

1. Cannot implement the type signatures of the required methods from the type class.
2. Can implement the type signatures but cannot satisfy the required laws.

Examples of the first kind are easier than those of the second kind because for the first kind, we just need to check whether one can implement a function with a given type signature, while for the second kind, we are required to prove that no implementation could possibly satisfy the laws.

Specific examples

• A type constructor that cannot have a functor instance because the type cannot be implemented:

  data F a = F (a -> Int)
  

This is a contrafunctor, not a functor, because it uses the type parameter a in a contravariant position. It is impossible to implement a function with type signature (a -> b) -> F a -> F b.

• A type constructor that is not a lawful functor even though the type signature of fmap can be implemented:

  data Q a = Q(a -> Int, a)
  fmap :: (a -> b) -> Q a -> Q b
  fmap f (Q(g, x)) = Q(\_ -> g x, f x)  -- this fails the functor laws!
  

The curious aspect of this example is that we can implement fmap of the correct type even though F cannot possibly be a functor because it uses a in a contravariant position. So this implementation of fmap shown above is misleading - even though it has the correct type signature (I believe this is the only possible implementation of that type signature), the functor laws are not satisfied (this requires some simple computations to check).

In fact, F is only a profunctor, - it is neither a functor nor a contrafunctor.

• A lawful functor that is not applicative because the type signature of pure cannot be implemented: take the Writer monad (a, w) and remove the constraint that w should be a monoid. It is then impossible to construct a value of type (a, w) out of a.

• A functor that is not applicative because the type signature of <*> cannot be implemented: data F a = Either (Int -> a) (String -> a).

• A functor that is not lawful applicative even though the type class methods can be implemented:

  data P a = P ((a -> Int) -> Maybe a)
  

The type constructor P is a functor because it uses a only in covariant positions.

instance Functor P where
   fmap :: (a -> b) -> P a -> P b
   fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))

The only possible implementation of the type signature of <*> is a function that always returns Nothing:

 (<*>) :: P (a -> b) -> P a -> P b
 (P pfab) <*> (P pa) = \_ -> Nothing  -- fails the laws!

But this implementation does not satisfy the identity law for applicative functors.

• A functor that is Applicative but not a Monad because the type signature of bind cannot be implemented.

I do not know any such examples!

• A functor that is Applicative but not a Monad because laws cannot be satisfied even though the type signature of bind can be implemented.

This example has generated quite a bit of discussion, so it is safe to say that proving this example correct is not easy. But several people have verified this independently by different methods. See Is `data PoE a = Empty | Pair a a` a monad? for additional discussion.

 data B a = Maybe (a, a)
   deriving Functor

 instance Applicative B where
   pure x = Just (x, x)
   b1 <*> b2 = case (b1, b2) of
     (Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
     _ -> Nothing

It is somewhat cumbersome to prove that there is no lawful Monad instance. The reason for the non-monadic behavior is that there is no natural way of implementing bind when a function f :: a -> B b could return Nothing or Just for different values of a.

It is perhaps clearer to consider Maybe (a, a, a), which is also not a monad, and to try implementing join for that. One will find that there is no intuitively reasonable way of implementing join.

 join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
 join Nothing = Nothing
 join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
 join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
 -- etc.

In the cases indicated by ???, it seems clear that we cannot produce Just (z1, z2, z3) in any reasonable and symmetric manner out of six different values of type a. We could certainly choose some arbitrary subset of these six values, -- for instance, always take the first nonempty Maybe - but this would not satisfy the laws of the monad. Returning Nothing will also not satisfy the laws.

• A tree-like data structure that is not a monad even though it has associativity for bind - but fails the identity laws.

The usual tree-like monad (or "a tree with functor-shaped branches") is defined as

 data Tr f a = Leaf a | Branch (f (Tr f a))

This is a free monad over the functor f. The shape of the data is a tree where each branch point is a "functor-ful" of subtrees. The standard binary tree would be obtained with type f a = (a, a).

If we modify this data structure by making also the leaves in the shape of the functor f, we obtain what I call a "semimonad" - it has bind that satisfies the naturality and the associativity laws, but its pure method fails one of the identity laws. "Semimonads are semigroups in the category of endofunctors, what's the problem?" This is the type class Bind.

For simplicity, I define the join method instead of bind:

 data Trs f a = Leaf (f a) | Branch (f (Trs f a))
 join :: Trs f (Trs f a) -> Trs f a
 join (Leaf ftrs) = Branch ftrs
 join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)

The branch grafting is standard, but the leaf grafting is non-standard and produces a Branch. This is not a problem for the associativity law but breaks one of the identity laws.

When do polynomial types have monad instances?

Neither of the functors Maybe (a, a) and Maybe (a, a, a) can be given a lawful Monad instance, although they are obviously Applicative.

These functors have no tricks - no Void or bottom anywhere, no tricky laziness/strictness, no infinite structures, and no type class constraints. The Applicative instance is completely standard. The functions return and bind can be implemented for these functors but will not satisfy the laws of the monad. In other words, these functors are not monads because a specific structure is missing (but it is not easy to understand what exactly is missing). As an example, a small change in the functor can make it into a monad: data Maybe a = Nothing | Just a is a monad. Another similar functor data P12 a = Either a (a, a) is also a monad.

Constructions for polynomial monads

In general, here are some constructions that produce lawful Monads out of polynomial types. In all these constructions, M is a monad:

1. type M a = Either c (w, a) where w is any monoid
2. type M a = m (Either c (w, a)) where m is any monad and w is any monoid
3. type M a = (m1 a, m2 a) where m1 and m2 are any monads
4. type M a = Either a (m a) where m is any monad

The first construction is WriterT w (Either c), the second construction is WriterT w (EitherT c m). The third construction is a component-wise product of monads: pure @M is defined as the component-wise product of pure @m1 and pure @m2, and join @M is defined by omitting cross-product data (e.g. m1 (m1 a, m2 a) is mapped to m1 (m1 a) by omitting the second part of the tuple):

 join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
 join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))

The fourth construction is defined as

 data M m a = Either a (m a)
 instance Monad m => Monad M m where
    pure x = Left x
    join :: Either (M m a) (m (M m a)) -> M m a
    join (Left mma) = mma
    join (Right me) = Right $ join @m $ fmap @m squash me where
      squash :: M m a -> m a
      squash (Left x) = pure @m x
      squash (Right ma) = ma

I have checked that all four constructions produce lawful monads.

I conjecture that there are no other constructions for polynomial monads. For example, the functor Maybe (Either (a, a) (a, a, a, a)) is not obtained through any of these constructions and so is not monadic. However, Either (a, a) (a, a, a) is monadic because it is isomorphic to the product of three monads a, a, and Maybe a. Also, Either (a,a) (a,a,a,a) is monadic because it is isomorphic to the product of a and Either a (a, a, a).

The four constructions shown above will allow us to obtain any sum of any number of products of any number of a's, for example Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a)) and so on. All such type constructors will have (at least one) Monad instance.

It remains to be seen, of course, what use cases might exist for such monads. Another issue is that the Monad instances derived via constructions 1-4 are in general not unique. For example, the type constructor type F a = Either a (a, a) can be given a Monad instance in two ways: by construction 4 using the monad (a, a), and by construction 3 using the type isomorphism Either a (a, a) = (a, Maybe a). Again, finding use cases for these implementations is not immediately obvious.

A question remains - given an arbitrary polynomial data type, how to recognize whether it has a Monad instance. I do not know how to prove that there are no other constructions for polynomial monads. I don't think any theory exists so far to answer this question.

참고URL : https://stackoverflow.com/questions/7220436/good-examples-of-not-a-functor-functor-applicative-monad