Тип "succ (zero)" отличается от типа "one" в GHC

Question

Попросив GHC напечатать тип "one" и "succ zero" (способ кодирования чисел лямбда-исчисления), я получаю два разных типа!Разве они не должны быть одинаковыми?Можете ли вы также показать мне, как получить его тип вручную?

zero = \ f x -> x
one = \ f x -> f x
succ = \ n f x -> f (n (f x))

:t one -- (t1 -> t2) -> t1 -> t2

:t succ zero -- ((t1 -> t1) -> t2) -> (t1 -> t1) -> t2

Answer 1

Итак, как было сказано в комментариях, правильное определение:

zero   f x = x
succ n f x = f (n f x)

"сделать еще один f после n применений f, начиная с x. "

Таким образом

one f x = succ zero f x = f (zero f x) = f x
two f x = succ one  f x = f (one  f x) = f (f x)

Изначально типы, которые являются производными, являются более общими,

zero     ::     t      -> t1 -> t1     -- most general
one      :: (t1 -> t ) -> t1 -> t      -- less general
succ one :: (t2 -> t2) -> t2 -> t2     -- most specific

, но это не такнезависимо от того, что все они совпадают (объединяются) между собой, и начиная с two = succ one тип устанавливается в наиболее конкретный (b -> b) -> (b -> b).

. Вы также можете определить

church :: Int -> (b -> b) -> b -> b           -- is derived so by GHCi
church n f x = foldr ($) x (replicate n f)
             = foldr (.) id (replicate n f) x
{- church n  = foldr (.) id . replicate n     -- (^ n) for functions -}

и иметьвсе типы должны быть точно такими же, как

church 0 :: (b -> b) -> b -> b
church 1 :: (b -> b) -> b -> b
church 2 :: (b -> b) -> b -> b

Это действительно не имеет значения.

Что касается производных типов, то все сводится к использованию правила modus ponens / application,

       f   :: a -> b
         x :: a
       -------------
       f x ::      b

Просто нужно быть осторожным, переименовывая каждый тип последовательно, чтобы на любом шаге не вводился захват переменной типа:

      succ n f x = f (n f x)
               x          ::      a
             f            :: t                              ,  t ~ ...
                      n   :: t -> a -> b
                   f      ::           b ->            c    ,  t ~ b -> c
      succ    n                       f           x :: c
      succ :: (t        -> a -> b) -> (b -> c) -> a -> c
           :: ((b -> c) -> a -> b) -> (b -> c) -> a -> c

(поскольку конечный тип результата, создаваемый succ, одинаковв качестве конечного типа результата, полученного с помощью f - то есть c), или, как выражается в GHCi,

      succ :: ((t1 -> t) -> t2 -> t1) -> (t1 -> t) -> t2 -> t
           --   b     c     a     b       b     c     a     c

Answer 2

Во-первых, вы хотите, чтобы zero был того же типа, что и one.В вашем уравнении для zero вы не используете f при rhs ->.Таким образом, компилятор не знает, какой тип выводить.В вашем уравнении для one вы хотите, чтобы f x (его результат) был того же типа, что и x (результат из zero).Но вы тоже этого не получите.Проще всего давать подписи, но при этом не использовать asTypeOf.

В уравнении для succ вы хотите, чтобы его результат был того же типа, что и f x, того же типа, что и x.

Не могли бы вы также показать мне, как получить его тип вручную?

Хорошо, давайте добьемся выше, используя asTypeOf.Затем вы можете использовать :t, чтобы найти типы ...

zero = \   f x -> (x `asTypeOf` f x)
one  = \   f x -> (f x `asTypeOf` x)
succ = \ n f x -> (f (n f x)
                 `asTypeOf` f x `asTypeOf` x)

(я использовал правильное определение для succ, для @LambdaFairy.)

Обратите внимание, что церковьцифры в рамке нетипизированного лямбда-исчисления - это то, что показывает Википедия.По мере того, как вы входите в более экзотические функции над ними (например, добавление или предшественник), вы обнаружите, что Haskell является типизированным лямбда-исчислением, и GHC прекратит / вы попадете под страшное ограничение мономорфизма.Тогда asTypeOf не может вам помочь;Вы должны прибегнуть к типу подписей (более высокого ранга).