Учитывая подпись типа Haskell, можно ли автоматически генерировать код?

Ответ 1

Djinn делает это для ограниченного подмножества типов Haskell, соответствующего логике первого порядка. Однако он не может управлять рекурсивными типами или типами, которые требуют рекурсии для реализации; поэтому, например, он не может написать термин типа (a -> a) -> a (тип fix), что соответствует предложению "если а означает а, то а", что явно ложно; вы можете использовать его, чтобы что-то доказать. В самом деле, именно поэтому fix порождает ⊥.

Если вы разрешаете fix, то писать программу, чтобы дать термин любого типа, тривиально; программа просто напечатала fix id для каждого типа.

Джинн - это, в основном, игрушка, но он может делать некоторые забавные вещи, такие как вывод правильных экземпляров Monad для Reader и Cont для типов return и (>>=). Вы можете попробовать, установив пакет djinn или используя lambdabot, который интегрирует его как команду @djinn.

Ответ 2

Oleg в okmij.org имеет реализацию этого. Существует короткое введение здесь, но грамотный источник Haskell содержит детали и описание процесса. (Я не уверен, как это соответствует Джинну, но это еще один пример.)

Есть случаи, когда нет уникальной функции:

fst', snd' :: (a, a) -> a
fst' (a,_) = a
snd' (_,b) = b

Не только это; бывают случаи, когда существует бесконечное число функций:

list0, list1, list2 :: [a] -> a
list0 l = l !! 0
list1 l = l !! 1
list2 l = l !! 2
-- etc.

-- Or 
mkList0, mkList1, mkList2 :: a -> [a]
mkList0 _ = []
mkList1 a = [a]
mkList2 a = [a,a]
-- etc.

(Если вам нужны только общие функции, рассмотрите [a] как ограниченные бесконечными списками для list0, list1 и т.д., т.е. data List a = Cons a (List a))

Фактически, если у вас есть рекурсивные типы, любые типы, связанные с ними, соответствуют бесконечному числу функций. Однако, по крайней мере, в приведенном выше случае существует счетное число функций, поэтому можно создать (бесконечный) список, содержащий все из них. Но, я думаю, тип [a] -> [a] соответствует несчетно бесконечному числу функций (снова ограничивайте [a] бесконечными списками), поэтому вы даже не можете их перечислить!

(Резюме: существуют типы, которые соответствуют конечному, счетно бесконечному и несчетно бесконечному числу функций.)

Ответ 3

Это невозможно вообще (а для таких языков, как Haskell, у которого даже нет сильного свойства нормализации) и возможно только в некоторых (очень) особых случаях (и для более ограниченных языков), например, когда тип кодомена имеет единственный конструктор (например, функция f :: forall a. a -> () может быть определен однозначно). Чтобы уменьшить набор возможных определений для заданной сигнатуры одному синглетному набору с одним определением, нужно дать больше ограничений (например, в виде дополнительных свойств, все еще трудно представить, как это может быть полезно без предоставления пример использования).

Из (n-) категориальной точки зрения типы соответствуют объектам, члены соответствуют стрелкам (конструкторы также соответствуют стрелкам), а определениям функций соответствуют 2-стрелки. Вопрос аналогичен вопросу о том, можно ли построить 2-категорию с требуемыми свойствами, указав только набор объектов. Это невозможно, так как вам нужна либо явная конструкция для стрелок и 2-стрелок (т.е. Запись терминов и определений), либо дедуктивная система, которая позволяет вывести необходимую структуру с использованием определенного набора свойств (которые еще нужно явно определить).

Существует также интересный вопрос: если ADT (т.е. подкатегория Hask), можно автоматически выводить экземпляры для Typeable, Data (да, используя SYB), Traversable, Foldable, Functor, Pointed, Applicative, Monad и т.д. (?). В этом случае у нас есть необходимые сигнатуры, а также дополнительные свойства (например, законы монады, хотя эти свойства не могут быть выражены в Haskell, но они могут быть выражены на языке с зависимыми типами). Есть несколько интересных конструкций:

http://ulissesaraujo.wordpress.com/2007/12/19/catamorphisms-in-haskell

который показывает, что можно сделать для списка ADT.

Ответ 4

Вопрос на самом деле довольно глубокий, и я не уверен в ответе, если вы спрашиваете о полной славе типов Haskell, включая семейства типов, GADT и т.д.

То, о чем вы спрашиваете, может ли программа автоматически доказать, что любой тип заселен (содержит значение), показывая такое значение. Принцип, называемый корреляцией Карри-Говарда, гласит, что типы могут быть интерпретированы как математические предложения, а тип заселен, если предложение конструктивно доказуемо. Поэтому вы спрашиваете, есть ли программа, которая может доказать, что определенный класс предложений является теоремами. На языке, подобном Агда, система типов достаточно сильна, чтобы выражать произвольные математические предложения, а доказать произвольные неразрешимы теоремой о неполноте Гёделя. С другой стороны, если вы опуститесь до (скажем) чистого Хиндли-Милнера, вы получите гораздо более слабую и (я думаю) разрешимую систему. С Haskell 98 я не уверен, потому что классы типов должны быть эквивалентны GADT.

С GADT, я не знаю, разрешимо это или нет, хотя, возможно, некоторые знающие люди здесь сразу узнают. Например, может быть возможно закодировать проблему остановки для данной машины Тьюринга как GADT, поэтому есть значение этого типа, если машина останавливается. В этом случае обитаемость явно неразрешима. Но, может быть, такая кодировка не совсем возможна, даже с типами семейств. В настоящее время я недостаточно свободно владею этим предметом, чтобы это было очевидно для меня в любом случае, хотя, как я уже сказал, может быть, кто-то еще знает ответ.

(Обновление:). Мне гораздо проще интерпретировать ваш вопрос: вы можете спросить, жив ли каждый тип Haskell. Ответ, очевидно, нет. Рассмотрим полиморфный тип

a -> b

Нет никакой функции с этой сигнатурой (не считая что-то вроде unsafeCoerce, что делает систему типов непоследовательной).