Добрый день. Меня зовут Тимур и я программист.

На днях я закончил одну фичу связанную с хромиумом (пробросил disk_cache в webextensions api, это дает прямой доступ как к http кешу так и к code cache и многим другим - первый шажок к антидетект браузеру), но перед тем как писать статью на эту тему решил взять паузу и немного остудить мозг. Обычно я в таких ситуациях устраиваю ревизию своих записей, спорю с самим собой из прошлого, иногда я его побеждаю иногда он меня, ниже один из таких этюдов, предлагаю обсудить.

Давайте поговорим об identity функциях. Да, именно так, во множественном числе.

Вот определение функции знакомое любому кто хотя бы вскользь касался функционального программирования:

id a = a

Тут все понятно, что мы получили на входе то мы и отдали. Это полиморфная identity функция. Ок. А что если мы хотим определить identity функцию только для аргументов определенного типа? В языках с номинативной системой типов это могло бы выглядеть как то так:

id :: examinedType -> examinedType;
id a = a

Но не будем пока торопиться вводить какой либо дополнительный синтаксис для описания типов. Просто пойдем вслед за кодом и посмотрим куда он нас приведет.

Например мы хотим написать id функцию для натуральных чисел, назовем ее nat. Как она могла бы выглядеть?

nat O = O
nat (S .n) = S (nat .n)

Пока никаких неожиданностей. Но что мы можем сказать глядя на эту функцию?
Во первых мы можем вывести тип входного параметра: someInferedTypeName: O | (S someInferedTypeName)
Причем вывести мы это можем не только глазами, это можно сделать программно. В отличии от исполнения вызова функции на аргументе, где мы бы пошли слева на право по клозам функции мы пойдем справа налево и с конца. Мы видим базис индукции:

nat O = O

и понимаем что O - это терминальный случай. Таким образом справа мы видим завершение работы функции а слева - входной параметр который к этому приведет. Запоминаем входной параметр - O и по этому же клозу понимаем что это часть типа nat (это утверждение всегда верно для identity функций, в этом их преимущество - легкость анализа)

Далее смотрим на индуктивный шаг:

nat (S .n) = S (nat .n)

из которого (справа) мы выводим тип результата:

S (что то, что возвращает nat .n)

а слева мы видим что к этому может привести - S .n где .n - это nat (а мы уже знаем что O это nat). Из этого же клоза мы понимаем что (S nat) это тоже nat. Других клозов у нас нет и мы готовы вывести тип аргумента:

nat = O | (S nat)
// или в нотации Coq:
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Что здесь произошло?
Очевидно что мы взяли легкую для анализа функцию и вывели тип аргумента (который совпадает с типом результата).

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

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

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

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

А теперь представим тип - диофатовы уравнения. Можем ли мы его выразить? Легко. Можем ли мы написать identity функцию для такого типа? Да, более того - она будет достаточно легка для анализа. Но как только мы попытаемся уточнить наш тип и, скажем, выразить тип диофатовых уравнений разрешимых в целых рациональных числах - и мы сталкиваемся с десятой проблемой Гилберта. То есть на словах мы можем описать какой тип мы хотим но далеко не всегда мы можем выразить это функцией. Почему так - интересный вопрос сам по себе, но это отдельная статья.

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

Вторым интересным свойством identity функций является то что мы всегда можем подобрать такой код что программно будет легко определить что это identity функция. Какой бы сложной ни была проверка на принадлежность аргумента к типу, код identity функции всегда можно свести к коду такого вида:

Definition SomeIdentityFunc (n) :=
  match (some_check n) with
  | true => n
  end.

Независимо от сложности логики some_check мы можем (в том числе программно) понять что SomeIdentityFunc является identity функцией для какого то типа данных. То есть она вернет n если n принадлежит какому то типу и не определена для других типов.

Здесь важно понять что речь идет не о том что мы можем проанализировать любую identity функцию а о том что для любого типа который мы можем описать - мы можем найти вариант identity функции легкий для узнавания.

Резюмируя вышесказанное - вместо парадигмы определения типа функции (или аргументов функции) мы смещаемся к парадигме - функция является описанием типа.

Dependent&refined types как раз являются реализацией этой парадигмы на минималках.

С этой парадигмой становится интереснее смотреть на доказательство Тьюринга и Curry–Howard correspondence. Никаких срывов покровов, разоблачений и прочего, там все хорошо и на своих местах, просто взгляд на эти вещи с пониманием того что не тип определяет функцию а функция определяет тип делает какие то моменты более понятными а какие то - просто очевидными. Но об этом в следующий раз.

Собственно все что хотел сегодня сказать.

А новостей на сегодня больше нет. С вами был Тимур, всем хорошего настроения!