Могу ли я проверить, имеет ли данная сигнатура типа функции потенциальную реализацию?

Question

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

foo :: a -> b
foo x = x

bar :: (a -> b) -> a -> c
bar f x = f x

В моем сценарии, однако, у меня есть только сигнатура функции, и мне нужно проверить, "заселена" ли она потенциальной реализацией - надеюсь, это объяснение имеет смысл вообще!

Из-за свойства параметричности я бы предположил, что для обоих foo а также bar реализации не существует и, следовательно, оба должны быть отклонены. Но я не знаю, как это сделать программно.

Цель состоит в том, чтобы отсортировать все или хотя бы подмножество недопустимых сигнатур типа, как указано выше. Я благодарен за каждый намек.

Answer 1

Цель состоит в том, чтобы отсортировать все или хотя бы подмножество недопустимых сигнатур типа, как указано выше. Я благодарен за каждый намек.

Возможно, вы захотите взглянуть на переписку Карри-Говарда.

В основном, типы в функциональных программах соответствуют логическим формулам. Просто замени -> с подтекстом, (,) с соединением (И) и Either с дизъюнкцией (ИЛИ). Обитаемые типы - это как раз те, которые имеют соответствующую формулу, которая является тавтологией в интуиционистской логике.

Существуют алгоритмы, которые могут определять доказуемость в интуиционистской логике (например, использование исключения-отсечения в последовательностях Генцена), но проблема в PSPACE-полноте, поэтому в целом мы не можем работать с очень большими типами. Однако для типов среднего размера алгоритм исключения вырезов работает нормально.

Если вам нужно только подмножество необитаемых типов, вы можете ограничиться теми, которые имеют соответствующую формулу, которая НЕ является тавтологией в классической логике. Это правильно, поскольку интуиционистские тавтологии также являются классическими. Проверка правильности формулы P это не классическая тавтология может быть сделано, спрашивая, not P является выполнимой формулой. Итак, проблема в NP. Не очень, но лучше, чем PSPACE-полная.

Например, оба вышеупомянутых типа

a -> b
(a -> b) -> a -> c

явно не тавтологии! Следовательно, они не заселены.

Напоследок обратите внимание, что в Haskell undefined :: T а также let x = x in x :: T для любого типа Tтак что технически каждый тип обитаем. Как только мы ограничиваемся завершением программ, в которых нет ошибок времени выполнения, мы получаем более осмысленное понятие "обитаемый", к которому относится переписка Карри-Ховарда.

Answer 2

Вот недавняя реализация этого как плагина GHC, который, к сожалению, требует GHC HEAD в настоящее время.

---

Он состоит из класса типов с одним методом

class JustDoIt a where
  justDoIt :: a

Такой, что justDoIt Проверки типов каждый раз, когда плагин может найти обитателя своего предполагаемого типа.

foo :: (r -> Either e a) -> (a -> (r -> Either e b)) -> (r -> Either e (a,b))
foo = justDoIt

Для получения дополнительной информации прочитайте пост в блоге Иоахима Брейтнера, в котором также упоминается несколько других вариантов: джинн (уже в других комментариях здесь), исключение, карриохид для Скалы, хезарфен для Идриса.