Хорошие примеры не functor/functor/Applicative/Monad?
Объясняя кому-то, что такое класс класса X, я изо всех сил пытаюсь найти хорошие примеры структур данных, которые в точности соответствуют X.
Итак, я запрашиваю примеры для:
- Конструктор типа, который не является функтором.
- Конструктор типа, который является функтором, но не является аппликативным.
- Конструктор типа, который является аппликативным, но не является монадой.
- Конструктор типа, который является Монадой.
Я думаю, что во всем мире есть много примеров Монады, но хороший пример Монады с некоторым отношением к предыдущим примерам может завершить картину.
Я ищу примеры, которые были бы похожи друг на друга, отличающиеся только аспектами, важными для принадлежности к определенному типу класса.
Если бы можно было подкрасть пример Arrow где-нибудь в этой иерархии (это между Аппликативным и Monad?), это тоже было бы здорово!
Ответы
Ответ 1
Конструктор типа, который не является функтором:
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
Конструктор типа, который является функтором, но не аппликативным:
У меня нет хорошего примера. Существует Const
, но в идеале я хотел бы получить конкретный немонид, и я не могу думать ни о чем. Все типы в основном являются числовыми, перечислениями, продуктами, суммами или функциями, когда вы приступаете к нему. Вы можете видеть ниже свиноматок, и я не согласен с тем, что Data.Void
- Monoid
;
instance Monoid Data.Void where
mempty = undefined
mappend _ _ = undefined
mconcat _ = undefined
Так как _|_
является юридическим значением в Haskell и фактически является единственным юридическим значением Data.Void
, это соответствует правилам Monoid. Я не уверен, что с ним связано unsafeCoerce
, потому что ваша программа больше не гарантируется, чтобы не нарушать семантику Haskell, как только вы используете какую-либо функцию unsafe
.
См. Haskell Wiki для статьи внизу (ссылка) или небезопасных функций (ссылка).
Интересно, можно ли создать такой конструктор типа, используя более богатую систему типов, такую как Agda или Haskell с различными расширениями.
Конструктор типа, который является аппликативным, но не Monad:
newtype T a = T {multidimensional array of a}
Вы можете сделать аппликатор из него, с чем-то вроде:
mkarray [(+10), (+100), id] <*> mkarray [1, 2]
== mkarray [[11, 101, 1], [12, 102, 2]]
Но если вы сделаете это монадой, вы можете получить несоответствие размеров. Я подозреваю, что подобные примеры редко встречаются на практике.
Конструктор типа, который является монадой:
[]
О стрелках:
Запрашивая, где находится Arrow в этой иерархии, вы спрашиваете, какая форма "красная". Обратите внимание на несоответствие вида:
Functor :: * -> *
Applicative :: * -> *
Monad :: * -> *
но
Arrow :: * -> * -> *
Ответ 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 :: ()}
- Монада. Бросьте свои собственные.
Самолет поймать...
Ответ 3
Я считаю, что другие ответы пропустили некоторые простые и распространенные примеры:
Конструктор типа, который является функтором, но не аппликативным. Простым примером является пара:
instance Functor ((,) r) where
fmap f (x,y) = (x, f y)
Но нет способа определить свой экземпляр Applicative
, не налагая дополнительных ограничений на r
. В частности, нет способа определить pure :: a -> (r, a)
для произвольного r
.
Конструктор типа, который является аппликативным, но не является монодой. Хорошо известный пример ZipList. (Это a 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 ~ > B). Далее, идиомы, встроенные в стрелки и стрелы, вставляются в монады.
Ответ 4
Хорошим примером для конструктора типа, который не является функтором, является Set
: вы не можете реализовать fmap :: (a -> b) -> f a -> f b
, потому что без дополнительного ограничения Ord b
вы не можете построить f b
.
Ответ 5
Я хотел бы предложить более систематический подход к ответу на этот вопрос, а также показать примеры, в которых не используются какие-либо специальные приемы, такие как "нижние" значения, бесконечные типы данных или что-либо подобное.
Когда конструкторы типов не могут иметь экземпляры классов типов?
В общем, есть две причины, по которым конструктор типов может не иметь экземпляра определенного класса типов:
- Невозможно реализовать сигнатуры типов необходимых методов из класса типов.
- Может реализовывать подписи типа, но не может соответствовать требуемым законам.
Примеры первого типа проще, чем второго типа, потому что для первого типа нам просто нужно проверить, можно ли реализовать функцию с заданной сигнатурой типа, в то время как для второго типа мы должны доказать, что реализации нет мог бы удовлетворить законы.
Конкретные примеры
Это контрафунктор, а не функтор, поскольку он использует параметр типа 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 fa = (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)
и Maybe (a, a, a)
нельзя дать законный экземпляр Monad
, хотя они, очевидно, Applicative
.
У этих функторов нет трюков - ни Void
ни bottom
, ни хитрой лени/строгости, ни бесконечных структур, ни ограничений класса типов. Applicative
экземпляр полностью стандартный. Функции return
и bind
могут быть реализованы для этих функторов, но не будут удовлетворять законам монады. Другими словами, эти функторы не являются монадами, потому что отсутствует определенная структура (но непросто понять, чего именно не хватает). Например, небольшое изменение в функторе может превратить его в монаду: data Maybe a = Nothing | Just a
data Maybe a = Nothing | Just a
монада. Другой подобный функтор data P12 a = Either a (a, a)
также является монадой.
Конструкции для полиномиальных монад
В общем, вот некоторые конструкции, которые производят законную Monad
из полиномиальных типов. Во всех этих конструкциях M
является монадой:
-
type M a = Either c (w, a)
где w
- любой моноид -
type M a = m (Either c (w, a))
где m
- любая монада, а w
- любой моноид -
type M a = (m1 a, m2 a)
где m1
и m2
- любые монады -
type M a = Either a (ma)
где m
- любая монада
Первая конструкция - WriterT w (Either c)
, вторая конструкция - WriterT w (EitherT cm)
. Третья конструкция является компонентным произведением монад: 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
. Я не знаю, как доказать, что нет других конструкций для полиномиальных монад. Я не думаю, что какая-либо теория существует до сих пор, чтобы ответить на этот вопрос.