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

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

foo :: a -> b
foo x = x

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

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

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

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


polymorphism parametric-polymorphism haskell hindley-milner
person Community    schedule 13.02.2018    source источник
comment
Вы можете найти djinn-lib и/или djinn-ghc несколько полезными. См. также djinn. См. также hedonisticlearning.com/djinn и обратите внимание, что lambdabot также умеет использовать djinn.   -  person dfeuer    schedule 13.02.2018
comment
См. также Учитывая подпись типа Haskell, возможно ли сгенерировать код автоматически? и Как работает Джинн?   -  person duplode    schedule 13.02.2018

Ответы (2)


arrow_upward
8
arrow_downward

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

Вы можете ознакомиться с перепиской Карри и Ховарда.

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

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

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

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

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

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

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

person chi    schedule 13.02.2018
comment
Существуют алгоритмы, которые могут определить доказуемость в интуиционистской логике. Можете ли вы предоставить ссылку? Интересно прочитать о том, как это работает; моя интуиция подсказывает мне, что доказуемость кажется чем-то, что может быть неразрешимым, поэтому, вероятно, будет для меня благодатной почвой для обучения :) - person Benjamin Hodgson♦; 14.02.2018
comment
Я искал быстрое алгоритмическое решение и нашел целую область для изучения. Думаю, пока достаточно проверить, не является ли что-то классической тавтологией. Спасибо! - person ; 14.02.2018
comment
@BenjaminHodgson Выше я неявно имею в виду простые типы / пропозициональную интуитивистскую логику, где это разрешимо. Как только вы начнете добавлять, например. Я считаю, что полиморфизм ранга 2, GADT и т. д. больше не разрешимы. Во всяком случае, для простых типов вы можете взять правила логического вывода Генцена (без CUT) и выполнить поиск вывода снизу вверх, пробуя все возможные правила недетерминистически. Удобно, идя снизу вверх, правила LJ включают только подформулы формулы цели, которые конечны, поэтому мы либо находим доказательство, либо снова посещаем то же состояние (что позволяет нам сократить поиск). - person chi; 14.02.2018
comment
@BenjaminHodgson Вы можете попробовать поиграть с правилами в этой классной онлайн-демонстрации. На каждом шаге восходящего поиска у нас есть только конечное число вариантов, а пространство поиска конечно из-за свойства подформулы. Таким образом, мы либо находим доказательство, либо возвращаемся к предыдущему состоянию (чтобы мы могли обнаружить, что ходим по кругу, и обрезать ветвь поиска). - person chi; 14.02.2018
comment
@chi Я проверил, не является ли fix для строго оцениваемых языков ((a -> b) -> a -> b) -> a -> b тавтологией для a == True и b == False, и результат положительный, потому что импликация ((a -> b) -> a -> b) дает True (учитывая, что -> является правой ассоциативностью), а a -> b дает False, а True -> False дает False, а это означает fix это не тавтология. Есть ли ошибка в моих рассуждениях, ведь fix конечно обитаем? - person ; 14.02.2018
comment
@ftor fix (и все, что связано с общей рекурсией) запрещен, поскольку в противном случае fix id :: T для любого T и все типы обитаемы, что не интересно. По сути, соответствие Карри-Ховарда выполняется в языке без рекурсии. (может быть разрешена некоторая форма рекурсии, например, примитивная рекурсия) - person chi; 14.02.2018

arrow_upward
7
arrow_downward

Вот недавняя реализация этого плагина 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

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

person Li-yao Xia    schedule 13.02.2018
comment
В нынешнем виде это не совсем самодостаточный ответ на вопрос. Не могли бы вы обобщить некоторые важные моменты ссылки? В случае с гниением ссылок здесь не будет ничего полезного для будущих читателей. - person jkeuhlen; 14.02.2018
comment
Спасибо что подметил это. Я добавил ссылку на сам пакет на Hackage и краткое описание того, что он делает. - person Li-yao Xia; 14.02.2018