мне кажется (не знаю точно), что Тайпскрипт как раз что-то такое и умеет.

Насколько мне известно не до таких высот чтоб прям выкупать ассоциации и айдентити

только Any смущает. Рассел же по-моему сто лет назад показал, что такого множества не существует.

Так Any в данном случае - это скаловский надтип всего же. Логично, что для любого типа A & его же надтип == A

А он существует вообще? В смысле, можно убедительно это показать? Я в таких тонкостях уже не разбираюсь, но это уже совсем дебри теории.

В скале? Да, надтип всех - это как раз Any. Вот картинка из дотти на эту тему:

Вот тебе вопрос, которым когда-то Рассел опрокинул на лопатки все тогдашние представления об основах математики: является ли Any частью самого себя? Я не уверен, что это интересный спор, но мне кажется что такой вопрос обесценивает эту диаграмму. Но для практических целей картинка годная, да. Но там яростный спор про теорию был изначально, не практику.

Нет, ты не правильно понимаешь парадокс рассела

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

Any - это не нонсенс для систем типов с сабтайпингом, это то как они работают по определению. Каждый тип является подтипом самого себя

То есть в теории Any НЕ есть множество всех множеств?

Нет. Тут нет никаких множеств, тут речь про типы. Мы же говорим про теорию типов, а не множеств.

Так она разве не целиком и полностью на теории множеств стоит? Я не встречал ничего, кроме просто применения теории множеств к конкретной проблеме. Но я и не особо вчитывался, если честно.

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

Значит про это я просто ничего не знаю. Я встречал только другие формулировки именно теории множеств, где парадокс Рассела фиксился достаточно топорно - накладывались какие-то аксиоматические запреты на то, что { x | x \notin x } нельзя написать. И вуаля: нет человека - нет проблемы. Опять же, не углублялся.

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

Понял. Спасибо, познавательно. А откуда ты черпал об этом инфу? Помнишь ещё годные источники?

По теории типов применительно к ЯП, я читал "Types and programming languages", хорошая книжка, достаточно понятная. По теории типов в плане альтернативны для оснований математики, с ходу не вспомню все источники, как-то читал HoTT (Homotopy Type Theory), но достаточно мельком. Ну и там везде хардкор, нужна хорошая математическая грамотность и интуиция.

хардкорной литературы хватает, но она написана профессионалами для профессионалов, для аматеров вроде меня это недоступное чтиво: просто нет возможности потратить столько времени на это, пренебрегая всем остальным. но обычно хватает первую четверть/половину книги прочесть, а дальше уже идут доказательства и следствия второстепенных вещей или их связь с другими областями математики, которые можно и оставить непрочтенными, но при этом уловить суть. "Types and programming languages" звучит безопасно))))

да - без ToListAsync сработали - действительно поля в алфавитном порядке нужны.

называется знай свои костыли)

называется знай свои костыли)

пакеж потом код)

Второй признак алкоголизма пошёл.

А какой первый?

Грише сейчас тяжко

ХЗ чо будет, а лет уже немало

[+_,+_]

Ну так. Моё лицо, когда увидел код выше впервые.

Лол, я только что прочитал текст выше кода. Such low ceremony, such newcomer-friendly. Совсем уже от реальности оторвались.

и угарает там над зумерками

ну на самом деле скала - это пост-ирония в чистом виде. Одерски специально придумал язык, код на котором не компилируется в 99% случаев, а попытки задокументировать произвольный код приводят к грамматически корректному английскому языку с нулевой семантикой.

В той скале, на которой я писал, подобной фигни не было. Но это были тесты, там сложность уровня hell world, апи подёргать, режим запуска акторов описать.

внезапно, TF все-таки про тестируемость, лол