Хорошие примеры не функтор / функтор / аппликатив / монада?

Question

Объясняя кому-то, что такое класс типов X, я изо всех сил пытаюсь найти хорошие примеры структур данных, которые точно X.

Итак, я прошу примеры для:

• Конструктор типа, который не является Functor.
• Конструктор типа, который является Functor, но не Applicative.
• Конструктор типа, который является Аппликативным, но не Монадой.
• Конструктор типа, который является Монадой.

Я думаю, что есть множество примеров Монады повсюду, но хороший пример Монады с некоторым отношением к предыдущим примерам может завершить картину.

Я ищу примеры, которые были бы похожи друг на друга, отличаясь только аспектами, важными для принадлежности к определенному классу типов.

Если бы кто-нибудь смог подобрать пример Arrow где-нибудь в этой иерархии (это между Applicative и Monad?), Это тоже было бы здорово!

Answer 1

Конструктор типа, который не является Functor:

newtype T a = T (a -> Int)

Из него можно сделать контравариантный функтор, но не (ковариантный) функтор. Попробуйте написать fmap и ты провалишься Обратите внимание, что версия контравариантного функтора обратная:

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

Конструктор типа, который является функтором, но не Applicative:

У меня нет хорошего примера. Есть Const, но в идеале я хотел бы конкретный немоноид, и я не могу думать ни о каком. Все типы в основном числовые, перечисления, продукты, суммы или функции, когда вы приступаете к этому. Вы можете увидеть ниже свиновод, и я не согласен с тем, Data.Void это Monoid;

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

поскольку _|_ является юридическим значением в Haskell, и на самом деле единственное юридическое значение Data.Voidэто соответствует правилам моноида. Я не уверен что unsafeCoerce связано с этим, потому что ваша программа больше не гарантирует, что не нарушит семантику Haskell, как только вы используете любую unsafe функция.

Обратитесь к Haskell Wiki за статьей о нижних ( ссылка) или небезопасных функциях ( ссылка).

Интересно, возможно ли создать такой конструктор типов, используя более богатую систему типов, такую ​​как Agda или Haskell с различными расширениями.

Конструктор типа, который является Аппликативным, но не Монадой:

newtype T a = T {multidimensional array of a}

Вы можете сделать Аппликатив из этого, например:

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

Но если вы сделаете это монадой, вы можете получить несоответствие размеров. Я подозреваю, что подобные примеры на практике редки.

Конструктор типа, который является Монадой:

[]

О Стрелках:

Спрашивать, где находится Стрелка в этой иерархии, все равно, что спрашивать, что это за форма "красная". Обратите внимание на несоответствие:

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

но,

Arrow :: * -> * -> *

Answer 2

Мой стиль может быть ограничен моим телефоном, но здесь идет.

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

не может быть Функтором. Если бы это было, мы бы

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

и Луна будет сделана из зеленого сыра.

между тем

newtype Dead x = Oops {oops :: Void}

это функтор

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

но не может быть аппликативным, иначе мы бы

oops (pure ()) :: Void

и Зеленый будет сделан из сыра Луны (что может произойти, но только позже вечером).

(Дополнительное примечание: Void, как в Data.Void это пустой тип данных. Если вы попытаетесь использовать undefined чтобы доказать, что это моноид, я буду использовать unsafeCoerce чтобы доказать, что это не так.)

радостно,

newtype Boo x = Boo {boo :: Bool}

является аппликативным во многих отношениях, например, как это было бы у Дейкстры,

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

но это не может быть монадой. Чтобы понять, почему нет, обратите внимание, что возвращение должно быть постоянно Boo True или же Boo Falseи, следовательно, что

join . return == id

не может удержаться.

О да я чуть не забыл

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

это монада Бросай свой.

Самолет, чтобы поймать...

Answer 3

Я считаю, что в других ответах пропущены некоторые простые и распространенные примеры:

Конструктор типа, который является Functor, но не Applicative. Простой пример - пара:

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

Но нет способа, как определить его Applicative экземпляр без наложения дополнительных ограничений на r, В частности, нет способа, как определить pure :: a -> (r, a) для произвольного r,

Конструктор типа, который является Аппликативным, но не Монадой. Хорошо известным примером является ZipList. (Это newtype который оборачивает списки и предоставляет разные Applicative экземпляр для них.)

fmap определяется обычным способом. Но pure а также <*> определяются как

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

так pure создает бесконечный список, повторяя данное значение, и <*> упаковывает список функций со списком значений - применяет i-ю функцию к i- му элементу. (Стандарт <*> на [] производит все возможные комбинации применения i-й функции к j- му элементу.) Но нет никакого разумного способа определить монаду (см. этот пост).

---

Как стрелки вписываются в иерархию функтор / аппликатив / монад? Видите, идиомы не обращают внимания, стрелки дотошны, монады неразборчивы от Сэма Линдли, Филиппа Уодлера, Джереми Яллопа. MSFP 2008. (Они называют аппликативные функторы идиомами.) Аннотация:

Мы вновь рассмотрим связь между тремя понятиями вычисления: монады Могги, стрелки Хьюза и идиомы Макбрайда и Патерсона (также называемые аппликативными функторами). Мы показываем, что идиомы эквивалентны стрелкам, удовлетворяющим изоморфизму типа A ~> B = 1 ~> (A -> B), и что монады эквивалентны стрелам, удовлетворяющим изоморфизму типа A ~> B = A -> (1 ~> Б). Далее, идиомы встраиваются в стрелки, а стрелки - в монады.

Answer 4

Хорошим примером для конструктора типа, который не является функтором, является Set: Вы не можете реализовать fmap :: (a -> b) -> f a -> f bпотому что без дополнительного ограничения Ord b ты не можешь построить f b,

Answer 5

Я хотел бы предложить более систематический подход к ответу на этот вопрос, а также показать примеры, в которых не используются специальные приемы, такие как "нижние" значения, бесконечные типы данных или что-то подобное.

Когда конструкторы типов не могут иметь экземпляры классов типов?

В общем, есть две причины, по которым конструктор типов может не иметь экземпляра определенного класса типов:

1. Невозможно реализовать сигнатуры типов необходимых методов из класса типов.
2. Может реализовывать подписи типа, но не может соответствовать требуемым законам.

Примеры первого типа проще, чем второго типа, потому что для первого типа нам просто нужно проверить, можно ли реализовать функцию с заданной сигнатурой типа, в то время как для второго типа мы должны доказать, что реализации нет мог бы удовлетворить законы.

Конкретные примеры

• Конструктор типа, который не может иметь экземпляр functor, потому что тип не может быть реализован:

data F a = F (a -> Int)

Это контрафунктор, а не функтор, потому что он использует параметр типа a в контравариантной позиции. Невозможно реализовать функцию с сигнатурой типа (a -> b) -> F a -> F b,

• Конструктор типа, который не является законным функтором, хотя подпись типа fmap может быть реализовано:

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!

Любопытным аспектом этого примера является то, что мы можем реализовать fmap правильного типа, хотя F не может быть функтором, потому что он использует a в контравариантной позиции. Так что эта реализация fmap показанное выше вводит в заблуждение - даже если он имеет правильную сигнатуру типа (я считаю, что это единственно возможная реализация этой сигнатуры типа), законы функтора не выполняются (для этого требуются некоторые простые вычисления).

По факту, F это всего лишь профессор, - он не является ни функтором, ни контрафунктором.

• Законный функтор, который не является аппликативным, потому что тип подписи pure не может быть реализовано: возьмите монаду Writer (a, w) и удалите ограничение, которое w должен быть моноидом. Тогда невозможно построить значение типа (a, w) снаружи a,

• Функтор, который не является аппликативным, потому что сигнатура типа <*> не может быть реализовано: data F a = Either (Int -> a) (String -> a),

• Функтор, который не является законно-аппликативным, хотя могут быть реализованы методы класса типов:

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

Конструктор типов P это функтор, потому что он использует a только в ковариантных позициях.

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

Единственно возможная реализация сигнатуры типа <*> это функция, которая всегда возвращает Nothing:

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

Но эта реализация не удовлетворяет закону тождества для аппликативных функторов.

• Функтор, который Applicative но не Monad потому что тип подписи bind не может быть реализовано.

Я не знаю таких примеров!

• Функтор, который Applicative но не Monad потому что законы не могут быть выполнены, даже если подпись типа bind может быть реализовано.

Этот пример вызвал немало дискуссий, поэтому можно с уверенностью сказать, что доказать правильность этого примера непросто. Но несколько человек подтвердили это независимо разными способами. См. `PoE данных a = Пусто | Пара монада? для дополнительного обсуждения.

 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

Несколько громоздко доказать, что нет законного Monad пример. Причина немонадного поведения заключается в том, что нет естественного способа реализации bind когда функция f :: a -> B b мог вернуться Nothing или же Just для разных значений a,

Это, возможно, яснее рассмотреть Maybe (a, a, a), что тоже не монада, и попробовать реализовать join для этого. Вы обнаружите, что не существует интуитивно разумного способа реализации 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.

В случаях, указанных ??? Кажется очевидным, что мы не можем производить Just (z1, z2, z3) любым разумным и симметричным образом из шести различных значений типа a, Конечно, мы могли бы выбрать произвольное подмножество этих шести значений, например, всегда брать первое непустое Maybe - но это не будет удовлетворять законам монады. возврате Nothing также не будет удовлетворять законам.

• Древовидная структура данных, которая не является монадой, хотя она имеет ассоциативность для bind - но не соответствует законам идентичности.

Обычная древовидная монада (или "дерево с ветвями в форме функтора") определяется как

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

Это бесплатная монада над функтором f, Форма данных представляет собой дерево, где каждая точка ветвления является "функторной" из поддеревьев. Стандартное двоичное дерево будет получено с type f a = (a, a),

Если мы изменим эту структуру данных, сделав также листья в форме функтора f мы получаем то, что я называю "полумонадой" - оно имеет bind который удовлетворяет законам естественности и ассоциативности, но его pure Метод не соответствует одному из законов идентичности. "Полумонады - это полугруппы в категории эндофункторов, в чем проблема?" Это тип класса Bind,

Для простоты я определяю join метод вместо 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)

Прививка ветви стандартная, но прививка листа нестандартная и дает Branch, Это не проблема для закона ассоциативности, но нарушает один из законов идентичности.

Когда у полиномиальных типов есть монады?

Ни один из функторов Maybe (a, a) а также Maybe (a, a, a) может быть дано законно Monad экземпляр, хотя они, очевидно, Applicative,

У этих функторов нет трюков - нет Void или же bottom в любом месте, без хитрой лени / строгости, без бесконечных структур и без ограничений класса типов. Applicative Экземпляр полностью стандартный. Функции return а также bind может быть реализовано для этих функторов, но не будет удовлетворять законам монады. Другими словами, эти функторы не являются монадами, потому что отсутствует определенная структура (но непросто понять, чего именно не хватает). Например, небольшое изменение в функторе может превратить его в монаду: data Maybe a = Nothing | Just a это монада Еще один подобный функтор data P12 a = Either a (a, a) это тоже монада.

Конструкции для полиномиальных монад

В общем, вот некоторые конструкции, которые производят законные Monad из полиномиальных типов. Во всех этих конструкциях M это монада:

1. type M a = Either c (w, a) где w любой моноид
2. type M a = m (Either c (w, a)) где m любая монада и w любой моноид
3. type M a = (m1 a, m2 a) где m1 а также m2 какие-нибудь монады
4. type M a = Either a (m a) где m любая монада

Первая конструкция WriterT w (Either c) вторая конструкция WriterT w (EitherT c m), Третья конструкция является компонентным произведением монад: pure @M определяется как компонентный продукт pure @m1 а также pure @m2, а также join @M определяется путем пропуска данных кросс-продукта (например, m1 (m1 a, m2 a) сопоставлен с m1 (m1 a) опуская вторую часть кортежа):

 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))

Четвертая конструкция определяется как

 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

Я проверил, что все четыре конструкции производят законные монады.

Я предполагаю, что нет других конструкций для полиномиальных монад. Например, функтор Maybe (Either (a, a) (a, a, a, a)) не получается ни через одну из этих конструкций и поэтому не является монадическим. Тем не мение, Either (a, a) (a, a, a) является монадическим, потому что оно изоморфно произведению трех монад a, a, а также Maybe a, Также, Either (a,a) (a,a,a,a) является монадическим, потому что оно изоморфно произведению a а также Either a (a, a, a),

Четыре конструкции, показанные выше, позволят нам получить любую сумму любого количества продуктов любого числа a х, например Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a)) и так далее. Все такие конструкторы типов будут иметь (как минимум один) Monad пример.

Конечно, еще предстоит выяснить, какие варианты использования могут существовать для таких монад. Другая проблема заключается в том, что Monad экземпляры, полученные с помощью конструкций 1-4, как правило, не являются уникальными. Например, конструктор типа type F a = Either a (a, a) можно дать Monad экземпляр двумя способами: по построению 4 с использованием монады (a, a) и по построению 3 с использованием типа изоморфизма Either a (a, a) = (a, Maybe a), Опять же, поиск вариантов использования для этих реализаций не сразу очевиден.

Остается вопрос - учитывая произвольный полиномиальный тип данных, как распознать, имеет ли он Monad пример. Я не знаю, как доказать, что для полиномиальных монад нет других конструкций. Я не думаю, что какая-либо теория существует до сих пор, чтобы ответить на этот вопрос.