Комментарии 7
Я извиняюсь за разметку, там в двух местах надо читать -> вместо - >
новый редактор себя ведет немного странно.
Какой интересный подход! Берём частичную функцию и говорим: на каком подмножестве она определена, на таком типе она и тотальна. Ахтыжхитраяжопа!
Характеристическая функция множества удобнее. Которая возвращает 0/1 (принадлежит/не принадлежит аргумент множеству). Тем более, у вас она явно присутствует под именем some_check. Не понимаю смысл такой обёртки, вижу лишь проблемы. Например, для классических характеристических функцих можно создавать комбинации. Типа
ВисокосныйГод(x) = ДелитсяНа4(x) И НЕ ДелитсяНа100(x)
Вы передаёте x=2024, и id-функция для ДелитсяНа100 - не определена, всё выражение - не определено. А должно быть определено.
Несмотря на низкий интерес сообщества к этой теме, выскажу свои замечания насчёт того, что в определённых кругах всем известно, чтобы интересующиеся могли пойти читать серьёзную литературу, а те, кто в теме, могли соотнести сказанное в этой статье с другими близкими направлениями. Так сказать, восполню отсутствующий в тексте раздел Related Works.
В теории категорий известно, что морфизмы важнее объектов. Применимо к категории типов (как бы она ни определялась) это значит, что функции важнее типов. В частности, существует способ сформулировать понятие категории исключительно на морфизмах, вообще не прибегая к упоминанию объектов (см. МакЛейн «Категории для работающего математика», первые главы). Применимо к категории типов это значит, что можно говорить о типизации и о типах вообще не упоминая типы, а говоря только о функциях. Например, ℕ — это не отдельная сущность, а класс всех функций f (которые мы бы назвали функция от натурального аргумента f : ℕ → A), с которыми может компоноваться любая функция из другого класса всех функций g (которые мы бы назвали натуральнозначными g : B → ℕ). А поскольку функция идентичности id : ℕ → ℕ принадлежит обоим классам, то в целом можно её использовать как каноничный представитель класса и, таким образом, как функцию, которая указывает на тип.
С другой стороны, можно проделать обратный переход (от нетипизированной системы функций к типизированной). Пример такого перехода описан в работе Данны Скотт «Relating Theories of the λ-calculus», в работах Ламбека. Суть состоит в том, что в нетипизированном языке чистых(!) функций можно выделить класс функций A, удовлетворяющих A(x) = A(A(x)) для вообще любого выражения x (вообще любой функции). Для каждой пары таких A и B можно выделить класс функций f таких, что f(x) = B(f(A(x))) для любого x (вообще любого, без ограничений). Можно показать, что каждая функция A ведёт себя как тип, а каждая функция f из второго класса как типизированная f : A → B.
В последних рассуждениях я неявно предположил, что теория обладает экстенсиональностью, т.е. что из f(x) = g(x) для любого x следует f = g. Если это не так, всё усложняется. Замечу, что с этой же проблемой должен был столкнуться автор текста где-то в окрестности следующего абзаца:
Вторым интересным свойством identity функций является то что мы всегда можем подобрать такой код что программно будет легко определить что это identity функция.
Далее мои мысли:
Dependent&refined types как раз являются реализацией этой парадигмы на минималках.
Refined types — это да, подходящая тема. А зависимые типы интересны и сами по себе. А поскольку они требуют некий рантайм на уровне типов, то без явной типизации там очень сложно.
Наконец, автор предложил порассуждать насчёт соответствия Карри-Говарда. В то время как классическая логика старается говорить о высказываниях и задвинуть доказательства под ковёр (например, мало кого интересует, каким доказательством доказана теорема Пифагора во время использования, ведь важно только то, что оно где-то существует), в предложенном подходе будет наблюдаться ровно обратная ситуация: доказательства (=функции) есть, а высказываний (=типов) нет. Впрочем, я плохо представляю, какой логике соответствует система refined types, поскольку с ними не работал вплотную.
P.S. редактор Хабры преждевременно отправил сообщение. Поэтому прошу прощения за резкость в первом абзаце, я перечитал текст и увидел полезные ссылки и сравнения.
Я извиняюсь за долгое молчание, ушел с головой в создание статьи по поводу chromium-а. Вопросы правильные, но что бы объяснить их придется отдельную статью выкатывать (что в общем то я и собираюсь сделать, но не сейчас) А если коротенько - суть в том что нам сиcтемы типов (каких бы их там навороченных не придумали) - не нужны, у нас есть язык описания функций и какой-то (постоянно пополняемый) инструментарий их анализа. И с этой точки зрения типом может быть любая функция которую мы уже умеем анализировать. И список таких функций постепенно расширяется. Там есть еще один заход с совсем другой стороны, это иерархия Хомского. Так вот, на нее можно посмотреть не как на описание грамматик а как на систему типов. То есть какой сложности должна быть функция для того что бы описать тип. Надо только разобраться с Тьюринг-полными грамматиками поскольку это слишком общая категория, там есть признаки по которым можно разбивать на подкатегории.
identity functions являются описаниями типов