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

Question

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

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

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

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

Проблема с этим кодом в том, что последние два экземпляра вызывают конфликт fundep. Я могу понять, почему, но мне кажется, что это не должно быть проблемой, так как их охранники (или как там это называется, я имею в виду (Greaterthan a b c) => часть) разные, так что aс и bs в последних двух декларациях 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).

(кстати, примеры из книги " Изучите Пролог сейчас")

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, если это возможно. Любая помощь будет оценена.

РЕДАКТИРОВАТЬ:

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

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

Answer 1

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

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

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

Тем не менее, я могу предложить "решение", которое работает для немного другого типа ввода: вместо того, чтобы подразумевать отсутствиеparent->childотношение (когда для такой пары не определено ни одного экземпляра) мы могли бы явно кодировать все существующие отношения, используя списки уровня типа. Тогда мы можем определить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 аргумент (и если это так, значит, мы нашли путь, т.е. потомок).

Answer 2

Для GreaterThan Например, я не вижу, как представить эти Booleans шаг верный исходному коду Пролога. Кажется, вы пытаетесь закодировать чувство решимости в своей версии на 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)

Answer 3

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

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

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

Answer 4

Я играл со второй проблемой, и вот что я узнал. Можно сформулировать задачу «а-ля» Пролог, но с некоторыми оговорками. Одно из этих предостережений заключается в том, что на самом деле между аргументами нет никаких функциональных зависимостей, это бинарный предикат, а не унарная функция.

Для начала покажу код:

      {-# LANGUAGE FunctionalDependencies
           , FlexibleInstances
           , UndecidableInstances
           , NoImplicitPrelude
           , AllowAmbiguousTypes
           #-}

data Anne
data Bridget
data Caroline
data Donna
data Emily

class Child a b | a -> b

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

----------------------------------------------------

data True -- just for nice output

class Descend a b where descend :: True

instance {-# OVERLAPPING #-} Descend a a
instance (Child a b, Descend b c) => Descend a c

(вы можете проверить это в GHCI, включив :set -XTypeApplicationsи запустить что-то вроде :t descend @Anne @Carolineа также :t descend @Caroline @Anne)

Таким образом, это в основном соответствует примеру Пролога с одним важным отличием: вместо descend(X,Y) :- child(X,Y)у нас есть

      instance {-# OVERLAPS #-} Descend a a

Я объясню на мгновение, почему это так, но сначала я объясню, что это меняет: в основном, Descendотношение становится рефлексивным, т.е. истинным для всех . Это не относится к примеру с Прологом, где рекурсия завершается на один шаг раньше.

Теперь о том, почему это так. Рассмотрим, как GHC реализует замену переменных типа во время разрешения экземпляра типа: он сопоставляет заголовок экземпляра, унифицируя переменные типа, затем проверяет ограничения экземпляра. Отсюда, например, будет решена следующая последовательность:

1. Первый Descend Anne Carolineсопоставляется с , удобно a=Anne, c=Caroline
2. Следовательно, мы ищем экземпляры и Descend b Caroline.
3. Как правило, GHC сдался бы здесь, так как не знал бы, что означает. Но так как в bфункционально зависит от a, Child Anne bрешается Child Anne Bridget, следовательно b=Bridget, и мы пытаемся решить.
4. Descend Bridget Carolineснова сопоставляется с Descend a c, a=Bridget, cеще раз Caroline.
5. Искать Child Bridget b, который решает Child Bridget Caroline. Тогда попробуй решить.
6. Descend Caroline Carolineсоответствует перекрывающемуся экземпляру Descend a aи процесс завершается.

Таким образом, GHC на самом деле не может остановить итерацию раньше из-за того, как сопоставляются экземпляры.

Тем не менее, если мы заменим Childс семейством закрытого типа становится работоспособным:

      {-# LANGUAGE TypeFamilies
           , FunctionalDependencies
           , FlexibleInstances
           , UndecidableInstances
           , TypeOperators
           , NoImplicitPrelude
           , AllowAmbiguousTypes
           , ScopedTypeVariables
           #-}

data Anne
data Bridget
data Caroline
data Donna
data Emily

data True
data False

type family Child' a where
 Child' Anne     = Bridget
 Child' Bridget  = Caroline
 Child' Caroline = Donna
 Child' Donna    = Emily
 Child' a        = False

class Child a b | a -> b

instance (Child' a ~ b) => Child a b

----------------------------------------------------

class Descend' a b flag
class Descend a b where descend :: True

data Direct
data Indirect

type family F a b where
  F False a = Direct
  F a a = Direct
  F a b = Indirect

instance (Child' a ~ c) => Descend' a c Direct
instance (Child a b, Descend' b c (F (Child' b) c))
  => Descend' a c Indirect
instance (Descend' a b (F (Child' a) b))
  => Descend a b

Танец с Descend'просто иметь возможность перегружать выбор экземпляра на основе контекста, как описано в https://wiki.haskell.org/GHC/AdvancedOverlap. Основное отличие в том, что мы можем подать заявку Child'несколько раз, чтобы «заглянуть вперед».