Oℕ
А теоркат про монады
Size: a a a
2020 May 23
DF
Можно через линтипы описать shared_ptr владеющий?
Oℕ
Dollar Føølish
Можно через линтипы описать shared_ptr владеющий?
Да
DF
Отлично
DF
Теперь мы нашли ответ
Oℕ
Ну как, через линтипы можно описать и обычные интуиционистские типы
DF
Будет страшно?
Oℕ
Ну страшнее, чем если иметь нужные типы сразу
SK
модульность в смысле хьюзность а не макквинность
@kremovtort почему это не в канале имени клапауция
λ
@kremovtort почему это не в канале имени клапауция
Что?
R
какие, интересно?
не смог найти. Будем считать, что это замечание снимается
Oℕ
Что?
Что
Oℕ
Прям слышу, как клайрат праздновать пошёл. Минус одно замечание от Романа
R
какие, интересно?
а в идрисе можно создать список типов, которые лежат в разных вселенных? То есть например
HCons Nat (HCons Type HNil) для некоторых HCons и HNil?Oℕ
Что значит в разных? Всегда есть вселенная, в которой они все лежат
R
Что значит в разных? Всегда есть вселенная, в которой они все лежат
пардон, агдина терминология. Там они лежат в разных из-за отсутствия кумулятивности. То есть в идрисе они норм даже в самый обычный список влезут?
Oℕ
пардон, агдина терминология. Там они лежат в разных из-за отсутствия кумулятивности. То есть в идрисе они норм даже в самый обычный список влезут?
Да
R
ок, спасибо. Что-то там такое было, что вселенные не могут зависеть от значений и это почему-то важно
AA
Dollar Føølish
Как по ученому называется RAII?
стек дисциплин, алгол
DF
А как это подгуглить? Discipline stack?