时间戳

首页 > 解决方案 > 在 Haskell 中检测冗余约束？

haskell - 在 Haskell 中检测冗余约束？

问题描述

有没有办法在 Haskell 中检测冗余约束？

例如：

class    (A a, B a) => C1 a -- C1 ~ A AND B
instance (A a, B a) => C1 a

class    (A a, B a, C a) => C2 a
instance (A a, B a, C a) => C2 a

f :: (C1 a, C2 a) => a
f = ...

在这里，C2 意味着 C1，并且在签名中使用 C1f是多余的，即重言式。

在现实世界的元编程情况下，这将更加复杂，并且将极大地帮助整理签名头，并帮助我理解和跟踪正在发生的事情。

考虑到 GHC 的形式主义，这在逻辑上是可能的吗？

GHC 中的基础设施是否可用？

标签： haskellconstraintsghc

解决方案

如果我把你的存根放在一个文件中：

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class A a
class B a
class C a

class    (A a, B a) => C1 a -- C1 ~ A AND B
instance (A a, B a) => C1 a

class    (A a, B a, C a) => C2 a
instance (A a, B a, C a) => C2 a

undefined然后，您可以通过将变量绑定到您有兴趣在 ghci 中减少的类型来了解冗余约束：

> x = undefined :: (C1 a, C2 a) => a

<interactive>:1:18: warning: [-Wsimplifiable-class-constraints]
    • The constraint ‘C1 a’ matches
        instance forall a. (A a, B a) => C1 a -- Defined at test.hs:8:10
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance
    • In an expression type signature: (C1 a, C2 a) => a
      In the expression: undefined :: (C1 a, C2 a) => a
      In an equation for ‘x’: x = undefined :: (C1 a, C2 a) => a

<interactive>:1:18: warning: [-Wsimplifiable-class-constraints]
    • The constraint ‘C2 a’ matches
        instance forall a. (A a, B a, C a) => C2 a
          -- Defined at test.hs:11:10
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance
    • In an expression type signature: (C1 a, C2 a) => a
      In the expression: undefined :: (C1 a, C2 a) => a
      In an equation for ‘x’: x = undefined :: (C1 a, C2 a) => a
*Main
> :t x
x :: forall {a}. (A a, B a, C a) => a

在这种情况下，前两个警告实际上只是一个快乐的意外，与您的存根有多简单有关；你不会总是得到它们。真正有趣的是第二个查询，:t x它减少了对您需要了解的基本事实的限制a。

推荐阅读