Я пытаюсь понять, считать ли такой дизайн намеренным, или потому что так вышло? :)

https://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf - отправляю к основополагающим документам)

Андрей Бауэр как бы пытался что-то с этим сделать в недавней статье Runners in Action...

Вы конкретно про Haskell спрашиваете или про варианты вообще (в других языках)?

https://arxiv.org/pdf/1910.11629.pdf - не совсем понимаю, зачем это нужно, если есть системы эффектов

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

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

Это развитие/модификация алгебраических эффектов (если это та статья — ссылку не смотрел). Бауэра смущало, что в конечном итоге необработаные эффекты всплывают "вникуда" — в IO, по факту. Они смоделировали куда.

Pi-calculus? 😃

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

Applicative?

Это тоже алгебраическая модель, и ее семантика дана в лучшем случае бисимуляцией.

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

Мне неочевидно, как аппликативы применимы к моделированию нескольких временных линий.
Можно чуть подробнее? :)

Временных линий?

Ну, в них можно ветки параллельно запускать. А моделирование нескольких временных линий - это как?

Ну вот например, есть у нас процессор, и сетевая карта.

У них свои тактовые генераторы, они работают асинхронно. У них у каждого свое время, отсюда и "временные линии"

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

а для моей программы все это скрыто либо за select, который, по сути, опрашивает сокет, либо за epoll.

Теперь внимание, вопрос: как скомпилировать лямбда-исчисление, чтобы были задействованы обе временные линии?
Как мне написать код, который бы описывал tcp-протокол не двумя конечными автоматами с обеих сторон, а одним лямбда выражением?

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

Я попрошу! Не все.

А какие работают на принципиально другом?

Да тут вообще непонятно по какому принципу выбран подход, и объявлено, что все так делают

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