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

Question

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

S (S K)

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

S (S K) X Y

Он заключает контракт на:

X Y

Я преобразовал S (SK) к соответствующим терминам Lambda и получили такой результат:

(\x y -> x y)

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

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

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

Затем я использовал WinGHCi для получения сигнатуры типа s (sk), и он вернул:

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

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

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

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))

Таким образом, передав 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 2

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

Answer 3

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

Мы начнем с типов 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 = (\f g x -> f x (g x))

Подстановка k для f приводит к (\f g x -> f x (g x)), заключающемуся в:

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

Важно Тип g и x должен соответствовать сигнатуре k.

Напомним, что k имеет сигнатуру этого типа:

   k :: t1 -> t2 -> t1

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

• Тип x - это тип первого аргумента k, который является типом 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 = (\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), который является типом (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 различаются.