从任意未知 Nats 中提取值

问题描述

给定类型级列表函数（来自this blog post）

type family Length (xs :: [*]) :: Nat where
    Length '[] = 0
    Length (_ ': xs) = 1 + Length xs

“硬编码”类型列表长度的值提取按预期工作

t1 :: Integer
t1 = natVal (Proxy :: Proxy (Length '[Int]))

还有t1 = 1。但是，创建一个从任意列表中获取值的函数似乎失败了。

t2 :: forall (xs :: [*]). Proxy xs -> Integer
t2 _ = natVal (Proxy :: Proxy (Length xs))

给出错误

    • No instance for (KNownNat (Length xs))
        arising from a use of ‘natVal’

这看起来很不幸但合理，因为只有文字是“已知的”。但是，强制满足以下约束会导致对模棱两可的类型的抱怨。

unsafeKNownConstr :: c :~: (KNownNat n :: Constraint)
unsafeKNownConstr = unsafeCoerce Refl

t3 :: forall (xs :: [*]). Proxy xs -> Integer
t3 _ = case Proxy :: Proxy (Length xs) of
         p@(_ :: Proxy l) -> case unsafeKNownConstr @(KNownNat l) of
                             Refl -> natVal @l p

具体来说，

    • Could not deduce (KNownNat n0) arising from a use of ‘natVal’
      from the context: KNownNat n0 ~ KNownNat (Length xs)
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,in a case alternative
...
      The type variable ‘n0’ is ambiguous

GHC (8.10.4) 在这里抱怨什么？或者，还有其他方法可以提取这些未知的 Nats 吗？

解决方法

你可以这样做：

t4 :: forall n xs. (n ~ Length xs,KnownNat n) => Proxy xs -> Integer
t4 _ = natVal $ Proxy @n

这表示您的调用者必须充分了解类型级别列表 xs 才能将 Length xs 完全解析为固定值，他们将能够为此生成一个KnownNat 实例。¹ 但是在 t4 中，您可以对静态未知的列表进行操作。

λ t4 $ Proxy @[Int,Char,Bool]
3
it :: Integer

---

您的尝试没有成功，因为 unsafeKnownConstr 的类型为 forall c n. c :~: KnownNat n。它承诺对于您喜欢的任何约束 c，它可以证明对于您喜欢的任何 KnownNat n 约束都等于 n。

除了这显然是一个虚假的承诺之外，当您使用 unsafeKnownConstr @(KnownNat l) 时，您只是在设置 c。 n 仍然是一个可以实例化为任何东西的类型变量。 GHC 不知道为 n 选择什么；这就是 GHC 抱怨的模棱两可的类型变量。实际上，您已经撒谎并告诉它任何任意选择的 n 都等于列表的长度，但是您实际上并没有选择使用 n，因此 GHC 无法告诉 什么 KnownNat 字典你想（错误地）考虑 KnownNat 的 Length xs 字典。

如果你修复了 unsafeKnownConstr 的第二个类型参数，那么你可以得到这样的东西来编译：

t3 :: forall (xs :: [*]). Proxy xs -> Integer
t3 _ = case Proxy :: Proxy (Length xs) of
         p@(_ :: Proxy l) -> case unsafeKnownConstr @(KnownNat l) @17928 of
                             Refl -> natVal @l p

然后允许您在 GHCI 中执行此操作：

λ t3 $ Proxy @[Int,Bool]
17928
it :: Integer

无论您选择什么值，不安全地强制 KnownNat 约束对您都不会很有用，因为它们确实包含信息：Nat 已知的值！>

---

¹ 或者他们也可以尝试解决它，并通过他们自己的类型将约束传递给他们自己的调用者。