从一系列较小的实例中推断出通用类型类实例？

Question

诚然，这个标题不是很描述，但我不知道如何用简短的标题来描述它。如果有任何建议，我将不胜感激！

我将展示我的问题的一个非常简化的版本:)

所以我有一个类型类

class Known f a where
    known :: f a

这应该能够在特定索引处生成给定类型的规范构造，这对于处理 GADT 和其他东西很有用。我给出了 this 的简化版本，其中包含相关部分。

所以显然有一个实例 Proxy:

instance Known Proxy a where
    known = Proxy

我们可以使用：

> known :: Proxy Monad
Proxy

但是还有一个实例 this HList-like type:

data Prod f :: [k] -> * where
    PNil :: Prod f '[]
    (:<) :: f a -> Prod f as -> Prod f (a ': as)

infixr 5 (:<)

其中 Prod f '[a,b,c] 大致相当于 (f a, f b, f c) 元组。相同的 Functor，不同的类型。

编写实例非常简单：

instance Known (Prod f) '[] where
    known = PNil
instance (Known f a, Known (Prod f) as) => Known (Prod f) (a ': as) where
    known = known :< known

效果很好：（假设是 Show 实例）

> known :: Prod Proxy '[1,2,3]
Proxy :< Proxy :< Proxy :< PNil

但是，我需要在所有 as 上创建一个 "polymorphic" 函数...但是 GHC 不喜欢它。

asProds :: forall as. Proxy as -> Prod Proxy as
asProds _ = known :: Prod Proxy as

出现这个错误：

No instance for (Known (Prod f) as)
  arising from a use of 'known'

我想这就是说 GHC 无法证明它会选择一个适用于 any as 的实例，或者，它不会'有一个为该实例构建 known 的策略。

作为一个人，我知道是这种情况，但有什么办法可以让它发挥作用吗？这些实例都是 "in scope" 并且可用...但是我如何告诉 GHC 如何以它满意的方式构建它？

Answer 1

如果 class 没有约束，则不能使用它的方法。只需添加约束：

asProds :: forall as. Known (Prod Proxy) as => Proxy as -> Prod Proxy as
asProds _ = known :: Prod Proxy as

注意 GHC 可以推断出这种类型：

asProds (_ :: Proxy as) = known :: Prod Proxy as
-- inferred constraint

由于类型被擦除，因此在没有字典的情况下运行无法从中构建实例。对于一个种类的所有居民都存在实例在逻辑上可能是正确的，但是对于程序我们需要字典 - 建设性证明 - 运行.

写出约束应该不会太困扰我们，因为如果我们有适用于所有情况的实例，那么当我们需要一个实例时，我们通常可以得到一个，只有不太频繁的例外。例外情况是当我们需要具有类型系列应用程序的开放类型的实例时。在那种情况下，我们必须编写函数，从其他已知实例中显式构建所需类型的实例。

从一系列较小的实例中推断出通用类型类实例？

Inferring general typeclass instance from a series of smaller ones?

haskell

typeclass

dependent-type

gadt