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

Обратите внимание на эту программу:

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

Ответы

Ответ 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, чтобы избежать такого hoisting (этот абзац не отображается в более новых версиях документа, поэтому мой используя условное ранее).

{-# 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])

Ответ 2

Вот несколько пугающий трюк, который вы могли бы попробовать. Всюду у вас будет переменная типа rank-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 в нечто TRULY произвольное.

Ответ 3

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