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

我有一个如下定义的类型族:

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？

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

还是我完全走错了轨道？我应该使用数据系列还是功能依赖项？

最佳答案

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

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

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

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

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

(如果您为n指定了给定的值)，从而允许类型族应用程序完全缩减，并使用类型为a的实例，该类型具有SymVal的实例:

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 (Vec a n)推导SymVal a，因为没有更多上下文，它就无法减少类型族应用程序，因此不知道选择哪个实例。如果您希望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语句，这是最主要的方法。)

然后，您可以使用此函数允许GHC从SymVal (Vec a n)约束中推断出SymVal a约束，只要您能够为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 ...