28

我试图理解逻辑编程语言（在我的例子中是 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) =>部分）是不同的，所以最后两个实例声明中a的 s 和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”之后找到一些关于此的提示。

4

4 回答 4

7

正如@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这里是必要的，因为 2nd 和 3rd 实例都PathExists可以匹配children不是空列表的情况，但 GHC 可以在我们的情况下确定更具体的情况，具体取决于列表的头部是否等于to参数（如果是，则意味着我们已经找到路径即后代）。

于 2012-12-17T04:01:23.860 回答
6

至于GreaterThan示例，我看不出引入这些Booleans 是如何忠实于原始 Prolog 代码的步骤。您似乎正试图在您的 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)

实际上使用data types，你可以写得更好（但我现在不能尝试，因为我这里只安装了 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)
于 2012-12-17T04:02:10.620 回答
2

对于 Ed'ka 解决方案，您可以使用：

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

而不是每个没有孩子的人一个实例。

于 2012-12-17T04:25:19.453 回答
0

我已经解决了第二个问题，这就是我发现的。可以制定问题“a-la”Prolog，但需要注意一些警告。其中一个警告是，Descend参数之间实际上没有任何函数依赖关系，它是一个二元谓词，而不是一元函数。

首先，让我展示一下代码：

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

:set -XTypeApplications（您可以通过启用和运行类似的东西在 GHCi 中进行测试:t descend @Anne @Carolineand :t descend @Caroline @Anne）

因此，这主要遵循 Prolog 示例，但有一个重要区别： descend(X,Y) :- child(X,Y)我们有

instance {-# OVERLAPS #-} Descend a a

我将暂时解释为什么会这样，但首先我将解释它的变化：基本上，这种Descend关系变成了反射性的，即Descend a a对所有人都是正确的a。这不是 Prolog 示例的情况，其中递归提前一步终止。

现在为什么会这样。考虑 GHC 在类型实例解析期间如何实现类型变量替换：它匹配实例头部，统一类型变量，然后检查实例约束。因此，例如，Descend Anne Caroline将使用以下序列解决：

  1. 首先Descend Anne Caroline是匹配Descend a c，方便a=Anne，c=Caroline
  2. 因此，我们查找实例Child Anne b和Descend b Caroline。
  3. 一般来说，GHC会在这里放弃，因为它不知道是什么b意思。但是由于 in 在Child b功能上依赖于a，因此Child Anne b被解析为Child Anne Bridget，因此b=Bridget，我们尝试解析Descend Bridget Caroline。
  4. Descend Bridget Caroline再次匹配Descend a c, a=Bridget,c又是Caroline.
  5. 查找Child Bridget b，解析为Child Bridget Caroline. 然后尝试解决Descend Caroline 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

如https://wiki.haskell.org/GHC/AdvancedOverlap中所述，跳舞Descend'只是为了能够根据上下文重载实例选择。主要区别在于我们可以多次申请以“向前看”。Child'

于 2021-03-09T16:18:32.547 回答