SB
но я могу быть очень не прав
Size: a a a
2020 May 15
AH
мне кажется (не знаю точно), что Тайпскрипт как раз что-то такое и умеет.
Насколько мне известно не до таких высот чтоб прям выкупать ассоциации и айдентити
SB
Насколько мне известно не до таких высот чтоб прям выкупать ассоциации и айдентити
Тоже не знаю. Но это круто, да.
DS
только Any смущает. Рассел же по-моему сто лет назад показал, что такого множества не существует.
Так Any в данном случае - это скаловский надтип всего же. Логично, что для любого типа A & его же надтип == A
SB
Так Any в данном случае - это скаловский надтип всего же. Логично, что для любого типа A & его же надтип == A
А он существует вообще? В смысле, можно убедительно это показать? Я в таких тонкостях уже не разбираюсь, но это уже совсем дебри теории.
DS
А он существует вообще? В смысле, можно убедительно это показать? Я в таких тонкостях уже не разбираюсь, но это уже совсем дебри теории.
В скале?
Да, надтип всех - это как раз Any. Вот картинка из дотти на эту тему:
Да, надтип всех - это как раз Any. Вот картинка из дотти на эту тему:
С
any это как обджект в джаве же
SB
Вот тебе вопрос, которым когда-то Рассел опрокинул на лопатки все тогдашние представления об основах математики: является ли Any частью самого себя? Я не уверен, что это интересный спор, но мне кажется что такой вопрос обесценивает эту диаграмму. Но для практических целей картинка годная, да. Но там яростный спор про теорию был изначально, не практику.
DS
Вот тебе вопрос, которым когда-то Рассел опрокинул на лопатки все тогдашние представления об основах математики: является ли Any частью самого себя? Я не уверен, что это интересный спор, но мне кажется что такой вопрос обесценивает эту диаграмму. Но для практических целей картинка годная, да. Но там яростный спор про теорию был изначально, не практику.
Нет, ты не правильно понимаешь парадокс рассела
DS
К Any и системом типов он не относится
SB
Нет, ты не правильно понимаешь парадокс рассела
Я не про сам парадокс, я про вопрос с которого началось. Мне кажется, что этот же вопрос станет отправной точкой в рассуждениях о том, что Any это нонсенс. Если хорошо в этом шаришь, то мне было бы интересно услышать развёрнутый ответ.
DS
Я не про сам парадокс, я про вопрос с которого началось. Мне кажется, что этот же вопрос станет отправной точкой в рассуждениях о том, что Any это нонсенс. Если хорошо в этом шаришь, то мне было бы интересно услышать развёрнутый ответ.
Any - это не нонсенс для систем типов с сабтайпингом, это то как они работают по определению. Каждый тип является подтипом самого себя
DS
Ну и ничто не мешает иметь тебе тип, который будет надтипом всех остальных.
SB
Any - это не нонсенс для систем типов с сабтайпингом, это то как они работают по определению. Каждый тип является подтипом самого себя
То есть в теории Any НЕ есть множество всех множеств?
SB
(которое не существует)
DS
То есть в теории Any НЕ есть множество всех множеств?
Нет. Тут нет никаких множеств, тут речь про типы. Мы же говорим про теорию типов, а не множеств.
DS
А во множествах проблема была в том, что в наивной теории множеств можно было определить множество через любой предикат
SB
Нет. Тут нет никаких множеств, тут речь про типы. Мы же говорим про теорию типов, а не множеств.
Так она разве не целиком и полностью на теории множеств стоит? Я не встречал ничего, кроме просто применения теории множеств к конкретной проблеме. Но я и не особо вчитывался, если честно.
DS
Так она разве не целиком и полностью на теории множеств стоит? Я не встречал ничего, кроме просто применения теории множеств к конкретной проблеме. Но я и не особо вчитывался, если честно.
Нет.
Теория типов - полностью независимая штука и была изначально придумана, как альтернатива теории множеств, чтобы уйти от парадоксов наивной теории множеств.
Теория типов - полностью независимая штука и была изначально придумана, как альтернатива теории множеств, чтобы уйти от парадоксов наивной теории множеств.
SB
Нет.
Теория типов - полностью независимая штука и была изначально придумана, как альтернатива теории множеств, чтобы уйти от парадоксов наивной теории множеств.
Теория типов - полностью независимая штука и была изначально придумана, как альтернатива теории множеств, чтобы уйти от парадоксов наивной теории множеств.
Значит про это я просто ничего не знаю. Я встречал только другие формулировки именно теории множеств, где парадокс Рассела фиксился достаточно топорно - накладывались какие-то аксиоматические запреты на то, что { x | x \notin x } нельзя написать. И вуаля: нет человека - нет проблемы. Опять же, не углублялся.