Pull to refresh

Категория Hask

Haskell *

Вступление


В этой небольшой статье я расскажу о теории категорий в контексте системы типов языка Haskell. Никакой зауми, никаких уловок – постараюсь объяснять всё наглядно. Я хочу показать тесную связь языка программирования с математикой, чтобы спровоцировать у читателя осознание одного, через другое и наоборот.

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

Эта статья во многом повторяет (в том числе заимствует иллюстрации) раздел из английской Haskell Wikibook, но тем не менее не является непосредственным переводом.

Что такое категория?



Примеры


Для наглядности рассмотрим сначала пару картинок изображающих простые категории. На них есть красные кружочки и стрелки:

Красные кружочки изображают «объекты», а стрелки – «морфизмы».

Я хочу привести один наглядный пример из реальной жизни, который даст какое-то интуитивное представление о природе объектов и морфизмов:

Можно считать города «объектами», а перемещения между городами – «морфизмами». Например, можно представить себе карту авиарейсов (как-то не нашёл я удачную картинку) или карту железных дорог – они будут похожи на картинки выше, только сложнее. Следует обратить внимание на два момента, которые кажутся в реальности само собой разумеющимися, но для дальнейшего имеют важное значение:
  • Бывает, что из одного города в другой никак не попасть поездом или самолётом – между этими городами нет морфизмов.
  • Если мы перемещаемся в пределах одного и того же города, то это тоже морфизм – мы как бы путешествуем из города в него же.
  • Если из Санкт-Петербурга есть поезд до Москвы, а из Москвы есть авиарейс в Амстердам, то мы можем купить билет на поезд и билет на самолёт, “скомбинировать” их и таким образом попасть из Санкт-Петербурга в Амстердам – то есть можно на нашей карте нарисовать стрелку от Санкт-Петербурга до Амстердама изображающую этот скомбинированный морфизм.
Надеюсь, с этим примером всё понятно. А теперь немного формализма для чёткости.
Читать дальше →
Total votes 52: ↑49 and ↓3 +46
Views 15K
Comments 101

Эндофункторы категории Hask и их моноидальная структура

Haskell *

Введение


В предыдущей статье я рассказал о понятиях категории и функтора в контексте категории Hask, состоящей из типов данных и функций языка Haskell. Теперь я хочу рассказать о другом примере категории, построенном из уже известных нам понятий, а так же о весьма важном понятии моноида.

Обозначения


В прошлый раз я хотел обозначить морфизм/функцию буквой f, но она была занята для обозначения функтора/переменной типа f – никакой проблемы с точки зрения языка Haskell в этом нет, но при невнимательном прочтении это может вызвать путаницу, и я использовал для морфизма букву g. Пустяк, но всё же, я считаю, что полезно визуально разделять сущности, имеющие разную природу. Обычные типы я буду называть их обычными именами, а вот переменные типов я буду называть маленькими греческими буквами, причём простые () – буквами из начала алфавита, а параметрические (∗ → ∗) – буквами из конца алфавита (θ не из конца, но она смотрится лучше, чем χ, которая слишком похожа на X). Итак, в терминологии категории Hask:
  • Объекты: α, β, γ, δ ∷ ∗
  • Функторы: θ, φ, ψ, ω ∷ ∗ → ∗
  • Морфизмы: f, g, h ∷ α → β
Ввиду того, что GHC довольно давно поддерживает unicode, эти обозначения ничего не меняют в отношении синтаксиса и носят чисто косметический характер.

Ещё одно замечание, касательно терминологии: как вы уже заметили, то, что я в прошлый раз называл словом “кайнд” (kind), я теперь называю словом “сорт” – это считается общепринятым переводом.

Категория с объектом Hask


Давайте рассмотрим категорию, в которой будет только один объект – сама категория Hask. Что же будет морфизмами в такой категории? Это должны быть какие-то отображения HaskHask, и мы уже знаем такой тип отображений – это эндофункторы категории Hask, то есть типы сорта ∗ → ∗, воплощения класса Functor. Теперь нужно продумать как устроены единичный морфизм и композиция в этой категории, так чтобы они удовлетворяли аксиомам.
Читать дальше →
Total votes 29: ↑28 and ↓1 +27
Views 7.6K
Comments 44

Легкая прогулка от функтора через монаду к стрелке

Programming *Haskell *C# *

Давайте совершим прогулку по цепочке Pointed, Functor, Applicative Functor, Monad, Category, Arrow, в процессе которой я попытаюсь показать что все это придумано не для того что бы взорвать мозг, а для решения вполне реальных проблем, притом существующих не только в haskell. Большая часть кода написана на C#, но думаю и без его знания можно будет понять что к чему.
Читать дальше →
Total votes 55: ↑43 and ↓12 +31
Views 27K
Comments 152

Заметки с MBC Symposium: попытки разобраться, почему работает deep learning

Machine learning *

Продолжаю рассказывать об интересных докладах на MBC Symposium (MBC, кстати, расшифровывается как Mind Brain Computation).


image


Surya Ganguli — человек из теоретического neuroscience, то есть, занимается тем, чтобы понять, как работает мозг, на основе измерений импульсов нейронов на различных уровнях.


И вот тут независимо от neuroscience в мире случается deep learning, и у нас получается некую искусственную систему чему-то научить.
В отличие от мозга, в котором у нас ограниченное разрешение, сложность с повторяемостью, итд итп, про deep network-то мы знаем абсолютно все, про все веса, про все состояния. Возникает вопрос — если мы собираемся разобраться, как работает мозг, может попробуем для начала понять как и почему работает вот такая маленькая система?


Без надежд, что мозг работает также, скорее с прицелом разработать какие-то методы, которые могут быть применимы потом.

Читать дальше →
Total votes 29: ↑29 and ↓0 +29
Views 15K
Comments 6

Классы типов в Scala (с небольшим обзором библиотеки cats)

Scala *Functional Programming *

При слове "полиморфизм" сразу вспоминается объектно-ориентированное программирование, в котором полиморфизм является одним из столпов (Полиморфизм для начинающих). (Причём, по-видимому, более важным, чем другие столпы.) Оказывается, что можно достичь сходного эффекта и другим путём, который в ряде случаев оказывается более предпочтительным. Например, с помощью классов типов можно приписать новые возможности уже существующим типам, у которых нельзя изменить предка, или, используя тип данных с несовместимыми классами, "решить" проблему множественного наследования.

Читать дальше →
Total votes 21: ↑21 and ↓0 +21
Views 17K
Comments 12

Context category

Search engines *Semantics *Algorithms *Natural Language Processing *
Translation

The mathematical model of signed sequences with repetitions (texts) is a multiset. The multiset was defined by D. Knuth in 1969 and later studied in detail by A. B. Petrovsky [1]. The universal property of a multiset is the existence of identical elements. The limiting case of a multiset with unit multiplicities of elements is a set. A set with unit multiplicities corresponding to a multiset is called its generating set or domain. A set with zero multiplicity is an empty set.

Read more
Total votes 1: ↑1 and ↓0 +1
Views 855
Comments 0

Concordance of sense

Search engines *Semantics *Algorithms *Natural Language Processing *
Translation

In [1,2,3] texts (sign sequences with repetitions) were transformed (coordinated) into algebraic systems using matrix units as word images. Coordinatization is a necessary condition of algebraization of any subject area. Function (arrow) (7) in [1]) is a matrix coordinatization of text. One can perform algebraic operations with words and fragments of matrix texts as with integers, but taking into account the noncommutativity of multiplication of words as matrices. Structurization of texts is reduced to the calculation of ideals and categories of texts in matrix form.

Read more
Total votes 1: ↑1 and ↓0 +1
Views 438
Comments 0

Collective meaning recognition

Search engines *Semantics *Algorithms *Natural Language Processing *
Translation

The published material is in the Appendix of my book [1]

Modern civilization finds itself at a crossroads in which to choose the meaning of life. Because of the development of technology, the majority of the world's population may be "superfluous" - not in demand in the production of values. There is another option, where each person is a supreme value, an absolute individual and can be indispensably useful in the technology of the collective mind.

In the eighties of the last century, the task of creating a scientific field of "collective intelligence" was set. Collective intelligence is defined as the ability of the collective to find solutions to problems more effectively than each participant individually. The right collective mind must be...

Read more
Total votes 2: ↑2 and ↓0 +2
Views 638
Comments 0