Skip to main content

Основные понятия и термины

Motoko предназначен для распределенного программирования с использованием модели акторов.

При программировании на Интернет-компьютере в Motoko каждый актор представляет канистру со смарт-контрактом в сети Internet Computer с интерфейсом Candid, написанным на Motoko, Rust, Wasm или другом языке, который компилируется в Wasm. В Motoko мы используем термин «актор» для обозначения любого контейнера, написанного на любом языке, который развертывается на компьютере в Интернете. Роль Motoko состоит в том, чтобы упростить создание этих акторов и упростить их программное использование после развертывания.

Прежде чем приступить к написанию распределенных приложений с использованием акторов, вы должны быть знакомы с некоторыми основными строительными блоками любого языка программирования и Motoko в частности. Чтобы вы могли начать, в этом разделе представлены следующие ключевые понятия и термины, которые используются в остальной части документации и которые необходимы для изучения программирования на Motoko:

  • программа (program)
  • объявление (declaration)
  • выражение (expression)
  • значение (value)
  • переменная (variable)
  • тип (type)

Если у вас есть опыт программирования на других языках или вы знакомы с современной теорией языков программирования, вы, вероятно, уже знакомы с этими терминами и с тем, как они используются. В том, как эти термины используются в Motoko, нет ничего уникального. Однако, если вы новичок в программировании, это руководство вводит каждый из этих терминов постепенно и с помощью упрощенных примеров программ, в которых не используются акторы или распределенное программирование. После того, как вы освоите базовую терминологию, вы сможете изучить более сложные аспекты языка. Более сложные возможности иллюстрируются соответственно более сложными примерами.

В разделе рассматриваются следующие темы:

Синтаксис программы Motoko

Каждая программа Motoko представляет собой свободную смесь объявлений и выражений, синтаксические классы которых различны, но связаны между собой (точный синтаксис программы см. в кратком справочнике по языку).

Для программ, которые мы развертываем на Интернет-Компьютере, действительная программа состоит из actor expression, введенного с помощью специального синтаксиса (ключевое слово actor), который мы обсуждаем в разделе Actors and async data.

В рамках подготовки к этому обсуждению в этой главе и в Mutable state мы рассматриваем программы, которые не предназначены для использования в качестве служб Интернет-Компьютера. Скорее, эти маленькие программы иллюстрируют фрагменты Motoko для написания таких сервисов, и каждая из них (обычно) может быть запущена сама по себе как (несервисная) программа Motoko, возможно, с некоторым выводом на терминал.

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

В качестве отправной точки, следующий фрагмент кода состоит из двух объявлений - для переменных x и y - за которыми следует выражение для формирования одной программы:

let x = 1;
let y = x + 1;
x * y + x;

Результат:

3 : Nat

Мы будем использовать вариации этой небольшой программы в нашем обсуждении ниже.

Во-первых, тип этой программы - Nat (натуральное число), и при выполнении она оценивается в значение 3 (натуральное число).

Введя блок с заключающими скобками (do { и }) и еще одну переменную (z), мы можем изменить нашу исходную программу следующим образом:

let z = do {
  let x = 1;
  let y = x + 1;
  x * y + x
};

Результат:

3 : Nat

Объявления переменных и выражения

Декларации вводят неизменяемые переменные, изменяемое состояние, акторы, объекты, классы и другие типы. Выражения описывают вычисления, в которых задействованы эти понятия.

Пока мы используем примеры программ, которые объявляют неизменяемые переменные и вычисляют простую арифметику.

Объявления переменных в сравнении с выражениями

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

Вспомним наш пример программы, впервые представленный выше:

let x = 1;
let y = x + 1;
x * y + x;

Результат:

3 : Nat

В действительности эта программа представляет собой список объявлений, состоящий из трех объявлений:

  1. неизменяемая переменная x, через объявление let x = 1;,

  2. неизменяемая переменная y, через объявление let y = x + 1;,

  3. и безымянная неявная переменная, содержащая значение конечного выражения, x * y + x.

Это выражение x * y + x иллюстрирует более общий принцип: каждое выражение можно рассматривать как объявление, когда это необходимо, поскольку язык неявно объявляет безымянную переменную со значением результата этого выражения.

Когда выражение появляется в качестве заключительного объявления, это выражение может иметь любой тип. Здесь выражение x * y + x имеет тип Nat.

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

Игнорирование выражений без единичной типизации в списках объявлений

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

let x = 1;
ignore(x + 42);
let y = x + 1;
ignore(y * 42);
x * y + x;

Результат:

3 : Nat

Объявления и подстановка переменных

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

Вспомним наш исходный пример:

let x = 1;
let y = x + 1;
x * y + x;

Результат:

3 : Nat

Мы можем вручную переписать приведенную выше программу, подставив объявленные значения переменных в каждое из их соответствующих вхождений.

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

1 * (1 + 1) + 1

Результат:

3 : Nat

Это тоже валидная программа - того же типа и с тем же поведением (значение результата 3) - что и исходная программа.

Мы также можем сформировать одно выражение с помощью блока.

От объявлений к блочным выражениям

Многие из приведенных выше программ состоят из списка объявлений, как в приведенном выше примере:

let x = 1;
let y = x + 1;
x * y + x

Результат:

3 : Nat

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

Блочные выражения. Мы можем сформировать блочное выражение из этого списка объявлений, заключив его в фигурные скобки. Блоки допускаются только в качестве подвыражений выражений потока управления, таких как if, loop, case и т.д. Во всех остальных местах мы используем do { ... } для представления блочного выражения, чтобы отличить блоки от объектных литералов. Например, do {} - это пустой блок типа (), а {} - пустая запись типа {}.

do {
    let x = 1;
    let y = x + 1;
    x * y + x
}

Результат:

3 : Nat

Это тоже программа, но такая, в которой объявленные переменные x и y приватно внутри области видимости блока, который мы объявили.

Эта блочная форма сохраняет автономность списка объявлений и его выбор имен переменных.

Объявления следуют за лексической областью видимости

Выше мы видели, что вложенность блоков сохраняет автономность каждого отдельного списка объявлений и выбора имен переменных. Теоретики языка называют эту идею lexical scoping. Это означает, что области видимости переменных могут вкладываться, но они не могут вмешиваться в процесс вложения.

Например, следующая (большая, вложенная) программа оценивается в 42, а не в 2, поскольку последние вхождения x и y в последней строке относятся к самым первым определениям, а не к более поздним в пределах вложенного блока:

let x = 40; let y = 2;
ignore do {
  let x = 1;
  let y = x + 1;
  x * y + x
};
x + y

Результат:

42 : Nat

В других языках, в которых отсутствует лексический охват, эта программа может иметь другое значение. Однако современные языки повсеместно предпочитают лексическое выделение, то есть то значение, которое дано здесь.

Помимо математической ясности, главным практическим преимуществом лексической рубрикации является безопасность и ее использование для построения композиционно безопасных систем. В частности, Motoko дает очень сильные свойства композиции. Например, вложение вашей программы в программу, которой вы не доверяете, не может произвольно переопределить ваши переменные с другими значениями.

Значения и оценка

Как только выражение Motoko получает (единственный) поток управления программы, оно оценивается с нетерпением, пока не сведется к результирующему значению.

При этом оно, как правило, передает управление подвыражениям и подпрограммам, прежде чем отдать управление из окружающего стека управления.

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

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

Примитивы (значение примитивного типа, примитивный тип данных)

Motoko допускает следующие примитивные формы значений:

  • Булевы значения (true и false).
  • Целые числа (..., -2, -1, 0, 1, 2, ...) - ограниченные и неограниченные варианты.
  • Натуральные числа (0, 1, 2, ...) - ограниченные и неограниченные варианты.
  • Текстовые значения - строки символов Юникода.

По умолчанию целые и натуральные числа не ограничены и не переполняются. Вместо этого они используют представления, которые растут, чтобы вместить любое конечное число.

По практическим причинам Motoko также включает ограниченные типы для целых и натуральных чисел, отличные от версий по умолчанию. Каждый ограниченный вариант имеет фиксированную ширину (одну из 8, 16, 32, 64) и каждый несет в себе потенциал "переполнения". Если и когда это событие происходит, оно является ошибкой и вызывает прерывание программы. В Motoko нет непроверенных, неперехваченных переполнений, за исключением четко определенных ситуаций, для явно обернутых операций (обозначаемых символом % в операторе). Язык предоставляет примитивные встроенные функции для преобразования между этими различными представлениями чисел.

Краткий справочник языка содержит полный список примитивных типов.

Непримитивные значения

Опираясь на вышеперечисленные примитивные значения и типы, язык допускает использование типов, определяемых пользователем, и каждой из следующих не примитивных форм значений и связанных с ними типов:

Мы обсудим использование этих форм в последующих главах. Точные языковые определения примитивных и непримитивных значений см. в кратком справочнике по языку.

Тип юнита по сравнению с типом void

В Motoko отсутствие типа называется void. Во многих случаях, когда читатели могут подумать, что возвращаемые типы «недействительны (void)» при использовании таких языков, как Java или C++, мы рекомендуем им думать вместо типа единицы, написанного ().

На практике, как и void, стоимость единицы измерения обычно равна нулю.

В отличие от типа void, существует единичное значение, но, как и возвращаемое значение типа void, это единичное значение не несет внутренних значений и, как таковое, всегда несет нулевую информацию.

Другой математический способ представить значение единицы - это кортеж, не содержащий элементов, - нулевой («нулевой») кортеж. Есть только одно значение с этими свойствами, поэтому оно математически уникально и, следовательно, не должно быть представлено во время выполнения.

Натуральные числа

Элементы типа состоят из обычных значений - 0, 1, 2, ... - но, как и в математике, они не привязаны к специальному максимальному размеру. Скорее, представление этих значений во время выполнения вмещает числа произвольного размера, что делает их "переполнение" (почти) невозможным. (Почти, потому что это такое же событие, как и окончание памяти программы, что всегда может произойти для некоторых программ в экстремальных ситуациях).

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

let x = 42 + (1 * 37) / 12: Nat

Результат:

45 : Nat

Эта программа вычисляет значение 45, также имеющее тип Nat.

Надежность типа / Сохранность типа (Type soundness)

Каждое выражение Motoko, которое проверяет тип, мы называем хорошо-типизированным. Тип выражения Motoko служит обещанием языка разработчику о будущем поведении программы, если она будет выполнена.

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

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

В любом случае, статическое и динамическое представления программы связаны статической системой типов и согласуются с ней. Это согласие является центральным принципом статической системы типов и обеспечивается Motoko как основной аспект ее дизайна.

Эта же система типов обеспечивает согласование асинхронных взаимодействий между статическими и динамическими представлениями программы, а также то, что результирующие сообщения, генерируемые "под капотом", никогда не расходятся во время выполнения. Это соглашение схоже по духу с соглашениями между вызывающим и вызываемым типами аргументов и возвращаемых типов, которые обычно ожидаются в типизированных языках.

Аннотации типов и переменных

Переменные связывают (статические) имена и (статические) типы с (динамическими) значениями, которые присутствуют только во время выполнения программы.

В этом смысле типы Motoko представляют собой форму доверенной, проверенной компилятором документации в исходном коде программы.

Рассмотрим эту очень короткую программу:

let x : Nat = 1

Результат:

1 : Nat

В этом примере компилятор считает, что выражение 1 имеет тип Nat, и что x имеет тот же тип.

В этом случае мы можем опустить эту аннотацию без изменения смысла программы:

let x = 1

Результат:

1 : Nat

За исключением некоторых специфических ситуаций, связанных с перегрузкой операторов, аннотации типов (как правило) не влияют на смысл программы в процессе ее выполнения.

Если они опущены и компилятор принимает программу, как это было описано выше, программа имеет тот же смысл (то же поведение), что и первоначально.

Однако иногда аннотации типов требуются компилятору для вывода других предположений и для проверки программы в целом.

Если они добавлены, а компилятор по-прежнему принимает программу, мы знаем, что добавленные аннотации согласуются с существующими.

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

let x : Nat = 1 : Nat

Результат:

1 : Nat

Однако если мы попытаемся сделать что-то, не совместимое с нашим аннотационным типом, программа проверки типов выдаст ошибку.

Рассмотрим эту программу, которая не является хорошо типизированной:

let x : Text = 1 + 1

Результат:

stdin:1.16-1.21: type error [M0096], expression of type
    Nat
cannot produce expected type
    Text

Аннотация типа Text не согласуется с остальной частью программы, поскольку типом 1 + 1 является Nat, а не Text, а эти типы не связаны подтипизацией. Следовательно, эта программа не является хорошо типизированной, и компилятор выдаст сигнал об ошибке (с сообщением и местом) и не будет компилировать или выполнять ее.

Ошибки типов и сообщений

С математической точки зрения, система типов языка Motoko является декларативной, что означает, что она существует независимо от какой-либо реализации, как концепция полностью в формальной логике. Аналогично, другие ключевые аспекты определения языка (например, его семантика выполнения) существуют вне реализации.

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

Сообщения об ошибках программы проверки типов пытаются помочь разработчику, когда он неправильно понимает или иным образом неправильно применяет логику системы типов, которая в этой книге объясняется косвенно.

Эти сообщения об ошибках будут развиваться с течением времени, и по этой причине мы не будем включать конкретные сообщения об ошибках в этот текст. Вместо этого мы попытаемся объяснить каждый пример кода в сопутствующем ему написанию.

Использование базовой библиотеки Motoko

По различным практическим причинам, связанным с разработкой языка, дизайн Motoko стремится к минимизации встроенных типов и операций.

Вместо этого, по мере возможности, базовая библиотека Motoko предоставляет типы и операции, которые делают язык полноценным. Однако, эта базовая библиотека все еще находится в стадии разработки и является неполной.

Базовая библиотека Motoko перечисляет набор модулей из базовой библиотеки Motoko, фокусируясь на основных возможностях, используемых в примерах, которые вряд ли будут радикально изменены. Тем не менее, все эти API базовой библиотеки, безусловно, будут меняться со временем (в разной степени), в частности, их размер и количество будут расти.

Чтобы импортировать из базовой библиотеки, используйте ключевое слово import. Укажите имя локального модуля, который будет импортироваться, в данном примере D для "Debug", и URL, по которому объявление import может найти импортируемый модуль:

import D "mo:base/Debug";
D.print("hello world");

Результат:

hello world
() : ()

В данном случае мы импортируем код Motoko (а не какую-то другую форму модуля) с префиксом mo:. Мы указываем путь base/, за которым следует имя файла модуля Debug.mo за вычетом его расширения.

Печать с использованием Debug.print и debug_show

Выше мы вывели текстовую строку с помощью функции print в библиотеке Debug.mo:

print: Text -> ()

Функция print принимает на вход текстовую строку (типа Text), а на выходе выдает значение единицы (типа unit, или ()).

Поскольку единичные значения не несут никакой информации, все значения типа unit идентичны, поэтому функция print не дает интересного результата. Вместо результата у нее есть побочный эффект. Функция print выводит текстовую строку в удобочитаемой форме на терминал вывода. Функции, которые имеют побочные эффекты, такие как выдача результата или изменение состояния, часто называют нечистыми. Функции, которые просто возвращают значения, без дополнительных побочных эффектов, называются чистыми. Ниже мы подробно рассмотрим возвращаемое значение (единичное значение) и свяжем его с типом void для читателей, более знакомых с этим понятием.

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

Примитив debug_show позволяет преобразовать большой класс значений в значения типа Text.

Например, мы можем преобразовать тройку (типа (Text, Nat, Text)) в отладочный текст без написания собственной функции преобразования:

import D "mo:base/Debug";
D.print(debug_show(("hello", 42, "world")))

Результат:

("hello", 42, "world")
() : ()

Используя эти преобразования текста, мы можем распечатать большинство данных Motoko, пока мы экспериментируем с нашими программами.

Работа с неполным кодом

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

Для разрешения таких ситуаций мы используем функции xxx, nyi и unreachable из базовой библиотеки Prelude, которые описаны ниже. Каждая из них включает в себя общий механизм ловушек, о котором мы расскажем ниже.

Используйте кратковременные отверстия

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

Предположим, что ранее человек импортировал прелюдию следующим образом:

import P "mo:base/Prelude";

Разработчик может заполнить любое недостающее выражение следующим:

P.xxx()

Результат всегда будет проверять тип во время компиляции, и всегда будет ловить во время выполнения, если и когда это выражение когда-либо будет выполняться.

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

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

P.nyi()

Документирование недостижимых путей кода

В отличие от описанных выше ситуаций, иногда код никогда не будет заполнен, поскольку он никогда не будет вычислен, предполагая согласованность внутренней логики инвариантов программ.

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

P.unreachable()

Как и в приведенных выше ситуациях, эта функция проверяет тип во всех контекстах, а при оценке отлавливает во всех контекстах.

Ловушки из-за сбоя выполнения

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

1/0; // traps due to division by 0

Результат:

stdin:1.1-1.4: execution error, arithmetic overflow
let a = ["hello", "world"];
a[2]; // traps due to out-of-bounds indexing

Результат:

stdin:2.1-2.5: execution error, index out of bounds
let true = false; // pattern match failure

Результат:

stdin:1.5-1.9: warning [M0145], this pattern of type
  Bool
does not cover value
  false
stdin:1.5-1.9: execution error, value false does not match pattern

Мы говорим, что код попадает в ловушку, когда его выполнение вызывает ловушку.

Выполнение кода прерывается при первой ловушке и не имеет дальнейшего хода.

Ловушки, возникающие внутри сообщений агента, более тонкие: они не прерывают работу всего агента, но предотвращают продолжение выполнения данного конкретного сообщения, откатывая все еще не зафиксированные изменения состояния. Другие сообщения агента продолжат выполнение.

Явные ловушки

Иногда может быть полезным принудительное выполнение безусловной ловушки с заданным пользователем сообщением.

Библиотека Debug предоставляет для этой цели функцию trap(t), которую можно использовать в любом контексте.

import Debug "mo:base/Debug";

Debug.trap("oops!");
import Debug "mo:base/Debug";

let swear : Text = Debug.trap("oh my!");

(Рассмотренные выше функции Prelude nyi(), unreachable() и xxx() являются простыми обертками для Debug.trap).

Утверждения

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

let n = 65535;
assert n % 2 == 0; // traps when n not even

Результат:

stdin:2.1-2.18: execution error, assertion failure
assert false; // unconditionally traps

Результат:

stdin:1.1-1.13: execution error, assertion failure
import Debug "mo:base/Debug";

assert 1 > 0; // never traps
Debug.print "bingo!";

Результат:

bingo!
() : ()

Поскольку утверждение может быть успешным и, следовательно, продолжить выполнение, его можно использовать только в контексте, где ожидается значение типа ().