AH
я не спец, но вроде только Void ненаселён.
Size: a a a
2020 October 16
Oℕ
в смысле уже в дотти?
в смысле даже не в 3.0, а в 3.1
DR
типы, у которых есть инстансы
Int населен 1,2,3 и т.д.
В противовес им есть ненаселенные типы, например Nothing
В противовес им есть ненаселенные типы, например Nothing
λ
RAFIZ
что такое населённые типы?
Давай ты видео коновалова и пилмор посмотришь?
E
я не спец, но вроде только Void ненаселён.
Nothing
SS
Здравствуйте! Подогреваю интерес к HoTT. Есть ли в принципе риал лайф идеи применения высших индуктивных типов?
Oℕ
да придумать ненаселённый тип несложно
λ
RAFIZ
что такое населённые типы?
В той фразе важно было слово "конечно".
Oℕ
Serhiy Stas
Здравствуйте! Подогреваю интерес к HoTT. Есть ли в принципе риал лайф идеи применения высших индуктивных типов?
добрый день, для этого есть соответствующие чаты
Oℕ
Там уже у всех интерес подогрет
DR
добрый день, для этого есть соответствующие чаты
кста, если есть ссылка на чат по Хотту - было бы приятно
SS
Извините
Oℕ
кста, если есть ссылка на чат по Хотту - было бы приятно
такого чата нет, есть чаты завтипов, просто типов и аренда
E
я не спец, но вроде только Void ненаселён.
у войда (который в скале Unit) есть ровно один инстанс
AS
у войда (который в скале Unit) есть ровно один инстанс
Void это который в скале Nothing.
E
Void это который в скале Nothing.
AS
Речь не про жава войд.
E
я понял
λ
Void это который в скале Nothing.
Nothing, это который в скале None?
Oℕ
а про haskell.spring.utils.Void