Types and type inference

Posted on January 24, 2020

So the writer who breeds more words than he needs, is making a chore for the reader who reads.
—Dr. Seuss, We Can Do better

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

Нижеизложенное является развитием идей структурной типизации.

Для того что бы понять идею достаточно рассмотреть одно определение типа и две функции. Тип описан в Coq нотации, функции даны в τ-lang нотации.

Тут не должно быть затруднений, мы описали индуктивно натуральные числа.

А теперь функция:

Должно быть понятно. Это identity функция. А теперь код который выражает саму суть размышлений:

Это тоже identity функция, но в отличие от первого варианта - не полиморфная. Она определена только на натуральных числах, любая другая структура (модель) вызовет ошибку на этой функции. Убедитесь пожалуйста в том что Вы понимаете как работает эта функция. Это важно. Если в понимании возникают затруднения - посмотрите пожалуйста описание τ-lang и практику применения. Если и это не помогло - напишите мне, постараюсь помочь.

Размышления над тем чем отличаются эти реализации identity приводят к интересным результатам.

В первую очередь, я полагаю, в глаза бросается схожесть ядра функции с определением типа. Речь об этом:

сравните с определением типа:

Они не просто похожи, я настаиваю на том что это одно и тоже. Просто мы смотрим на один тот же процесс с разных сторон. С противоположных сторон.

Давайте разбираться. Начнем с типа.

О чем нам говорит объявление типа? Оно говорит нам что символ O принадлежит типу nat (является натуральным числом). Это выражено в первом клозе. А еще оно говорит нам что натуральное число может быть получено конструктором S которому в качестве параметра передано другое натуральное число. Ок. Какое натуральное число мы можем создать если никаких других натуральных чисел нет? Только O. А вот уже имея натуральное число мы можем применить второй клоз и получить (S O), затем (S (S O)) и так далее. То есть мы как бы берем терминатор (O) и начинаем наматывать на него возможные преобразования, получая на каждой итерации новое значение. В данном случае - процесс бесконечный, соотв. множество значений nat - бесконечное множество. Думаю тут не должно возникнуть проблем с пониманием, это то как работает индукция - есть базис и есть induction step(s).

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

Мы получили на входе какое то число. Если это O то возвращаем O и выполнение завершается. Ок. Тут очевидно. Второй клоз интереснее. Если конструктор S - мы дублируем его в результате (справа от =>). Кроме того, мы берем параметр конструктора и передаем его в обвязке num num a'. Если мы знаем что эта обвязка - fixpoint (а мы знаем это в этом конкретном случае, как это вычисляется - я выложу отдельной статьей) - то получается мы рекурсивно вызываем функцию с параметром конструктора S. То есть, если мы посмотрим на параметр a', мы как бы разматываем клубок конструкторов, до тех пор пока не встретится O.

Надеюсь эта часть понятна. Основная мысль - индуктивное определение типа говорит нам как создавать значения этого типа - наматывание клубка. Рекурсивное определение функции identity на этом типе говорит нам как размотать значение этого типа. Можно identity воспринимать как фильтр, пропускающий только значения определенного типа, но об этом позже. Пока только наматывание и разматывание.

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

Глядя на клозы мы можем определить на каком условии эта функция завершится. Terminating case у нас в клозе | O => O. Этот клоз сработает если на входе будет символ (CGT) O. Мы это понимаем глядя на левую часть клоза. Отлично. Других завершающих клозов у нас нет, то есть ядро клубка у нас одно. Или, давайте уже переходить к нормальной терминологии, induction basis у нас равен единице. Ведь то что мы рассматриваем - это обычная структурная индукция.

Ок, идем дальше. Второй клоз - рекурсивный. Сам по себе он не завершится. Но он выйдет из рекурсии если a' (опять же слева от =>) будет равно O. А это возможно если у нас на входе (S O). Мы можем это понять глядя на pattern matching клоза. То есть мы понимаем что вторым возможным значением из области определения identity будет (S O). Почему? Потому что pattern matching этого клоза умеет разматывать только S конструкторы. То есть по левой части клоза мы можем восстановить индуктивное определение типа структуры с которой этот клоз может работать.

Что дальше? А дальше просто - других клозов у нас нет, условие выхода рекурсивного клоза в терминальный мы отработали, остается только понять, как еще мы можем попасть в рекурсивный клоз. А попасть в него мы можем если на входе будет бОльшая структура. Например (S (S O)). Как мы можем это понять? Так же, как мы вывели (S O) - находясь в рекурсивном клозе и глядя на его pattern matching.

То есть что произошло? Мы вывели тип данных области определения функции identity. Это будет тип:

Ровно та информация, что заключена в описании типа nat в Coq нотации.

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

Подведу промежуточный итог:

  • Тип - это информация о структуре данных. В номинативных системах типов (например Calculus of constructions, Calculus of Inductive Constructions, Hindley–Milner type system ) тип является просто меткой, тегом, каким то названием. Сама информация о структуре данных, соответствующих этому типу - в выводе типов не используется. В τ-lang можно реализовать структурную типизацию и использовать эту информацию в выводе типов.
  • есть множество функций для которых мы можем вывести область определения через структурную индукцию
  • знание области определения функции равносильно решению halting problem для этой фунции.

Давайте продолжим.

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

А можем ли мы так же выводить тип области значений? Оказывается что да, можем. Причем размышления и техника исполнения абсолютно та же что при выводе типа области определения, но смотреть мы будем на правые части клозов. Давайте пройдемся.

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

Хорошо. Мы можем (конкретно для этой функции) выводить тип области определения и области значений. То есть по сути мы вывели тип самой функции - nat -> nat.

Давайте теперь познакомимся с RealWorld. Помните, тот самый из haskell:

RealWorld is deeply magical. It is primitive, but it is not unlifted (hence ptrArg). We never manipulate values of type RealWorld; it’s only used in the type system, to parameterise State#.

У нас в τ-lang тоже есть такой, но он парень простой, без пафоса. Это символ *. Про него будет отдельная статья с подробностями, пока что достаточно знать одно его свойство - он является множеством всех возможных значений. То есть он содержит вообще все что мы можем смоделировать. Ок.

А теперь, прежде чем продолжить, напомню одно свойство τ-lang - если на вход match функции (FDEF, не FCOMP) попадает структура с конструктором для которого нет подходящего pattern - исполнение кода аварийно завершается. В τ-lang нет исключений, обработки ошибок такого рода. Позже мы это все смоделируем в стейт-машинах, но в самом интерпретаторе этого нет. Вместо этого мы считаем что данная функция не определена на этом значении.

А теперь с двумя этими хинтами в голове давайте снова взглянем на нашу функцию identity:

Это apply который не будет выполняться - по той простой причине что у нас нет значения аргумента. Вместо этого мы говорим что на входе может быть любое возможное значение. Ок. При этом мы знаем что можно вывести тип значений на выходе (тип области значений). А тип области определения мы вывели ранее. Значит мы можем размышлять следующим образом:

Что бы мы ни подали на входе этой функции (*):

  • либо ее исполнение завершится аварийно (модель на входе будет не nat)
  • либо модель на входе - nat и тогда результат - тоже nat

Мы можем перефразировать это умозаключение - результатом выполнения этой функции всегда будет nat (потому что если функция выполнилась - она вернула nat, ничего другого она вернуть не может)

Это подводит нас к простой мысли:

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

И это действительно важный момент с которым мы будем неоднократно сталкиваться.

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