Ну а собственно свободная теорема - это та, которая следует исключительно из типа полиморфной функции:
Для любой f :: forall a . [a] -> [a] и любой g :: a -> b верно
map g . f = f . map g
Здесь = означает эквивалентность. При наличии в языке _|_ (жопа: ошибка или отсутствие останова) на g должно быть наложено требование строгости: g _|_ должно равняся _|_.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2007-12-07 11:27 pm (UTC)Для любой f :: forall a . [a] -> [a] и любой g :: a -> b верно
Здесь = означает эквивалентность. При наличии в языке _|_ (жопа: ошибка или отсутствие останова) на g должно быть наложено требование строгости: g _|_ должно равняся _|_.