Есть ли в Haskell какие-либо действительные определения этого лямбда-оператора?

Question

У меня есть следующее определение для функции в Haskell.

> q7 :: forall a. forall b. ((a -> b) -> a) -> a

Мне предлагается либо создать для него определение, либо указать, почему определение не существует. Вот мои мысли:

q7 принимает любые типы для a и b. Оператор (a -> b) -> a будет реализован, если взять два элемента и вернуть последний. Теперь, если я пойду на один уровень дальше, я могу просто вернуть тот же самый "a", чтобы выполнить ((a -> b) -> a) -> a. Я вижу проблему в том, что a и b могут быть любого типа, поэтому для каждого экземпляра a может ли a быть другого типа? Например, может ли это быть что-то вроде ((Int -> Bool) -> [Char]) -> Int? Я, наверное, убил этот синтаксис. Если у кого-то есть какие-либо намеки или кто-то может подтвердить или опровергнуть мои идеи, я был бы очень признателен!

Answer 1

Оператор (a -> b) -> a будет реализован, если взять два элемента и вернуть последний.

Вы путаете это с a -> b -> a (что также может быть написано a -> (b -> a). Это не то же самое.

(a -> b) -> a - это функция, которая принимает один аргумент и возвращает значение типа a. Аргумент имеет тип a -> b, что означает, что это функция, которая принимает значение типа a и возвращает значение типа b. Это мало чем отличается от (например) функции filter:

filter :: (a -> Bool) -> [a] -> [a]

Он принимает два аргумента: функцию предиката типа a -> Bool и список типа [a] и возвращает новое отфильтрованное значение [a], передавая каждый элемент списка предикату.

---

Я вижу проблему в том, что a и b могут быть любого типа, поэтому для каждого экземпляра a может быть другой тип?

Нет, если бы он мог иметь другое имя. a может быть любым типом, но как только вы выберете тип для a, каждый a в сигнатуре этого типа будет означать этот тип. b - это другая буква, поэтому она может отличаться от a.

---

Итак, для вашей сигнатуры типа ((a -> b) -> a) -> a вы должны написать функцию, которая принимает один аргумент (другую функцию) и возвращает a. Функция аргумента имеет тип (a -> b) -> a, что означает, что она принимает функцию типа a -> b в качестве аргумента и возвращает a.

func :: ((a -> b) -> a) -> a
func f = ...

Аргумент f, в случае его вызова, вернет a, который вы затем сможете вернуть из func:

func :: ((a -> b) -> a) -> a
func f = f x
  where x :: a -> b
        x = ...

Однако для вызова f вам нужно передать ему функцию a -> b для всех типов a и b. Поскольку у вас нет такой функции, и вообще нет возможности написать такую ​​функцию, я думаю, что это невозможно реализовать.

Answer 2

Предположим, у вас есть функция

pierce :: ((a -> b) -> a) -> a

Импорт

data Void

из Data.Void.

Теперь мы можем играть в игры.Мы можем создавать экземпляры a и b в типе pierce для того, что нам нравится.Давайте определим

type A p = Either p (p -> Void)

и создадим экземпляр с помощью

a ~ A p
b ~ Void

Итак

pierce :: ((A p -> Void) -> A p) -> A p

Давайте напишем помощника:

noNegate :: forall p r. (A p -> Void) -> r
noNegate apv = absurd (n m)
  where
    m :: p -> Void
    m = apv . Left

    n :: (p -> Void) -> Void
    n = apv . Right

Теперь мы можемпойти на убийство:

lem :: Either p (p -> Void)
lem = pierce noNegate

Если бы существовала эта функция, это было бы очень странно.

lem @Void = Right id
lem @() = Left ()
lem @Int = Left ... -- some integer, somehow

Поведение этой функции кажется таким странным, потому что оно нарушает параметричность, которую использует функции Haskell.не может сделать, но все только ухудшается.

Возможно (но немного раздражает) кодировать произвольную машину Тьюринга как тип Haskell.И можно спроектировать тип, представляющий доказательство того, что конкретная машина Тьюринга остановится (в основном трассировка выполнения с индексированием типа).Применение lem к такому типу трассировки решило бы проблему остановки.

---

Благодаря лени Хаскелла некоторые «невозможные» функции оказываются полезными, хотя и частичными.Например,

fix :: (a -> a) -> a

формально абсурден, поскольку fix id утверждает, что дает вам все, что вы хотите.pierce не такая функция.Давайте попробуем написать это:

pierce :: ((a -> b) -> a) -> a
pierce f = _

Что должно идти с правой стороны? только способ сделать a - применить f.

pierce f = f _

Теперь мы должны предоставить что-то типа a -> b.У нас его нет.Мы не знаем, что такое b , поэтому мы не можем использовать обычную хитрость, начиная с какого-нибудь конструктора b, чтобы получить удар.Ничто не может улучшить нашу b.Поэтому самое лучшее, что мы можем сделать, это

pierce f = f (const undefined)

, который не выглядит отдаленно полезным.

Answer 3

Это невозможно, за исключением случаев использования бесконечной рекурсии или ошибок во время выполнения, поэтому невозможно завершиться.

Мы можем доказать, что это действительно невозможно, используя некоторые результаты теоретической информатики. Я не знаю, есть ли более простой способ показать, что это действительно невозможно.

Если бы был способ написать завершающую программу с этим типом, с помощью соответствия Карри-Ховарда , мы получили бы, что логическая формула ((a -> b) -> a) -> a (здесь, читаемая -> как) подразумевает ") является теоремой пропозициональной интуиционистской логики.

Такая формула известна как Закон Пирса и является одним из ключевых примеров формулы, которая НЕ доказуема в интуиционистской логике (напротив, она является теоремой в классической логика).

В качестве достаточно простого способа доказать, что закон Пирса не является интуиционистской теоремой, можно запустить процедуру принятия решения для логической логики высказываний и заметить, что она выводит «не теорему». В качестве такой процедуры мы могли бы выполнить поиск доказательства без вырезов в исчислении секвенций Жжена Гензена: таким образом, нам нужно только проверить конечное (и небольшое) количество возможных доказательств и наблюдать, что каждая попытка не удалась.