Anonymous
В ТЕОРИИ все работает )))
Ayrat
В ТЕОРИИ все работает )))
До встречи с сабтайпингом
Ayrat
Юнион типы должны их поддерживать! string|int должен быть подтипом string|int|guid!
Ayrat
Что не правда для ДУ
Vasily
Совсем неправда
Anonymous
Юнион типы должны их поддерживать! string|int должен быть подтипом string|int|guid!
а можешь показать как это из определений следует? по момему определению это неверно
Vasily
Но тех, кто выбрался из башни из слоновой кости, это почему-то не останавливает
Ayrat
а можешь показать как это из определений следует? по момему определению это неверно
Из определения вхождения множеств. В общем все операции над множествами и их теоремы можно переносить на юнион типы
Ayrat
На ДУ тоже можно, но там своя специфика с disjoint сетами
Anonymous
т.е. по-твоему string | int это подмножество string | int | любой другой тип?
Vasily
Экзактли
Ayrat
Это же даже очевидно слегка
Anonymous
а, ну так. то определение, которые я выше дал, этому не удовлетворяет, поэтому мы и не понимаем друг друга. или я чего-то не понимаю в том определении, которое сам написал.
Ayrat
Любое значение string|int является значением типа string|int|любой тип
Vasily
В теории, можно обобщить на размеченные
Vasily
Если добавить соответствие имени
Ayrat
Если добавить соответствие имени
Ну в общем да. В матане там у дисжоинт сетов просто пара - (тип, тег) вместо просто типа для идентификации сета
Anonymous
Любое значение string|int является значением типа string|int|любой тип
A | B | C = { (1, A), (2, B), (3, C) }. A | B = { (1, A), (2, B) }. не вижу противоречий. оба множества получены по тому определению что я выше написал, только маркеры выбираются детерменированно.
Vladislav
слишком сложно у вас тут для конца недели
Anonymous
явно видно что A | B \in A | B | C
Ayrat
И сразу все по пизде идёт
Vasily
Подтасовка фактов
Vasily
Подгон под теорию
Vasily
Короче, товарищ хочет быть прав
Anonymous
Тут ты маркеры сам расставил. Представь что там гуиды ацко уникальные
это уже деталь реализации! кто мне запретит сказать что существует f: множество_всех_возможных_du -> Nat например?
Vasily
Но не хочет признавать проебы
Anonymous
Но не хочет признавать проебы
я понимаю что на практике это может быть сложно, но мне было интересно где в теории проеб. его там нет.
Vasily
Чувак, тут практики
Anonymous
выше я показал, что вопрос "assum f such that .. is injective`. и все.
Ayrat
это уже деталь реализации! кто мне запретит сказать что существует f: множество_всех_возможных_du -> Nat например?
Ну если ты схолпнешь все теги в ноль, ты можешь типа получить из дисжоинт сетов юнионы, но только на бумаге)
Vasily
За теорией тебе в скала чат
Anonymous
Чувак, тут практики
чувак, там выше я Айрата спросил ГДЕ В ТЕОРИИ пойдет по пизде?
Vasily
Короче, хочется оказаться правым, аж зудит
Ayrat
Короче, давайте уточним. В фшарпе реализованы DU.
Ayrat
Юнионов нет
Anonymous
не, просто не хочется теорию и практику путать, это так себе на самом деле.
Vasily
За недорого могу провести сеанс психотерапии
Ayrat
В ТС насколько я знаю наоборот
Vladislav
Юнионов нет
Можно на структурах
Anonymous
но я вас понял, с точки зрения практики это СлОжНа рЕаЛиЗоВаТь
Ayrat
В скала 2 через сраку (силед трейт + кейс классы) можно ДУ, юнионы хз. В скала 3 есть и то, и другое
Vasily
В дотнете нереально
Vasily
Из- за нестираемых типов
Vladislav
В дотнете нереально
https://github.com/dotnet/csharplang/issues/1554#issuecomment-391140809
Ayrat
https://github.com/dotnet/csharplang/issues/1554#issuecomment-391140809
Это поди про сишные юнионы
Vladislav
Да
Vladislav
А есть другие?
Vasily
Ну вообще да
Ayrat
Ну да, открыл, увидел лейауты в структурах
Vasily
Сишные юнионы
Vasily
Они про размещение в памяти
Vasily
И в сишарпе они отлично делались на атрибутах
Ayrat
John A De Goes on Twitter: "In Scala 3, type intersections & unions are associative, commutative, and have an identity: A & (B & C) =:= (A & B) & C A & B =:= B & A A & Any =:= A Any & A =:= A A | (B | C) =:= (A | B) | C… https://mobile.twitter.com/jdegoes/status/1245305980512067585
Ayrat
Вот так сишные юнионы не могут. Они просто для хранения даты
Ayrat
Ayrat
В самом твите получше!
Anonymous
так это ж обыкновенная теория множеств, не?
Ayrat
Из определения вхождения множеств. В общем все операции над множествами и их теоремы можно переносить на юнион типы
Anonymous
только Any смущает. Рассел же по-моему сто лет назад показал, что такого множества не существует.
Ayrat
Ты видел?)
Anonymous
я не смотрел, если честно. вчера завел себе твиттер только. но в CS там теория множеств во всю в ходу.
Anonymous
кастомные операторы никто не придумывает
Ayrat
Да не, я о том как ведут себя типы
Anonymous
но за A & Any = A его очень быстро бы забодали
Ayrat
То есть в скала 3, компилятор будет выкупать это всё в компайл тайме
Anonymous
мне кажется (не знаю точно), что Тайпскрипт как раз что-то такое и умеет.
Anonymous
но я могу быть очень не прав