具有类型级别 Bool 的 GADT - 使 (&&) 类型运算符隐含对其参数的约束

Question

总而言之，我试图了解如何告诉 ghc a && b ~ True 应该暗示 a ~ True 和 b ~ True 在 GADT 的上下文中。

给定一个数据构造函数：

data Foo :: Bool -> * where
    ...
    Bar :: Foo j -> Foo k -> Foo (j && k)
    ...

，例如，Eq (Foo True):

的实例

instance Eq (Foo True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = foo11 == ff21 && foo12 == foo22
   ....

编译器给出以下错误：

Could not deduce: k1 ~ k
      from the context: 'True ~ (j && k)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:4-14
      or from: 'True ~ (j1 && k1)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:21-31
      `k1' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:21-31
      `k' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:4-14
      Expected type: Foo k
        Actual type: Foo k1
    * In the second argument of `(==)', namely `f22'
      In the second argument of `(&&)', namely `f12 == f22'
      In the expression: f11 == f21 && f12 == f22
    * Relevant bindings include
        f22 :: Foo k1 (bound at Main.hs:12:29)
        f12 :: Foo k (bound at Main.hs:12:12)

（以及 j 和 j1 的等效误差）

这明显是在抱怨它不知道f12 :: Foo k和f22 :: Foo k1是同一个类型

最近我一直在使用 typelit-nat-normalise 来解决类似的问题（添加了 typenat），并且我搜索了一个类似的库来解决 bool 的这些问题 - 但无济于事。

我找到了 typelevel-rewrite-rules，我认为这可能使我能够为此编写某种重写规则，但我无法计算出告诉编译器的语法：

(a && b ~ True) 表示 (a ~ True) AND (b ~ True)。我相信这会解决这个问题。

Answer 1

我相信在当前的 GHC 中，这种类型族的“反转”是不可能的，至少在没有不安全函数的情况下是不可能的。

即使有不安全的功能，我也不知道添加它是否安全。种类是一种奇怪的野兽，通常包含的术语比人们预期的要多。例如。 type family X :: Bool编译，还是不能证明X ~ 'True和X ~ 'False.

下面的代码没有完全回答这个问题，但我想说的是，如果我们可以向 Foo 添加一些约束，以便携带一些单例，那么我们可以写出想要的 Eq实例。

下面的代码或许可以进一步简化。不过，它就在这里。下面，我定义了“转换”函数 fooT1, fooT2 以说服 GHC 在 Foo k 和 Foo j 中我们确实有 k ~ j ~ 'True.

{-# LANGUAGE GADTs, ScopedTypeVariables, TypeApplications,
    DataKinds, TypeOperators, KindSignatures,
    FlexibleInstances, AllowAmbiguousTypes #-}
{-# OPTIONS -Wall #-}

import Data.Singletons
import Data.Singletons.Prelude.Bool

data Foo :: Bool -> * where
    Bar :: (SingI j, SingI k) =>
           Foo j -> Foo k -> Foo (j && k)

fooT1 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True) 
      => Foo a -> Foo b -> Foo 'True
fooT1 f _ = case (sing @a, sing @b) of
   (STrue, STrue) -> f

fooT2 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True)
      => Foo a -> Foo b -> Foo 'True
fooT2 _ f = case (sing @a, sing @b) of
   (STrue, STrue) -> f

instance Eq (Foo 'True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = 
      fooT1 foo11 foo12 == fooT1 foo21 foo22 &&
      fooT2 foo11 foo12 == fooT2 foo21 foo22

请注意，模式匹配 (STrue, STrue) 是详尽无遗的，GHC 不会发出任何警告。

具有类型级别 Bool 的 GADT - 使 (&&) 类型运算符隐含对其参数的约束

GADT with Type level Bool - making (&&) type operator imply constraints for its arguments

haskell

ghc

typechecking