а
Потому что массив2 — не потомок массив3
Size: a a a
2019 December 29
а
Автор так и сказал
А⚙
Нет, там где нужен массив с 3мя и более элементами ты не поставишь массив с 2мя элементами
Я тоже так подумал
λ
λ
Ну я дурак
λ
Я сначала прочитал неправильно, а потом по конструировании контрпримера вообще дерево перевернул
NV
Я тоже так подумал
Ну ты понял почему так?
NV
Subtyping always fails
Сабтайпинг это мощный и удобный механизм, который есть в практически любом языке
λ
Сабтайпинг это мощный и удобный механизм, который есть в практически любом языке
Не видел ни одного языка где в сабтайпинге действительно выражалось, что-то полезное, вроде отношения длин массивов
NV
Даже в этом случае. Если у тебя программа покрыта типами массивов с аннотацией размеров, сабтайпинг позволяет избежать лишних церемоний с кастами
DS
Не видел ни одного языка где в сабтайпинге действительно выражалось, что-то полезное, вроде отношения длин массивов
В расте сабтайпинг лайфтаймов
DS
Если их, конечно, считать честными типами
NV
В расте сабтайпинг лайфтаймов
В расте вариантность сабтайпов сделана не очень удобно, к сожалению, она выводится неявно из мест использования лайфтаймов. Но это полезно
DS
В расте вариантность сабтайпов сделана не очень удобно, к сожалению, она выводится неявно из мест использования лайфтаймов. Но это полезно
Я скорее как пример чего-то явно полезного, но при этом нестандартного
NV
Если их, конечно, считать честными типами
Ну лайфтайм может быть подмножеством другого лайфтайма, так что сабтайпинг там применим, и сам лайфтайм — это настоящий кайнд рядом с типами
λ
В расте сабтайпинг лайфтаймов
Это да, но это далеко от мейнстримного сабтайпига
DS
Это да, но это далеко от мейнстримного сабтайпига
Но это все равно отдельный кайнд от именно что типов языка
NV
Но это все равно отдельный кайнд от именно что типов языка
Да, но параметризованные лайфтаймами типы тоже подчиняются сабтайпингу
NV
Не видел ни одного языка где в сабтайпинге действительно выражалось, что-то полезное, вроде отношения длин массивов
В принципе нет ни одного мейнстримного языка, где выражаются длины массивов, увы
λ
В ссрефлекте в кок есть сигма, которая через коэрции пытается походить на сабтайпинг, но там все равно инвариант приведенный выше не выразим