NI
На одном e строится _функтор_.
Который работает для любых a.
Который работает для любых a.
Size: a a a
2019 October 08
NI
Ну и аппликатив и монада, если далее.
NI
Ну тут же понятно, что в одном применении, Reader — это параметризированный тип, а в другом — конструктор.
ЕО
Тут дело не в количестве трафика скорее, а в его характере :)
NI
Ну я стараюсь быть поближе к категориям, а не к хаскелю ;-)
Но исходный вопрос, в общем-то, был про хаскель.
Но исходный вопрос, в общем-то, был про хаскель.
ЕО
Ну я стараюсь быть поближе к категориям, а не к хаскелю ;-)
Но исходный вопрос, в общем-то, был про хаскель.
Но исходный вопрос, в общем-то, был про хаскель.
Ну он скорее про категориальную семантику хаскеля
A
Ну тут же понятно, что в одном применении, Reader — это параметризированный тип, а в другом — конструктор.
не понял
A
нет, исходный вопрос был про категории, потому что я вообще пытался это дело написать на плюсах (в качестве упражнения)
NI
не понял
Так понятнее?
newtype Reader e a = ReaderConstr (e -> a)
instance Functor (Reader e) where
fmap f (ReaderConstr g) = ReaderConstr (\x -> f (g x))
newtype Reader e a = ReaderConstr (e -> a)
instance Functor (Reader e) where
fmap f (ReaderConstr g) = ReaderConstr (\x -> f (g x))
A
надо немножко побиться лбом об стену, может пойму
ЕО
Мне кажется, что если хочешь как-то запрограммировать понятия теорката, то лучше брать сразу агду и писать на ней
NI
Очень, очень страшная вещь!!
http://learnyouanagda.liamoc.net/toc.html
Оно неполное, но представление даст.
http://learnyouanagda.liamoc.net/toc.html
Оно неполное, но представление даст.
Oℕ
я могу сказать, что как-то теоркат можно и на аренде пописать
Oℕ
learnyouanarend ещё не завели
Oℕ
Но обязательн заведём
NR
Ну Statebox же сделали idris-ct, нормально всё выражается
A
я читал lyah где-то лет 6 назад, остановился на ... а, вот, записано, про random
Oℕ
Ну Statebox же сделали idris-ct, нормально всё выражается
не очень
NR
не очень
Можно подробнее?
Oℕ
Можно подробнее?
В формулировке категории используется встроенное равенство = индексированный индуктивный тип с одним конструктором, а не сетоид. Его замечательно использовать, однако построить его обычно сложно. Поэтому во всех нетривиальных случаях пишется вот это
https://github.com/statebox/idris-ct/blob/master/src/Basic/Functor.lidr#L165
https://github.com/statebox/idris-ct/blob/master/src/Basic/Functor.lidr#L165
