Типы и функции

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

Кому нужны типы?

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

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

Внимание, вопрос - мы хотим, чтобы обезьяны были довольны, или мы хотим писать корректные программы?

Обычная задача эксперимента с печатающими обезьянами - написание полного собрания сочинений Шекспира. Наличие программ проверки орфографии и грамматики резко увеличит вероятность ее выполнения. Можно пойти дальше и ввести проверку типов. Например, если Ромео описан как человек, то он не должен прорасти листьями и не будет ловить фотоны своим мощным гравитационным полем.

Типы нужны для компонуемости

Теория категорий рассматривает композиции стрелок. Но не все стрелки могут быть скомпонованы. Целевой объект одной стрелки должен совпадать с исходным объектом следующей. В программировании мы передаем результат одной функции другой. Программа не будет работать, если целевая функция не способна корректно обработать результат исходной функции. Композиция требует совместимых объектов. Чем мощнее система типов языка программирования, тем лучше можно описать и автоматически проверить требования к совместимости.

Единственный серьезный аргумент против сильной статической типизации, что я слышал, - проверка типов может не пропустить некоторые семантически корректные программы. Это крайне редко происходит на практике, да и любой язык предоставляет хоть какие-то способы обойти систему типов, если это действительно необходимо. Даже в Haskell есть unsafeCoerce. Но подобные инструменты должны использоваться рассудительно. Грегор Замза, персонаж Франца Кафки, обошел систему типов, когда превратился в огромного жука, и все мы прекрасно знаем, чем закончилась его история.

Другой частый аргумент - работа с типами обременяет программиста. Я мог бы выразить сочувствие этому мнению, так как я тоже писал объявления итераторов в C++, но не буду - есть технология под названием вывод типов, которая позволяет компилятору определять большинство типов из контекста, в котором они используются. В C++ теперь можно объявить переменную как auto, и компилятор разберется, какой у нее тип.

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

Статическая сильная типизация часто используется в качестве оправдания отсутствию тестов. Иногда можно услышать, как Haskell-программисты говорят: "Если код компилируется, он должен быть корректным." Конечно, нет никакой гарантии, что корректная в смысле типов программа так же корректна в смысле выдачи правильных результатов. Такое наплевательское отношение привело к тому, что в нескольких исследованиях Haskell не оказался на голову выше в плане качества кода, как можно было бы ожидать. Похоже, что при коммерческой разработке ошибки исправляются только до достижения определенного уровня качества, определяемого экономикой разработки программного обеспечения и терпимостью конечного пользователя, но практически не связанного с языком программирования или методологией. Лучшим критерием было бы измерение количества проектов, которые не укладываются в расписание или выпускаются с сильно урезанной функциональностью.

Что же касается аргумента, утверждающего, что юнит-тестирование может заменить сильную типизацию, то давайте рассмотрим обычный подход к рефакторингу в статически типизированных языках при смене типа аргумента отдельной функции. В статически типизированном языке достаточно изменить объявление функции, а затем исправить все ошибки при сборке. В динамически типизированном языке факт, что функция ожидает другие данные, нельзя распространить на места вызова этой функции. Юнит-тестирование может выловить некоторые несовпадения, но тестирование - это почти всегда вероятностный процесс, не детерминированный. Тестирование - слабая замена доказательству.

Что такое типы?

Простейшее интуитивное представление типов - это множества значений. Тип Bool (помните, что названия конкретных типов начинаются с заглавной буквы в Haskell?) - это множество из двух элементов: True и False. Тип Char - множество всех символов Юникода, например, 'a' или 'ą'.

Множества могут быть конечными и бесконечными. Тип String, который является синонимом для списка Char - это пример бесконечного множества.

Когда мы объявляем, что x является Integer:

x :: Integer

мы говорим, что x - это элемент множества целых чисел. Integer в Haskell является бесконечным множеством и может быть использован для арифметики с произвольной точностью. Так же есть конечное множество Int, которое соответствует машинному типу, по аналогии с int из C++.

Есть некоторые тонкости, которые запутывают такое отождествление типов и множеств. Например, есть проблемы с полиморфными функциями с циклическими определениями и с тем, что не существует множества всех множеств, но, как я и обещал, я не буду ярым сторонником математики. Самое замечательное в том, что существует категория множеств, которая называется Set, и мы будем просто работать с ней. В Set объектами являются множества, а морфизмами (стрелками) - функции.

Set - особенная категория, потому что мы можем заглянуть внутрь объектов и составить интуитивное представление о многих понятиях. К примеру, мы знаем, что пустое множество не содержит элементов. Мы знаем, что существуют особые множества из одного элемента. Мы знаем, что функции сопоставляют элементы одного множества элементам другого. Они могут сопоставить два элемента одному, но не могут сопоставить один элемент двум. Мы знаем, что тождественная функция сопоставляет каждый элемент множества ему самому, и так далее. План следующий: постенно забыть всю эту информацию и вместо этого выразить эти понятия в терминах теории категорий, то есть в терминах объектов и стрелок.

В идеальном мире мы бы просто сказали, что типы в Haskell являются множествами, а функции - это математические функции на множествах. Есть только одна маленькая проблема: математическая функция не исполняет никакого кода - она просто знает ответ. Haskell-функция должна вычислить ответ. Не проблема, когда ответ можно получить за конечное число шагов, и неважно, насколько большим это число может быть. Но существуют вычисления с рекурсией, и они могут никогда не завершиться. Мы не можем просто запретить незавершающиеся функции в Haskell, так как проблема различения завершающихся и незавершающихся функций неразрешима - это известная проблема останова. Вот почему информатики придумали блестящее решение, или крупный хак (зависит от точки зрения), - расширить каждый тип одним специальным значением, которое называется bottom и обозначается _|_ (или ⊥ в Юникоде). Это значение соответствует незавершающемуся вычислению. Так что функция, определенная как:

f :: Bool -> Bool

может вернуть True, False или _|_; последнее означает, что функция никогда не остановится.

Интересно, что как только мы примем bottom как часть системы типов, становится удобно трактовать каждую ошибку времени исполнения как bottom и даже позволять функциям явно возвращать bottom. Последнее обычно делается с использованием выражения undefined, как в этом случае:

f :: Bool -> Bool
f x = undefined

Это определение проходит проверку типов, потому что undefined возвращает bottom, который является членом любого типа, включая Bool. Можно даже написать:

f :: Bool -> Bool
f = undefined

(без x), так как bottom является членом типа Bool -> Bool.

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

Из-за bottom категория типов и функций Haskell называется Hask, а не Set. С точки зрения теории это неиссякаемый источник осложнений, так что на данном этапе я воспользуюсь моим тесаком и обрублю эту ветвь рассуждений. С точки зрения практики нормально игнорировать незавершающиеся функции и bottom и рассматривать Hask как честный Set (см. библиографию в конце главы).

Зачем нам нужна математическая модель?

Как программист Вы хорошо знакомы с синтаксисом и грамматикой Вашего языка программирования. Эти аспекты обычно описаны с использованием формальной нотации в самом начале спецификации языка программирования. Но смысл, или семантику, языка описать значительно сложнее - описание семантики занимает намного больше страниц, редко достаточно формально и почти всегда неполно. Отсюда следуют бесконечные дискуссии между адвокатами языков программирования и целая индустрия книг, посвященных толкованию тонких моментов из стандартов языков программирования.

Существуют формальные инструменты для описания семантики языка программирования, но, из-за их сложности, они в основном используются для упрощенных академических языков, а не для мастодонтов программирования из реальной жизни. Один такой инструмент под названием операционная семантика описывает механику выполения программы. Он определяет формализованный идеализированный интерпретатор. Семантика промышленных языков, таких как C++, обычно описывается с использованием неформальных операционных рассуждений, часто в терминах некой "абстрактной машины".

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

И неважно, что программисты никогда не проводят формального доказательства корректности. Мы всегда "думаем", что мы пишем корректные программы. Никто не сидит у клавиатуры с мыслью: "О, я просто набросаю пару строчек кода и посмотрю, что произойдет". Мы думаем, что написанный код будет выполнять определенные действия, которые приведут к желаемым результатам. Мы обычно довольно удивлены, когда это не так. Это значит, что мы рассуждаем о программах, когда пишем их, и мы обычно делаем это, запуская интерпретатор у нас в голове. Просто очень сложно отслеживать все переменные. Компьютеры хорошо выполняют программы, а люди нет! В противном случае нам не нужны были бы компьютеры.

Но есть альтернатива. Она называется денотационная семантика и основана на математике. В денотационной семантике каждой конструкции языка программирования дается ее математическая интерпретация. Так что, если нужно доказать свойство программы, необходимо доказать математическую теорему. Можно подумать, что доказывать теоремы тяжело, но на самом деле люди развивают математические методы тысячи лет, поэтому есть немало накопленных знаний на эту тему. К тому же, в сравнении с теоремами, которые доказывают профессиональные математики, теоремы, встречаемые в программировании, очень простые, если не тривиальные.

Рассмотрим определение функции факториала в Haskell - в языке, который вполне поддается денотационной семантике:

fact n = product [1..n]

Выражение [1..n] определяет список целых чисел от 1 до n. Функция product перемножает все элементы списка. Похоже на определение факториала, взятое из книги по математике. Сравним с C:

int fact(int n) {
    int i;
    int result = 1;
    for (i = 2; i <= n; ++i)
        result *= i;
    return result;
}

Стоит ли продолжать?

Да, признаюсь, это был дешевый трюк. Функция факториала имеет очевидный математический смысл. Проницательный читатель может спросить: "Какова математическая модель для чтения символа с клавиатуры или для отправки пакета по сети?" Долгое время это был неудобный вопрос, ведущий к довольно запутанным объяснениям. Казалось, что денотационная семантика не подходит для значительного числа важных задач, необходимых для написания полезных программ и которые операционная семантика описывала с легкостью. Прорыв произошел при помощи теории категорий. Евгенио Моджи установил, что вычислительный эффект может быть представлен с помощью монад. Это оказалось важным наблюдением, которое не только вдохнуло новую жизнь в денотационную семантику и сделало чистые функциональные программы более полезными, но и пролило новый свет на традиционное программирование. Я расскажу о монадах позже, когда мы нарастим наш инструментарий в теории категорий.

Одним из важнейших преимуществ наличия математической модели программирования является возможность выполнения формальных доказательств корректности программного обеспечения. Это может показаться не столь важным для обычной коммерческой разработки, но есть области программирования, где стоимость сбоя может быть непомерной или где на кону жизни людей. Но даже при разработке веб-приложений для системы здравоохранения хорошо знать, что к функциям и алгоритмам из стандартной библиотеки Haskell прилагаются доказательства корректности.

Чистые и грязные функции

Функции в C++ или другом императивном языке программирования и функции в понимании математиков - разные вещи. Математическая функция просто отображает одни значения на другие значения.

Мы можем реализовать математическую функцию в языке программирования - такая функция, получив входное значение, рассчитает выходное значение. Функция вычисления квадрата числа, вероятнее всего, умножит входное значение на него же. Она будет делать это при каждом вызове, и гарантируется, что функция будет выдавать одинаковый результат при каждом вызове с одним и тем же входным значением. Квадрат числа не зависит от смены фаз Луны.

Так же, расчет квадрата числа не должен иметь побочного эффекта в виде угощения Вашей собаки вкусняшками. "Функция", которая имеет подобные побочные эффекты, не может быть легко смоделирована как математическая функция.

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

Примеры типов

Как только Вы поймете, что типы - это множества, Вы можете задуматься о некоторых довольно экзотических типах. К примеру, какой тип соответствует пустому множеству? Нет, это не void из С++, хотя в Haskell такой тип называется как раз-таки Void. Это тип, в котором нет никаких значений. Вы можете определить функцию, которая принимает Void в качестве аргумента, но никогда не сможете ее вызвать. Чтобы ее вызвать, потребуется передать значение типа Void, а таких значений не существует. Что же касается возвращаемых значений, то здесь нет никаких ограничений. Она может вернуть любой тип (хотя никогда не вернет, потому что не будет вызвана). Другими словами, это функция, полиморфная по возвращаемому значению. У Haskell-программистов есть название для нее:

absurd :: Void -> a

(Напомню: a - это переменная типа, которая может быть любым типом.) Это название неслучайно. Существует более глубокое толкование типов и функций в терминах логики, называемое изоморфизмом Карри-Говарда. Тип Void представляет ложь, а тип функции absurd соответствует утверждению, что из ложного высказывания следует все, что угодно - как в латинской поговорке “ex falso sequitur quodlibet.”

Следующим рассмотрим тип, соответствующий множеству-одиночке. Это тип, который имеет только одно возможное значение. Это значение просто "есть". Вы можете не сразу это заметить, но таким типом является void из C++. Подумайте о функциях, определенных для этого типа. Функция, принимающая void, всегда может быть вызвана. Если это чистая функция, она всегда вернет одно и то же значение. Вот пример такой функции:

int f44() { return 44; }

Вы можете подумать, что эта функция принимает в качестве аргумента "ничто", но, как мы уже увидели, функция с аргументом "ничто" не может быть вызвана, потому что не существует значения, представляющего "ничто". Так что же принимает эта функция? Концептуально, она принимает фиктивное значение, у которого всегда есть только один экземпляр, так что нам не нужно указывать его явно. В Haskell, однако, есть символ для такого значения - пустая пара скобок, (). Так что, из-за забавного совпадения (а совпадение ли это?), вызов функции void выглядит одинаково и в C++, и в Haskell. Также, из-за любви Haskell к краткости, тот же символ () используется для обозначения типа, его конструктора и единственного значения, соответствующего множеству-одиночке. Та же самая функция в Haskell:

f44 :: () -> Integer
f44 () = 44

На первой строке объявлено, что f44 принимает аргумент типа () (произносится как "unit") и возвращает значение типа Integer. Вторая строка определяет f44 путем сопоставления с образцом (pattern matching) единственного конструктора unit (а именно ()) и возвращения числа 44. Вы можете вызвать эту функцию, предоставив значение unit ():

f44 ()

Обратите внимание, что каждая функция с аргументом типа unit эквивалентна выбору единственного элемента из возвращаемого типа (в примере мы берем Integer 44). На самом деле, можно рассуждать о f44 как о другом представлении числа 44. Это пример того, как мы можем заменить явное упоминание элементов множества на функции (стрелки). Функции от unit на любой тип A - это взаимно однозначное соответствие для элементов множества A.

Что насчет функций с возвращаемым типом void (unit в Haskell)? В C++ такие функции используются для побочных эффектов, но мы знаем, что это не настоящие функции в математическом смысле этого слова. Чистая функция, которая возвращает unit, не делает ничего - она отбрасывает аргумент.

Математически, функция из множества A на множество-одиночку сопоставляет каждый элемент A единственному элементу этого множества-одиночки. Для любого A существует только одна такая функция. Вот эта функция для Integer:

fInt :: Integer -> ()
fInt x = ()

Мы передаем в функцию любое целое число, а она возвращает unit. Следуя принципу краткости, Haskell позволяет использовать подстановочный шаблон (подчеркивание) для отбрасываемого аргумента. Таким образом, не нужно придумывать для него название. Так что верхний пример можно переписать так:

fInt :: Integer -> ()
fInt _ = ()

Обратите внимание, что реализация этой функции не только не зависит от значения аргумента - она даже не зависит от типа аргумента.

Функции, которые могут быть реализованы одинаково для любого типа, называются параметрически полиморфными. Вы можете реализовать целое семейство таких функций одним уравнением, используя переменную типа вместо конкретного типа. Как мы можем назвать полиморфную функцию от любого типа к типу unit? Конечно, мы назовем ее unit:

unit :: a -> ()
unit _ = ()

В C++ мы можем написать эту функцию следующим образом:

template<class T>
void unit(T) {}

Далее в типологии типов мы рассмотрим множество из двух элементов. В C++ оно называется bool, а в Haskell - предсказуемо - Bool. Различие в том, что в C++ bool - это встроенный тип, в то время как в Haskell он может быть определен таким образом:

data Bool = True | False

(Читать это определение следует так - Bool может быть либо True, либо False.) В принципе, можно определить булев тип в C++ как перечисление:

enum bool {
    true,
    false
};

Но в C++ перечисление на самом деле - это число. Можно использовать "enum class" из C++11, но тогда придется уточнять его значения названием класса (bool::true или bool::false), не говоря уже о необходимости подключать соответствующий заголовочный файл в любом модуле, который его использует.

Чистые функции из Bool просто выбирают два значения из целевого типа, одно из которых соответствует True, а другое - False.

Функции, возвращающие Bool, называются предикатами. К примеру, библиотека Haskell Data.Char полна такими предикатами как, например, isAlpha или isDigit. В C++ есть похожая библиотека, в которой определены среди прочего isalpha и isdigit, но эти функции возвращают int, а не булевы значения. Настоящие предикаты определены в std::ctype и имеют вид ctype::is(alpha, c), ctype::is(digit, c) и так далее.

Упражнения

1. Определите функцию высшего порядка (или функциональный объект) memoize в Вашем любимом языке программирования. Эта функция принимает в качестве аргумента чистую функцию f и возвращает функцию, которая ведет себя почти как f, за исключением того, что она вызывает оригинальную функцию только один раз для каждого аргумента, сохраняет результат, а затем возвращает этот сохраненный результат при каждом вызове с тем же аргументом. Вы можете отличить мемоизированную функцию от оригинальной, сравнив производительность. Например, попробуйте мемоизировать функцию, которая требует немало времени на вычисление. Нужно будет подождать результат при первом обращении к функции, но при последующих вызовах с тем же аргументом Вы получите результат немедленно.

2. Попробуйте мемоизировать функцию из стандартной библиотеки Вашего языка программирования, которую Вы обычно используете для генерации случайных чисел. Работает ли полученная функция?

3. Большинство генераторов случайных числе могут быть инициализированы неким seed. Реализуйте функцию, которая принимает seed, вызывает генератор случайных чисел с этим seed и возвращает результат. Мемоизируйте эту функцию. Работает ли полученная функция?

4. Какая из этих функций C++ чистая? Попробуйте мемоизировать их и понаблюдайте, что происходит, если Вы вызовете несколько раз мемоизированную версию и оригинальную.

   • Функция факториала из примера в тексте главы.

   • std::getchar()

   • bool f() {
       std::cout << "Hello!" << std::endl;
       return true;
     }

     int f(int x)
     {
       static int y = 0;
       y += x;
       return y;
     }

1. Сколько существует различных функций из Bool на Bool? Можете ли Вы реализовать их все?

2. Нарисуйте категорию, все объекты которой - это типы Void, () (unit) и Bool, а стрелки соответствуют всем возможным функциям между этими типами. Обозначьте стрелки названиями этих функций.

Библиография

1. Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons, Fast and Loose Reasoning is Morally Correct. Эта статья обосновывает игнорирование bottom в большинстве случаев.

Ценные комментарии

sclv

Уточнение: я думаю, Вы немного путаете денотационную и категориальную семантики. Я только что проверил статью Моджи "Понятие вычисления и монады", и он действительно противопоставляет свой подход, который он описывает как категориальную семантику, остальным трем семантикам: денотационной, логической и операционной. Также денотационная семантика до Моджи уже могла рассматривать эффекты, только не так удобно - на самом деле, подход (с точки зрения Стрейчи, а не Скотта) был мотивирован попытками понять языки наподобие C, и, в действительности, в работе Стрейчи впервые была представлена идея lvals!

По похожим причинам это утверждение ложно: "В чистом функциональном языке, например в Haskell, все функции чистые. Поэтому есть возможность назначить этим языкам денотационную семантику и моделировать их, используя теорию категорий." Ложность заключается в том, что мы так же можем дать императивным языкам денотационную семантику и моделировать их, используя теорию категорий (или, скорее, моделировать, применяя денотационную семантику с заимствованиями из теории категорий - подлинная категориальная семантика быстро становится пугающей и не используется для "реальных" языков, насколько я знаю). Вот, к примеру, статья о денотационной семантике ANSI C (реализованной, конечно, на Haskell :P) - http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-2001-dsac.pdf.

Я считаю, что денсем и теория категорий (что не одно и то же - классический денсем основан на теории множеств) должны преподноситься не как единственный способ решения проблем, но как способ с определенными преимуществами.

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

Bartosz Milewski

@sclv: Рад, что Вы не даете мне расслабиться ;-). Я заменил "есть возможность" на "проще" в некорректном предложении (что хорошо в блогах - можно их улучшать со временем).

Что касается денотационной семантики против категориальной семантики, то предпочел бы избежать проведения настолько тонких различий. Думаю, что Ваше ключевое наблюдение - "классический денсем основан на теории множеств". Тогда я бы сказал, что "современный денсем основан на теории категорий".

philipjf

@sclv: Не самое важное замечание, но идея, что денотационная семантика означает "интерпретацию в категории", стала довольно распространенной. К примеру, Карвальо в "Execution Time of λ-Terms via Denotational Semantics and Intersection Types" говорит, что "фундаментальная идея денотационной семантики заключается в том, что типы нужно интерпретировать как объекты категории C, а термы - в качестве стрелок в C таким образом, что если терм t редуцируется к терму t', тогда они интерпретируются одной и той же стрелкой." Уверен, что если бы я попробовал, то мог бы найти других людей, говорящих по сути то же самое.

Я не знаю, согласен ли я с такой точкой зрения: разные люди имеют в виду разные понятия, когда говорят "денотационная семантика", - часто имеется в виду нечто вроде "семантики Скотта". В контексте логики "денотационная семантика" обычно отличается от других моделей тем, что она моделирует доказательства, а не просто доказуемость. Тем не менее, есть определенное преимущество во взгляде "денотационная значит категориальная" - он дает конкретное направление для исследований по поиску моделей, которое выглядит примерно так: 1. укажите, что нужно в категории, чтобы моделировать Ваш язык 2. придумайте категорию с этими свойствами. Это направление исследований, которого явно придерживаются такие люди, как Ларс Биркендаль (по крайней мере, я слышал, что он описывает свою работу подобным образом), и похоже на то, что происходит с такими людьми, как Самсон Абрамски. Так что, хотя это может быть не универсальная перпектива, но, кажется, было бы сложно спорить, что плохая.

И наконец, вопрос, была ли "классическая денотационная семантика" категориальной, - это вопрос о том, что означает "традиционная денотационная семантика". Но если предполагается, что это был ранний Скотт, то ответ таков: хотя Скотт и избегал использования категориального языка, я думаю, довольно ясно, что он был вдохновлен категориальными идеями. Они явно прослеживаются в статьях, как "Data Types as Lattices", но я думаю, что эти идеи подразумевались в “Outline of a mathematical theory of computation.” Действительно, собственная версия истории Скотта подчеркивает важность теории категорий для развития лямбда-исчисления и описывает его основной вклад как теорему о том, что "категория $x = y$-топологических пространств с отношением эквивалентности и непрерывными функциями, соответствующими эквивалентности, является декартово замкнутой". Источник - http://youtu.be/7cPtCpyBPNI.

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

sclv

@philipjf. Моя точка зрения заключалась не в том, что люди свободно используют термины для обозначения многих понятий. Дело в том, что приведенная историческая ссылка вводит в заблуждение, особенно, если читатель обратится к работе Моджи, он увидит, что тот обсуждает категориальную семантику в отличие от денотационной!

...

В конце концов, в Haskell был практичный, хоть и неудобный, подход к вводу/выводу даже до монад. Большая часть работы Плоткина над эффектами предлагает альтернативную историю, в которой монады не были так чрезмерно задействованы, и наводит на мысль, какими иными путями мы могли пойти в итоге. Эти пути, конечно, в конце концов были бы очень категориальными, но несколько иными.

James Iry

Я не любитель фраз "сильная типизация" и "слабая типизация", потому что они часто используются для обозначения разных понятий. Я слышал и читал ВСЕ следующие значения в обычных разговорах и академических статьях:

1) слабая = динамическая, сильная = статическая;

2) слабая = много автоматических приведений (например, JavaScript и C++), сильная = относительно немного (к примеру, Scheme и Haskell);

3) слабая = неопределенное поведение/небезопасная работа с памятью (C, Fortran, Pascal и C++), сильная = безопасная работа с памятью (большинство популярных языков [без учета FFI и прочего]);

4) слабая = относительно ограниченные статические системы типов (например, все динамически типизированные языки программирования, но так же C и Pascal), сильная = относительно богатые системы типов (Haskell и Scala). Думаю, что по такому определению Java и C# были бы среднесильными, а Agda - ультрасильной. Что-то похожее;

5) слабая = эффекты никак не отслеживаются в типах, сильная = эффекты отслеживаются в типах.

Прочитал пост и подозреваю, что Вы имели в виду как минимум #4, но так же, может быть, #5. Но это не точно.

Joker_vD

Никто не сидит у клавиатуры с мыслью: "О, я просто набросаю пару строчек кода и посмотрю, что произойдет".

Ну... Я действительно иногда так делаю. Обычно в том случае, когда используемый мной интерфейс плохо задокументирован - где "плохо" означает "недодокументирован", или "переусложнен", или и то, и другое (как с практически любым "асинхронным" API).

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

Денотационная семантика прекрасная и волнующая, но большинство людей на самом деле предпочтут аксиоматическую семантику для рассуждений о корректности: я бы сказал, что рассуждения наподобие "эти переменные гарантированно имеют такие и такие значения на данном этапе выполнения, так что вызов этой функции с таким и таким параметрами не подкинет каких-либо сюрпризов, а после этого состояние программы будет удовлетворять этому и этому условию" - это применение не операционной и определенно не денотационной семантики. Разумеется, выбор некоторых математических объектов предоставит нужные нам аксиомы для вывода заключений, которые нас интересуют, но после осознания, что это именно те аксиомы, которые нам нужны, мы можем работать просто с ними - без "интерпретации" в терминах тех математических объектов.

Bartosz Milewski

@Joker_vD: То, что Вы называете аксиомами, на самом деле теоремы, и они могут быть выведены из любой версии семантики. Примером аксиоматической семантики является описание слабых атомарных операций в C++ - одна из наиболее неприступных областей определения языка. Насколько я знаю (и я говорил с Хансом Боэмом на эту тему), нет никакой операционной модели для слабых атомарных операций - только набор аксиом о видимости записей.

Uglemat

Упражнение № 6 вызывает вопросы в моем разуме начинающего. Существует две функции типа () -> Bool. Это отдельные морфизмы? Похоже на то, потому что меня просят обозначить морфизмы, но моя интуиция подсказывает мне, что они идентичны.

Bartosz Milewski

@Uglemat: Эти две функции не идентичны потому, что они возвращают разные результаты для одних и тех же аргументов.

true () = True false () = False true () /= false ()

Ваша интуиция, скорее всего, подсказывает Вам, что обращение True и False (функция отрицания) - это изоморфизм, что верно. Но это не значит, что две функции одинаковы.

Uglemat

@Milewski На самом деле я думал, что hom(A, B) может иметь максимум один элемент. Потому что не будет ли излишним наличие более одного элемента? Потому что какая еще информация содержится в морфизме помимо двух объектов? Должно ли конкретное "поведение" морфизма считаться как часть его информации? Полагаю, что все эти вопросы из-за того, что я не понимаю, что такое морфизм. При проверке типов нельзя различить два морфизма с одинаковыми начальными и конечными объектами, так как оба эквивалентны в мире типов, где конкретная реализация "спрятана", - может быть, это и заставило меня задуматься об этом.

Bartosz Milewski

@Uglemat: Есть две точки зрения. Когда мы смотрим на абстрактную категорию, мы не должны "понимать" что такое морфизм. Мы просто говорим, что существует два морфизма между двумя объектами, и все. Структура категории заключается в том, сколько морфизмов существует между двумя любыми объектами и как они компонуются.

Но здесь мы пытаемся выстроить категорию, имитируя структуру языка программирования. Так что мы смотрим на язык, его типы и его функции, и выстраиваем соответствующую категорию. Существует тип () и тип Bool. Они соответствуют двум объектам в нашей категории. Тогда существует две функции от () к Bool. Они приведут к возникновению двух морфизмов между двумя объектами.

Абстрагироваться значит забывать о реализации. В категории мы больше не помним, почему два морфизма должны были быть разными - они просто разные.

Uglemat

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

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

Bartosz Milewski

Я пытаюсь использовать термин "множество морфизмов" (hom-set) для обозначения именно множества морфизмов. В Википедии говорится, что некоторые распространяют понятие множества морфизмов на нечто большее, чем множество (я пытаюсь использовать термин "объект морфизмов" (hom-object) в этом случае). Но когда говорится, что множество морфизмов не является множеством, в виду имеется класс - нечто, что может быть больше множества.

Да, существуют объекты, которые больше, чем множество. Например, коллекция всех множеств не является множеством. К счастью, нам, программистам, не нужно переживать из-за этих тонкостей.

Nikolay

Может быть, в своих статьях Вы где-то это упоминали, и я просто упустил это из виду, но Hask = Set + | означает, что категория Set состоит только из счетных множеств. Это упрощение сделано специально, или теория категорий не рассматривает несчетные множества? Важно ли это вообще, потому что я начинаю чувствовать, что многие понятия не имеют значения в этой области математики?

Bartosz Milewski

Set - категория всех множеств: счетных и несчетных.

Ezo

Мое решение #1: https://ideone.com/pxX5As

Есть идеи, как избавиться от явного параметра типа Arg?

Также решение к 6 заданию:

absurd Void ———–> () absurd Void ———–> Bool discard Bool —————> () True () ——————-> Bool False () —————-> Bool

Верно? Должно ли быть две стрелки от unit к bool?

Bartosz Milewski

Думаю, есть какие-то хитрости с шаблонами и типажами, которые могут устранить необходимость в явном параметре типа Arg.

Да, должно быть две стрелки от unit () к bool (но только одна от Void). И не забудьте тождественные стрелки.

rpominov

Относительно упражнения #6:

Должно ли быть два морфизма Bool -> Void и () -> Void? Мы можем определить такие функции, но не можем их вызвать - так же, как с "absurd", да?

И должен ли быть морфизм "not" Bool -> Bool? Если да, то он будет похож на "тождество", но не будет удовлетворять условиям "тождества". Если нет, то почему? Ведь существует функция "not", а все функции должны быть представлены в категории в форме морфизмов, правильно?

Bartosz Milewski

@ rpominov: Как Вы определите функцию Bool -> Void? Что она вернет, если вызвать ее с аргументом True? not - правомерный морфизм, который не является тождеством. Таким образом, действительно существует два морфизма Bool -> Bool. (К слову, not отсутствует в решении Ezo).

pominov

Думаю, теперь я понял. Меня смутило значение слова "определить". Я думал, что это означает "определение" сигнатуры функции. Я не понял, что для Void -> Bool мы можем определить не только сигнатуру, но и тело функции, однако все равно не сможем ее вызвать. В то время как для Bool -> Void мы не можем определить тело функции, то есть такого морфизма быть не может.

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

Спасибо!

Iwan Satria

Могу я узнать, что означает это предложение? Возможно, пример?

"Единственный серьезный аргумент против сильной статической типизации, что я слышал, - проверка типов может не пропустить некоторые семантически корректные программы." ...

Bartosz Milewski

@Iwan: По сути, везде, где Вы видите явное приведение типов, программист переопределяет систему типов. Программист смог рассудить, что, несмотря на формальное несоответствие типов, код будет работать корректно. У программиста было больше информации, чем у компилятора (прим. пер.: вообще, в оригинале здесь написано type checker, но адекватный русскоязычный термин мне неизвестен). Даже в Haskell можно время от времени увидеть unsafeCoerce в качестве средства обхода системы типов, например, для лучшей производительности. (См. обсуждение на Stack Overflow.)

karkunow

Решение к 6 упражнению похоже на https://goo.gl/cE0mEI. ...

Но возникает вопрос: что является тождественной функцией для типа Void? В математике это просто пустая функция от ∅ к ∅. Но мы не можем объявить ее в Haskell. Так что это немного странно 🙂

Bartosz Milewski

@karkunow: Вы можете объявить и реализовать ее в Haskell

import Data.Void

idVoid :: Void -> Void
idVoid x = x

Вы не сможете ее вызвать. Но это другая история.

Валентин Тихомиров

Вы можете объявить idVoid :: Void -> Void и определить эту функцию как idVoid x = x в Haskell, но вы не сможете ее вызвать.

В самом деле, Void -> Void - это лишь частный случай параметрической функции f x = x, как и 0 ^ 0 - частный случай общей формулы a ^ b за исключением того, что 0 ^ 0 нельзя вычислить. То есть, можно определить 0 ^ 0 как частный случай a ^ b, но нельзя вычислить значение этого выражения.

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

https://docs.google.com/document/d/1NcZ07pwYLbQif9hYqY8d82dh2FMf-6b-HXDuccWKfx8/pub

Было сложнее определить функцию от Void к чему-либо, кроме Void или Unit. Я не смог сопоставить Void и Boolean. По моему рассуждению должна существовать только одна такая функция. Но какая из них?

Эта таблица также иллюстрирует 5 главу. Ясно видно, что ⊥ удовлетворяет определению терминального объекта, так как всегда существует только одна функция типа a → ⊥ и ни одной функции типа ⊥ → a за исключением ⊥ → ⊥, который содержит неопреденное количество функций. Так же видно, что у unit () всегда одно отображение от него к любому типу, что делает его идеальным терминальным объектом. В то же время, unit отображается на любое значение в Вашей системе системе типов, как Вы говорите в этой главе, что делает его не таким уж и терминальным.

Bartosz Milewski

@Valentin: По соглашению предполагается, что0 ^ 0 равно 1, так что корректные числа все-таки получаются во всех случаях.

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

Тот факт, что () отображается на любой другой объект (за исключением Void) , никак не мешает ему быть терминальным.

Насчет функции от Void к Bool. Формально, в Haskell можно объявить две такие функции:

vtob  v = True
vtob' v = False

но легко убедиться, что это одна и та же функция.

Я не давал определения того, что для функций (в смысле отображений между множествами) значит быть равными. Так что вот оно: две функции равны, если для всех аргументов они возвращают одинаковые значения. Это называется "экстенсиональное" равенство. Для всех x, f x = g x. В случае с Voidмножество аргументов пустое, так что vtob и vtob' равны "в вакууме".

Либо, если Вы предпочитаете доказательство от противного, попробуйте показать, что vtob отличается от vtob'. Для этого придется найти аргумент, при котором они возвращают разные значения. Удачи в поисках!

nicolasblackburn

Мне кажется, что рассматривать типы только как множества как-то неполноценно. Не обязательно ли также снабдить множества правилами композиции, чтобы описать типы полностью? Взять хоть пример с булевым типом - ясно, что этот тип отличается от, скажем, классов эквивалентности целых чисел по модулю 2. Так как мощность обоих множеств равна двум, их отличают друг от друга именно правила композиции.

Bartosz Milewski

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

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

nicolasblackburn

Спасибо за ответ.

Да, теперь я понял. Читая Ваши статьи, я постоянно забываю, что мы говорим о множествах, а не группах или других структурах, оснащенных правилами композиции. Я допустил такую же ошибку в следующей главе: я не понял, почему было сказано, что "сумматоры" - морфизмы, потому что очевидно, что они не сопоставляют тождество слева к тождеству справа. Но теперь я понял, что у множеств нет тождественного элемента, а морфизмы между множествами - это функции, так что все это наконец обрело смысл.

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

gregnwosugreg

Мне кажется, что возможно реализовать только () -> (), а все остальное невозможно или абсурдно?

Bartosz Milewski

Что насчет двух возможных функций () -> Bool, к примеру?

mcmayer

@bartosz, Вы говорите, что "... в нескольких исследованиях Haskell не оказался на голову выше в плане качества кода, как можно было бы ожидать."

На какие исследования Вы ссылаетесь? ...

(Пояснение: я регулярно сталкиваюсь с сопротивлением императивных программистов, не желающих принять подходы ФП. Например, почему-то слово на букву 'M' часто вызывает сильную негативную реакцию, и на этом все заканчивается. Я ищу убедительные доказательства в поддержку утверждения, что чистые функциональные языки, такие как Haskell, в сочетании с их фундаментом, теорией категорий, - не просто академические игрушки.

Bartosz Milewski

Вот кое-какая литература: A Large Scale Study of Programming Languages and Code Quality in Github, A Comparative Study of Programming Languages in Rosetta Code. Они содержат ссылки на другие исследования.

Хороший источник - Why Haskell Matters.

Timur

Что касается Bool -> Void и () -> Void , не будет ли следующее правильным морфизмом?

bottom = bottom

btov :: Bool -> Void
btov _ = bottom

Так как Hask включает bottom, корректно ли говорить, что эта функция является морфизмом?

Bartosz Milewski

Каверзный вопрос. Вот почему я постоянно ограничиваю мои утверждения о Haskell, говоря "игнорируя bottom". Некоторые люди, как, например, Андрей Бауэр или Роберт Харпер, даже сомневаются в том, что Hask на самом деле является категорией.

Łukasz Oduliński

...

Мне интересна пятая задача из упражнений.

У меня получилось 4 различных функций с сигнатурой Bool -> Bool:

not :: Bool -> Bool
not True = False
not False = True

id :: Bool -> Bool
id a = a

false :: Bool -> Bool
false _ = False

true :: Bool -> Bool
true _ = False

Конечно, может быть и такая функция:

andTrue a = True && a

Но она похожа на функцию id. Может быть еще одна:

andFalse a = False && a

Но она похожа на false.

Итак, исходя из вышесказанного, моя интуиция подсказывает мне, что существует 4 различных функции Bool -> Bool. Я прав?

Bartosz Milewski

@Łukasz: позже Вы увидите, что эти функции могут быть представлены в виде $Bool ^ {Bool}$, или $x = y$, что на самом деле равно 4.