τ-lang: description

Posted on January 12, 2020

Ниже изложено (неформально) описание τ-lang и стандартного препроцессора (type-checker, proof-checker и структурная индукция в τ-lang не входят и реализуются в τ2-lang). Тут у нас просто интерпретатор на прямой подстановке (term rewriting system).

Программой на τ-lang является вызов функции с параметрами (apply). Синтаксис языка Lisp/ML-подобный. Кодировка используется utf-8 но это соглашение больше часть парсера а не самого языка τ-lang.

Язык описания структуры

Операторами языка описания структуры являются: обычные скобки - ( ) и НЕКОТОРЫЕ пробельные символы (whitespace characters) а именно:

  • пробел U+0020
  • tab \t U+0009
  • new line \n U+000A
  • carriage return \r U+000D

В дальнейшем этот набор пробельных символов будет обозначаться как [space].

Структура - это важно. В тот момент когда вам покажется что программа состоит чуть менее чем полностью из скобочек - вспомните о том сколько операторов описания структуры вы имеете в обычном языке программирования - помимо скобок и пробельных символов у вас есть еще как минимум: [ ] { } ; , ' " и это лишь малая их часть. Во многих языках операторы структуры прячутся в ключевых словах, в других операторах которые на самом деле являются функциями, в ограничениях на имена переменных и тому подобное.

В τ-lang как и в lisp любая структура описывается скобками. Собственно на этом схожесть с lisp заканчивается.

Идентификаторы

Идентификатор (имя параметра) может быть любой комбинацией любых символов utf‑8 кроме:

  • [space]
  • скобок ( )

Служебные идентификаторы:

  • =>
  • match
  • |
  • _
  • *

Идентификатор, объявленный пользователем, не может быть комбинацией символов => но может их содержать, т.е. 1=>, =>e, a=>b - валидные идентификаторы. Тоже справедливо и для остальных служебных идентификаторов.

Идентификаторы match и | зарезервированы для синтаксиса function definition.

Идентификатор _ зарезервирован и имеет особое значение:

  • в объявлении функции как имя параметра - указывает на то что параметр в теле функции не используется
  • в вызове функции (apply) в качестве аргумента - указывает на отсутствие аргумента и превращает apply в partial apply
  • в левой части clause - указывает на совпадение с любым символом (polymorphic match)
  • в правой части clause - соответствует тому символу который дал совпадение (в левой части также должен быть _)

Идентификатор * является квантором всеобщности (∀) в τ2-lang и в τ-lang никак не участвует, тем не менее идентификатор зарезервирован в целях совместимости парсеров.

let

Явного создания переменных/констант в языке нет (то есть нет let), неявное присваивание происходит при вызове функции либо pattern-matching-е.

  • при вызове функции переданные значения привязываются к именам параметров объявленным в definition функции
  • pattern-matching рассматривается в function definition.

Других способов связать значение с именем - нет. Как следствие - переприсваивания в языке нет, все метки по определению - константы. Так же нет понятия ссылок и указателей - все параметры передаются по значению, по крайней мере это так выглядит. Что происходит под капотом не имеет значения если это соглашение выполняется.

Функции

Функция объявляется так:

Имена параметров функции должны быть уникальны в пределах объявления функции.

В теле функции видны только символы переданные в качестве параметров. Какого либо глобального контекста нет. Любой неизвестный символ в теле функции (справа от =>) трактуется как constructor ground term (CGT).

Важное следствие - рекурсивных функций не бывает, так как в теле функции не виден символ под которым она объявлена (точнее нет символа в момент объявления, привязка к символу может произойти только в момент apply). Рекурсивным может быть только вызов а не сама функция. Рекурсивным вызовом является вызов функции при котором в функцию одним из параметров передается символ под которым она объявлена И при этом в последующей цепочке вызовов эта функция вновь вызывается. То есть передача функции параметром не делает вызов автоматически рекурсивным - если функция не вызывается в дальнейшем.

Есть два способа объявить функцию - function definition и functions composition.

Function definition:

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

В τ-lang деструктуризации на функциях нет (одна из причин существования τ2-lang), то есть аргумент для match не может быть function definition или functions composition.

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

Число параметров имеет значение: структура (S S O) не совпадет с паттерном S a' так как паттерн предполагает наличие одного аргумента в то время как (S S O) содержит два аргумента. Для матчинга этой структуры необходим паттерн S a' b'.

Можно объявлять несколько клозов на один и тот же конструктор если в паттерне указано разное число параметров, например так:

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

Проверка паттернов происходит в порядке их объявления.

Имена параметров в деструктуризации не должны конфликтовать с именами параметров функции. Но в разных клозах можно использовать одинаковые имена - пространства имен клозов не пересекаются. Это видно по второму и третьему клозам предыдущего примера.

Functions composition:

часть справа от => является вызовом функции (apply).

partial apply.

Идентификатор _ при вызове функции имеет особое значение и показывает отсутствие аргумента. Если функция вызвана с числом аргументов меньшим чем указано в сигнатуре и/или в переданных аргументах присутствуют идентификаторы _ - вызов трактуется как partial apply и вычисленным значением этого apply будет функция. Например вот этот apply:

вернет функцию аналогичную объявлению:

При таком вызове:

вернется:

Аналогично partial apply работает и на function definition.

polymorphic match

В function definition в деструктуризации параметра также можно использовать идентификатор _:

В левой части клоза _ обозначает соответствие любому символу. В правой части клоза вместо _ подставляется символ который попал в клоз. Описанная выше функция будет работать с любой структурой заканчивающейся на O:

вернет (S(S(S(S O)))) В тоже время мы можем вызвать эту функцию на другой структуре:

(a =>
    (double a => double double a)
    (double a =>
        match a
        | O => O
        | _ a' => _ ( _ (double a'))
    )
    a
) (L(L O))

И получить (L(L(L(L O)))) Или даже так:

(a =>
    (double a => double double a)
    (double a =>
        match a
        | O => O
        | _ a' => _ ( _ (double a'))
    )
    a
) (L(S O))

что даст (L(L(S(S O))))

Идентификатор _ может использоваться не только для конструктора - то есть в левой части клоза он может стоять на любой позиции. При этом на первой позиции идентификатор _ означает совпадение с любым конструктором, на любой другой - то что этот параметр не используется (то есть также как в объявлении функции). Более того - в паттерне можно использовать _ несколько раз:

Этот код вернет R. Обобщенно - эта функция возвращает конструктор параметра при условии что параметр построен при помощи одноарного конструктора. Первый _ указывает на совпадение с любым конструктором, второй _ - на то что параметр не используется (но обязан быть). В правой части клоза _ содержит в себе имя конструктора с которым паттерн дал совпадение.

препроцессор

Препроцессор, как и парсер, не является частью языка (τ-lang начинается с ast, на нем же и заканчивается), и тем не менее понятно что без композиции/декомпозиции исходников сильно неудобно, поэтому он (препроцессор) есть.

Препроцессор определяет две операции - import и export

Начнем с export - его синтаксис гораздо проще:

Где name - это символ под которым экспортируется сущность, ast - любое допустимое τ-lang выражение.

У import гораздо больше возможных форм:

path - это имя модуля откуда происходит импорт, без кавычек и прочего. Как это имя трансформируется в сам модуль - не так важно. В текущей реализации - это имя файла в той же директории что и код, без указания расширения (.tau добавляется автоматически), вместо разделителей используются точки (при поиске файла превращаются в платформно зависимый pathSeparator (\ для windows и / для *nix).

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

Разберем простой пример с quicksort (в репе в директории examples). В файле core/nat.tau мы видим экспорты:

Это две функции - less then и greater or equal, определенные на натуральных числах. Давайте теперь посмотрим как они импортируются в quicksort.tau:

Как использовать импортированные символы? Препроцессор смотрит на все экспорты (а если мы явно не указали экспорт - то весь оставшийся код будет экпортирован под символом main) и в тех экспортах которые:

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

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

В работе импорта/экспорта важно понять два момента:

  • для использования импортированных символов они должны быть указаны в аргументах экспортируемого apply - препроцессор не лезет дальше в код - только аргументы первого вызова.
  • при экспорте можно указывать partial apply - именно он и будет импортирован. Но в процессе вычисления он будет преобразован в функцию. Это преобразование происходит не в препроцессоре, это работа exec.

Есть еще один, пока не решенный момент. Видно ли экспортируемые символы в самом модуле? То есть можно ли использовать символ в экспорте если он не был импортирован а объявлен в предыдущем экспорте? Пока нет, но возможно в будущем я это реализую.

upd March 6, 2020 - реализовано. Теперь символ, объявленный в экспорте может использоваться в последующих экспортах также как и импортированные символы. Открытый вопрос - совпадение экпортированного символа с импортированным ранее. На данный момент он просто обновляется. Есть мысль что можно ввести ограничение и требовать уникальности идентификаторов. Пока думаю над этим.


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