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

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

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

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

Зв'язування

Кожне зв'язування має ідентичність відносно функції 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 (див. зразки).
• Аналізований вираз (scrutinee) case зв'язує в охопній області видимості. Кожна клауза починається з цієї області; визначення її зразка попередні до guard, який лише читає. Імена, зв'язані кожною клаузою, експортуються з однією ідентичністю (пізніші клаузи повторно використовують ідентичність, яку імені дала раніша клауза); імена, зв'язані лише деякими клаузами або небезпечні в будь-якій, після цього небезпечні. Експорти об'єднуються консервативно, як в OTP erl_lint (icrt_export); попередження OTP, коли пізніший зразок зіставляє експортоване ім'я, не видається. Клаузи if дотримуються тих самих правил з guard і без зразка.
• begin/end — це послідовність в охопній області видимості.
• Читання незв'язаних, небезпечних змінних і символу підстановки є помилками з місцем у коді. Повідомлення зберігають формулювання компілятора (unbound variable X, unsafe variable X); корпус зв'язувань перевіряє кожне з них на відповідність класу OTP unbound_var/unsafe_var.
• Comprehension обчислює кожен кваліфікатор по черзі в області видимості, залишеній попередніми. Зразки генераторів зв'язують нові імена, які затіняють зовнішні (читання всередині зразка надають перевагу іменам, які він уже зв'язав); група zip зв'язує всі свої зразки разом. Шаблони читають як сусідні вирази. Область видимості після comprehension — та сама, що й до нього: його імена там незв'язані.
• Кожна клауза анонімної fun починається з області видимості в місці fun: імена голови нові й затіняють зовнішні, guards читають їх, і ніщо, зв'язане всередині, не видно після fun. Кожне зовнішнє визначення, прочитане всередині, записується як захоплення (Function::captures, у порядку визначення). Ім'я іменованої fun — це ще одне визначення, з якого починається кожна клауза (Function::fun_names); воно ніколи не захоплюється. Змінні fun M:F/A є читаннями виразу fun (Function::fun_operands).

Обходи ітеративні з бюджетом модуля 1,000,000 одиниць роботи. Вичерпання або будь-яка семантична помилка очищає таблиці зв'язувань і нормалізації модуля.

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

Приватний граф типів представляє всі розібрані форми типів незалежно від розміщення в runtime: синглтони, діапазони, контейнери, ролі полів map, добутки функцій і нерозв'язані застосування. Об'єднання сплощуються та позбавляються дублікатів; term() — верхній елемент, none() — нижній. Типові значення: 16,384 вузли, 16 членів об'єднання, 100,000 елементів роботи на трансляцію. Вичерпання розширює до term() з видимим прапорцем і ніколи не звужує представлення.

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

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

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

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

• Експортовані вхідні дані та вхідні дані функцій, які називає fun F/A, є довільними термами. Функція, в яку входять лише прямі виклики з пакета (не експортована й не названа fun), бере як вхідні дані об'єднання фактів про аргументи з місць її виклику (step 58F, semantic/types/inference_inputs), зіставлених зі зразками голови кожної клаузи; рекурсивні виклики теж враховуються. Вхідні дані починаються з none() (функція, яку ніщо не викликає, ніколи не виконується й виводиться як none()) і зростають за проходами пакета: 8 проходів об'єднують, пізніші розширюють, як рекурсивні результати; вхідні дані, що не встановилися після 16 проходів, стають term() (з повідомленням про розширення).
• Літерали мають точні факти (step 58B): цілі числа будь-якого розміру та символи є синглтонами, атоми — синглтонними атомами, числа з рухомою комою — float(), рядки — непорожніми списками своїх символів ([] для ""), а -/+ від літерального числа зберігають його факт. Кортежі зберігають факти своїх елементів; maps, побудовані зі сталими ключами (факт одного значення: ціле число, атом, [] або кортеж чи map із таких), зберігають факт значення кожного ключа, ключ, заданий двічі, зберігає своє останнє значення, а будь-який інший ключ дає map(). Побудова bitstring підраховує свій розмір: літеральні, розмірні та UTF-кодовані літеральні символи — точно, UTF-сегмент іншого значення — за його кодуванням (UTF-8: від 8 до 32 бітів по байтах), а сегмент binary/bitstring — за фактом свого значення або будь-яким кратним свого unit (<<1, Rest/binary>> є nonempty_binary()). Операнд, який ніколи не дає значення (none()), робить побудову none().
• Оператори та вбудовані функції (step 58C, semantic/types/inference_operators) обчислюють свій результат із фактів своїх операндів. Цілочислові синглтони згортаються точно до 4,096 бітів на операнд і результат (включно з bignums; більший є integer()); інші цілі числа використовують інтервальну арифметику для +, -, * невід'ємних діапазонів, band з невід'ємним операндом (X band 15 є 0..15), rem на обмежений дільник (X rem 10 є -9..9), bnot, унарного - і abs/1; операнд із рухомою комою дає 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().
• Функції тотожності/проєкції зберігають точні відношення з аргументами, що поширюються через вкладені локальні та віддалені виклики зі свіжими змінними для кожного виклику.
• Контейнери (step 58D, semantic/types/inference_containers): список [E1, ..., En | T] об'єднує свої елементи перед фактом хвоста (правильний список, коли хвіст ним є, nonempty_improper_list(H, T), коли хвіст не список, term(), коли він невідомий); ++, --, hd/1, tl/1, element/2, setelement/3, tuple_to_list/1 і map_get/2 читають і перебудовують факти елементів член за членом об'єднання, причому член, що генерував би виняток, нічого не додає. Оновлення map зберігає точні ключі (:= для відсутнього ключа відкидає цей член) і дає map() для невідомого map. Records на кортежах є кортежами: побудова заповнює типові значення (undefined, якщо його немає), доступ і оновлення читають і встановлюють поле відповідних кортежів, а #r.f — це індекс поля. Спискова comprehension — це, можливо, порожній список фактів її шаблонів, binary comprehension — будь-яка кількість копій розміру її шаблону, map comprehension — map().
• Funs (step 58E, semantic/types/inference_funs): fun F/A — це fun своєї арності, що повертає виведений результат функції (вбудованої функції або, зі змінною арністю, fun()), fun M:F/A — fun, що повертає term(), а анонімна fun — fun, що повертає об'єднані результати своїх клауз, з урахуванням захоплених значень. Виклик значення об'єднує результати його funs цієї арності, які вибирають його аргументи (step 58L; term() для невідомої fun, none(), коли жоден член не можна так викликати). Анонімна fun, цілком зв'язана зі змінною й викликана через неї, обчислюється знову для цього виклику з її зразками, що зіставляються з фактами аргументів, щонайбільше на 4 таких виклики вглиб, а факти її першого обчислення потім відновлюються (Double = fun(Y) -> Y * 2 end, Double(3) є 6). apply/2,3 і динамічні виклики залишаються term(). Оскільки fun F/A може називати функцію, виведену пізніше, проходи по пакету також повторюються, доки кожна така fun не прочитає остаточний результат своєї функції; інакше останній прохід дає їм результати term().
• Присвоєння цілих значень у тілі та псевдоніми копіюють факт правої частини (Y = 42, Z = Y, id(Z) виводиться як 42); зразки кортежів, списків, maps і records на кортежах дають своїм змінним факти частин, з якими вони зіставляються, у зіставленнях у тілі, клаузах case (з аналізованого виразу), клаузах of у try (зі значення його тіла) та генераторах (з елементів їхніх вхідних даних або ключів і значень map). Недоведені значення залишаються term() без відношень.
• Звуження (narrowing) (step 58G, semantic/types/inference_narrowing, inference_scopes, meet): усередині клаузи функції, case, receive чи fun кожен зразок перетинається зі значенням, яке він зіставляє (літерал, форма кортежу, списку, 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), а /=, =/= з константою зсувають рівну їй межу діапазону всередину (step 58H1). Значення, яке може бути числом із рухомою комою чи іншим термом, не звужується. Кон'юнкція застосовує кожну перевірку по черзі, диз'юнкція об'єднує те, що доводить кожна альтернатива, 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 факт змінної — це об'єднання її фактів у кінці кожної клаузи, що завершується (step 58H), тож case X of forever -> ...; N when is_integer(N), N >= 0 -> ... end залишає X як non_neg_integer() | forever.
• try і maybe (step 58J1): try — це об'єднання значень його клауз of (значення його тіла, якщо of немає) і значень його клауз catch; тіло after нічого не додає. Клаузи of починаються з фактів у кінці тіла й зіставляють його значення, як клаузи case (неможлива клауза нічого не додає); клаузи catch і тіло after починаються з фактів перед try, а зразок класу зіставляється з error | exit | throw. maybe — це об'єднання значення його тіла, значень його клауз else і, якщо else немає, значень, на яких можуть зазнати невдачі його зіставлення ?=: факт зіставлюваного значення без форми зразка, коли зразок зіставляє всю свою форму (нові змінні, використані один раз, літеральні атоми та цілі числа, [], кортежі з них), інакше весь факт. Кожен зразок ?= перетинається зі своїм значенням і публікує свої змінні для решти тіла; ?=, який ніколи не може зіставитися, зупиняє тіло. Клаузи else починаються з фактів перед maybe і зіставляють об'єднані невдалі значення, як клаузи case. Факти після try об'єднують факти в кінці його тіла (якщо of немає) і кожної клаузи, що завершується; після maybe — факти в кінці його тіла, кожної клаузи else, що завершується, і, якщо else немає, факти перед ним.
• Використання (step 58H, 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 (звужений факт простої змінної, інакше факт зразка); його домен успіху (step 58H) — це об'єднання за клаузами, що завершуються, його факту в місці їхнього звичайного повернення. --print-types показує домен успіху як вхідні дані (bounded(1..10) -> 1..10, inc(X) -> X + 1 як inc(number()) -> number()) або домен входу функції, яка ніколи не повертається. Виклик, що повертається, звужує свої аргументи-змінні до домену викликаної функції, окрім випадку всередині рекурсивної компоненти, яка ще розв'язується.
• Результати клауз об'єднуються консервативно: проєкція зберігається, лише якщо кожна клауза повертає той самий аргумент. case чи if об'єднує результати своїх клауз так само; зв'язування, визначене кількома його клаузами, залишається term().
• Типи функцій (step 58K, semantic/types/function_types): поряд з описаним вище підсумком-об'єднанням функція зберігає по одному типу функції на кожну можливу клаузу, як перевантаження -spec: факти аргументів після голови та guard (звужений факт простої змінної, інакше факт зразка) і результат клаузи (none() для клаузи, яка завжди генерує виняток; неможливі клаузи нічого не додають). Клауза, тіло якої закінчується case або if, розбивається на один тип функції на кожну можливу гілку, з фактами аргументів після зразка та guard цієї гілки та результатом гілки (один рівень: вкладений case далі не розбивається). Типи функцій із рівними вхідними даними зливаються (їхні результати об'єднуються); понад 8 останні зливаються в один з об'єднаними вхідними даними та результатами. Рекурсивні компоненти ітерують їх разом із результатами, на кожному раунді об'єднуючи (а потім розширюючи) результат кожного типу; компонента, яка не збігається, зберігає лише свої підсумки-об'єднання. Факт анонімної fun зберігає по одному типу функції на кожну можливу клаузу (її зразки та guard над будь-яким аргументом), fun F/A — типи функцій F/A; funs, що об'єднуються, зберігають свої типи функцій, лише коли вони рівні, інакше вони об'єднуються в одну fun з їхніми об'єднаними результатами та будь-якими вхідними даними (перетин із fun будь-яких вхідних даних, як робить використання F(A), їх зберігає). Спеціалізація, домени та перевірки специфікацій читають підсумок-об'єднання.
• Виклики вибирають типи функцій (step 58L): виклик функції з типами функцій читає по черзі кожен тип, з вхідними даними якого перетинається кожен факт аргументу, і зупиняється після точного (зразки з нових змінних, використаних один раз, літеральні атоми та цілі числа, [] і кортежі з них; без guard або лише true і перевірки типів простих змінних-аргументів; для гілки — аргумент як аналізований вираз case), вхідні дані якого містять аргументи: жодна пізніша клауза не може бути виконана. Його результат — це об'єднання результатів вибраних типів, причому результат, рівний аргументу, є фактом цього аргументу в межах результату типу; якщо нічого не вибрано, виклик стає none() (він може лише згенерувати function_clause). Невідомі аргументи вибирають кожен тип, тобто об'єднання; функція без типів функцій (бюджет, компонента, що не збіглася) використовує свій підсумок-об'єднання. Після повернення виклику його аргументи-змінні звужуються до домену успіху та до об'єднаних вхідних даних вибраних типів. Виклики значень fun вибирають типи функцій факту fun так само, а анонімна fun, обчислена знову для виклику (див. Funs), входить у свої клаузи, перевіряє guards і виходить із них, як case, тож клауза, з якою її аргументи не можуть зіставитися, нічого не додає (F = fun(1) -> one; (_) -> other end, F(2) є other). Рекурсивні компоненти збігаються за результатами та типами функцій.
• Виклики обчислюють свою викликану функцію знову (step 58M): коли факти аргументів виклику лежать у межах вхідних даних викликаної функції та вужчі хоча б в одному, тіло викликаної функції обчислюється знову з ними як вхідними даними, як зв'язана анонімна 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() (з повідомленням про розширення, як при вичерпанні бюджету), а фінальний раунд переобчислює факти виразів; факти виразів попередніх раундів відкидаються, тож залишаються лише факти з остаточних припущень.
• Спільний бюджет роботи обмежує виведення; вичерпання втрачає точність і повертається до узагальненого коду, ніколи не відхиляє програму.
• Специфікації, що суперечать виведенню, є помилками (step 58I, semantic/types/contracts). Оголошений тип стає фактами, які він містить (або більше): вбудовані типи — за іменем (byte() є 0..255, timeout() є non_neg_integer() | infinity, iodata() і iolist() — списки будь-якої форми), псевдоніми — за своїм визначенням, opaque- і nominal-типи — за своїм визначенням усередині свого модуля і як будь-який терм поза ним, віддалені типи — через пакет, змінні типів — через свої обмеження when (необмежена — будь-який терм), maps і records — за своєю категорією. Специфікація суперечить коду, коли її факти не мають жодного спільного значення з тим, що доводить виведення: виведеним результатом (якщо він не невідомий і не none(): функція, яка ніколи не повертається, підходить до будь-якого результату), доменом входу аргументу або фактами аргументів виклику щодо кожного перевантаження. none()/no_return() допускає лише функцію, яка ніколи не повертається. Помилка називає функцію, оголошений тип у записаному вигляді та виведений. Оскільки виведені факти можуть містити більше значень, ніж дає код, суперечністю є лише неперетинна пара: оголошений тип, вужчий за виведений, приймається. Специфікації -callback не перевіряються. Компілятор OTP не перевіряє специфікацій (відмінності).

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

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

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

Пониження (lowering) використовує ці факти. Згенерований IR ніколи не перетворює ціле число на вказівник у купу; кожен результат сервісу, що може зазнати збою, завантажується лише на шляху його успіху, а перевірки форми домінують над видобуванням. Політика спеціалізації: specialization.md.

--print-types

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

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

%% inferred: mixed(_) -> 1..2
mixed(X) ->
    case X of
        1 ->
            1;
        _ ->
            2
    end :: 1..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 залишається при функції одразу після нього, відокремлений від інших форм порожнім рядком.
• Вирази, факт яких каже більше, ніж term(), анотуються як Expression :: Type (відомий тип приховує відношення з аргументом, яке показується лише для значення, про яке нічого іншого не відомо): у дужках усередині інших виразів, без них для цілого виразу тіла. Літеральні терми (літерали, а також кортежі, списки, побудовані 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 охоплює літерали, арифметику та порівняння, виклики локальних та інших функцій, об'єднання цілих чисел і діапазони, цілі числа або числа з рухомою комою, списки, рядки, кортежі, maps з атомами та іншими ключами, funs, що повертаються та застосовуються, binaries, відношення з аргументами та значення try/maybe. Сьогодні виведення знаходить літеральні та побудовані значення, результати операторів і вбудованих функцій, контейнери та їхні частини, funs та їхні виклики, локальні вхідні дані від викликачів, об'єднання цілих чисел і відношення з аргументами, звуження за використаннями та домени успіху (141 зі 141 функції).
• narrowing.erl охоплює кожну перевірку типу, guards у case, аналізовані вирази з істинною перевіркою, andalso, фільтри comprehension, зразки кортежів/списків/maps, всеохопні клаузи, guards діапазонів, суперечності, диз'юнкції, клаузу після однієї перевірки типу, звуження після виклику, звуження, які не повинні просочуватися, і діапазони порівнянь: кожен оператор з будь-якого боку, дві змінні, =/= на межі та всередині неї, доповнення, guards у case та if, orelse, зворотний відлік із guard і операнди, які не повинні звужуватися (51 з 51).
• base_types.erl має по функції на кожен базовий і вбудований тип мови типів (pid(), reference(), bitstrings і binaries, діапазони, byte(), char(), non_neg_integer(), boolean(), string(), iolist(), mfa(), timeout(), no_return(), ...): її -spec називає тип, тож кожен вбудований тип перевіряється на розв'язуваність, а її тіло дає таке значення. Категорії очікуються під своїми вбудованими іменами, обмежені множини цілих чисел — як діапазони. Кожна функція досягає свого очікуваного типу.
• clauses.erl охоплює типи функцій (step 58K): перевірки типів і літеральні зразки в кожній клаузі, злиті рівні вхідні дані, клаузу, в яку викликачі ніколи не входять, більше клауз, ніж дозволяє бюджет, рекурсивну функцію, одну клаузу, case та if, що завершують тіло, вкладений case і case, що не є останнім, багатоклаузні анонімні funs, fun F/A, об'єднання рівних і різних funs, і клаузу, яка завжди генерує виняток; а також вибір під час виклику (step 58L): перевірку типу, першу точну гілку, невідомі аргументи, відсутність допустимого типу, звуження після виклику, літеральний аргумент, діапазон через дві клаузи, вкладені виклики, локальну функцію з кількома викликачами, рекурсивну викликану функцію та багатоклаузні funs — зв'язані, у кортежі, передані локальній функції та викликані з невідомим аргументом; і обчислення для кожного виклику (step 58M): результати для кожного виклику, вкладеність до бюджету глибини й понад нього, викликану функцію понад бюджет розміру, рекурсивну викликану функцію та невідомі аргументи.

Друк типів

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