断言类型类适用于类型族应用程序的所有结果

Question

我有一个类型族定义如下：

type family Vec a (n :: Nat) where
  Vec a Z = a
  Vec a (S n) = (a, Vec a n)

我想断言应用这个类型族的结果总是满足 SBV 包中的 SymVal 类约束：

forall a . (SymVal a) => SymVal (Vec a n)

有SymVal 实例a,b，所以只要SymVal a 成立，那么SymVal (Vec a n) 应该成立，对于n 的任何值。如何确保 GHC 看到 SymVal 始终针对类型族应用程序的结果实现？

但是，我不知道如何表达。我写一个实例吗？派生条款？我不是在创建新类型，只是将数字映射到现有类型。

还是我完全走错了路？我应该使用数据族还是函数依赖项？

Answer 1

做不到。你只需要把约束放在任何地方。真是太可惜了。

Answer 2

我不知道您需要这些 SymVal (Vec a n) 实例的确切上下文，但一般来说，如果您有一段代码需要实例 SymVal (Vec a n)，那么您应该将其添加为上下文：

foo :: forall (a :: Type) (n :: Nat). SymVal (Vec a n) => ...

当使用特定的n 调用foo 时，约束求解器将减少类型族应用程序并使用实例

instance ( SymVal p, SymVal q ) => SymVal (p,q)

在该过程结束时，约束求解器将需要SymVal a 的实例。这样你就可以拨打foo:

• 如果您为n 指定给定值，允许类型族应用程序完全归约，并使用具有SymVal 实例的类型a：

bar :: forall (a :: Type). SymVal a => ...
bar = ... foo @a @(S (S (S Z))) ...

baz :: ...
baz = ... foo @Float @(S Z) ... -- Float has a SymVal instance

• 通过提供相同的上下文来延迟实例搜索：

quux :: forall (a :: Type) (n :: Nat). SymVal (Vec a n) => ...
quux = ... foo @a @n ...

GHC 不能自动从SymVal a 推导出SymVal (Vec a n)，因为没有进一步的上下文它不能减少类型族应用程序，因此不知道选择哪个实例。如果您希望 GHC 能够执行此推论，则必须将 n 作为参数显式传递。这可以用单例来模拟：

deduceSymVal :: forall (a :: Type) (n :: Nat). Sing n -> Dict (SymVal a) -> Dict (SymVal (Vec a n))
deduceSymVal sz@SZ Dict =
  case sz of
    ( _ :: Sing Z )
      -> Dict
deduceSymVal ( ss@(SS sm) ) Dict
  = case ss of
      ( _ :: Sing (S m) ) ->
        case deduceSymVal @a @m sm Dict of
          Dict -> Dict

（请注意，这些令人讨厌的 case 语句将被模式中的类型应用程序消除，mais c'est la vie。）

然后，您可以使用此函数允许 GHC 从 SymVal a 约束推导出 SymVal (Vec a n) 约束，只要您能够为 n 提供单例（相当于将 n 显式传递为反对对其进行参数化）：

flob :: forall (a :: Type) (n :: Nat). (SymVal a, SingI n) => ...
flob = case deduceSymVal @a (sing @n) Dict of
  Dict -- matching on 'Dict' provides a `SymVal (Vec a n)` instance
    -> ... foo @a @n ...