Comments 5
Спасибо! А как лайк поставить несколько раз? :)
Если честно, уровень абстракции растёт очень быстро. Общая суть понятна, но детали без достаточного опыта работы с подобным лишь взрывают мозг.
Странно, что U с -1 начинаются, конечно, какой-то dreamberd.) Это из-за изначально неудачно подобранного соглашения?
И ещё интересно, но уже просто для улучшения понимания:
Возьмём такой псевдокод на C++:
template <template <class T1> class T>
struct S{};Это ведь S: (*–>*)–> * , верно? Ну, то есть "(*–>*)–> *" — это род S, да?
А если так, то для:
struct T{};
template <T t>
struct S{};Род S это T –> *, верно?
Ещё из вопросов: можно пример "родов родов" , ибо что-то принадлежащее, если я правильно понимаю, U_2 или выше не знаю как представить. Типа такого:
//Псевдокод
kind T<n: uint> = * -> (if n = 0 then * else T<n - 1>), где "суперрод" у T это uint -> хз, где хз это не-generic суперрод?
Тяжело такое представлять, как и задачи, где подобное можно применить практически.
Обзор предназначен не столько как учебное пособие, которое "нужно понимать с первого прочтения". Да и неточности есть... Основная задача - расширение кругозора читателя)) Делюсь тем, что показалось любопытным мне самому.
Изначально нумерацию вселенных придумали только для типов. Типы значений шли с индексом "0". А позднее, когда нумерация устоялась пришло понимание, что в эту иерархию стоит добавить и значения, пришлось согласиться на "-1".
На плюсах уже почти двадцать лет не писал. Подзабыл уже синтаксис... Загуглил "c++ hkt" и обнаружил, что плюсы тоже умеют в типы высокого рода. Вот какой-то пример, что-то похоже на то, что у вас.
В Scala нет поддержки "видов видов", но это есть, например, в Agda - если правильно понимаю, там можно писать код, полиморфный по вселенным типов. В разделе Вычисления на уровне типов демонстрируется, что типы связаны с видами типов также, как значения с типами - для них справедливы те же самые концепции, которые можно транслировать по индукции на более высокие вселенные. Например, концепция моноида, позволяющая из нескольких "чего-то" получить одно "что-то" полезна в вселенных любого индекса. Полиморфное по вселенным описание моноида позволило бы уменьшить ядро языка, упростить его, предоставив программистам меньшее количество, но более полезных инструментов.
Кроме того, знакомство с фундаментальными идеями позволяет легче воспринимать другие, основанные на них понятия. После такого знакомства мир уже никогда не станет таким как прежде)))
Обобщённые типы. Часть 1/3. Полиморфные типы высокого рода