在Haskell中实例化类型变量

Question

在Haskell中实例化类型变量

haskellprologtypeclassunificationsuccessor-arithmetics

5

编辑：问题已解决。 我不知道在源文件中启用语言扩展并不会在 GHCi 中启用语言扩展。解决方法是在 GHCi 中输入 :set FlexibleContexts。

我最近发现，在 Haskell 中，类和实例中的类型声明是 Horn 子句。因此，我将《Prolog 艺术》第 3 章中的算术运算编码到了 Haskell 中。例如：

fac(0,s(0)).
fac(s(N),F) :- fac(N,X), mult(s(N),X,F).

class Fac x y | x -> y
instance Fac Z (S Z)
instance (Fac n x, Mult (S n) x f) => Fac (S n) f

pow(s(X),0,0) :- nat(X).
pow(0,s(X),s(0)) :- nat(X).
pow(s(N),X,Y) :- pow(N,X,Z), mult(Z,X,Y).

class Pow x y z | x y -> z
instance (N n) => Pow (S n) Z Z
instance (N n) => Pow Z (S n) (S Z)
instance (Pow n x z, Mult z x y) => Pow (S n) x y

在Prolog中，证明过程中会为(逻辑)变量实例化值。然而，我不知道如何在Haskell中实例化类型变量。也就是说，我不知道Haskell中与Prolog查询相对应的方法。

?-f(X1,X2,...,Xn)

这里有一个假设，我认为

:t undefined :: (f x1 x2 ... xn) => xi

会导致Haskell实例化xi，但即使启用了FlexibleContexts，这也会导致Non type-variable argument in the constraint错误。

- emi

2

请记住，这不会将Prolog嵌入到Haskell的类型系统中。类型类求解器不进行回溯。 - luqui

你说得对；然而，我并没有觉得它会这样做。实际的嵌入需要更多的工作：)。 - emi

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Ed'ka · Accepted Answer

我不确定Prolog示例，但我会用Haskell以下方式定义:

{-# LANGUAGE MultiParamTypeClasses, EmptyDataDecls, FlexibleInstances,
FlexibleContexts, UndecidableInstances, TypeFamilies, ScopedTypeVariables #-}

data Z
data S a
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three 


class Plus x y r
instance (r ~ a) => Plus Z a r
instance (Plus a b p, r ~ S p) => Plus (S a) b r

p1 = undefined :: (Plus Two Three r) => r


class Mult x y r
instance (r ~ Z) => Mult Z a r
instance (Mult a b m, Plus m b r) => Mult (S a) b r

m1 = undefined :: (Mult Two Four r) => r


class Fac x r
instance (r ~ One) => Fac Z r
instance (Fac n r1, Mult (S n) r1 r) => Fac (S n) r

f1 = undefined :: (Fac Three r) => r


class Pow x y r
instance (r ~ One) => Pow x Z r
instance (r ~ Z) => Pow Z y r
instance (Pow x y z, Mult z x r) => Pow x (S y) r

pw1 = undefined :: (Pow Two Four r) => r

-- Handy output
class (Num n) => ToNum a n where
    toNum :: a -> n
instance (Num n) => ToNum Z n where
    toNum _ = 0
instance (ToNum a n) => ToNum (S a) n where
    toNum _ = 1 + toNum (undefined :: a) 

main = print $ (toNum p1, toNum m1, toNum f1, toNum pw1)

更新:

如下方danportin的评论所述，在TypeFamilies中，"懒惰模式"（在实例上下文中）在这里是不需要的（他最初的代码更短更简洁）。

然而，在这个问题的背景下，我能想到一个应用这种模式的例子是：假设我们想将布尔逻辑添加到我们的类型级算术中：

data HTrue
data HFalse

-- Will not compile
class And x y r | x y -> r
instance And HTrue HTrue HTrue
instance And a b HFalse -- we do not what to enumerate all the combination here - they all HFalse

但是由于“功能依赖冲突”，这段代码无法编译。而且，在我看来，我们仍然可以表达这种重叠的情况，而不需要使用功能依赖。

class And x y r
instance (r ~ HTrue) => And HTrue HTrue r
instance (r ~ HFalse) => And a b r

b1 = undefined :: And HTrue HTrue r => r   -- HTrue
b2 = undefined :: And HTrue HFalse r => r  -- HFalse

这绝对不是一种最好的方法（它需要IncoherentInstances）。也许有人可以提出另一种更少“创伤性”的方法。