Проверка завершения в функциональных программах

Question

Существуют ли функциональные языки, которые могут указывать в контроллере типов, гарантированно ли завершаются определенные вычисления? В качестве альтернативы, вы можете сделать это только на Haskell?

Что касается Haskell, то в этом ответе плакат говорит, что

Обычный способ думать об этом состоит в том, что каждый тип Haskell "отменяется"- он содержит ⊥. То есть, Bool соответствует {⊥, True, False} а не просто {True, False}, Это говорит о том, что программы на Haskell не гарантированно завершаются и могут иметь исключения.

С другой стороны, эта статья об Агде утверждает, что

Правильная программа Agda - это программа, которая проходит и проверку типа, и проверку завершения

Т.е. все программы Agda будут прерваны, а Bool в Агде соответствует точно {True, False},

Так, например, в Haskell вы можете иметь значение типа IO a, который сообщает контролеру типов, что IO необходим для вычисления рассматриваемого значения. Не могли бы вы иметь тип Lifted a который утверждает, что рассматриваемое вычисление не может завершиться? То есть вы разрешаете не прекращение, но разделяете его в системе типов. (Очевидно, что, как в Agda, вы можете только разделить значения на "определенно завершается" и "может не заканчиваться"). Если нет, существуют ли языки, которые делают это?

Answer 1

Вы, конечно, могли бы. Однако это не было бы идеально. По определению, некоторые вычисления, которые завершаются, должны находиться в Lifted, Это называется проблемой остановки.

Теперь, прежде чем отказаться от этой идеи, это не так уж плохо на звуки. Coq, Agda и многие другие прекрасно работают с эвристикой для проверки завершения.

Языки, где это на самом деле имеет значение, такие, как Coq и Agda, где вы пытаетесь доказать теоремы. Например, скажем, у нас есть тип

 Definition falsy := exists n, n > 0 /\ 0 > n.
 -- Read this as, 
 --   "The type of a proof that for some number n, n > 0 and n < 0"

В синтаксисе Coq. /\ значит и. Теперь, чтобы доказать такое свойство в Coq или Agda, нам нужно написать что-то вроде

Definition out_proof : falsy = ____.
-- Read this as
--   "A proof that there exists a number n < 0 and n > 0"

куда ____ является доказательством того, что для некоторого числа n, n > 0 а также 0 > n, Теперь это ужасно сложно, так как falsy ложно Ясно, что не существует числа, которое было бы меньше или больше 0.

Тем не менее, если мы допустили неопределенность с неограниченной рекурсией,

 Definition bottom_proof : falsy = bottom_proof.

Этот тип проверяет, но явно противоречив! Мы только что доказали что-то ложное! Таким образом, помощники, доказывающие теорему, применяют некоторую форму проверки завершения, в противном случае они бесполезны.

Если вы хотите быть прагматичным, вы можете использовать этот поднятый тип, чтобы в основном сказать проверщику типов: "Отойди, я знаю, что это может не закончиться, но я в порядке с этим". Что полезно для написания реальных вещей, таких как, скажем, веб-сервер или что-то еще, где вы можете захотеть, чтобы он работал "навсегда".

По сути, вы предлагаете разделить язык, с одной стороны, у вас есть "проверенный код", о котором вы можете безопасно доказать, а с другой - "небезопасный код", который может зацикливаться вечно. Вы правы в сравнении с IO, Это точно та же идея, что и разделение побочных эффектов на Haskell.

Изменить: Corecursive данные

Вы упомянули основные данные, но это не совсем то, что вы хотите. Идея в том, что вы делаете цикл навсегда, но вы делаете это "продуктивно". В сущности, с помощью рекурсии самый простой метод проверки вашего завершения - это то, что вы всегда выполняете рекурсию со сроком, строго меньшим, чем у вас в настоящее время.

Fixpoint factorial n := match n with
  | 0 => 1
  | S n' => n * factorial n'

С corecursion ваш конечный термин должен быть "больше", чем ваш вклад.

Cofixpoint stream := Cons 1 stream

Опять же это не позволяет

 Cofixpoint stream := stream