Тип подпись комбинатора не соответствует сигнатуру его эквивалентной функции лямбда

Question

Рассмотрим комбинатор:

S (S K) 

применить его к аргументам XY:

S (S K) X Y 

Он стягивается:

X Y 

Я преобразовал S (SK) в соответствующие лямбда-термины и получил этот результат:

(\x y -> x y) 

Я использовал инструмент Haskell WinGHCi, чтобы получить тип подписи (\ х у -> х у) и он вернулся:

(t1 -> t) -> t1 -> t 

Это имеет смысл для меня.

Далее я использовал WinGHCi, чтобы получить тип подписи с (s к) и он вернулся:

((t -> t1) -> t) -> (t -> t1) -> t 

Это не имеет смысла для меня. Почему разные типы подписей?

Примечание: я определил с, к, и я, как:

s = (\f g x -> f x (g x)) 
k = (\a x -> a) 
i = (\f -> f) 

Answer 1

Спасибо всем, кто ответил на мой вопрос. Я изучил ваши ответы. Чтобы быть уверенным, что я понимаю, что я узнал, я написал свой собственный ответ на мой вопрос. Если мой ответ неправильный, пожалуйста, дайте мне знать.

Мы начнем с типами k и s: первая работа

k :: t1 -> t2 -> t1 
    k = (\a x -> a) 

    s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
    s = (\f g x -> f x (g x)) 

Давайте на определивших тип подписи (s k).

Напомним s 's определение:

s = (\f g x -> f x (g x)) 

Подставив k для f результатов в (\f g x -> f x (g x)) контрактов на:

(\g x -> k x (g x)) 

Важно тип г и х должны быть согласованы с k-х типа.

Напомним, что k имеет этот тип подписи:

k :: t1 -> t2 -> t1 

Таким образом, для этой функции определения k x (g x) мы можем сделать вывод:

• Тип x тип первого аргумента k «s , который является типом t1.

• Тип k «ы второго аргумента t2, поэтому результат должен быть (g x)t2.

• g имеет x, поскольку его аргумент, который мы уже определили, имеет тип t1. Таким образом, подпись типа (g x) - (t1 -> t2).

• Тип результата k «ы является t1, поэтому результат (s k) является t1.

Таким образом, тип подписи (\g x -> k x (g x)) это:

(t1 -> t2) -> t1 -> t1 

Далее k определяется всегда возвращает свой первый аргумент.Так что это:

k x (g x) 

контракты на это:

x 

И это:

(\g x -> k x (g x)) 

контракты на это:

(\g x -> x) 

Хорошо, теперь мы выяснили (s k) :

s k :: (t1 -> t2) -> t1 -> t1 
    s k = (\g x -> x) 

Теперь давайте определим подпись типа s (s k).

Мы действуем аналогичным образом.

Напомним s 's определение:

s = (\f g x -> f x (g x)) 

Подставив (s k) для f результатов в (\f g x -> f x (g x)) контрактов на:

(\g x -> (s k) x (g x)) 

Важно Тип g и x должны соответствовать (s k)-х типа.

Напомним, что (s k) имеет этот тип подписи:

s k :: (t1 -> t2) -> t1 -> t1 

Таким образом, для этой функции определения (s k) x (g x) мы можем сделать вывод:

• Тип x тип первого аргумента (s k) «s , который является типом (t1 -> t2).

• Тип (s k) «ы второго аргумента t1, поэтому результат должен быть (g x)t1.

• g имеет x, поскольку его аргумент, который мы уже определили, имеет тип (t1 -> t2). Таким образом, подпись типа (g x) - ((t1 -> t2) -> t1).

• Тип результата (s k) «ы является t1, поэтому результат s (s k) является t1.

Таким образом, тип подписи (\g x -> (s k) x (g x)) это:

((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

Ранее мы определили, что s k имеет такое определение:

(\g x -> x) 

То есть, это функция, которая принимает два аргументы и возвращает вторую.

Таким образом, это:

(s k) x (g x) 

контракты на это:

(g x) 

И это:

(\g x -> (s k) x (g x)) 

контракты на это:

(\g x -> g x) 

Хорошо, теперь мы выяснили s (s k).

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 
    s (s k) = (\g x -> g x) 

Наконец, сравните тип подписи s (s k) с сигнатурой типа этой функции:

p = (\g x -> g x) 

Тип p является:

p :: (t1 -> t) -> t1 -> t 

p и s (s k) имеют такое же определение (\g x -> g x), так почему у них есть разные подписи?

Причина, по которой s (s k) имеет подпись другого типа, чем p, заключается в том, что нет ограничений на p. Мы видели, что s в (s k) ограничен согласованием с типом сигнатуры k, а первое s в s (s k) ограничено, чтобы соответствовать сигнатуре типа (s k). Таким образом, подпись типа s (s k) ограничена из-за его аргумента. Хотя p и s (s k) имеют то же определение, ограничения на g и x отличаются.

Answer 2

Мы начнем с типами k и s

k :: t1 -> t2 -> t1 
k = (\a x -> a) 

s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
s = (\f g x -> f x (g x)) 

Так проходит k в качестве первого аргумента s мы унифицировать тип k с первым аргументом s и использовать s по типу

s :: (t1 -> t2 -> t1) -> (t1 -> t2) -> t1 -> t1 

, следовательно, мы получаем

s k :: (t1 -> t2) -> t1 -> t1 
s k = (\g x -> k x (g x)) = (\g x -> x) 

Затем в s (s k), наружный s используется при типа (t3 = t1 -> t2, t4 = t5 = t1)

s :: ((t1 -> t2) -> t1 -> t1) -> ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

применения, что s k капель тип первого аргумента и оставляет нас с

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

В резюме: В Haskell тип s (s k) получен из типов его подчиненных подвыражений, а не от его влияния на его аргумент (ы). Поэтому он имеет менее общий тип, чем лямбда-выражение, которое обозначает эффект s (s k).

Answer 3

Система типа, которую вы используете, в основном такая же, как просто типизированное лямбда-исчисление (вы не используете никаких рекурсивных функций или рекурсивных типов). Простое типизированное лямбда-исчисление не является полностью общим; он не является Тьюрингом, и он не может использоваться для записи общей рекурсии.Исчисление комбинаторов SKI является завершением Turing и может использоваться для записи комбинаторов с фиксированной запятой и общей рекурсии; поэтому полная мощность вычисления комбинатора SKI не может быть выражена в просто типизированном лямбда-исчислении (хотя это может быть в нетипизированном лямбда-исчислении).