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

Question

这个标题肯定不是很具描述性,但我不知道如何在简短的标题中描述这一点.我很感激任何建议!

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

所以我有一个类型类

class Known f a where
    known :: f a

这应该能够在某个索引处生成给定类型的规范构造,对于使用GADT和东西很有用.我给的简化版本,这与初步认识的部分.

所以显然有一个例子Proxy:

instance Known Proxy a where
    known = Proxy

我们可以使用哪个:

> known :: Proxy Monad
Proxy

但是这个类似HList的类型也有一个实例:

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

infixr 5 (:<)

其中a 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......但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无法证明它会选择一个适用于任何 实例的实例as,或者它没有known为该实例构建的策略.

作为人类,我知道情况就是这样,但有什么方法可以让它发挥作用吗？这些实例都在"范围内"并且可用......但是我如何告诉GHC如何以满足的方式构建它？

Answer 1

如果类没有约束,则不能使用其方法.只需添加约束:

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

由于类型被擦除,因此在没有字典的情况下,没有任何实例可以构建运行时.从逻辑上讲,所有居民都存在一种情况,但对于程序,我们需要字典 - 建设性的证据 - 才能运行.

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