Семантичний аналіз

Виконується після синтаксичного аналізу в типовій компіляції та в --print-types; дії, що працюють лише із синтаксисом, його пропускають. Помилки зупиняють уражений пакет до LLVM; діагностика зберігає походження з макросів і включень, а наступні вхідні дані все одно діагностуються.

Перевірки модулів і викликів

• Оголошення модуля обов'язкове й унікальне; арність функцій 0..255; без повторних визначень; кожен експорт існує (повторний експорт дає попередження, як в OTP). Імена в лапках і Unicode-імена зберігають свою точну ідентичність.
• Перевіряється кожна функція, включно з невикористаним і недосяжним кодом.
• Виклики розв'язуються в межах пакета за модулем/іменем/арністю. Віддалені виклики (включно з самокваліфікованими) потребують експортів. Відсутні/приватні викликані функції та повторні модулі є помилками.
• fun F/A має називати функцію модуля (function F/A undefined); fun M:F/A і виклики значень (F(Args)) не розв'язуються під час компіляції (funs). Кожне окреме значення fun отримує запис Module::funs після аналізу зв'язувань.
• Самостійна, взаємна та міжмодульна рекурсія приймаються. Граф викликів розбивається на сильно зв'язні компоненти (ітеративний алгоритм Тар'яна) у порядку «викликана функція перед викликачем»; компонента рекурсивна, коли має кілька членів або член викликає сам себе.

Поведінки

Слідує поведінкам (behaviours) OTP, erl_internal:add_predefined_functions і check_behaviour з erl_lint.

• Модуль, що оголошує -callback, отримує попередньо визначену в OTP експортовану функцію behaviour_info/1: callbacks дає оголошені callbacks у порядку вихідного коду, optional_callbacks — ті, що є в коректно сформованих списках -optional_callbacks (callbacks, кваліфіковані модулем, пропускаються). Фронтенд додає її як функцію на рядку -module (driver/predefined). Як і в OTP, власний вихідний код модуля не може її назвати: -export, локальний виклик, fun behaviour_info/1 чи -spec для неї є невизначеною функцією; віддалені виклики (також самокваліфіковані) до неї доходять. -callback поряд із написаною вручну behaviour_info/1 є помилкою (cannot define callback attibute for F/A when behaviour_info is defined, написання OTP).
• -behaviour(M) і -behavior(M) можуть повторюватися. M розв'язується в пакеті; ім'я бібліотечного модуля (library.md) додає цей модуль так само, як літеральний виклик. Діагностика використовує текст OTP на імені атрибута:
  • undefined callback function F/A (behaviour 'M') для кожного обов'язкового, не необов'язкового callback, який модуль не експортує (відсортовано);
  • conflicting behaviours -- callback F/A required by both 'M2' and 'M1' (line L, column C), коли попередня поведінка також його вимагає (необов'язковий callback враховується, коли експортований);
  • behaviour M undefined, коли M немає в пакеті або він не має behaviour_info/1 (поведінка OTP, якої бібліотека Clause ще не надає, як-от application), а також помилки OTP щодо імен модулів для імен, які не можуть бути модулями (the module name must not be empty, ... must be an atom, ...).
• Попередження не спричиняють збою компіляції. Параметри -compile nowarn_behaviours (уся перевірка, включно з помилками імен модулів), nowarn_undefined_behaviour_func, nowarn_undefined_behaviour і nowarn_conflicting_behaviours їх вимикають.
• Не обчислюється: написана вручну експортована behaviour_info/1 модуля поведінки, тож callbacks його користувачів не перевіряються, а попередження OTP про погано визначені та застарілі callbacks ніколи не виникають (відмінності).
• Докази: tests/fixtures/lint (діагностика, згенерована OTP, CTest lint_diagnostics), executables_behaviours, випадки CLI semantic.

Імпорти

Слідує правилам імпорту з erl_lint.

• -import(Module, [F/A, ...]) робить локальний виклик F(...) віддаленим викликом Module:F(...): модуль має бути в пакеті (бібліотечний модуль приєднується до нього, як при літеральному виклику) й експортувати функцію або бути модулем вбудованих функцій (-import(io, [format/2]), -import(erlang, [display/1])). Імпорт має пріоритет над автоімпортованим BIF з тим самим іменем.
• Помилки з текстом OTP: function F/A already imported from M (тоді весь атрибут ігнорується), defining imported function F/A, creating a fun from imported name F/A is not allowed. Імпортована функція в guard є недопустимим викликом у guard (крім guard BIF з erlang).
• Попередження import directive overrides auto-imported BIF F/A -- ..., якщо його не названо в no_auto_import або не задано nowarn_bif_clash; Clause знає автоімпортовані BIF, які реалізує.
• Докази: executables_imports, випадки lint imports_conflicts, imports_fun, imports_bif, семантичні випадки CLI.

Попередньо визначені функції

Слідує модулям OTP і erl_internal:add_predefined_functions. Фронтенд додає module_info/0,1 до кожного скомпільованого модуля (після згенерованої behaviour_info/1) як функції Erlang, що повертають літеральні дані (driver/predefined, semantic/module_info); Module::predefined_ рахує ці кінцеві форми, які завжди експортовані й не потрапляють у --print-types.

• module_info() дає [{module,_},{exports,_},{attributes,_},{compile,_},{md5,_}]; module_info(Key) також відповідає на functions, nifs ([]) і native (false), а для будь-якого іншого ключа генерує badarg.
• exports: експортовані функції в порядку визначення (escripts додають main/1), потім behaviour_info/1, якщо згенерована, module_info/0, module_info/1. functions: кожна функція в порядку визначення, потім ті самі попередньо визначені.
• attributes: кожен атрибут, крім module, експортів та імпортів, форм type/spec/callback, records, export_type, optional_callbacks, export_record, compile, file, документації та feature, у порядку вихідного коду; значення, що не є списком, загортається в список (-tags(a) дає {tags,[a]}). Без -vsn першим іде {vsn,[N]}, де N — це md5, прочитаний як беззнакове ціле число big-endian, як його виводить OTP.
• md5: MD5 надрукованого вихідного коду модуля (print_source: макроси розгорнуто, включення вбудовано, коментарі й форматування відкинуто). compile: [{version,ClauseVersion},{options,[]},{source,AbsolutePath}].
• На відміну від behaviour_info/1, власний вихідний код модуля їх бачить: локальні виклики та fun module_info/1 працюють. Визначення будь-якої з них є помилкою (function module_info/0 already defined); її експорт, як і будь-який повторний експорт, дає лише попередження (function module_info/0 already exported).
• Атрибути є даними; лише on_load, nifs і неінертні параметри -compile відхиляються як такі, що змінюють поведінку.
• Згенеровані функції не мають рядка вихідного коду (OTP їм його не дає): ні налагоджувальних розташувань, ні коментарів із вихідним кодом в IR, ні записів --print-types. module_info/0 містить ті самі літерали, що й module_info/1, тож не робить викликів.
• Докази: executables_module_info (stdout OTP; похідні значення — за формою), випадки tests/fixtures/lint module_info_defined, exports_repeated.

Зв'язування

Кожне зв'язування має ідентичність відносно функції clause[N].local[M]. Входження — це визначення, читання або перевірки точної рівності, позначені контекстом голови/guard/тіла. Аналіз детермінований.

• Кожна клауза починає з порожнього середовища. Кандидати в голові збирають попередні визначення; guards їх читають; тіло бачить їх лише в разі успіху.
• _ нічого не зв'язує; _Name — звичайна змінна. Повторене ім'я є обмеженням точної рівності.
• Зіставлення в тілі відвідують праву частину перед лівою; ланцюжки обробляються справа наліво. Зразок у дужках P1 = P2 є псевдонімом, а не послідовністю.
• Сусідні вирази читають ті самі вхідні імена; їхні визначення експортуються після всього виразу. {X = 1, X} — читання незв'язаної змінної; {X = 4, X = 3} допустимий і завершується збоєм під час виконання.
• Визначення в правій частині andalso/orelse або всередині catch Expr після цього небезпечні (OTP vtunsafe); імена, зв'язані до catch, залишаються придатними. Кожне ім'я, зв'язане всередині try, після нього небезпечне; клаузи of бачать імена тіла, клаузи catch бачать їх як небезпечні, а тіло after бачить кожне ім'я, зв'язане раніше в try, як небезпечне. Змінна стека клаузи catch має бути новою (OTP stacktrace_bound), а її guard не повинен її читати (stacktrace_guard). maybe нічого не експортує: кожен ?= зв'язує для наступних виразів тіла, клаузи else бачать імена тіла як небезпечні, і кожне ім'я, зв'язане всередині, після нього небезпечне. Guards ніколи не публікують зв'язувань; зіставлення в guards є помилками навіть тоді, коли недосяжні.
• Ключі map читають лише вхідні зв'язування; розміри binary також читають попередні сегменти того самого binary (див. зразки).
• Аналізований вираз case зв'язує в охопній області видимості. Кожна клауза починає з цієї області; визначення в її зразку попередні до guard, який лише читає. Імена, зв'язані кожною клаузою, експортуються з однією ідентичністю (пізніші клаузи повторно використовують ідентичність, яку попередня клауза дала цьому імені); імена, зв'язані лише деякими клаузами або небезпечні в будь-якій, після цього небезпечні. Експорти об'єднуються консервативно, як в erl_lint з OTP (icrt_export); попередження OTP, коли пізніший зразок зіставляє експортоване ім'я, не видається. Клаузи if слідують тим самим правилам із guard і без зразка.
• begin/end — послідовність в охопній області видимості.
• Читання незв'язаних, небезпечних і шаблонних (_) змінних є помилками з розташуванням. Повідомлення зберігають формулювання компілятора (unbound variable X, unsafe variable X); корпус зв'язувань перевіряє кожне щодо класу unbound_var/unsafe_var з OTP.
• Comprehension обчислює кожен кваліфікатор по черзі в області видимості, залишеній попередніми. Зразки генераторів зв'язують нові імена, що затінюють зовнішні (читання всередині зразка надають перевагу іменам, які він уже зв'язав); zip-група зв'язує всі свої зразки разом. Шаблони читають як сусідні вирази. Область видимості після comprehension — та сама, що була до неї: її імена там незв'язані.
• Кожна клауза анонімного fun починає з області видимості в місці fun: імена в голові нові й затінюють зовнішні, guards їх читають, і ніщо зв'язане всередині не видно після fun. Кожне зовнішнє визначення, прочитане всередині, записується як захоплення (Function::captures, у порядку визначення). Ім'я іменованого fun — це ще одне визначення, з якого починає кожна клауза (Function::fun_names); воно ніколи не захоплюється. Змінні fun M:F/A є читаннями виразу fun (Function::fun_operands).

Обходи ітеративні з бюджетом модуля в 1 000 000 одиниць роботи або 32 на вираз, якщо це більше (згенерованим парсерам, як-от erl_parse з OTP, потрібно близько 10 на вираз). Розв'язання служб має бюджет того самого розміру; воно переглядає форми -compile і -import модуля щодо стану автоімпорту імені один раз на ім'я, а не один раз на виклик (кожна з тисяч клауз erl_parse викликає hd/1). Вичерпання або будь-яка семантична помилка очищує таблиці зв'язувань і нормалізації модуля.

Типи та специфікації

Приватний граф типів представляє всі розібрані форми типів незалежно від розкладки в runtime: одиничні значення (singletons), діапазони, контейнери, ролі полів map, добутки функцій і нерозв'язані застосування. Об'єднання сплощуються й позбуваються дублікатів; term() — верхній елемент, а none() — нижній. Значення за замовчуванням: 1 048 576 вузлів, 256 членів об'єднання, 200 000 елементів роботи на обхід оголошеного типу (розв'язання, переклад, розгортання) і 8 000 000 на прохід виведення по всій програмі; налагоджувальне збирання clau (без NDEBUG) дозволяє 16 000 і 1 000 000, щоб великі програми все одно швидко компілювалися, і може розширювати більше. Вичерпання розширює до term() з видимим прапорцем і ніколи не звужує представлення.

Оголошені метадані (-type, -opaque, -nominal, -export_type, -spec, -callback, -optional_callbacks) слідують довіднику з typespec OTP і зафіксованій поведінці erl_lint/erl_internal/erl_types:

• Локальні псевдоніми можуть затінювати імена вбудованих типів. Віддалені типи пакета мають бути експортовані. Відсутні типи, дублікати, некоректні метадані, одиничні змінні типів, некоректні межі та специфікації для відсутніх функцій є помилками. Недоступні зовнішні типи дають попередження й стають term().
• Кожен псевдонім або перевантаження має власну область видимості змінних; повторені формальні параметри слідують підстановці OTP за останнім аргументом.
• Рекурсивні псевдоніми залишаються скінченними іменованими посиланнями; непрозорі (opaque) тіла розгортаються лише у своєму модулі; номінальні імена зберігаються всюди, і лише перевірка специфікацій читає визначення номінального типу, всередині його модуля.
• Обчислення констант точне, обмежене 10 000 десяткових цифр на значення.

Виведення типів

Виведення типів (inference) відокремлене від оголошених типів і ніколи не довіряє специфікаціям.

• Вхідні дані експортованих функцій і функцій, які називає fun F/A, є довільними термами. Функція, в яку входять лише прямими викликами з пакета (не експортована й не названа fun), бере як вхідні дані об'єднання фактів про аргументи в місцях її виклику (semantic/types/inference_inputs), що зіставляються зі зразками голови кожної клаузи; рекурсивні виклики також враховуються. Вхідні дані починаються з none() (функція, яку ніщо не викликає, ніколи не виконується й виводиться як none()) і зростають упродовж проходів пакета. Кожне вхідне значення підіймається сходинками залежно від кількості своїх змін: перші 4 зміни об'єднують, наступні 2 розширюють, як рекурсивні результати, наступні 2 також замінюють контейнери всередині контейнера на term(), а подальша зміна дає term() (з повідомленням про розширення). Вхідні дані, що не усталилися після 63 проходів, стають term() (з повідомленням про розширення). Рекурсивна компонента вважається витратною, щойно одне розв'язання витратить понад 2^17 об'єднань ґратки (враховуючи вкладені) і понад 1/16 найбільшої кількості об'єднань, витрачених одним проходом дотепер; коли вхідні дані її членів знову змінюються, вони одразу стають term() (з повідомленням про розширення), тож подальші розв'язання більше не слідують за коливаннями вхідних даних її викликачів.

• Проходи після першого обходять лише компоненти, для яких змінилося щось із прочитаного ними (semantic/types/inference_incremental): компонента зберігає свої підсумки й факти виразів, поки вхідні дані її членів, кожен прочитаний підсумок (виклики, fun F/A, apply) і вхідні дані викликаних функцій, які вона обчислювала повторно, залишаються незмінними, а бюджети проходу й повторного аналізу дали б їй ті самі відповіді (бюджет повторного аналізу витрачено так само, як на початку її останнього обходу, або він знову дозволив би чи відхилив би все); її робота все одно враховується в бюджеті проходу. Результати збігаються з обходом кожної компоненти. Завершальний прохід із вхідними даними term() обходить їх усі. Після проходу лише вхідні дані функцій, обійдених у ньому або викликаних функцією, обійденою в ньому, знову об'єднуються з їхніх викликів; факти аргументів і вхідні дані решти залишаються такими, як після останнього об'єднання.

• Літерали мають точні факти: цілі числа будь-якого розміру й символи є одиничними значеннями, атоми — одиничними атомами, числа з плаваючою комою — float(), рядки — непорожніми списками своїх символів ([] для ""), а -/+ від літерального числа зберігають його факт. Кортежі зберігають факти своїх елементів; maps, побудовані зі сталими ключами (факт одного значення: ціле число, атом, [] або кортеж чи map із таких), зберігають факт значення кожного ключа, ключ, заданий двічі, зберігає своє останнє значення, а будь-який інший ключ дає map(). Побудова bitstring рахує свій розмір: літеральні, розмірені та UTF-кодовані літеральні символи — точно, UTF-сегмент іншого значення — за його кодуванням (UTF-8: від 8 до 32 бітів байтами), а сегмент binary/bitstring — за фактом свого значення або будь-яким кратним своєї одиниці (<<1, Rest/binary>> дає nonempty_binary()). Операнд, що ніколи не дає значення (none()), робить побудову none().

• Оператори та вбудовані функції (semantic/types/inference_operators) обчислюють свій результат із фактів своїх операндів. Одиничні цілі числа згортаються точно до 4 096 бітів на операнд і результат (включно з bignums; більше дає integer()); інші цілі числа використовують інтервальну арифметику для +, -, * невід'ємних діапазонів, band з невід'ємним операндом (X band 15 дає 0..15), rem на обмежений дільник (X rem 10 дає -9..9), bnot, унарного - і abs/1; операнд float дає float(), невідомий — number(), а / завжди дає float(). Порівняння згортаються, коли значення операндів можуть порівнюватися лише одним чином (одиничні атоми чи цілі числа, діапазони цілих чисел, що не перетинаються, числа проти не-чисел), і дають boolean() в іншому разі; and/or/xor/not і andalso/orelse комбінують істиннісні значення, які можуть мати їхні операнди (правий операнд andalso є результатом, коли лівий — true). Таблиця дає кожній вбудованій функції мосту її результат: pid() для self/0 і spawn/1,3, reference(), port(), non_neg_integer() для розмірів, string(), nonempty_string(), binary(), list(), tuple(), atom(), boolean() для перевірок типів, true/ok для вбудованих функцій із побічними ефектами, повідомлення для ! і send/2; trunc/1 і подібні зберігають цілочислові операнди; невідомі вбудовані функції дають term(). Операція, що завжди генерує виняток (1 + a, 1 div 0, error/1, exit/1, throw/1, halt/0,1), дає none(), а erlang:raise/3 повертає лише badarg. Згортання ніколи не змінює згенерований код: переповнення та збої залишаються результатами часу виконання.

• Тіло, чий вираз ніколи не завершується (none()), дає none(); так само й виклик із таким аргументом. Шляхи, що генерують винятки, нічого не додають до об'єднання, тож функція, яка завжди генерує виняток, виводиться як none().

• Функції тотожності/проєкції зберігають точні відношення з аргументами, які поширюються через вкладені локальні та віддалені виклики зі свіжими змінними для кожного виклику.

• Контейнери (semantic/types/inference_containers): список [E1, ..., En | T] об'єднує свої елементи перед фактом хвоста (правильний список, коли хвіст є правильним списком, nonempty_improper_list(H, T), коли хвіст не є списком, nonempty_maybe_improper_list(), коли він невідомий або може бути неправильним: комірка ніколи не порожня, також у зразку на кшталт [H | _]); ++, --, hd/1, tl/1, element/2, setelement/3, tuple_to_list/1 і map_get/2 читають і перебудовують факти елементів член за членом об'єднання, причому член, що згенерував би виняток, нічого не додає. Оновлення map зберігає точні ключі (:= для відсутнього ключа відкидає цей член) і дає map() для невідомого map. Records на кортежах є кортежами: побудова заповнює значення за замовчуванням (undefined, якщо його немає), доступ і оновлення читають і встановлюють поле відповідних кортежів, а #r.f — це індекс поля. Спискова comprehension — це, можливо, порожній список фактів її шаблонів, бінарна comprehension — будь-яка кількість копій розміру її шаблону, map comprehension — map().

• Funs (semantic/types/inference_funs): fun F/A — fun своєї арності, що повертає виведений результат функції (вбудованої функції, або, зі змінною арністю, fun()), fun M:F/A — fun, що повертає term(), а анонімний fun — fun, що повертає об'єднані результати своїх клауз, з урахуванням захоплених значень. Виклик значення об'єднує результати його funs цієї арності, які вибирають його аргументи (term() для невідомого fun, none(), коли жоден член не можна так викликати). Анонімний fun, цілком зв'язаний зі змінною й викликаний через неї, обчислюється знову для цього виклику, а його зразки зіставляються з фактами аргументів, щонайбільше на 4 таких виклики вглиб, і факти його першого обчислення потім відновлюються (Double = fun(Y) -> Y * 2 end, Double(3) дає 6). apply(F, Args) (також erlang:apply/2) — це виклик F з аргументами, які містить Args: елементами літерального правильного списку, інакше — елементами його факту ([], список відомих позицій або стільки копій елемента правильного списку, скільки приймає єдина арність F); зв'язаний анонімний fun обчислюється знову, як вище (apply(fun kind/1, [1]) вибирає kind(1)). apply(M, F, Args), де M і F — відомі атоми, що називають експортовану функцію пакета, читає функціональні типи цієї функції, як fun F/A. Аргументи невідомої довжини, інші цілі та M:F(Args) зі змінними іменами залишаються term(). Оскільки fun F/A і apply/3 можуть називати функцію, виведену пізніше, проходи по пакету також повторюються, доки кожне таке читання не побачить кінцевий результат своєї функції; інакше останній прохід дає їм результати term().

• Присвоєння цілих значень у тілі та псевдоніми копіюють факт правої частини (Y = 42, Z = Y, id(Z) виводить 42); зразки кортежів, списків, maps і records на кортежах дають своїм змінним факти частин, з якими вони зіставляються, у зіставленнях у тілі, клаузах case (з аналізованого виразу), клаузах of виразу try (зі значення його тіла) і генераторах (з елементів їхніх вхідних даних або ключів і значень map). Недоведені значення залишаються term() без відношень.

• Звуження (semantic/types/inference_narrowing, inference_scopes, meet): усередині клаузи функції, case, receive або fun кожен зразок перетинається (meet) зі значенням, яке зіставляє (форма літерала, кортежу, списку, record на кортежі, map або bitstring; факт зв'язаної змінної), змінна аналізованого виразу case звужується разом із ним, а guard звужує змінні, які перевіряє. Перевірки типів (is_atom/1 до atom(), is_boolean/1, is_integer/1, is_float/1, is_number/1, is_binary/1, is_bitstring/1, is_list/1 до maybe_improper_list(), is_tuple/1, is_map/1, is_function/1,2, is_pid/1, is_port/1, is_reference/1, is_record/2,3 до кортежу record, is_map_key/2 — свій map до map(), і старі імена guards) перетинаються з фактом свого аргументу; порівняння з цілочисловими константами (<, =<, >, >=, ==, =:=, з будь-якого боку, включно зі згорнутими константами) звужують значення, про яке вже доведено, що воно ціле, до діапазону, причому межі однієї перевірки накопичуються (10 >= X, X >= 0 дає 0..10); два доведені цілі числа, що порівнюються, звужують одне одного за своїми межами (X > Y з Y у 0..5 робить X щонайменше 1), а /=, =/= з константою зсувають рівну їй межу діапазону всередину. Значення, що може бути float або іншим термом, не звужується. Кон'юнкція застосовує кожну перевірку по черзі, диз'юнкція об'єднує те, що доводить кожна альтернатива, not і хибні перевірки нічого не доводять. Клауза після тієї, чиї зразки — усі прості змінні, а весь guard був однією перевіркою типу, бачить це значення без перевіреної категорії; після одного порівняння з цілочисловою константою те саме значення (проста змінна цієї клаузи), доведене як ціле, бачить порівняння хибним (f(N) when N >= 0 -> ...; f(N) when is_integer(N) -> ...: друга клауза бачить neg_integer()). Правий операнд andalso, клауза true виразу case Test of і те, що йде після фільтра comprehension, бачать перевірку істинною. Порожній перетин робить клаузу неможливою: вона нічого не додає до результату. Звужені факти діють лише всередині своєї клаузи чи операнда; catch, правий операнд orelse і кожна клауза відновлюють факти, що були до них. Після case, if, receive, try або maybe факт змінної — це об'єднання її фактів у кінці кожної клаузи, що завершується, тож case X of forever -> ...; N when is_integer(N), N >= 0 -> ... end залишає X як non_neg_integer() | forever.

• try і maybe: try — це об'єднання значень його клауз of (значення його тіла без of) і значень його клауз catch; тіло after нічого не додає. Клаузи of починають з фактів у кінці тіла й зіставляють його значення, як клаузи case (неможлива клауза нічого не додає); клаузи catch і тіло after починають з фактів до try, причому зразок класу зіставляється з error | exit | throw. maybe — це об'єднання значення його тіла, значень його клауз else і, без else, значень, на яких можуть не вдатися його зіставлення ?=: факт зіставленого значення без форми зразка, коли зразок зіставляє всю свою форму (нові змінні, використані один раз, літеральні атоми й цілі числа, [], кортежі з них), інакше весь факт. Кожен зразок ?= перетинається зі своїм значенням і публікує свої змінні для решти тіла; ?=, що ніколи не може зіставитися, зупиняє тіло. Клаузи else починають з фактів до maybe і зіставляють об'єднані невдалі значення, як клаузи case. Факти після try об'єднують факти в кінці його тіла (без of) і кожної клаузи, що завершується; після maybe — факти в кінці його тіла, кожної клаузи else, що завершується, і, без else, факти до нього.

• Використання (semantic/types/inference_uses): операція, що генерує виняток, якщо операнд не має певного типу, доводить цей тип для змінної, яку вона прочитала, після повернення з операції: арифметика й унарні -/+ — number(), div, rem, бітові оператори й bnot — integer(), and/or/xor, not і лівий операнд andalso/orelse — boolean(), ++ і -- — list(), викликане значення — fun цієї арності, змінне ім'я модуля чи функції — atom(), оновлення map — map(), доступ до record на кортежі чи його оновлення — кортеж record, сегмент binary — свій тип (<<X:8>>: integer()), а його розмір — non_neg_integer(), і по одному рядку на кожну перевірку аргументу вбудованої функції мосту (hd/1, tl/1 — nonempty_maybe_improper_list(), length/1 — list(), element/2 — pos_integer() і tuple(), map_get/2 і is_map_key/2 — map(), atom_to_list/1 — atom(), ...). Операція зберігає свою перевірку під час виконання. Імена, зв'язані з тим самим значенням (Y = X, змінний зразок case на змінному аналізованому виразі), звужуються разом.

• Домени входу й успіху: домен входу кожного аргументу — це об'єднання по можливих клаузах функції його факту після голови й guard (звужений факт простої змінної, інакше факт зразка); його домен успіху — об'єднання по клаузах, що завершуються, його факту в місці їхнього нормального повернення. --print-types показує домен успіху як вхідні дані (bounded(1..10) -> 1..10, inc(X) -> X + 1 як inc(number()) -> number()) або домен входу функції, яка ніколи не повертається. Виклик, що повертається, звужує свої змінні аргументи до домену викликаної функції, крім випадку всередині рекурсивної компоненти, яка ще розв'язується.

• Результати клауз об'єднуються консервативно: проєкція зберігається, лише якщо кожна клауза повертає той самий аргумент. case або if об'єднує результати своїх клауз так само.

• Функціональні типи (semantic/types/function_types): окрім підсумку-об'єднання вище, функція зберігає по одному функціональному типу на кожну можливу клаузу, як перевантаження -spec: факти аргументів після голови й guard (звужений факт простої змінної, інакше факт зразка) і результат клаузи (none() для клаузи, що завжди генерує виняток; неможливі клаузи не додають жодного). Клауза, чий результат є залежним фактом від її аргументів (case або if, що її завершує, або змінна, зв'язана з таким, вкладені на будь-якій глибині), розділяється на один функціональний тип на кожну клаузу цього факту, а факти її параметрів перетинаються з аргументами, які вони називають. Функціональні типи з рівними вхідними даними зливаються (їхні результати об'єднуються); понад 32 останні зливаються в один з об'єднаними вхідними даними й результатами. Рекурсивні компоненти ітерують їх разом із результатами, кожен раунд об'єднуючи (потім розширюючи) результат кожного типу; компонента, що не збігається, зберігає лише свої підсумки-об'єднання. Факт анонімного fun зберігає по одному функціональному типу на кожну можливу клаузу (її зразки й guard над будь-яким аргументом), fun F/A — функціональні типи F/A; funs, що об'єднуються, зберігають свої функціональні типи, лише коли вони рівні, інакше вони об'єднуються в один fun з їхніх об'єднаних результатів із будь-якими вхідними даними (перетин із fun з будь-якими вхідними даними, як це робить використання F(A), їх зберігає). Спеціалізація, домени й перевірки специфікацій читають підсумок-об'єднання.

• Виклики вибирають функціональні типи: виклик функції з функціональними типами читає по черзі кожен тип, з вхідними даними якого перетинається кожен факт аргументу, і зупиняється після точного (зразки з нових змінних, використаних один раз, літеральних атомів і цілих чисел, [] і кортежів із них; без guard або лише true і перевірки типів простих змінних-аргументів; для розгалуження — аргумент як аналізований вираз case), вхідні дані якого містять аргументи: жодна пізніша клауза не може бути вибрана. Його результат — об'єднання результатів вибраних типів, причому результат, рівний аргументу, є фактом цього аргументу в межах результату типу; якщо нічого не вибрано, виклик дає none() (він може лише згенерувати function_clause). Невідомі аргументи вибирають кожен тип, тобто об'єднання; функція без функціональних типів (бюджет, компонента, що не збіглася) використовує свій підсумок-об'єднання. Після повернення з виклику його змінні аргументи звужуються до домену успіху та до об'єднаних вхідних даних вибраних типів. Виклики значень fun так само вибирають функціональні типи факту fun, а анонімний fun, обчислений знову для виклику (див. Funs), входить у свої клаузи, перевіряє їхні guards і виходить із них, як case, тож клауза, з якою його аргументи не можуть зіставитися, нічого не додає (F = fun(1) -> one; (_) -> other end, F(2) дає other). Рекурсивні компоненти збігаються за результатами й функціональними типами.

• Виклики обчислюють викликану функцію знову: коли факти аргументів виклику лежать у межах вхідних даних викликаної функції й вужчі в одному з них, тіло викликаної функції обчислюється знову з ними як вхідними даними, як зв'язаний анонімний fun, а результат виклику — це результат вибраних функціональних типів, перетнутий з результатом цього обчислення (two_callers() -> {add_one(10), add_one(20)} дає {11, 21}); аргументи виклику також звужуються до домену успіху цього обчислення. Підсумок викликаної функції, її функціональні типи й записані факти виразів ніколи не змінюються (спеціалізація читає лише їх). Бюджети: 4 вкладені обчислення, викликані функції щонайбільше з 256 виразів, 4 096 одиниць роботи на виклик із пулу в 262 144 на прохід по пакету (окремо від власного бюджету пакета); рекурсивні компоненти ніколи не обчислюються знову. Після вичерпання бюджету виклик зберігає результат вибраних функціональних типів.

• receive — це об'єднання його клауз і тіла after, яке з тайм-аутом infinity ніколи не виконується.

• Рекурсивна компонента починає результат кожного члена з none() у своєму першому розв'язанні, а в пізніших проходах — із підсумків, якими завершилося її останнє розв'язання: тоді перший обхід кожного члена замінює його підсумок тим, що знайшов обхід (попередній підсумок до цього слугує лише припущенням для викликів), тож застарілі функціональні типи ніколи не залишаються. Вона повторно виводить члени, доки жоден результат не змінюється; кожен раунд об'єднує новий результат із попереднім (розширює його після перших 8 раундів, домен виведення), а незавершений рекурсивний виклик нічого не додає до об'єднання. Функція, яка ніколи не може повернутися, залишається none(). Компонента, що не збіглася після 8 раундів плюс 4 на кожного члена, або чиї раунди витратили понад восьму частину бюджету проходу, розширює кожного члена до term() (з повідомленням про розширення, як при вичерпанні бюджету), а завершальний раунд повторно обчислює факти виразів; факти виразів попередніх раундів відкидаються, тож залишаються лише факти з кінцевих припущень. Така компонента запам'ятовується: пізніші проходи одразу дають її членам term() і виконують лише той завершальний раунд, замість того щоб знову ітерувати до межі. Прохід, що розширює всі вхідні дані до term(), забуває запам'ятовані компоненти, тож кожна отримує ще одне розв'язання з цими вхідними даними.

• Раунди ніколи не зменшують підсумок члена: його функціональні типи об'єднуються з типами попереднього раунду тип за типом (результати об'єднуються, змінені вхідні дані об'єднуються, і тип більше не точний), або, коли кількість типів змінилася, типи обох раундів зливаються. Як запобіжник, кожен член зберігає свої останні 4 підсумки, і член, що повертається до будь-якого з них, стає term() без функціональних типів до кінця розв'язання, що дає змогу іншим членам збігтися.

• Раунд обходить лише членів, які читають підсумок, змінений з часу їхнього останнього обходу: кожен обхід відзначає підсумки, які він читає (виклики, результати викликів, fun F/A), змінений підсумок позначає своїх читачів, а непозначений член зберігає свої факти виразів. Перший раунд обходить кожного члена. Член зберігає свій останній обхід між розв'язаннями: розв'язання повторно бере результат того обходу разом із фактами виразів і роботою, поки прочитані ним члени мають ті самі результати й функціональні типи, а решта прочитаного ним не змінилася й дала б ті самі відповіді, як для збереженої компоненти в інкрементних проходах. Результати збігаються з його обходом.

• Спільний бюджет роботи обмежує виведення; вичерпання втрачає точність і повертається до загального коду, ніколи не відхиляючи програму.

• Специфікації, що суперечать виведенню, діагностуються (semantic/types/contracts), але ніколи не стають фактами, тож програма в будь-якому разі поводиться так, як каже її код. Оголошений тип стає фактами, які він містить (або більше): вбудовані типи — за іменем (byte() — це 0..255, timeout() — non_neg_integer() | infinity, iodata() і iolist() — списки будь-якої форми), псевдоніми — за своїм визначенням, непрозорі й номінальні типи — за своїм визначенням усередині свого модуля і як будь-який терм поза ним, віддалені типи — через пакет, змінні типів — через свої межі when (без обмежень: будь-який терм), maps і records — за своєю категорією. Суперечить лише пара, що не перетинається, оскільки виведені факти можуть містити більше значень, ніж створює код:

  • домен входу аргументу, що не має спільних значень зі специфікацією, є помилкою;
  • виведений результат без спільних значень (якщо він не невідомий і не none(), що підходить до будь-якого результату) або виклик, факти аргументів якого відхиляє кожне перевантаження, є попередженням (виклик може бути на шляху, який ніколи не виконується);
  • none()/no_return() допускає лише функцію, яка ніколи не повертається.

  Діагностика називає функцію, оголошений тип так, як його написано, і виведений. Специфікації -callback не перевіряються. Компілятор OTP не перевіряє специфікацій (відмінності).

Залежні факти

semantic/types/dependent. case, if або try ... of поводиться як fun від змінних, які звужують його клаузи, застосований до них: його значення є залежним фактом, по одному функціональному типу на кожну можливу клаузу.

• Параметри: змінні, зв'язані до конструкції, які читають її аналізований вираз (останній вираз тіла try) і guards, у порядку вихідного коду (змінні, які зв'язують зразки її клауз, нові в кожній клаузі й не є параметрами); щонайбільше 4, звуження пізніших забувається. Кожна можлива клауза зберігає факти параметрів після свого зразка й guard та своє значення (none() для клаузи, що ніколи не завершується); вона точна, як функціональний тип під час вибору виклику, коли case або try зіставляє параметр або кортеж параметрів із точним зразком і guard, або коли if має точний guard.
• Аналізований вираз, що є кортежем змінних, звужує кожну змінну до її елемента зіставленого значення, а змінна зразка-кортежу зв'язується з тим самим значенням, що й елемент аналізованого виразу на її позиції (case {X, Y} of {A, b} when is_integer(A) -> ... звужує X і Y).
• try ... of залежить від своїх клауз of; його клаузи catch можуть іти за будь-яким значенням його тіла, тож їхні об'єднані значення об'єднуються зі значенням кожної клаузи (try X of 1 -> one; _ -> other catch _:_ -> error end дає $try_of_operator(X :: 1) -> error | one; (X :: _) -> error | other).
• receive і maybe ... else залишаються об'єднанням своїх клауз: їхні клаузи зіставляють повідомлення або невдале значення ?=, яке ніщо поза ними не може назвати, тож жодне читання не могло б вибрати серед них.
• Клауза, чиє значення саме є залежним (вкладений case або if, або читання залежної змінної), вносить по одному функціональному типу на кожну свою клаузу над об'єднанням обох списків параметрів, з перетнутими вхідними даними. Типи, у які ніколи не можна ввійти (вхідні дані none() або в межах вхідних даних попереднього точного типу), відкидаються, так само як і параметри, чиї факти однакові в кожному типі; рівні вхідні дані зливаються, і понад 32 типи останні зливаються, як для функціональних типів. Конструкція, чиї решта типів дають те саме значення або яка не звужує жодного параметра, є своїм простим об'єднанням.
• Кожен інший споживач читає стертий факт — об'єднання значень клауз. Факти, що виходять за межі обійденої функції (результати, функціональні типи, факти funs), стираються; об'єднання зберігають залежність, лише коли обидві сторони мають однакову.
• Змінна, зв'язана із залежним значенням, його зберігає. Читання змінної вибирає клаузи, у які входять поточні факти її параметрів (у порядку вибору виклику: точна клауза, вхідні дані якої їх містять, зупиняє вибір) і чиї значення перетинаються з власним звуженим фактом змінної, а факт читання — це об'єднання їхніх значень (Y = case X of 1 -> one; _ -> other end, case X of 1 -> Y end читає one).
• Змінна, яку зв'язує кожна клауза case або if, є об'єднанням її фактів у кінці клауз, що завершуються, залежним від параметрів конструкції так само, як її значення: case X of 1 -> Y = 5; _ -> Y = 6 end, Y виводить (1) -> 5; (_) -> 6. Те саме об'єднання застосовується після receive, try і maybe, без залежності.
• Оператори, вбудовані функції, побудова кортежів, списків, maps і records та виклики функцій пакета (їхні функціональні типи вибираються, як під час вибору виклику, аргументи повторно не звужуються) із залежними операндами обчислюються один раз для кожної комбінації клауз операндів, зі значеннями цих клауз замість фактів операндів і перетнутими вхідними даними: читання однієї змінної беруть ту саму клаузу, інші операнди комбінуються, щонайбільше 16 комбінацій (понад це використання є простим об'єднанням). R + 1 з R = case X of a -> 1; b -> 2 end виводить (a) -> 2; (b) -> 3.
• Звуження залежної змінної (зразок, guard, використання) також звужує її параметри до об'єднання вхідних даних тих клауз, у які ввійдено і чиї значення перетинаються зі звуженим фактом, а також їхні параметри по черзі, на 4 рівні вглиб: після R = case X of a -> 1; b -> 2 end вираз case R of 1 -> X end читає X як a.
• Залежний результат клаузи функції розділяє її (див. Функціональні типи): параметри, що називають аргумент, або ім'я, зв'язане з його значенням, перетинаються з його вхідними даними; інші відкидаються (такий тип точний, лише якщо їхні вхідні дані — будь-який терм). nested_case(X, L) з case X of 1 -> case L of spanish -> uno; _ -> one end; _ -> other end виводить (1, spanish) -> uno; (1, _) -> one; (_, _) -> other.
• --print-types позначає залежне значення як функціональний тип, названий за його конструкцією, з кожним вхідним значенням після імені його параметра: case X of 1 -> one; _ -> other end закінчується на end. % $case_of_operator(X :: 1) -> one; (X :: _) -> other; if друкує $if_operator, try ... of — $try_of_operator.

Домен виведення

semantic/types/lattice. Факт — це множина значень, які може мати змінна чи результат. Факти об'єднуються там, де сходиться потік керування (клаузи, гілки), і розширюються між раундами рекурсивної компоненти; кожен бюджет нижче коректно розширюється до більшої множини й ніколи не відхиляє програму. Факти друкуються як типи Erlang, категорії — за своїми вбудованими іменами.

• Об'єднання зберігає по одному члену на кожну об'єднану форму, у порядку термів Erlang їхніх значень: числа, атоми, reference(), funs, port(), pid(), кортежі, maps, [], списки, bitstrings, потім оголошені іменовані типи; понад 8 членів стають term().
• Контейнери вкладаються щонайбільше на 4 рівні; факт, глибший за це, стає term().
• Об'єднання відкидає точний член-кортеж, який містить інший точний кортеж того самого розміру (з двох, що містять один одного, залишається попередній), тож одна множина значень має одне об'єднання, а рекурсії по деревах усталюються.
• Рекурсивні компоненти об'єднуються впродовж 8 раундів (цикли до 8 функцій збігаються точно), потім розширюються (виведення типів).
• Звуження (Lattice::meet) — це перетин фактів, значення, які містять обидва (або більше, але none() лише тоді, коли спільних немає). Порожній перетин означає, що шлях не може виконатися.
• Факти — це вузли графа, які ніколи не змінюються, тож граф зберігає відповідь кожного об'єднання двох фактів, перетину й перевірки включення (within) до кінця пакета: майже всі вони повторюються. Збережена відповідь усе одно враховує виконані нею об'єднання для відмови з урахуванням вартості, тож результати від неї не залежать; відповідь, обчислена, коли бюджет вузлів розширив факт, не зберігається.

На -O2 зі спеціалізацією типів пониження використовує ці факти для вилучення перевірок (спеціалізація); специфікації ніколи не стають фактами.

Кеш виведення

Модулі в каталогах кешу виведення можуть почати компіляцію з результатами, збереженими попередньою компіляцією: підсумками, локальними вхідними даними та фактами виразів своїх функцій. infer тримає їх незмінними в кожному проході, ніколи не обходить компоненту, всі члени якої їх повторно використовують, і обходить кожну іншу функцію як зазвичай, читаючи збережені підсумки, як і будь-які інші.

• Від чого залежать факти модуля. Експортовані функції та функції, які називає fun F/A, починають з term(); вхідні дані кожної іншої функції надходять від її викликачів, які перебувають у тому самому модулі; факт називає функцію іншого модуля лише через атом: віддалений виклик, fun M:F/A або apply/2,3 на факті-атомі (і читає розкладку record іншого модуля лише через native record, який він кваліфікує або імпортує), а кожен факт-атом походить з атома, який модуль записує, або з факту модуля, якого він досягає. Отже, факти модуля залежать лише від його власного коду й коду модулів пакета, які називають його атоми, транзитивно. Ключ його збережених результатів покриває саме це: ідентичність clau, відбиток модуля (його вихідний код, кожен файл, який він включає, параметри препроцесингу та відповідь parse transform), попередньо визначені форми, статус escript і бібліотеки, а також те саме для кожного модуля пакета, якого досягають його атоми. Модуль, досягнутий у такий спосіб, що не має відбитка, робить модуль некешованим.
• Живість. Живість експортів лише вилучає функції, а вилучений викликач лише звужує вхідні дані функцій, які він викликав: факти, обчислені з більшою кількістю живих функцій, залишаються дійсними. Збережені результати повторно використовуються, коли вони містять кожну функцію, живу зараз (results do not fit в іншому разі); пропущені функції нічого не отримують.
• Змішування. Збережені та свіжі результати можуть зустрітися в одному пакеті: факти кожного модуля дійсні для кожного запуску програми, хоч би що казали факти іншого модуля, тож свіжий модуль, що читає збережений підсумок (або навпаки), залишається коректним. Рекурсивна компонента з членами обох видів обходиться повністю.
• Точність. Повторно використані результати — це результати компіляції, яка їх зберегла. Результати свіжого модуля все ж можуть відрізнятися від компіляції без кешу: бюджет проходу більше не платить за повторно використані модулі, а ідентичності графа, за якими впорядковано кілька членів об'єднання, нумеруються інакше.

--print-types

Друкує кожен модуль пакета (у порядку вхідних даних/цілей, бібліотечні модулі після них) як вихідний код Erlang (друк вихідного коду) з тим, що знайшло виведення типів. Вивід іде в stdout і призначений для читання людиною, це не Erlang і не формат обміну. Попередження залишаються в stderr.

%% module "branches" source="branches.erl" target="" declared=complete inferred=complete
-module(branches).
-export([mixed/1]).

%% inferred: mixed(1) -> 1; (_) -> 2
mixed(X) ->
    case X of
        1 ->
            1;
        _ ->
            2
    end. % $case_of_operator(X :: 1) -> 1; (X :: _) -> 2

• Рядок %% module називає модуль, його вихідний код, ціль проєкту та чи завершилися оголошені й виведені типи, чи їх було розширено через ліміт.
• Оголошення (-type, -spec, -callback, records) з'являються так, як написано.
• Над кожною функцією %% declared: f(Inputs) -> Result дає кожне перевантаження її -spec у розв'язаному вигляді (з обмеженнями when), а %% inferred: f(Inputs) -> Result — те, що знайшло виведення, тож їх можна порівняти. Вхідні дані — це домен успіху кожного аргументу (від term() для експортованих функцій і тих, які називає fun F/A, від об'єднаних аргументів викликачів для інших функцій). Функція з кількома функціональними типами друкує по одній сигнатурі на тип, кожну зі своїми вхідними даними: f(integer()) -> integer(); (atom()) -> string() (semantic::types::function_source). -spec залишається з функцією одразу після нього, відокремлений від інших форм порожнім рядком.
• Найзовнішніший вираз кожного рядка (вираз тіла або аналізований вираз case), чий факт каже більше, ніж term(), позначається завершальним коментарем % Type після пунктуації рядка (відомий тип приховує відношення з аргументом, яке показується лише для значення, про яке більше нічого не відомо): щонайбільше одна позначка на рядок, жодної для вкладених у нього виразів, тож вивід залишається коректним Erlang. Вираз тіла на кількох рядках несе свою позначку на останньому рядку (end, % ...). Літеральні терми (літерали, а також кортежі, списки, побудовані maps і bitstrings з літералів) не позначаються; зіставлення показує своє значення. Залежне значення друкується як функціональний тип своєї конструкції (залежні факти).
• Значення, про яке виведення довело, що воно дорівнює одному з аргументів функції, і про яке більше нічого не відомо, друкується як ім'я цього аргументу, змінна типу: змінна, яку дає йому перша клауза, що зв'язує весь аргумент, інакше _argumentN (з 1, також коли попередній аргумент узяв це ім'я). Вхідні дані аргументу показують те саме ім'я, коли це будь-який терм: second(_, Y) -> Y, keep(Acc, number()) -> Acc. Змінна показує лише свій тип, її ім'я вже каже, яким аргументом вона є.

Очікування виведення

tests/fixtures/inference/*.erl записують, що виведення має знайти для кожної функції і що воно знаходить сьогодні. Кожен модуль стає CTest inference_<module> (tests/compiler/inference/expectations.py):

%% expect: sum() -> 3
%% today: sum() -> _
sum() -> 1 + 2.

• expect: — це сигнатура, яку --print-types має надрукувати у своєму рядку %% inferred:; today:, присутній, поки виведення не дотягує, — та, яку він друкує зараз.
• Перевірка порівнює вивід із today, якщо він є, інакше з expect; кожна функція модуля потребує рядка expect. Рядок today, який виведення вже наздогнало, провалює перевірку, доки його не вилучено.
• expectations.py <clau> <fixture> --record переписує рядки today з поточного виводу (дія супровідника: перегляньте diff).
• values.erl покриває літеральні та побудовані значення, результати операторів і вбудованих функцій, контейнери та їхні частини, funs та їхні виклики, локальні вхідні дані від викликачів, об'єднання й діапазони цілих чисел, відношення з аргументами та значення try/maybe; narrowing.erl — перевірки типів, guards, зразки, діапазони порівнянь, диз'юнкції та звуження, які не повинні просочуватися; base_types.erl — по одній функції на кожен базовий і вбудований тип мови типів, чия -spec має розв'язатися і чиє тіло створює таке значення; clauses.erl — функціональні типи, вибір виклику й обчислення для кожного виклику в межах і за межами їхніх бюджетів; dependent.erl — залежні факти; trees.erl і parsers.erl — рекурсії по деревах і форми згенерованих парсерів; widening.erl — лічильники всередині контейнерів, які розширюються й усталюються.
• tests/fixtures/inference/contracts/ містить перевірки специфікацій (CTest inference_contracts).
• tests/fixtures/inference/budgets/walkers.erl — прохід компілятора у звичній для Erlang формі (великий record стану, що передається між взаємно рекурсивними функціями обходу, результати яких — об'єднання багатьох record). CTest inference_walkers (tests/compiler/inference/walkers.py) утримує кількість його проходів, кроків роботи, об'єднань ґратки та розв'язань, раундів і обходів членів групи функцій обходу в межах бюджетів приблизно на чверть вище за поточні показники, а також запускає програму.

Друк типів

semantic::types::type_source(graph, type) (semantic/types/printing) подає тип із графа типів у синтаксисі типів Erlang: _ для будь-якого терму (term(), записується через TERM_SOURCE для стислості; синтаксис типів читає _ як any()), none(), атоми й цілі числа, 1..5, {ok, T}, tuple(), [T], [T, ...], #{K => V, K := V}, #r{f :: T}, <<_:B, _:_*U>>, fun((A) -> R), A | B. Fun з кількома функціональними типами друкує їх у нотації Clause, fun((1) -> one; (_) -> other): синтаксис типів Erlang не має перевантаженого типу fun, а об'єднання типів fun означає інше. Цілі числа об'єднання друкуються в порядку значень там, де стоїть його перше ціле число, послідовні — як діапазон (1 | 2 | 3 | 5 друкується як 1..3 | 5; факт зберігає одиничні значення). Попередньо визначені типи erlang втрачають свій модуль; посилання на оголошені типи залишаються іменованими. Бюджет вузлів обмежує текст; понад нього, а також глибше за 32 рівні вкладеності, замість тексту стоїть ....

clau --print-types answer.erl client.erl
clau --print-types --project project.toml --target demo --verbose