Являются ли все экземпляры Monad в Haskell разными способами для отображения из Hask в Hask?

Question

Я читаю Haskell/Category theory и вот definition of monad из этой статьи:

Монада представляет собой особый тип функтора из категории к той же категории , который поддерживает некоторые дополнительные структуры. Итак, до определений. Монада есть функтор М: С-> С, наряду с двумя морфизмов для каждого объекта X в C:

единица измерения: Х -> М (Х)

присоединиться: М (M (X)) -> M (X)

Как я понимаю, в Haskell return эквивалентно unit. Но с return я могу написать:

x :: [Int] -- x is a member of Lst category 
x = return 5 

и это правильный код в Haskell. Теперь, как вы можете видеть, 5 здесь не является членом Lst, но return работает на него.

Таким образом, я предполагаю, что Lst не С из М: C-> C. Но кто же тогда?

Может быть, правильный ответ Hask, но я не уверен, что «функтор из категории ее подкатегории» так же, как «функтор из категории к одной и той же категории».

Answer 1

Это общая точка смятения, и вы задали вопрос достаточно ясно, чтобы он отвечал.

Я не уверен, что «функтор из категории в это подкатегорию» так же, как «функтор из категории к одной и той же категории».

Это не то же самое. Функтор состоит из четырех частей данных: категории источников C, целевой категории D, отображения объектов C на объекты D и отображения морфизмов C в морфизмы D, удовлетворяющих некоторым условиям. Если вы измените D, вы измените функтор.

Однако, когда мы определяем функтор, мы часто имеем некоторый выбор в категории D.Я делаю вывод из вашего вопроса, что Lst является подкатегорией Hask, чьи объекты являются типами формы [a], хотя я не уверен, что должны быть морфизмы Lst. Мы могли бы определить функтор [] любого из этих двух форм:

1. []: Hask ->Lst (т.е. целевая категория [] является Lst)

2. []: Hask ->Hask (т.е. , целевая категория [] составляет)

Это технически разные функторы, и мы должны сделать выбор. В этом контексте правильный выбор - выбор 2. Нам нужны исходные и целевые категории, чтобы быть одинаковыми, потому что нам нужно применить [] к выходу [], в join. Таким образом, C = Hask и M = [].

В общем, редко бывает полезно рассмотреть такие категории, как Lst, которые определяются как изображение какого-либо конструктора типов. Я не уверен, откуда эта (очень распространенная) идея. Я рекомендую отложить идею «категории Lst». На данный момент достаточно одной категории!

Для аналогий рассмотрим функцию, квадратичную вещественное число f (x) = x^2. Мы можем рассматривать это как функцию f: R -> R от вещественных чисел до вещественных чисел, даже при том, что f (x) принимает только неотрицательные действительные значения. Цель f не должна быть равна изображению f (значения, которые фактически достигаются f на его входных значениях).

Answer 2

Монада по определению является эндофуктором. Код типа Functor действительно представляет собой endofunctors, поскольку экземпляры Functor определены для конструкторов типов, которые представляют собой функции уровня типа, которые берут тип и возвращают новый тип (то есть имеют вид * -> *).

return :: Monad m => a -> m a, так что не удивительно, что return может принимать значение типа Int и возвращает значение типа [Int].