Вам спасибо за отзыв! В этой публикации только первая часть обзора. Если сочтёте, что другие части также достойны внимания читателей, то можете проголосовать и там))
Спасибо за уточнение. Действительно, теория категорий не позиционировалась как обобщение теории типов. Хотел лишь сказать, что она базируется на некоторых идеях, сформулированных в теории типов, т.е. по сути выросла из неё, вобрав её в себя как небольшую часть. Но, не смотря на это, теорию категорий всё ещё можно сформулировать на языке теории типов. Этот факт показался мне достойным упоминания в предыдущем комментарии))
К сожалению, не хватает компетенции, чтобы ответить за все системы логики, но теория типов разрабатывалась для самого обоснования математики, чтобы была возможность проверить, корректны ли рассуждения в этом весьма гибком формализме, или нет. Конструктивная теория типов привнесла существенные выразительные возможности, а HoTT вообше претендует на звание фундамента всей математики. Теория категорий зародилась как обобщение теории типов, но и её саму можно выразить с помощью типов!
Дейстаительно, инструмены статической типизации отвечают за доказательство корректности программы. Вот только во многих языках они.. "альтернативно продвинутые")). Например, при слабой системе вывода типов случаются ложноотрицательные вердикты, а изменяемые переменные приводят к ложноположительным и т.п.
В Scala достаточно мощная система типов, в сравнении с Java, C# и т.п., но до каких нибудь Coq или Agda ему далеко...
Там речь шла о том, что и `Int64`, и `double` занимает в памяти 8 байт, и каждое сочетание бит там может интерпретироваться как корректное значение любого из этих типов. Разные NaNы также являются корректными в том смысле, что их можно использовать во всех операциях (результатом как правило будут также NaNы, но это уже на важно).
Создавалось-то оно как бестиповое, но типы в нём появились достаточно скоро. Лямбда-выражения в современных языках построены именно на типизированном лямбда-исчислении.
Среди законов Мёрфи есть такой: "Если есть хоть один шанс, что вас поймут неправильно, то вас ОБЯЗАЕЛЬНО поймут неправильно"))
Никаких противоречий в своих словах не вижу. В этой статье не излагался какой-либо "подход", полезность которого осталась не раскрытой. Это именно фрагментарный обзор (местами сложной) теории, без глубоких деталей. С акцентом на не раз уже упомянутую в комментариях "неизбежность", естественность появления представленных абстракций.
Представленный материал интересен мне самому, я верю что найдутся читатели, с кем я смогу разделить эти интересы. Да, такой формат и стиль изложения может понравиться не всем, но, как говорится, всем не угодишь... Важным показателем для меня являются оценки под статьёй и комментарии читателей, в том числе и Ваш. Постараюсь учесть все мнения при подготовке следующей статьи.
Не нужно воспринимать эту статью как некое научное откровение. Это именно что популярный поверхностный обзор известных положений теории типов. Уверен, что у аудитории достаточно высокий уровень, чтобы именно в таком ключе воспринимать эту работу. После прочтения у читателя может возникнуть много вопросов, на некоторые пробую ответить сам, ответы на другие несложно найти в свободном доступе.
Все совпадения названий с "книжными" совершенно случайны!)) Кажется, что контекстуальный смысл слова "индекс" раскрыт в статье, разве нет?
В любом случае, тут я не раскрываю "свою теорию типов". Как и было упомянуто в начале, это лишь поверхностный обзор основных понятий теории. А за деталями лучше обращаться к специализированной литературе. Мною допущено много вольностей в изложении, но если есть принципиальные ошибки, которые могут ввести читателя в заблуждение - буду рад их исправить.
isAssignable, судя по названию, как раз проверяет наличие неявного преобразования. Оно может предоставляться как вручную, так и автоматически, если классы связаны наследованием.
Да, все эти вопросы вокруг примерно одной и той же проблемы. Есть разные алгоритмы её решения, но, сугубо на мой взгляд, было бы проще не создавать саму проблему)) "Наследование" - очень популярная, но не самая лучшая идея))
Лямбда-исчисление тоже не стоит на месте. Обобщённые типы - это отображения из типа в тип, то бишь функции, что вполне укладываются в лямбда-исчисление. Вообще - это тема моего следующего проекта для хабра))
Ни в коем случае не стараюсь как-нибудь принизить "практиков", кого бы Вы не имели ввиду))
Ассемблер создавался, чтобы была возможность записать программу не в виде дырок на перфокарте, а текстом. С прицелом на кроссплатформенность. Семантика языка целиком определялась архитектурой тогдашних процессоров, которые проектировались ведущими учёными. Впрочем, это был по-прежнему язык для пенетрации перфокарт, а не для консольного ввода.
Фортран, Алгол уже создавались по заказу целыми комитетами, куда входили так же самые достойные учёные. Все остальные языки уже шли по их стопам и не особо отступали от первоначальных конструктов.
Деление людей на практиков и "тех, других" вообще кажется не совсем корректным))
Типы - это вполне конкретная абстракция)) Не так важно, кто их придумал, как то, что начиная с определённого периода они начинают изучаться и использоваться повсеместно. Те определения которые лежат в основе теории типов появились вследствие накопившегося объёма проблем, для решения которого старые абстракции не работали, или были неудобны. Именно это я и называю "неизбежностью".
Спасибо за отзыв! Хотел, разбить статью, но не получилось - каждый раздел получается незаконченным, оторванным от основной темы.. Видимо, опыта пока малоато))
Понятие подипизации есть в разных языках, но в каждом оно может иметь какие-то отличительные особенности. Где-то вполне допускается неявное привеление от bool к int (0 или 1), а в других языках - нет.
"Гибкость" подтипищации упомянута в сравнении с наследованием, которое часто путают с подтипищацией. Подтипищация проявлятся как наличие неявного преобразования от одного типа к другому. Во многих языках мы можем сами создаватьнеявные преобразования (гибкость)) - иерархия наследования нас не ограничивает.
Уровень статьи выше "начального", но далёк от "сложного"))
Бинарную операцию в моноиде можно трактовать как функцию из пары значений (ну или в каррированном виде). С другой стороны, нейтральный элемент можно понимать как нулярную операцию, не принимающую аргументов типов А - функция из типа единицы. Итого, моноид - это пара функций. Ловкость рук и никакого мошенничества))
Алгоритм определяется прежде всего своей сигантурой. Например, на входе список типа А, а на выходе значение типа А. Если мы ничего не знаем про тип А, но на предоставили моноид для типа А, то мы можем свернуть этот список. При разных типах и разных моноидах результат будет, конечно, разный, но сам алгоритм свёртки списка не измениться. Попробуйте сами написать такой алгоритм, например, с циклом foreach (на входе список тип А и моноид для него, а на выходе значение типа А) - алгоритм не будет зависеть от того, что именно пониматься под А.
Несколько аргументов на вход функции - это кортеж - произведение типов, которое также отображается на диаграмме типов. А значит там есть место и для функции от нескольких переменных.
По поводу заморочек с универсальным свойствами - часть ответов есть в самой статье, а за подробностями обычно предлагаю перейти по этой ссылке.
Про каррирование тоже можно отдельную статью написать)). Обычно используется в тех случаях, когда какая функция требует на вход функцию меньшего числа аргументов, чем у нас есть, а первый аргумент можно фиксировать. Иногда сразу опеределяют функции в каррированном виде, а в других случаях можно воспользоваться методами, уже реализованными в стандартной библиотеке языка. В статье подчёркивается сам факт наличия такого изоморфизма. А примеров применения его в интернете не мало (боюсь у меня сейчас не найдётся возможности написать что-нибудь прямо в этом ответе((( )
Метод без параметров эквивалентен функции из единицы. Просто в теории типов речь всегда идёт о функциях одного аргумента (даже если это кортеж).
В статье говорится не о равенстве типов (А, Nothing) и Nothing, а об их изоморфизме - значения обоих типов невозможно получить честным (чистым) способом.
С множественным наследованием та же беда, что и с пересечением типов в Scala. Чтобы как-то обеспечить предсказуемость поведения нужно идти на какие-то компромиссы, гвоздями прибивать какие-то дополнительные правила к спецификации языка...
"Сторонние" типы в формулировании универсальных свойств нужны как раз для того, чтобы как-то определить способ, как из них выброать самый оптимальный - универсальный.
Обзор и так получился гигантским. Очень много деталей оказалось за бортом. Для тех, кто заинтересуется, оставлены лишь прямые ссылки, или намёки для загугливания.
Многие понятия были сформулированы ещё в теории типов раньше, чем на её основе появилась теория категорий. Тут лишь хотелось бы подчеркнуть, что понятие универсального свойства автоматически следует из желания чётко сформулировать, что такое типы "А и В", "А или В" и другие. Без чёткой формулировки мы не сможем оперировать этими понятиями, чтобы конструктивно доказывать корректность алгоритма.
Типы в этой схеме фиксированы, но тут играет роль понятие коммутативности путей. В данном случае пути "c" и "b * а" не коммутативны - не для всех исходных значений будет получен одинаковый результат. "Коммутативность" входит и в понятие универсального свойства - "существует единственный морфизм, делающий диаграмму коммутативной".
Типы изоморфные (при слабой типизации всегда можно переломать указатель с одного типа на другой и обратно без потерь), но разные. С этими типами могут быть связанные разные наборы функций, а типы как раз и отличаются разным набором входящих и исходящих отображений - положением на общей диаграмме типов.
Важный момент. Наверное стоило раскрыть его подробнее.
Вычисления обычно проводяься так: на входе у нас есть значение типа А (возможно, несколько значерий, объединённых типом-произведением), передав его в одну функцию, получаем значение типа В и так далее. Получаетя цепочка вида А->В->...->R - по сути это один из путей на диагрмме типов. Задача состоит в том, чтобы найти путь до R как можно короче.
Допустим есть три функции А->В, В->С и А->С. Очевидно, что если мы хотим получить значение типа С из А, то вызов последней функции будет оптимальнее, чем последоаптельный вызов пнрвых двух - путь на диаграмме короче. Уникальность универсального морфизма и определяет его оптимальность - из всех возможных путей он оказыаается самым коротким. Строя вычисления, основанные на универсальных свойствах типов как раз и получается находить наиболее коротеие пути вычислений.
Под факторизацией здесь понимается разделение длинного пути вычисления на отдельные шаги-функции. По сути, декомпощиция задачи. Возможно, не самое удачное использование слова "факторизация"...
По поводу типа Either я в статье отметил, что не зотел углублятся в тему обобщённых типов - что это и почему их можно захотеть. Надеюсь написать об этом отдельную статью, и её публикация окажется достаточно обоснованной))
Вам спасибо за отзыв! В этой публикации только первая часть обзора. Если сочтёте, что другие части также достойны внимания читателей, то можете проголосовать и там))
Спасибо за уточнение. Действительно, теория категорий не позиционировалась как обобщение теории типов. Хотел лишь сказать, что она базируется на некоторых идеях, сформулированных в теории типов, т.е. по сути выросла из неё, вобрав её в себя как небольшую часть. Но, не смотря на это, теорию категорий всё ещё можно сформулировать на языке теории типов. Этот факт показался мне достойным упоминания в предыдущем комментарии))
К сожалению, не хватает компетенции, чтобы ответить за все системы логики, но теория типов разрабатывалась для самого обоснования математики, чтобы была возможность проверить, корректны ли рассуждения в этом весьма гибком формализме, или нет. Конструктивная теория типов привнесла существенные выразительные возможности, а HoTT вообше претендует на звание фундамента всей математики. Теория категорий зародилась как обобщение теории типов, но и её саму можно выразить с помощью типов!
Дейстаительно, инструмены статической типизации отвечают за доказательство корректности программы. Вот только во многих языках они.. "альтернативно продвинутые")). Например, при слабой системе вывода типов случаются ложноотрицательные вердикты, а изменяемые переменные приводят к ложноположительным и т.п.
В Scala достаточно мощная система типов, в сравнении с Java, C# и т.п., но до каких нибудь Coq или Agda ему далеко...
Понял, о чём вы. Сложно рассуждать о мощности множества значений типа double, когда некоторые из значений могут оказаться не равны сами себе))
Буду за компом - посмотрю, можно ли переписать это место корректнее. Спасибо!
Там речь шла о том, что и `Int64`, и `double` занимает в памяти 8 байт, и каждое сочетание бит там может интерпретироваться как корректное значение любого из этих типов. Разные NaNы также являются корректными в том смысле, что их можно использовать во всех операциях (результатом как правило будут также NaNы, но это уже на важно).
Создавалось-то оно как бестиповое, но типы в нём появились достаточно скоро. Лямбда-выражения в современных языках построены именно на типизированном лямбда-исчислении.
Среди законов Мёрфи есть такой: "Если есть хоть один шанс, что вас поймут неправильно, то вас ОБЯЗАЕЛЬНО поймут неправильно"))
Никаких противоречий в своих словах не вижу. В этой статье не излагался какой-либо "подход", полезность которого осталась не раскрытой. Это именно фрагментарный обзор (местами сложной) теории, без глубоких деталей. С акцентом на не раз уже упомянутую в комментариях "неизбежность", естественность появления представленных абстракций.
Представленный материал интересен мне самому, я верю что найдутся читатели, с кем я смогу разделить эти интересы. Да, такой формат и стиль изложения может понравиться не всем, но, как говорится, всем не угодишь... Важным показателем для меня являются оценки под статьёй и комментарии читателей, в том числе и Ваш. Постараюсь учесть все мнения при подготовке следующей статьи.
Не нужно воспринимать эту статью как некое научное откровение. Это именно что популярный поверхностный обзор известных положений теории типов. Уверен, что у аудитории достаточно высокий уровень, чтобы именно в таком ключе воспринимать эту работу. После прочтения у читателя может возникнуть много вопросов, на некоторые пробую ответить сам, ответы на другие несложно найти в свободном доступе.
Все совпадения названий с "книжными" совершенно случайны!))
Кажется, что контекстуальный смысл слова "индекс" раскрыт в статье, разве нет?
В любом случае, тут я не раскрываю "свою теорию типов". Как и было упомянуто в начале, это лишь поверхностный обзор основных понятий теории. А за деталями лучше обращаться к специализированной литературе. Мною допущено много вольностей в изложении, но если есть принципиальные ошибки, которые могут ввести читателя в заблуждение - буду рад их исправить.
isAssignable, судя по названию, как раз проверяет наличие неявного преобразования. Оно может предоставляться как вручную, так и автоматически, если классы связаны наследованием.
Да, все эти вопросы вокруг примерно одной и той же проблемы. Есть разные алгоритмы её решения, но, сугубо на мой взгляд, было бы проще не создавать саму проблему)) "Наследование" - очень популярная, но не самая лучшая идея))
Лямбда-исчисление тоже не стоит на месте. Обобщённые типы - это отображения из типа в тип, то бишь функции, что вполне укладываются в лямбда-исчисление. Вообще - это тема моего следующего проекта для хабра))
Ни в коем случае не стараюсь как-нибудь принизить "практиков", кого бы Вы не имели ввиду))
Ассемблер создавался, чтобы была возможность записать программу не в виде дырок на перфокарте, а текстом. С прицелом на кроссплатформенность. Семантика языка целиком определялась архитектурой тогдашних процессоров, которые проектировались ведущими учёными. Впрочем, это был по-прежнему язык для пенетрации перфокарт, а не для консольного ввода.
Фортран, Алгол уже создавались по заказу целыми комитетами, куда входили так же самые достойные учёные. Все остальные языки уже шли по их стопам и не особо отступали от первоначальных конструктов.
Деление людей на практиков и "тех, других" вообще кажется не совсем корректным))
Типы - это вполне конкретная абстракция)) Не так важно, кто их придумал, как то, что начиная с определённого периода они начинают изучаться и использоваться повсеместно. Те определения которые лежат в основе теории типов появились вследствие накопившегося объёма проблем, для решения которого старые абстракции не работали, или были неудобны. Именно это я и называю "неизбежностью".
Спасибо за отзыв! Хотел, разбить статью, но не получилось - каждый раздел получается незаконченным, оторванным от основной темы.. Видимо, опыта пока малоато))
Понятие подипизации есть в разных языках, но в каждом оно может иметь какие-то отличительные особенности. Где-то вполне допускается неявное привеление от bool к int (0 или 1), а в других языках - нет.
"Гибкость" подтипищации упомянута в сравнении с наследованием, которое часто путают с подтипищацией. Подтипищация проявлятся как наличие неявного преобразования от одного типа к другому. Во многих языках мы можем сами создаватьнеявные преобразования (гибкость)) - иерархия наследования нас не ограничивает.
Уровень статьи выше "начального", но далёк от "сложного"))
Бинарную операцию в моноиде можно трактовать как функцию из пары значений (ну или в каррированном виде). С другой стороны, нейтральный элемент можно понимать как нулярную операцию, не принимающую аргументов типов А - функция из типа единицы. Итого, моноид - это пара функций. Ловкость рук и никакого мошенничества))
Алгоритм определяется прежде всего своей сигантурой. Например, на входе список типа А, а на выходе значение типа А. Если мы ничего не знаем про тип А, но на предоставили моноид для типа А, то мы можем свернуть этот список. При разных типах и разных моноидах результат будет, конечно, разный, но сам алгоритм свёртки списка не измениться. Попробуйте сами написать такой алгоритм, например, с циклом foreach (на входе список тип А и моноид для него, а на выходе значение типа А) - алгоритм не будет зависеть от того, что именно пониматься под А.
Несколько аргументов на вход функции - это кортеж - произведение типов, которое также отображается на диаграмме типов. А значит там есть место и для функции от нескольких переменных.
По поводу заморочек с универсальным свойствами - часть ответов есть в самой статье, а за подробностями обычно предлагаю перейти по этой ссылке.
Про каррирование тоже можно отдельную статью написать)). Обычно используется в тех случаях, когда какая функция требует на вход функцию меньшего числа аргументов, чем у нас есть, а первый аргумент можно фиксировать. Иногда сразу опеределяют функции в каррированном виде, а в других случаях можно воспользоваться методами, уже реализованными в стандартной библиотеке языка. В статье подчёркивается сам факт наличия такого изоморфизма. А примеров применения его в интернете не мало (боюсь у меня сейчас не найдётся возможности написать что-нибудь прямо в этом ответе((( )
Метод без параметров эквивалентен функции из единицы. Просто в теории типов речь всегда идёт о функциях одного аргумента (даже если это кортеж).
В статье говорится не о равенстве типов (А, Nothing) и Nothing, а об их изоморфизме - значения обоих типов невозможно получить честным (чистым) способом.
С множественным наследованием та же беда, что и с пересечением типов в Scala. Чтобы как-то обеспечить предсказуемость поведения нужно идти на какие-то компромиссы, гвоздями прибивать какие-то дополнительные правила к спецификации языка...
"Сторонние" типы в формулировании универсальных свойств нужны как раз для того, чтобы как-то определить способ, как из них выброать самый оптимальный - универсальный.
Обзор и так получился гигантским. Очень много деталей оказалось за бортом. Для тех, кто заинтересуется, оставлены лишь прямые ссылки, или намёки для загугливания.
Многие понятия были сформулированы ещё в теории типов раньше, чем на её основе появилась теория категорий. Тут лишь хотелось бы подчеркнуть, что понятие универсального свойства автоматически следует из желания чётко сформулировать, что такое типы "А и В", "А или В" и другие. Без чёткой формулировки мы не сможем оперировать этими понятиями, чтобы конструктивно доказывать корректность алгоритма.
Типы в этой схеме фиксированы, но тут играет роль понятие коммутативности путей. В данном случае пути "c" и "b * а" не коммутативны - не для всех исходных значений будет получен одинаковый результат. "Коммутативность" входит и в понятие универсального свойства - "существует единственный морфизм, делающий диаграмму коммутативной".
Типы изоморфные (при слабой типизации всегда можно переломать указатель с одного типа на другой и обратно без потерь), но разные. С этими типами могут быть связанные разные наборы функций, а типы как раз и отличаются разным набором входящих и исходящих отображений - положением на общей диаграмме типов.
Важный момент. Наверное стоило раскрыть его подробнее.
Вычисления обычно проводяься так: на входе у нас есть значение типа А (возможно, несколько значерий, объединённых типом-произведением), передав его в одну функцию, получаем значение типа В и так далее. Получаетя цепочка вида А->В->...->R - по сути это один из путей на диагрмме типов. Задача состоит в том, чтобы найти путь до R как можно короче.
Допустим есть три функции А->В, В->С и А->С. Очевидно, что если мы хотим получить значение типа С из А, то вызов последней функции будет оптимальнее, чем последоаптельный вызов пнрвых двух - путь на диаграмме короче. Уникальность универсального морфизма и определяет его оптимальность - из всех возможных путей он оказыаается самым коротким. Строя вычисления, основанные на универсальных свойствах типов как раз и получается находить наиболее коротеие пути вычислений.
Под факторизацией здесь понимается разделение длинного пути вычисления на отдельные шаги-функции. По сути, декомпощиция задачи. Возможно, не самое удачное использование слова "факторизация"...
По поводу типа Either я в статье отметил, что не зотел углублятся в тему обобщённых типов - что это и почему их можно захотеть. Надеюсь написать об этом отдельную статью, и её публикация окажется достаточно обоснованной))