Ist es möglich, kirchliche Kodierungen zu verwenden, ohne die Argumentation der Gleichungen zu stören?

Dieses Programm bedenken: {-# LANGUAGE RankNTypes #-} import Prelude hiding (sum) type List h = forall t . (h -> t -> t) -> t -> t sum_ :: (Num a) => List a -> a sum_ = \ list -> list (+) 0 toList :: [a] -> List a toList = \ list cons nil -> ...