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