AG
Size: a a a
2020 May 21
AG
Теперь осталось узнать что значит ресурс
то, что сложно найти, легко потерять и невозможно забыть
AG
например мутабельная память
KC
то, что сложно найти, легко потерять и невозможно забыть
Каждый раз когда алекс кидает что-то такое я хочу изучать идрис
KC
Но потом проходит через 5 минут
KC
Не знаю к счастью ли
AG
сепарирующая конъюнкция (звезда) сопряжена с сепарирующей импликацией (ванд)
curryW : All $ (p ^*^ q) ~* r :-> p ~* (q ~* r)
curryW wpq_r =
MkWand $ \sp1, pm =>
MkWand $ \sp2, qr =>
let (_ ** (sp3, sp4)) = splitAssoc sp1 sp2 in
app wpq_r sp3 (MkStar pm sp4 qr)
uncurryW : All $ p ~* (q ~* r) :-> (p ^*^ q) ~* r
uncurryW wpqr = MkWand $ \sp1, (MkStar pl sp2 qr) =>
let (_ ** (sp3, sp4)) = splitUnassoc sp1 sp2 in
app (app wpqr sp3 pl) sp4 qr
AG
типа если R для полного счастья не хватает P вместе с Q, то можно втыкать их по отдельности, и наоборот
AG
Теперь осталось узнать что значит ресурс
ну в алгебраических терминах это любой частичный коммутативный моноид
KC
Стало чуть проще
KC
Хотя бы слова знакомые пошли
Oℕ
Хотя бы слова знакомые пошли
какиие
AG
Reader
для ридера ванд и нужен:
Reader : Ctx -> Ctx -> Pred ST -> Pred ST
Reader g1 g2 p = Env g1 ~* Env g2 ^*^ p
KC
какиие
Большая их часть
AG
т.е. это просто линейный пожиратель линейных словарей линейных кложур :)
w
т.е. это просто линейный пожиратель линейных словарей линейных кложур :)
Есть и инхаус для широких задач, кликхаус например
AG
расскажи про ванд
узнали?