Haskell的类型系统和逻辑编程 - 如何将Prolog程序移植到类型级别

Question

我试图理解逻辑编程语言(在我的例子中是Prolog)和Haskell的类型系统之间的关系.

我知道两者都使用统一和变量来根据关系查找值(或类型,在Haskell的类型系统中).作为练习更好地理解它们之间的相似点和不同点的练习,我尝试在Haskell的类型级别中重写一些简单的prolog程序,但是我遇到了一些问题.

首先,我重写了这个简单的prolog程序:

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

它工作正常,但我不能用这个Prolog扩展它:

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) =>部分,我的意思是部分)是不同的,所以最后两个声明声明中的as和bs实际上是不同的价值观并没有冲突.

---

我试图重写的另一个程序是这样的:

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).

(顺便说一句,例子来自Learn Prolog Now书)

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的类型级别,如果可能的话.任何帮助将不胜感激.

编辑:

Ed'ka的解决方案有效,但方式完全不同.我还在努力了解何时我们可以在类型系统中运行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这里是必要的,因为第二个和第三个实例都PathExists可以匹配children不是空列表的情况,但GHC可以在我们的情况下确定更具体的一个,这取决于列表的头部是否等于to参数(如果它是它意味着我们已经找到路径即后代).

Answer 2

至于这个GreaterThan例子,我不知道如何引入这些Booleans是忠实于原始Prolog代码的步骤.您似乎正在尝试编写Prask版本中不存在的Haskell版本中的可判定性.

总而言之,你可以做到

{-# 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)