> Я совершенно не уверен, что могу делать допущение подобное a = pure a'
С точки зрения бананов и линз тип
pure :: (Functor f) => a -> f a
задаёт f-коалгебру (pure там - это psi в анаморфизме). Ну и для функторов есть изоморфизм между f a и a. Так что вроде можно, но я не настолько крут в бананах, чтобы поставить тут ЧТД :)
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
zaluzianskya and ![[community profile]](https://www.dreamwidth.org/img/silk/identity/community.png)
skylark_photos
no subject
Date: 2007-12-06 05:19 pm (UTC)С точки зрения бананов и линз тип
задаёт f-коалгебру (pure там - это psi в анаморфизме). Ну и для функторов есть изоморфизм между f a и a. Так что вроде можно, но я не настолько крут в бананах, чтобы поставить тут ЧТД :)