问题 如何将两个类型约束与逻辑或Haskell结合起来?


在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

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

我如何逻辑或两个约束在一起?


11509
2018-04-21 00:36


起源

怎么样?当两者都满意时,它会让你消除歧义。 - Theo Belaire


答案:


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

那就是采摘 R 什么时候 b 很满意但是 a 并没有打破开放世界的假设,因为它涉及决定一个实例  满意;1 即使您添加了“两个满意的”构造函数,您也可以使用它来决定实例是否  礼物(通过看你是否得到一个 L 或者 R)。

因此,我不相信这样的 要么 约束是可能的;如果你可以观察到你得到的实例,那么你可以通过添加一个实例创建一个行为改变的程序,如果你不能观察到你得到的实例,那么它就没用了。

1 此实例和正常实例分辨率之间的差异(也可能失败)通常是编译器无法确定是否满足约束;在这里,您要求编译器确定不能满足约束。一个微妙但重要的区别。


13
2018-04-21 01:17



是否有可能具有逻辑或哪些可以满足可能的约束而不是简单的可满足约束? - Steven Stewart-Gallus


我来这里是为了回答你关于咖啡馆的问题。不确定这里的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在这里

我如何逻辑或两个约束在一起?

更棘手。对于类型平等方法, == 使用封闭类型系列。所以你可以写一个封闭类型的家庭返回类型 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指出的那样,你无法测试约束是否存在 满足的。类型相等是特殊的。


0
2017-07-23 22:58