Как восстановить выражение Haskell из типа

Я пишу программу, которая для данной сигнатуры типа реконструирует выражение Haskell этого типа, например.: for a -> b -> a возвращает \x -> \_ -> x. Я читал о теории этой проблемы, и я знаю, что существует этот изоморфизм Говарда-Карри. Я представляю, что моя программа анализирует входные данные и представляет их как термины. Тогда я бы уволил SLD-разрешение, которое скажет мне, можно ли построить термин данного типа (например, для Pierce это невозможно). Я еще не знаю, как на самом деле создать выражение Haskell во время этого разрешения. Я видел код djinn, но это немного сложно, и я хочу понять общее представление о том, как это работает.

Ответы

Ответ 1

Если вы используете Curry-Howard для подключения подмножества Haskell к некоторой интуиционистской логике, очень просто извлечь программу Haskell из доказательственного термина. По сути, условия доказательства должны уже иметь ту же структуру, что и программы Haskell, но просто используют разные имена конструкторов. Я думаю, что вы можете использовать один и тот же тип алгебраических данных для обоих терминов и терминов Haskell, если вы переводите имена конструкторов в голову в зависимости от ситуации. Например:

type Name = String

data Type                  -- aka. Formula
  = Function Type Type     -- aka. Implication
  | TypeVar Name           -- aka. PropositionalVar

data Term                  -- aka. Proof
  = Lambda Name Type Term  -- aka. ImplicationIntroduction
  | Apply Term Term        -- aka. ImplicationElimination
  | TermVar Name           -- aka. Start / Identity / Axiom / Copy

Вам нужно будет использовать контекст переменных в области видимости (например, гипотезы, которые вы можете предположить).

type TypingContext = Map Name Type -- aka. Hypotheses

Для таких типов вам просто нужно написать функцию:

termOf :: Type -> TypingContext -> Maybe Term

Но, возможно, в качестве первого шага лучше сначала написать обратную функцию, как упражнение:

typeOf :: Term -> TypingContext -> Maybe Type

Базовая структура этих двух функций должна быть схожей: сопоставление шаблонов с вещью, которую вы имеете, решаете, какие правила ввода (например, правила проверки) применимы, называть себя рекурсивно, чтобы построить частичный результат, завершить частичный результат путем упаковки в конструкторе, который соответствует правилу типирования (правило проверки). Разница в том, что typeOf может просто пройти весь термин и вывести все из строя, а termOf, вероятно, должен угадать и отступить, если догадки не сработают. Вероятно, вам действительно нужна монада списка для termOf.

Преимущество написания typeOf заключается в следующем:

  • Это должно быть проще, потому что условия, как правило, содержат больше информации, чем типы, поэтому termOf может использовать эту дополнительную информацию, а typeOf должна создать дополнительную информацию.
  • Доступна большая помощь, потому что многие люди реализуют typeOf как упражнение, но мало кто реализует termOf как упражнение.