Можно ли использовать церковные кодировки, не нарушая уравнивания?

Question

Имейте в виду эту программу:

{-# 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 нарушает уравновешенные рассуждения. Есть ли способ иметь церковные списки в Хаскеле, не нарушая его??

Answer 1

У меня сложилось впечатление, что GHC просачивает всех для всех как можно больше:

forall a t. [a] -> (a -> t -> t) -> t -> t)

а также

forall a. [a] -> forall t . (h -> t -> t) -> t -> t

может использоваться взаимозаменяемо, как засвидетельствовано:

toList' :: forall a t. [a] -> (a -> t -> t) -> t -> t
toList' = toList

toList :: [a] -> List a
toList = toList'

Что может объяснить, почему sumТип не может быть проверен. Вы можете избежать такого рода проблем, упаковав ваше полиморфное определение в newtype обертка, чтобы избежать такого подъема (этот абзац не появляется в более новых версиях документа, поэтому я использовал условное ранее).

{-# LANGUAGE RankNTypes #-}
import Prelude hiding (sum)

newtype List h = List { runList :: forall t . (h -> t -> t) -> t -> t }

sum_ :: (Num a) => List a -> a
sum_ xs = runList xs (+) 0

toList :: [a] -> List a
toList xs = List $ \ c n -> foldr c n xs

sum :: (Num a) => [a] -> a
sum = sum_ . toList

main = print (sum [1,2,3])

Answer 2

Вот несколько пугающий трюк, который вы можете попробовать. Везде, где у вас будет переменная типа ранга 2, используйте пустой тип; и везде, где вы выбрали бы экземпляр переменной типа, используйте unsafeCoerce, Использование пустого типа гарантирует (насколько это возможно), что вы не делаете ничего, что может наблюдать за тем, что должно быть ненаблюдаемым значением. Следовательно:

import Data.Void
import Unsafe.Coerce

type List a = (a -> Void -> Void) -> Void -> Void

toList :: [a] -> List a
toList xs = \cons nil -> foldr cons nil xs

sum_ :: Num a => List a -> a
sum_ xs = unsafeCoerce xs (+) 0

main :: IO ()
main = print (sum_ . toList $ [1,2,3])

Вы могли бы написать немного более безопасную версию unsafeCoerce, лайк:

instantiate :: List a -> (a -> r -> r) -> r -> r
instantiate = unsafeCoerce

затем sum_ xs = instantiate xs (+) 0 отлично работает как альтернативное определение, и вы не рискуете List a в нечто поистине произвольное.

Answer 3

Обычно эквациональное мышление имеет место только в "базовой системе F", которую представляет Хаскель. В этом случае, как уже отмечали другие, вас сбивают с толку, потому что Хаскелл движется foralls влево и автоматически применяет нужные типы в различных точках. Вы можете исправить это, предоставив подсказки о том, где приложение типа должно происходить через newtype оберток. Как вы видели, вы также можете манипулировать, когда приложение типа происходит путем расширения eta, поскольку правила типизации Хиндли-Милнера различны для let и для лямбды: foralls вводятся через правило "обобщение", по умолчанию, в lets (и другие, эквивалентные именованные привязки) в одиночку.