τ-lang: usage

Posted on January 10, 2020
I’m gonna show you as gently as I can how much you don’t know.
— Dennis “Cutty” Wise (Chad L. Coleman), The Wire, Season 4: Refugees

Практика применения.

Let it be

Первое (наверно) что бросается в глаза программисту пришедшему с императивных языков - это отсутствие присваивания в τ-lang. На самом деле присваивание конечно есть, но оно спрятано в двух местах - вызов функции (apply) и сопоставление по образцу (pattern-matching). Тем кто пришел с функциональных языков будет полегче, кто знаком с λ-calculus - совсем привычно. Давайте последовательно разберем.

Возьмем простую функцию NOT - если она получает на входе true - возращает false, если false - возвращает true. Вот она:

Но как нам теперь назвать ее not что бы использовать в дальнейшем в коде? Для того что бы привязать значение к имени - это значение должно быть в вызове функции (apply), вот так:

В этом примере в теле функции будет доступна константа с именем someName и значением someValue. Вот более конкретный пример с функцией not:

Первая строка - это объявление функции у которой первый параметр имеет имя not. Вторая и далее строки - это объявление первого параметра apply. При вызове этой функции значение (в данном случае объявление функции not) будет привязано к имени параметра (not)

Другая возможность привязать значение к имени - это pattern matching или деструктуризация. Предположим у нас есть некоторая структура, например:

и эта структура передается вот этой функции:

match делает деструктуризацию state и сравнивает клоз на совпадение конструктора и числа аргументов. Поскольку совпадение есть, происходит присваивание, такое что в том месте где у нас расположен … body … нам доступны константы:

  • regs со значением (L (REG ax (S (S O))) (L (REG bx O) EMPTY))
  • cache значением которого будет символ CACHE (constructor ground term)
  • mem значением которого будет символ MEM (constructor ground term)
В принципе думаю этого достаточно что бы понять как связывать в τ-lang значение с именем.

Recursion

Как вы помните, в τ-lang нет рекурсивных функций, есть рекурсивные вызовы. Если вы знакомы с Y-комбинатором из λ-calculus то понять дальнейшее не составит труда.

Вот пример apply функции складывающей два натуральных числа:

Обратите внимание на первое объявление функции:

sum - это не имя этой функции, sum - это имя первого параметра этой функции. И если мы передадим этой функции первым параметром ее саму же (или точнее объявление такой же функции) - то вызов станет рекурсивным. Но мы можем передать в параметре sum другую функцию, например (sum a b => a) и вызов в этом случае становится нерекурсивным.

Но вернемся к рекурсивному вызову. Итак нам надо передать в параметре sum такую же функцию. Поэтому мы дублируем ее и передаем первым параметром в apply.

А теперь обратите внимание как происходит вызов в теле функции: sum sum a' b - мы точно так же вызываем sum и передаем ее же первым параметром. Именно поэтому и первый и все последующие (вложенные или порожденные) вызовы будут рекурсивными.

Результат вызова: (S(S(S(S(S O)))))

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

Что здесь происходит? Объявляется функция у которой два параметра - a и b (складываемые числа), при этом телом функции является apply в котором функцией является еще одно объявление:

(sum a b => sum sum a b).

Это объявление - так называемая рекурсивная обвязка. В итоге у нас функция сложения смотрит в мир с нормальным интерфейсом на два параметра, а сама рекурсивная обвязка спрятана в теле функции.

Вызов (3+2):

Если мы импортируем ее из модуля, то выглядит вообще почти как в нормальном языке программирования:

Присваивание при импорте и экспорте

Но как же так? Если можно сделать import - очевидно что происходит связывание какого то символа (имени) со значением (импортируемой сущностью). То есть это третий способ связать значение с именем?

Да, возможность такая есть, но я не отношу ее к возможностям языка. Это возможность которую дает препроцессор, а он не является частью языка. Если мы заглянем под капот то увидим что препроцессор читает содержимое модулей и подставляет значения в apply, то есть суть процесса сводится к первому сценарию который мы рассмотрели выше. Именно поэтому я не включаю этот сценарий в список возможностей предоставляемых самим языком τ-lang.

Тем не менее при импорте происходит другой интересный процесс, который я предлагаю рассмотреть.

Partial apply

Помните что происходит при partial apply? Мы:

  • берем функцию на n аргументов,
  • передаем ей m аргументов, n и m такие что m < n,
  • и на выходе получаем функцию на n-m аргументов.

А теперь давайте еще раз взглянем на функцию sum:

Видите как внешняя функция-обвязка объявляет два аргумента - a и b и затем в своем теле передает их в другую функцию? Этот шаблон будет нам частно встречаться.

А теперь давайте представим что произойдет если мы развернем эту функцию и возьмем только ее тело?

Это partial apply, у функции (в первой строке) - три аргумента а передается только один. Этот partial apply вернет нам функцию, давайте подумаем какую? У нас указан аргумент sum - значит его в сигнатуре новой функции не будет. А вот a и b не указаны - именно они и составят сигнатуру этой функции. И в таком же порядке будут переданы в теле:

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

Те кому это напомнило η-конверсию из λ-calculus - совершенно правы, это она и есть.

Типизация

Ок. τ-lang - не типизированный язык, откуда может появиться типизация? Да, язык не типизированный, но во первых у нас рано или поздно будет τ2 c type checker-ом, а во вторых никто нам не мешает и на нетипизированном языке писать типизированные функции.

Давайте взглянем на функцию sum (да, мы с ней еще не закончили).

Если вы читали про вывод типов в τ-lang то, думаю, не составит особого труда вычислить тип аргумента a. Этот аргумент может быть только натуральным числом - то есть CGT O с примененным к нему ноль либо большее число раз индуктивным шагом (S nat).

  • Если в аргументе a встретится иной конструктор (не S либо O) - это приведет к аварийному завершению (в match a).
  • Если встретится конструктор O не с нулевым числом аргументов - аварийное завершение.
  • Если встретится конструктор S не с одним аргументом (ноль либо больше одного аргументов) - аварийное завершение.
  • Если не встретится конструктор O - функция не завершится (на самом деле недостижимый кейс - для того что бы не было конструктора O у конструктора S должно быть отличное от 1 число аргументов, что само по себе приведет к аварийному завершению, либо аргумент-конструктор отличный от S или O - что тоже приведет к аварийному завершению.

Выглядит неплохо. А какой тип у аргумента b? Хм. Контроля структуры аргумента b (match b) у нас нет, то есть он может быть любой моделью. То есть его тип - * а сама функция полиморфна по отношению к этому аргументу. И мы можем сделать например так:

и получить (S (L e EMPTY)). Вряд ли это то что мы хотим на самом деле. Ок. Но как нам указать что аргумент b должен быть натуральным числом?

Помните про структурную identity (мы ее рассматривали там же, в выведении типов)? Давайте используем ее:

Помните я говорил что функция является объявлением типа? Этот пример - наглядная демонстрация.

Мы изменили функцию sum добавив параметром функцию, и передаем этим параметром функцию-тип nat. А в клозе, возвращавшем b мы также возвращаем b но уже пропустив через nat. В итоге если b - натуральное число - то оно же и вернется. Если нет - то исполнение аварийно завершится.

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

Но самое приятное в этой ситуации - что то же самое сможет сказать и type-checker.