14

在 Haskell 中，我们能够将类型的约束与逻辑与结合起来。

考虑以下

type And (a :: Constraint) b = (a, b)

或更复杂的

class (a, b) => And a b
instance (a, b) => And a b

我想知道如何在 Haskell 中逻辑地或两个约束在一起。

我最接近的尝试是这个，但它并不完全奏效。在这次尝试中，我用标签来具体化类型约束，而不是用隐式参数去具体化它们。

data ROr a b where
 L :: a => ROr a b
 R :: b => ROr a b

type Or a b = (?choose :: ROr a b)

y :: Or (a ~ Integer) (Bool ~ Integer) => a
y = case ?choose of
 L -> 4

x :: Integer
x = let ?choose = L in y

它几乎可以工作，但用户必须应用最后一部分，编译器应该为我做这件事。同样，当两个约束都满足时，这种情况不会让人们选择第三种选择。

我怎样才能在逻辑上或两个约束在一起？

4

2 回答 2

14

我相信没有办法自动选择ROr a b; b如果满足，但后来也满足，它将违反开放世界假设a；任何冲突解决规则都必然会导致添加一个实例来改变现有代码的行为。

也就是说，选择R何时b满足但a不破坏开放世界假设，因为它涉及确定实例不满足；1即使您添加了一个“都满意”的构造函数，您也可以使用它来确定实例是否不存在（通过查看是否获得 anL或 an R）。

因此，我不相信这样的或约束是可能的；如果你可以观察到你得到了哪个实例，那么你可以通过添加一个实例来创建一个行为发生变化的程序，如果你不能观察到你得到了哪个实例，那么它就没什么用了。

1这和正常的实例解析（也可能失败）之间的区别在于，通常编译器无法决定是否满足约束；在这里，您要求编译器确定不能满足约束。一个微妙但重要的区别。

于 2012-04-21T01:17:06.930 回答
0

我来这里是为了回答你关于咖啡厅的问题。不确定这里的 q 是否相同，但无论如何......

具有三个参数的类型类。

   class Foo a b c | a b -> c where
     foo :: a -> b -> c
   instance Foo A R A where ...
   instance Foo R A A where ...

除了函数依赖之外，我想表达的参数 a 和 b 中至少有一个是 c，

import Data.Type.Equality
import Data.Type.Bool

class ( ((a == c) || (b == c)) ~ True)
      => Foo a b c  | a b -> c  where ...

你需要打开一堆扩展。特别是UndecidableSuperClasses，因为类约束中的类型族调用在 GHC 中是不透明的。

你的q在这里

我怎样才能在逻辑上或两个约束在一起？

更棘手。对于类型相等方法，==使用封闭类型族。所以你可以写一个 Closed Type Family 返回 kind Constraint，但我怀疑有一个通用的解决方案。对于您的Foo班级：

type family AorBeqC a b c :: Constraint where
  AorBeqC a b a = ()
  AorBeqC a b c = (b ~ c)

class AorBeqC a b c => Foo a b c  | a b -> c  where ...

它可能有较差的和非对称类型的改进行为：如果 GHC 可以看到它们a, c是分开的，它将进入第二个等式并使用它(b ~ c)来改进；如果它看不到它们是分开的，也看不到它们是统一的，它就会卡住。

通常，正如@ehird 指出的那样，您无法测试约束是否不可满足。类型相等是特殊的。

于 2018-07-23T22:58:40.957 回答