flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

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

Ожидание было такое: ActorRef[T] — это новая машинерия в системе типов, и делать её надо вместе с равенством над параметром типа, одной работой. Ожидание неверно. Параметрический тип в языке уже есть (flang/cat/POLY.md, фазы 1–5), и ссылки хватает его одного.

Устройство — три строки:

тип «Ссылка» от «Т»
  вариант «Ссылка на» содержит «имя»: строка, «принимает»: строка

тотальная функция «Послать» от «Т»
  принимает адресат: «Ссылка» от «Т», груз: «Т»
  возвращает «Действие»

«Т» — фантомный параметр: в значении его нет, он живёт только в объявлении. Имя внутри ссылки — обычная строка и вправе приехать с провода. Тип груза сверяется с «Т» обычным сопоставлением первого порядка, тем же, каким проверяется любой вызов полиморфной функции.

Чем подтверждено. Ветка u/ssylka, bootstrap/flang 0.5.1, три прогона на flang/conc/examples/:

  1. node-work-by-reference.flang — узел копит ссылки на тех, кто представился, и шлёт работу по имени из поля сообщения. flang check: 8 функций, все с доказанным завершением; flang test: примеров 5, прошло 5.
  2. node-work-by-reference-forged.flang — та же программа, груз чужого типа. FLANG_TYPE ... аргумент «груз» функции «Послать»: ожидался «Задание», получен «Строка журнала», код возврата 1.
  3. Тот же узел без ссылки, сырым `вариант «отправить» с «кому» равным вычисленное и «что» равным грузом чужого типа: замечаний ноль. То есть сегодня дыра открыта полностью, и ссылка её закрывает, а не приоткрывает.

Обе программы напечатаны в Elixir и ПРОГНАНЫ на BEAM — у этой цели планировщик есть (flang emit --target elixir, make build, запрос {"run":"…"}). Разница видна в одной строке итога:

со ссылкой:  "живые":["узел-7","Узел"]  "отказы":[]
             состояние «узел-7» → {"входы":["раз"]}
без ссылки:  "живые":["Узел"]           "отказы":[["узел-7","FLANG_MATCH_NOT_EXHAUSTIVE"]]
             состояние «узел-7» → {"входы":[]}

И там и там прогонщик отвечает "ok":true, исход обоих — "покой". То есть без ссылки работник умирает, работа теряется, а прогон это ЗАСЧИТЫВАЕТ. Это и есть цена, которую платят за снятие запрета без замены, — измеренная, а не рассуждённая.

Фантомный параметр разрешён, проверено отдельной программой: параметр, не встречающийся ни в одном варианте, принимается.

Чем ограничено — два места, где ссылка ещё не самодостаточна.

Этот предел снят 21 августа 2026, разбор — в a-computed-addressee-costs-one-named-failure. Ниже оставлен замер, которым он был предъявлен.

Динамическим остаётся ровно одно и по существу: имя с провода может назвать процесс другого вида. Замерено прогоном на BEAM: узел, которому с провода назвали «Журнал» (он принимает «Строка журнала»), чеканит «Ссылка» от «Задание», письмо доезжает, и «Журнал» умирает — "отказы":[["Журнал","FLANG_MATCH_NOT_EXHAUSTIVE"]] при "ok":true и исходе «покой». Ловится это одним сравнением строк, и сравнивать есть что: доставленная ссылка несёт "принимает":"Задание" прямо в значении, а у адресата в объявлении стоит «Строка журнала». Сличается это при доставке — планировщик уже ищет адресата по имени, и сравнить объявленный принимает адресата с полем принимает ссылки стоит одного сравнения строк. Отказ при этом ИМЕНОВАННЫЙ, а не падение получателя на неполном разборе. Так же устроен Akka Typed: тип ActorRef[T] статичен, а поиск по ServiceKey[T] проверяется при работе.

Связано: a-computed-addressee-costs-one-named-failure, an-addressee-must-be-a-literal-for-the-payload-type-not-for-the-scheduler, a-node-cannot-be-an-ordinary-program-because-of-the-literal-addressee, equality-on-a-type-parameter-is-banned-only-in-bodies, a-message-payload-travels-as-a-ticket-not-as-a-value