Можно ли использовать церковные кодировки, не нарушая уравновешенные рассуждения?
Имейте в виду эту программу:
{-# 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 -> foldr cons nil list
sum :: (Num a) => [a] -> a
-- sum = sum_ . toList -- does not work
sum = \ a -> sum_ (toList a) -- works
main = print (sum [1,2,3])
Оба определения суммы идентичны с точностью до эквалайзера. Тем не менее, компилируем второе определение работ, но первое нет, с этой ошибкой:
tmpdel.hs:17:14:
Couldn't match type ‘(a -> t0 -> t0) -> t0 -> t0’
with ‘forall t. (a -> t -> t) -> t -> t’
Expected type: [a] -> List a
Actual type: [a] -> (a -> t0 -> t0) -> t0 -> t0
Relevant bindings include sum :: [a] -> a (bound at tmpdel.hs:17:1)
In the second argument of ‘(.)’, namely ‘toList’
In the expression: sum_ . toList
Кажется, чтоRankNTypes
нарушает уравновешенные рассуждения. Есть ли способ иметь церковные списки в Хаскеле, не нарушая его ??