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

我有一堆复杂的类型级别的函数，其计算如下：

(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指出，在某些情况下，这是可以与GADTs解决，但我的具体情况是这样的：

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) forall n . KnownNat n => KnownNat (NestedIfs n)来自我上面提到的一般推论。

---

这个问题不难，但是不合适。 你期待什么样的价值回到类型c (If pab) :: 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 cab 。 这正是如何表达你的请求 - 你想要一个证明，两个说给定cx和cy举行， c (If 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

链接地址: http://www.djcxy.com/p/7463.html

上一篇: Infer constraints of type families from constraints of arguments

下一篇: What is the monomorphism restriction?