haskell - 从参数的约束推断类型族的约束

Question

我有一堆复杂的类型级函数，它们的计算结果如下:

(If (EqNat n 2)
  1
  (If (EqNat n 1)
    2
    (If (EqNat n 0) 3 0)))

现在显然在这种情况下这个表达式是 KnownNat 。更多的一般来说我们可以说:

forall (c :: * -> Constraint) (p :: Bool) a b .
(c a, c b) => c (If p a b)

有没有办法教 GHC 推断这一点？

编辑:@chi 指出，在某些情况下，这可以通过 GADT 解决，但我的特殊情况是这样的:

module M1 (C(..)) where

type familiy NestedIfs (n :: Nat) :: Nat
type NestedIfs n = <<complex nested ifs like the above that evals to literals>>

class C a (n :: Nat) where
  f :: KnownNat n => a -> NestedIfs n -> Bool

然后

module M2 () where
import M1

instance C Int n where
    f = ...require that KnownNat (NestedIfs n)...

NestedIfs无法访问M2但也许 GHC 应该能够推断forall n . KnownNat n => KnownNat (NestedIfs n)来自我上面提到的一般推论。

Answer 1

这个问题并不难，但是不适定。您期望从 c (If p a b)::Constraint 类型返回什么值？您可能想问的是如何填写此正文

bisect :: forall b c x y. SingI b => Proxy b -> (c x, c y) :- c (If b x y)

在这里，正如评论中所述，我强制 c 成为单例，以便我可以获得 Either (c :~: True) (c :~: False) (您可以将我的 SingI 约束理解为强制 c::Bool 必须为 True 或 False，不幸的是，这在类型级别上并不是一个简单的请求，因为 Any 也有类型 Bool)。 :- 来自 constraints包裹。这是一种表示约束 (a,b) 隐含约束 If c a b 的方式。这就是确切如何表达您的请求 - 您需要一个证明，证明给定的 c x 和 c y 成立，c (如果 b x y) 也成立。

填充该函数的主体实际上只需要很少的代码:

{-# LANGUAGE DataKinds, TypeFamilies, ConstraintKinds, TypeOperators, RankNTypes,
    ScopedTypeVariables, PolyKinds #-}

import Data.Constraint
import Data.Singletons.Prelude hiding ((:-))

bisect :: forall b c x y. (SingI b) => Proxy b -> (c x, c y) :- c (If b x y)
bisect _ = unmapDict $ case sing :: Sing b of
                         STrue -> mapDict weaken1
                         SFalse -> mapDict weaken2