Приятный синхронизм: сразу двое ребят в один день прислали отчёты - второй курс по гомотопической теории типов 🔥
Типы и пути
Тип является пространством.
Элементы/объекты — точками.
Пути — доказательствами равенства, при этом имеют очень похожие свойства с обычной группой.
Тип ведёт себя как группоид.
А за счёт появления путей между путями и т. п. получаем бесконечный группоид.
И в моей голове возникал вопрос: зачем это нужно? Оказалось, всё просто — чтобы рассматривать тип не как болванку со значениями, а как пространство, где важны точки, пути и отношения между путями. Поэтому два условно одинаковых перехода/пути можно сравнивать, исследовать различия между ними и доказывать их равенство или согласованность на более высоком уровне.
И в целом это какая-то чёрная магия, которая даёт основу для формальной верификации, поскольку мы математически выразили состояния, переходы и их свойства прямо в системе типов.
И здесь как раз понятно, зачем были нужны HIT — чтобы конструировать тип сразу с его топологической структурой.
Дополнительно долго разбирался с деформациями, базово понял, но в геометрическом смысле сломал себе голову.
Pi, Sigma, Universes
Можно выразить максимально строгие инварианты на уровне системы типов, в том числе для иерархий.
Очень зашла практика на эти темы. Это, по сути, самый высший уровень MISU (наверное?).
Хочется как-то прикрутить такое в .NET, даже загорелся попробовать, хотя бы только для зависимых типов (но, скорее всего, просто будут обычные типы без доказательств и на уровень компиляции это не поднимется).
Truncation
Позволяет работать с "богатым" типом на необходимом уровне детализации, при этом отсекаем структуру, которая для нас несущественна.
Чем-то напоминает интерфейсы: тип можно рассматривать через ограниченные представления — конкретный интерфейс.
Univalence/Equivalence
Математики задумались над тем, что, если две структуры эквивалентны, то одну можно заменить другой и наоборот.
И тут появляется унивалентность — основная идея HoTT, которая превращает эквивалентность в путь между точками пространства (типами), вместе с идеей транспорта — переноса значения по пути равенства.
По сути, можем переносить данные и структуру между эквивалентными типами за счёт транспорта туда/обратно.
И это важно для формальной верификации — транспорт позволяет не потерять уже доказанную корректность при переходах.
Голову я себе поломал знатно, было очень увлекательно и как всегда очень познавательно.
Спасибо вам большое за этот курс.
Только вперед!
Для .NET например есть F* :) Ну и всяческие пруверы вроде Lean или Rocq. А дальше кстати разбираем реализацию CoC на F#, я её уместил в 100 строк)
"самый высший уровень MISU" -- это LPF (теоркат), в котором начинаем это всё комбинировать(ладно, понадобится ещё (M)PF — как об этом всём правильно думать)
Прохождение далось непросто, основное, на чем себя ловил - мнимое понимание пройденной темы: после изучения теории создается ощущение, что все ясно, но когда принимаешься делать практику, понимаешь, что это далеко не так. В этом плане для меня оказались крайне полезны практические задания. Несмотря на то, что их выполнение заняло несколько больше, чем ожидал, я сейчас (как мне кажется) довольно уверенно ориентируюсь в основных концепциях HoTT (подтвердил мини-экзаменом, который устроил себе через llm).
Из пройденных тем больше всего усилий потребовалось на осознание высших путей и infinity groupoid, это был определенный "взрыв мозга" для меня.
Главным итогом курса считаю то, что мне удалось достаточно детально помоделировать и попрактиковаться в том, чтобы мыслить о реальных задачах через призму типов и взаимоотношений между ними.
Большое спасибо за курс!
"когда принимаешься делать практику, понимаешь, что это далеко не так" - да, это классическая проблема. Ключевые понятия некоторой теории в принципе освоить достаточно легко, а вот решать прикладные задачи, доказывать теоремы, требуется ощутимо другое мышление. Программирование похоже, но не так выразительно, как в математике.
С другой стороны, у нас есть такое преимущество, что по большому счёту достаточно взять вот именно эти все базовые понятия HoTT просто как форму думания-рассуждения о коде на уровне (оч.сильной) системы типов, а строить из них что-то работающее с помощью теории категорий.
Не я это придумал конечно, многие святые computer science об этом говорили, от Воеводского, Steve Awodey, Mike Shulman, Emily Riehl, Dan Licata, Robert Harper, Benedikt Ahrens...
(например, категории, функторы, естественные преобразования и т.д. определяются внутри HoTT, используя его систему типов)
"The power of CT to dynamically compose appropriate granular units of computations and HoTT to help with semantics and validate the compositions, is necessary for this...
Think of it like a “high-level programming language” … that gets automatically “compiled” to the low-level “assembly language” of mathematical objects.
The power of CT to dynamically compose … and HoTT to help with semantics and validate the compositions, is necessary for this...
I will also describe my work on using HoTT as a programming language and its applications in computer science...."
Какие-то связочки с прикладухой (прежде всего крайне экзотическая формальная верификация) есть конечно, например Foundations of Systems Architecture Design, INCOSE... (там кстати, совместно с CT и HoTT применяются Abstract State Machines), да только практически все они требуют уровня PhD.
А вот к прозаической практике уровня обычного миддла в этих темках приблизился (задауншифтился) я первым в мире :)
И остался соответственно заключительный шаг -- (Meta) Principles Framework, где работаем уже внутри этой странной склейки HoTT+CT+ASM, в идеале в формате ELI5 (explain like I'm 5 years old). И я даже уже придумал форму (ну ок, похитил у мудрейших), в которой этому обучать наиболее продуктивно, в идеале даже без особой дополнительной прокачки. Тем более, что актуально это уже больше для подготовки спек/скиллов хорошему AI.
Типы и пути
Тип является пространством.
Элементы/объекты — точками.
Пути — доказательствами равенства, при этом имеют очень похожие свойства с обычной группой.
Тип ведёт себя как группоид.
А за счёт появления путей между путями и т. п. получаем бесконечный группоид.
И в моей голове возникал вопрос: зачем это нужно? Оказалось, всё просто — чтобы рассматривать тип не как болванку со значениями, а как пространство, где важны точки, пути и отношения между путями. Поэтому два условно одинаковых перехода/пути можно сравнивать, исследовать различия между ними и доказывать их равенство или согласованность на более высоком уровне.
И в целом это какая-то чёрная магия, которая даёт основу для формальной верификации, поскольку мы математически выразили состояния, переходы и их свойства прямо в системе типов.
И здесь как раз понятно, зачем были нужны HIT — чтобы конструировать тип сразу с его топологической структурой.
Дополнительно долго разбирался с деформациями, базово понял, но в геометрическом смысле сломал себе голову.
Pi, Sigma, Universes
Можно выразить максимально строгие инварианты на уровне системы типов, в том числе для иерархий.
Очень зашла практика на эти темы. Это, по сути, самый высший уровень MISU (наверное?).
Хочется как-то прикрутить такое в .NET, даже загорелся попробовать, хотя бы только для зависимых типов (но, скорее всего, просто будут обычные типы без доказательств и на уровень компиляции это не поднимется).
Truncation
Позволяет работать с "богатым" типом на необходимом уровне детализации, при этом отсекаем структуру, которая для нас несущественна.
Чем-то напоминает интерфейсы: тип можно рассматривать через ограниченные представления — конкретный интерфейс.
Univalence/Equivalence
Математики задумались над тем, что, если две структуры эквивалентны, то одну можно заменить другой и наоборот.
И тут появляется унивалентность — основная идея HoTT, которая превращает эквивалентность в путь между точками пространства (типами), вместе с идеей транспорта — переноса значения по пути равенства.
По сути, можем переносить данные и структуру между эквивалентными типами за счёт транспорта туда/обратно.
И это важно для формальной верификации — транспорт позволяет не потерять уже доказанную корректность при переходах.
Голову я себе поломал знатно, было очень увлекательно и как всегда очень познавательно.
Спасибо вам большое за этот курс.
Только вперед!
Для .NET например есть F* :) Ну и всяческие пруверы вроде Lean или Rocq. А дальше кстати разбираем реализацию CoC на F#, я её уместил в 100 строк)
"самый высший уровень MISU" -- это LPF (теоркат), в котором начинаем это всё комбинировать
Прохождение далось непросто, основное, на чем себя ловил - мнимое понимание пройденной темы: после изучения теории создается ощущение, что все ясно, но когда принимаешься делать практику, понимаешь, что это далеко не так. В этом плане для меня оказались крайне полезны практические задания. Несмотря на то, что их выполнение заняло несколько больше, чем ожидал, я сейчас (как мне кажется) довольно уверенно ориентируюсь в основных концепциях HoTT (подтвердил мини-экзаменом, который устроил себе через llm).
Из пройденных тем больше всего усилий потребовалось на осознание высших путей и infinity groupoid, это был определенный "взрыв мозга" для меня.
Главным итогом курса считаю то, что мне удалось достаточно детально помоделировать и попрактиковаться в том, чтобы мыслить о реальных задачах через призму типов и взаимоотношений между ними.
Большое спасибо за курс!
"когда принимаешься делать практику, понимаешь, что это далеко не так" - да, это классическая проблема. Ключевые понятия некоторой теории в принципе освоить достаточно легко, а вот решать прикладные задачи, доказывать теоремы, требуется ощутимо другое мышление. Программирование похоже, но не так выразительно, как в математике.
С другой стороны, у нас есть такое преимущество, что по большому счёту достаточно взять вот именно эти все базовые понятия HoTT просто как форму думания-рассуждения о коде на уровне (оч.сильной) системы типов, а строить из них что-то работающее с помощью теории категорий.
Не я это придумал конечно, многие святые computer science об этом говорили, от Воеводского, Steve Awodey, Mike Shulman, Emily Riehl, Dan Licata, Robert Harper, Benedikt Ahrens...
(например, категории, функторы, естественные преобразования и т.д. определяются внутри HoTT, используя его систему типов)
"The power of CT to dynamically compose appropriate granular units of computations and HoTT to help with semantics and validate the compositions, is necessary for this...
Think of it like a “high-level programming language” … that gets automatically “compiled” to the low-level “assembly language” of mathematical objects.
The power of CT to dynamically compose … and HoTT to help with semantics and validate the compositions, is necessary for this...
I will also describe my work on using HoTT as a programming language and its applications in computer science...."
Какие-то связочки с прикладухой (прежде всего крайне экзотическая формальная верификация) есть конечно, например Foundations of Systems Architecture Design, INCOSE... (там кстати, совместно с CT и HoTT применяются Abstract State Machines), да только практически все они требуют уровня PhD.
А вот к прозаической практике уровня обычного миддла в этих темках приблизился (задауншифтился) я первым в мире :)
И остался соответственно заключительный шаг -- (Meta) Principles Framework, где работаем уже внутри этой странной склейки HoTT+CT+ASM, в идеале в формате ELI5 (explain like I'm 5 years old). И я даже уже придумал форму (ну ок, похитил у мудрейших), в которой этому обучать наиболее продуктивно, в идеале даже без особой дополнительной прокачки. Тем более, что актуально это уже больше для подготовки спек/скиллов хорошему AI.
❤15✍6