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

Question

我有一系列复杂的类型级别函数，它们的计算结果如下：

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

显然，在这种情况下，这个表达式是一个KnonNat。更一般地说，我们可以说：

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应该能够推断出for all n.已知n=




Answer 1

这个问题并不难，但不太合适。您希望返回类型为c（如果p a b）：：Constraint的值是多少？你可能想问的是，如何填写这篇文章的正文

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

正如评论中所指出的，我强迫c成为一个单身汉，这样我就可以得到中的任意一个（c:~:True）（c:~:False）（您可以将我的SingI约束解读为强制执行c:：Bool必须是True或False，不幸的是，在类型级别上，这不是一个微不足道的请求，因为Any也有kindBool）。：-来自约束包。这是一种表示约束（a，b）意味着约束（如果c a b）。这正是表达你的要求的方式——你想要一个证据，证明在给定cx和cy的情况下，c（如果bxy）也会成立。

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

{-# 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