Функции лямбда-хаскеля - две, казалось бы, эквивалентные функции, одна работает, а другая ошибочна

Question

Эта лямбда-функция возвращает 1:

  (\x y -> 1) 1 p

, где p = (\ xy -> 1)

Хорошо, это имеет смысл для меня - лямбда-функция возвращает 1, независимоиз своих аргументов.

Теперь эта лямбда-функция генерирует ошибку (ошибка бесконечного типа):

  (\x y -> x y x) p 1

Это не имеет смысла для меня.Если эта функция применяется к аргументам, то здесь результат замены p на x и 1 на y:

  p 1 p

Заменить первое p на его определение:

  (\x y -> 1) 1 p

Эй!Это идентично приведенному выше, который возвращает 1.

Вопрос: почему (\ xy -> 1) 1 p успешно, тогда как (\ xy -> xyx) p 1 завершается неудачей?

/ Роджер

Answer 1

Возьмем это выражение (где оба p должны иметь один и тот же тип, потому что лямбда-переменная не может иметь два типа одновременно, если вы явно не указываете полиморфный тип):

p 1 p

Какой тип p в этом контексте? Допустим, 1 - это Int для простоты. Начнем с простой попытки:

(p :: Int -> ? -> Int) 1 p

Итак, что за знак вопроса? Ну, это должен быть тип p, потому что это аргумент, который вы приводите. Итак:

(p :: Int -> (Int -> ? -> Int) -> Int) 1 p

Опять та же проблема, то же решение:

(p :: Int -> (Int -> (Int -> ? -> Int) -> Int) -> Int) 1 p

Теперь вы понимаете, почему у нас проблема с бесконечными типами: хотя нам не нужно , чтобы узнать тип второго аргумента p; Поскольку система типов Haskell является строгой (иначе говоря, не ленивой), ей все равно нужно выяснить тип, и она застревает с этим бесконечным типом.

Этот код успешно выполняется:

(\x y -> 1) 1 p

... потому что функция слева может иметь тип , отличный от p, потому что это разные функции, поэтому мы не сталкиваемся с той же проблемой при объединении типов:

((\ x y -> 1) :: a -> b -> Int) 1 (p :: c -> d -> Int)

Answer 2

В дополнение к тому, что сказал dflemstr, тип ламбы никогда не будет зависеть от значений, к которым он применяется. Средство проверки типов сначала находит тип лямбды, а затем проверяет, правильно ли он применяется.

Следовательно, ваше утверждение о том, что после бета-замены выражения будут одинаковыми, не имеет значения: лямбда, тем не менее, должна быть хорошо напечатана.