Система типа Haskell и логическое программирование - как подключить программы Prolog к типу уровня

Я пытаюсь понять связь между языком логического программирования (Prolog в моем случае) и системой типа Haskell.

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

Сначала я переписал эту простую прологическую программу:

numeral(0).
numeral(succ(X)) :- numeral(X).

add(0,Y,Y).
add(succ(X),Y,succ(Z)) :- add(X,Y,Z).

как:

class Numeral a where
    numeral :: a
    numeral = u

data Zero
data Succ a

instance Numeral Zero
instance (Numeral a) => Numeral (Succ a)

class (Numeral a, Numeral b, Numeral c) => Add a b c | b c -> a where
    add :: b -> c -> a
    add = u

instance (Numeral a) => Add a Zero a
instance (Add x y z) => Add (Succ x) (Succ y) z

он отлично работает, но я не мог продлить его с помощью этого Пролога:

greater_than(succ(_),0).
greater_than(succ(X),succ(Y)) :- greater_than(X,Y).

Я пробовал это:

class Boolean a
data BTrue
data BFalse
instance Boolean BTrue
instance Boolean BFalse

class (Numeral a, Numeral b, Boolean r) => Greaterthan a b r | a b -> r where
    greaterthan :: a -> b -> r
    greaterthan = u

instance Greaterthan Zero Zero BFalse
instance (Numeral a) => Greaterthan (Succ a) Zero BTrue
instance (Numeral a) => Greaterthan Zero (Succ a) BFalse
instance (Greaterthan a b BTrue)  => Greaterthan (Succ a) (Succ b) BTrue
instance (Greaterthan a b BFalse) => Greaterthan (Succ a) (Succ b) BFalse

Проблема с этим кодом заключается в том, что последние два экземпляра вызывают конфликты с фондом. Я могу понять, почему, но мне кажется, что это не должно быть проблемой, так как их защитные части (или что бы это там называлось, я имею в виду часть (Greaterthan a b c) =>) различны, так что a и b в последние два объявления insance - фактически разные значения, и конфликтов нет.

Другая программа, которую я попыталась переписать, была следующей:

child(anne,bridget).
child(bridget,caroline).
child(caroline,donna).
child(donna,emily).

descend(X,Y) :- child(X,Y).
descend(X,Y) :- child(X,Z),
                descend(Z,Y).

(btw, примеры из Learn Prolog Now book)

data Anne
data Bridget
data Caroline
data Donna
data Emily

class Child a b | a -> b where
    child :: a -> b
    child = u

instance Child Anne Bridget
instance Child Bridget Caroline
instance Child Caroline Donna
instance Child Donna Emily

class Descend a b | b -> a where
    descend :: b -> a
    descend = u

instance (Child a b) => Descend a b
instance (Child a c, Descend c b) => Descend a b

И я получаю ошибку "дубликатов экземпляров" в последней строке. Я думаю, что это аналогичная проблема, даже если у меня есть разные части защиты, я получаю ошибки, потому что части тела (я имею в виду Descend a b части) одинаковы.

Итак, я ищу способы портировать программы Prolog на уровень типа Haskell, если это возможно. Любая помощь будет оценена.

EDIT:

Решение Ed'ka работает, но совершенно по-другому. Я все еще пытаюсь понять, когда мы можем запустить программу Prolog в системе типов, когда/почему нам нужно написать другой алгоритм, чтобы заставить его работать (например, в решении Ed'ka), и когда/почему нет пути к внедрить программу в систему типов Haskell.

Возможно, я могу найти некоторые указания об этом после прочтения "Fun With Functional Dependencies".

Ответ 1

Поскольку @stephen tetley уже указывал, когда GHC пытается сопоставить объявление экземпляра, он считает, что только глава экземпляра (материал после = > ) полностью игнорирует контекст экземпляра (материал before = > ), как только однозначный экземпляр найден, он пытается для соответствия контексту экземпляра. Ваш первый проблемный пример явно имеет дублирование в голове экземпляра, но его можно легко устранить, заменив два конфликтующих экземпляра еще одним общим экземпляром:

instance (Greaterthan a b r)  => Greaterthan (Succ a) (Succ b) r

Второй пример, однако, намного сложнее. Я подозреваю, что для работы в Haskell нам нужна функция уровня типа, которая может генерировать два разных результата в зависимости от того, определен ли конкретный экземпляр или нет для определенных аргументов типа (т.е. Если есть instance Child Name1 Name2 - рекурсивно сделать что-то с Name2 иначе return BFalse). Я не уверен, можно ли это кодировать с помощью типов GHC (я подозреваю, что это не так).

Однако я могу предложить "решение", которое работает для немного другого типа ввода: вместо подразумевания отсутствия отношения parent->child (когда для такой пары не задан ни один экземпляр) мы могли бы явно кодировать все существующие отношения, используя type- списки уровней. Затем мы можем определить функцию типа Descend типа, хотя она должна полагаться на многострадальное расширение OverlappingInstances:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
  FlexibleInstances, FlexibleContexts, TypeOperators,
  UndecidableInstances, OverlappingInstances #-}

data Anne
data Bridget
data Caroline
data Donna
data Emily
data Fred
data George

-- Type-level list
data Nil
infixr 5 :::
data x ::: xs

-- `bs` are children of `a`
class Children a bs | a -> bs

instance Children Anne (Bridget ::: Nil)
instance Children Bridget (Caroline ::: Donna ::: Nil)
instance Children Caroline (Emily ::: Nil)
-- Note that we have to specify children list for everyone
-- (`Nil` instead of missing instance declaration)
instance Children Donna Nil
instance Children Emily Nil
instance Children Fred (George ::: Nil)
instance Children George Nil

-- `or` operation for type-level booleans 
class OR a b bool | a b -> bool
instance OR BTrue b BTrue
instance OR BFalse BTrue BTrue
instance OR BFalse BFalse BFalse

-- Is `a` a descendant of `b`?
class Descend  a b bool | a b -> bool
instance (Children b cs, PathExists cs a r) => Descend a b r

-- auxiliary function which checks if there is a transitive relation
-- to `to` using all possible paths passing `children`
class PathExists children to bool | children to -> bool

instance PathExists Nil a BFalse
instance PathExists (c ::: cs) c BTrue
instance (PathExists cs a r1, Children c cs1, PathExists cs1 a r2, OR r1 r2 r)
    => PathExists (c ::: cs) a r

-- Some tests
instance Show BTrue where
    show _ = "BTrue"

instance Show BFalse where
    show _ = "BFalse"

t1 :: Descend Donna Anne r => r
t1 = undefined -- outputs `BTrue`

t2 :: Descend Fred Anne r => r
t2 = undefined -- outputs `BFalse`

OverlappingInstances необходимо здесь, так как 2-й и 3-й экземпляры PathExists могут совпадать с случаем, когда children не является пустым списком, но GHC может определить более конкретный в нашем случае в зависимости от того, равен ли глава списка равным к аргументу to (и если это означает, что мы нашли путь, то есть потомок).

Ответ 2

Что касается примера GreaterThan, я не вижу, как введение этих Boolean является шагом, верным исходному коду Пролога. Кажется, вы пытаетесь кодировать чувство разрешимости в вашей версии Haskell, которая отсутствует в версии Prolog.

Итак, в целом вы можете просто сделать

{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class Numeral a where

data Zero
data Succ a

instance Numeral Zero
instance (Numeral a) => Numeral (Succ a)

class (Numeral a, Numeral b) => Greaterthan a b where

instance (Numeral a) => Greaterthan Zero (Succ a)
instance (Greaterthan a b)  => Greaterthan (Succ a) (Succ b)

Фактически с видами данных, вы можете написать его лучше (но я не могу попробовать это сейчас, так как у меня только установлен ghc 7.2 ):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

data Numeral = Zero | Succ Numeral

class Greaterthan (a :: Numeral) (b :: Numeral) where

instance Greaterthan Zero (Succ a)
instance (Greaterthan a b)  => Greaterthan (Succ a) (Succ b)

Ответ 3

Для решения Ed'ka вы можете использовать:

import Data.HList.TypeCastGeneric2
instance TypeCast nil Nil => Children a nil

вместо одного экземпляра для каждого человека, у которого нет детей.