AR
Как нагуглить?
Size: a a a
2021 April 13
AG
ну вообще как раз теории типов отвязаны от множеств
˸A
ютуб сразу в релейтед выводит - если открыть видео со скриншота
Вот первая лекция https://www.youtube.com/watch?v=VKQ8qvvrT4U
Вот первая лекция https://www.youtube.com/watch?v=VKQ8qvvrT4U
˸A
в теории - да.
а в реальности у нас в языках - обычные множества типов
а в реальности у нас в языках - обычные множества типов
AG
мне кажется уже на полиморфных типах эта семантика начинает давать сбой
AG
не говоря про всякие индексированные дела
JS
только с самого начала пересечение не моделируется
JS
и объединение не везде и не так
˸A
опять же, если их теоретически из категорий строить - то да
а на практике в большинстве типизированных языков мы можем написать
а на практике в большинстве типизированных языков мы можем написать
A & B и A | B (я пишу на Тайпскрипт)JS
что входит в это большинство кроме Тайпскрипта?
JS
и как определён
Int & String?AG
по большому счёту кроме жвм-плеяды java-scala-ceylon - ничего :)
˸A
number & string = never
по сути, пустое множество значенийAG
типы пересечений со старта гробят разрешимость тайпчекинга
AG
поэтому их ставят туда где без сабтайпинга никак
JS
а как в Java пересекаются и объединяются типы?
˸A
ладно, не большинство языков, а большинство часто-используемых типизированных языков)))
AG
<T extends A & B>JS
это имеет смысл, если у них общий предок?