вторник, октября 19, 2010

Haskell monads для физматовца. Краткое введение

Ну что, попробую пополнить ряды haskell newbies ;)

Я не уверен, что данная заметка сделает концепцию монад понятнее для профессиональных программистов на чём-нибудь типа Java. Но я надеюсь, что она поможет людям с некоторым математическим бэкграундом. Но даже им, думаю, эта заметка поможет в практическом программировании только в сочетании с другими monad tutorials.

АФАИК, во многих наших провинциальных вузах на физмат-специальностях теория категорий (вместе с современной теорией множеств) игнорируется полностью (т.е. о её существовании за 4-5-6 лет ни разу не упоминают даже, как это было у меня). Я не собираюсь излагать всю теорию — кому нужно, смотрите книжки или хотя бы википедию. Я изложу только то, что нужно для нашего применения.

Категории

Итак. Вводится понятие категории. Это некая очень абстрактная сущность (абстрактнее даже, чем множество). В некотором смысле, категория состоит из двух вещей: набора объектов и набора морфизмов. Относительно этих объектов и морфизмов выполняются какие-то там аксиомы. Из них следует, что категорию можно представлять в виде направленного графа, где вершины — это объекты категори, а дуги — это морфизмы категории. Существенно, что у морфизма, как у дуги графа, есть «начало» и «конец» (называемые домен и кодомен), и это объекты той же категории. Домен и кодомен морфизма (начало и конец дуги графа) могут совпадать. Такой морфизм называется эндоморфизмом.

Классический пример категории — Set. Объекты категории Set — это всевозможные множества, а морфизмы — это функции между этими множествами.

Более интересный для нас пример: категория Hask. Здесь объекты — это типы данных, возможные в языке Haskell, а морфизмы — функции языка Haskell.

Функторы

Следующее понятие: функтор. Функтор — это, условно говоря, отображение одной категории в другую. При этом функтор отображает объекты первой категории в объекты второй, а морфизмы первой — в морфизмы второй категории. К тому же накладываются определённые ограничения — аксиомы.

Если функтор отображает категорию саму в себя, такой функтор называется эндофунктором.

Возьмём нашу категорию Hask. Любой полиморфный тип данных языка Haskell с одним тИповым аргументом задаёт отображение, сопоставляющему каждому объекту категории Hask (т.е. типу языка Haskell) какой-то другой объект (другой тип). Например, конструктор типов [] сопоставляет любому типу a тип [a] (список элементов типа a). Конструктор типов Maybe сопоставляет каждому типу a другой тип — Maybe a (значение типа a или никакого значения). Таким образом, мы можем привести много примеров отображений класса объектов категории Hask в объекты той же категории. Пусть, например, у нас есть конструктор типов C (т.е. где-то написано data C a = …).

Если теперь такое отображение объектов (конструктор типов C с одним параметром) дополнить отображением морфизмов, то получим функтор, действующий из Hask в Hask (говорят «эндофунктор на категории Hask»). Напомню, морфизм категории Hask между объектами (типами) a и b — это любая функция типа a → b. Согласно аксиомам функторов, морфизм между объектами a и b должен отображаться в морфизм между объектами (C a) и (C b). Таким образом, отображение морфизмов должно быть функцией следующего вида:

    fmap :: (a -> b) -> (C a -> C b)

В модуле Prelude определён класс типов Functor:

    class Functor f where
fmap :: (a -> b) -> (f a -> f b)

Итак, любой тип, являющийся экземпляром класса Functor, является эндофунктором на категории Hask (т.е., название класса Functor не вполне точное, его бы следовало назвать, скажем, HaskEndoFunctor). При этом сам конструктор типов задаёт отображение объектов (типов), а связанная с ним функция fmap задаёт отображение морфизмов (функций).

Моноиды

Моноид — это термин несколько из другой (хоть и смежной) области — из абстрактной алгебры. Моноид определяется следующими вещами:

  • Множество M;

  • Бинарная операция ⊕ на этом множестве; от неё требуется ассоциативность;

  • Нейтральный элемент ε этой операции, входящий в множество (т.е. такой, что (∀a ∈ M) ε⊕a = a⊕ε = a).

Можно видеть, что моноид — это ослабление понятия группы. Благодаря этому, очень многие структуры являются моноидами. Ну, скажем, множество действительных чисел с операцией сложения. Или множество списков элементов какого-то одного типа с операцией (++).

Монады

Ну а теперь главное определение ;). Монада — это моноид в категории эндофункторов. Расшифровываю.

Пусть у нас есть какой-нибудь эндофунктор на категории Hask (т.е. тип f, являющийся экземпляром класса Functor). Дополним его структурой моноида. Для этого нам понадобится бинарная операция и её единичный элемент. Подходящая бинарная операция традиционно называется bind (и в haskell обозначается >>=). Подходящий единичный элемент традиционно называется return. В Haskell это выражается в следующее определение:

    class Monad m where
(>>=) :: m a -> (a -> m b) -> m b -- бинарная операция
return :: a -> m a -- единичный элемент

В модуле Prelude объявлены экземпляры класса Monad для некоторых типов: [], Maybe, итп.

К чему это я всё

Из всего вышесказанного можно вывести очевидную вещь: монады — очень абстракная сущность. Настолько абстрактная, что чуть ли не всё на свете является монадой.

С другой стороны, это очень простая штука: некий аналог действия «композиция функций», только при композиции используется какая-то дополнительная информация.

9 комментариев:

  1. как же оно все подзабылос.

    да и хаскел сказался мне другим. ну поглядим.

    ОтветитьУдалить
  2. Подходящая бинарная операция традиционно называется bind (и в haskell обозначается >>=).
    Не-не-не. Вводим моноидальную структуру в категории эндофункторов. Обобщаем моноид (теоретико-множественный) до моноида в моноидальной категории (monoid object). А бинарная операция — это
    join :: m (m a) -> m a
    или в математике
    μ : естественное преобразование m∘m→m

    ОтветитьУдалить
  3. > в виде направленного графа, где вершины — это объекты категори, а дуги — это морфизмы категории.

    Неправильно. Если уж вы собираетесь представлять категорию дграфами, то стрелки будут путями.

    ОтветитьУдалить
  4. Вы очень неплохо дали определение монады. Но так и не понятно как они используются, для чего было вообще введено такое понятие?

    ОтветитьУдалить
  5. Но так и не понятно как они используются, для чего было вообще введено такое понятие?
    Ну, если брать монады вообще, то AFAIK монада — это аксиоматизация категории алгебраических структур. Это наиболее общая мотивация, которая мне известна. А частные случаи можно поискать в интернете.

    ОтветитьУдалить
    Ответы
    1. Автор очень хорошо изложил основные понятия, однако вывод о монадах какой-то излешне поверхностный.
      Если говорить о монадах в функциональных ЯП, то это просто паттерн, позволяющий привести функцию одного вида к функции другого вида, используемый для инкапсуляции побочных эффектов.

      Исходя даже из этого определения становится понятно, что монада является моноидом в категории эндофункторов, исходя из указанных определений, но её роль, и что же она на самом деле из себя представляет автор проигнорировал.

      Удалить
    2. Если говорить о монадах в функциональных ЯП, то это просто паттерн, позволяющий привести функцию одного вида к функции другого вида, используемый для инкапсуляции побочных эффектов.
      Однако зависимость декларации от рефакторинга является слишком поверхностной. Чтобы трактовать проблематику посредника в агрегации функций, недостаточно механически выучить теорию категорию. Глубокое проникновение в сущность отношения «общее-частное» приводит к транквилизации путей сообщения. Таким образом, автор вполне обоснованно проигнорировал шизофрению принципов ООП.

      Удалить
  6. читайте Conceptual mathematics : a first introduction to categories /. F. William Lawvere and Stephen H. Schanuel

    http://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0CB0QFjAA&url=http%3A%2F%2Ffef.ogu.edu.tr%2Fmatbil%2Feilgaz%2Fkategori.pdf&ei=SjQHVfWKGInmyQOSjoDICg&usg=AFQjCNH0AaJJcY9f0yxe8ttoN5Vu9XC0cA&sig2=JuIzPmANeQpYEBAEC0dL1w&bvm=bv.88198703,d.bGQ

    ОтветитьУдалить