Programming Language Design

18 June 2026 12:35

Задача интенсиональной эквивалентности решается через введение нормальной формы.

Programming Language Design

18 June 2026 12:33

И когда белые ящики, тоже нерешаемая. )

Programming Language Design

18 June 2026 12:29

Если реализация поменялась, можно кинуть варн (даже на несходящиеся части внутри коллбека) и кинуть ошибку компиляции/впихнуть старую реализацию

Programming Language Design

25 February 2026 15:44

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

Programming Language Design

25 February 2026 15:38

понятия не имею. повторяю, это скопировано из https://raw.githubusercontent.com/marvinborner/optimal-effects/refs/heads/bachelor/thesis.pdf, страница 16

Programming Language Design

25 February 2026 15:36

из пдфки так скопировалось

Programming Language Design

25 February 2026 15:15

оно ведь соответствует ей, да?

Programming Language Design

25 February 2026 11:40

например, недавно вышел тезис Марвина Борнера про оптимальные эффекты через token-passing semantics. можно начать изучать этот тезис, который дает ссылки на другую литературу по эффектам в лямбда-исчислении.
https://raw.githubusercontent.com/marvinborner/optimal-effects/refs/heads/bachelor/thesis.pdf

Programming Language Design

25 February 2026 11:39

но ваше развитие как PLD дизайнера начинается не с изобретения велосипеда, а с исследования prior art.

Programming Language Design

25 February 2026 11:37

Скучно перекладывать жсоны на работе

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

Programming Language Design

25 February 2026 11:32

Господа!

В общем я тоже занимаюсь аутизмом в меру сил и делаю свой нескучный язык. Но я взял за основу уже существующий calculus (самое близкое это combinator calculus, но не оно)

Соответственно, у меня есть несколько правил редукции термов. Я захотелось мне сделать что-то похожее на ml, в том отношении, что мне не хочется полностью всё заворачивать в монады для io и мутабельности. Проблема тут в том, что в чистом исчислении такое не сделаешь без монад или их аналогов. Но! Я могу попробовать наворотить новых правил редукции. Я думал сделать прям отдельные правила, с отдельными "комбинаторами" типа seq или print и сделать их интринсиками. Мне не понравилось, по многим причинам, например потому что не скейлится. После обсуждений с чатомгпт пришли к такой схеме: оставить чистое исчисление, но кодировать специальные термы (он называл их request, но я предпочитаю opcode по аналогии с машинными инструкциями) структурно, а не номинально.

Пример: терм (который мы выбрали определенным образом, я написал рандомный) S K K I K S S это условно print, бинарный комбинатор и когда его встречает редусер, то он делает сайд-эффект. По такому принципу можно сделать и стейтменты, и io и даже мутации или лямбды (но там немного сложнее)

Вопрос: вы встречали языки которые так делают?

Programming Language Design

25 February 2026 11:22

Ну, а в чём вопрос то?

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

Например в языке есть нечто что я пока называю формами — то там идёт оперирование типизированными синтаксическими конструкциями — переписывание деревьев/термов короче

Programming Language Design

25 February 2026 10:52

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

let e1 := a * b;
let e2 := e1 * c;
let a * let b * let c := d;
let program := e2;

Programming Language Design

25 February 2026 10:48

ну как же? синтаксически конструкции b * c * d в программе не существует, но значение такое строится

Programming Language Design

25 February 2026 10:43

кстааати. а можно написать правило вида let a * (let b * let c) := ..., редуцирующее a * (b * c)?

Programming Language Design

18 June 2026 12:35

Но, проблема останова тоже нерешаемая... однако жеж живем и даже иногда работаем... )

Programming Language Design

18 June 2026 12:33

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

Programming Language Design

18 June 2026 12:28

Который указывает компилятору, как менять аст взятой функции

Programming Language Design

25 February 2026 15:42

короче, не помню. когда-то просто из принципа научился читать нотацию Лафонта, но потом забыл из-за ненадобности. в тезисе диаграммы есть, а если хочется умственного онанизма, можно почитать Цицерона в оригинале, и то интереснее будет.

Programming Language Design

25 February 2026 15:37

а чем отличаются скобки [] от скобок ()? этого тоже в Лафонтовской нотацией нет

Programming Language Design

25 February 2026 15:35

а что такое ∘? по-моему этого не было в Лафонтовской нотации

Programming Language Design

25 February 2026 15:14

потыкался в гпт с целью понять лафонтовскую нотацию 𝛿∘[𝑎(x1, … , x𝑛), 𝑎(y1, … , y𝑛)] ⋈ 𝑎[𝛿∘(x1, y1), … , 𝛿∘(x𝑛, y𝑛)], но это совершенно бестолковая затея, т.к. Т9 путается в показаниях и противоречит себе
может кто-то пояснить, как это правило соответствует этой диаграмме?

Programming Language Design

25 February 2026 11:39

Да, поэтому такой вопрос и возник, относительно возможностей такого кодирования эффектов (и не только) через термы

Programming Language Design

25 February 2026 11:38

Касаемо языка -- не хочется оставаться только с чистым исчислением, хочется сделать более императивный по форме язык, с сохранением функционального ядра. То есть я не против добавить seq mut и возможно ещё несколько стандартных императивных вещей, типа циклов

Programming Language Design

25 February 2026 11:36

какую бизнес-проблему вы решаете?

Programming Language Design

25 February 2026 11:23

вопрос: соответствует ли моё предположение реальности

Programming Language Design

25 February 2026 10:55

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

Programming Language Design

25 February 2026 10:50

Короче я не понял это сообщение.

Перефразируйте пожалуйста.

Programming Language Design

25 February 2026 10:47

Вот тут мне не понятно

Programming Language Design

25 February 2026 10:41

потому что теоретически если сделать { let a := b * c; a * d }, то синтаксически правило let b * let c * let d := .... не будет возможно редуцировать