6

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

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始终针对类型系列应用程序的结果实施？

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

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

4

2 回答 2

5

做不到。你只需要把约束放在任何地方。这是一个真正的无赖。

于 2019-07-04T00:44:45.157 回答
4

我不知道您需要这些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

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

然后，您可以使用此函数来允许 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 ...
于 2019-07-04T01:15:36.140 回答